103 lines
2.2 KiB
Agda
103 lines
2.2 KiB
Agda
module dep where
|
||
|
||
data Nat : Set where
|
||
zero : Nat
|
||
suc : Nat → Nat
|
||
|
||
one = suc zero
|
||
|
||
data L (A : Set) : Set where
|
||
[] : L A
|
||
_::_ : A → L A → L A
|
||
|
||
data Vect (A : Set) : Nat → Set where
|
||
vnil : Vect A zero
|
||
vcons : {n : Nat} → A → Vect A n → Vect A (suc n)
|
||
|
||
infix 2 _+_
|
||
infix 3 _*_
|
||
|
||
_+_ : Nat → Nat → Nat
|
||
n + zero = n
|
||
n + suc m = suc (n + m)
|
||
|
||
_*_ : Nat -> Nat -> Nat
|
||
n * zero = zero
|
||
n * suc m = n * m + n
|
||
|
||
inner : {n : Nat} → Vect Nat n → Vect Nat n → Nat
|
||
inner vnil vnil = zero
|
||
inner (vcons x xs) (vcons y ys) = x * y + inner xs ys
|
||
|
||
append : {A : Set} {n m : Nat} → Vect A n → Vect A m → Vect A (m + n)
|
||
append vnil ys = ys
|
||
append (vcons x xs) ys = vcons x (append xs ys)
|
||
|
||
data Fin : Nat → Set where
|
||
fzero : {n : Nat} → Fin (suc n)
|
||
fsuc : {n : Nat} → Fin n → Fin (suc n)
|
||
|
||
_!!_ : {A : Set} {n : Nat} → Vect A n → Fin n → A
|
||
vnil !! ()
|
||
vcons x xs !! fzero = x
|
||
vcons x xs !! fsuc m = xs !! m
|
||
|
||
data Bool : Set where
|
||
true : Bool
|
||
false : Bool
|
||
|
||
if_then_else_ : {A : Set} → Bool → A → A -> A
|
||
if true then b1 else b2 = b1
|
||
if false then b1 else b2 = b2
|
||
|
||
_≤_ : Nat → Nat → Bool
|
||
zero ≤ n = true
|
||
(suc m) ≤ zero = false
|
||
(suc m) ≤ (suc n) = m ≤ n
|
||
|
||
Proposition = Set
|
||
|
||
data Absurd : Proposition where
|
||
|
||
data Truth : Proposition where
|
||
t : Truth
|
||
|
||
data _∧_ (A B : Proposition) : Proposition where
|
||
and : A → B → A ∧ B
|
||
|
||
fst : {A B : Proposition} → A ∧ B → A
|
||
fst (and a b) = a
|
||
|
||
snd : {A B : Proposition} → A ∧ B → B
|
||
snd (and a b) = b
|
||
|
||
_×_ = _∧_
|
||
|
||
data _∨_ (A B : Proposition) : Proposition where
|
||
inl : A → A ∨ B
|
||
inr : B → A ∨ B
|
||
|
||
case : {A B C : Proposition} → A ∨ B → (A → C) → (B → C) → C
|
||
case (inl a) f g = f a
|
||
case (inr b) f g = g b
|
||
|
||
lemma : {A : Proposition} → A → A ∧ Truth
|
||
lemma a = (and a t)
|
||
|
||
comm∧ : {A B : Proposition} → A ∧ B → B ∧ A
|
||
comm∧ (and a b) = (and b a)
|
||
|
||
True : Bool → Proposition
|
||
True true = Truth
|
||
True false = Absurd
|
||
|
||
refl≤ : (n : Nat) → True (n ≤ n)
|
||
refl≤ zero = t
|
||
refl≤ (suc n) = refl≤ n
|
||
|
||
data SList : Nat → Set where
|
||
snil : SList zero
|
||
scons : {n : Nat} (m : Nat) → True (n ≤ m) → SList n → SList m
|
||
|
||
slist1 = scons one t (scons zero t snil)
|