reorganize and add plfa

self/Dep.agda

@@ -0,0 +1,102 @@
+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)

self/Distrib.agda

@@ -0,0 +1,26 @@
+module distrib where
+
+data _∨_ (A B : Set) : Set where
+  inl : A → A ∨ B
+  inr : B → A ∨ B
+
+data _∧_ (A B : Set) : Set where
+  _and_ : A → B → A ∧ B
+
+and_dist_over_or : {a b c : Set} → a ∧ (b ∨ c) → (a ∧ b) ∨ (a ∧ c)
+and_dist_over_or (a₁ and (inl x)) = inl (a₁ and x)
+and_dist_over_or (a₁ and (inr x)) = inr (a₁ and x)
+
+and_dist_over_or′ : {a b c : Set} → (a ∧ b) ∨ (a ∧ c) → a ∧ (b ∨ c)
+and_dist_over_or′ (inl (x and x′)) = x and (inl x′)
+and_dist_over_or′ (inr (x and x′)) = x and (inr x′)
+
+or_dist_over_and : {a b c : Set} → (a ∨ b) ∧ (a ∨ c) -> a ∨ (b ∧ c)
+or_dist_over_and ((inl x) and (inl y)) = inl x
+or_dist_over_and ((inl x) and (inr y)) = inl x
+or_dist_over_and ((inr x) and (inl y)) = inl y
+or_dist_over_and ((inr x) and (inr y)) = inr (x and y)
+
+or_dist_over_and′ : {a b c : Set} → a ∨ (b ∧ c) → (a ∨ b) ∧ (a ∨ c)
+or_dist_over_and′ (inl x) = (inl x) and (inl x)
+or_dist_over_and′ (inr (x and y)) = (inr x) and (inr y)

self/Peano.agda

@@ -0,0 +1,86 @@
+module peano where
+
+data ℕ : Set where
+  zero : ℕ
+  suc : ℕ → ℕ
+
+_+_ : ℕ → ℕ → ℕ
+zero + zero = zero
+zero + n = n
+(suc n) + n′ = suc (n + n′)
+
+_*_ : ℕ → ℕ → ℕ
+zero * n = zero
+(suc zero) * n = n
+(suc n) * n′ = n′ + (n * n′)
+
+data _even : ℕ → Set where
+  ZERO : zero even
+  STEP : ∀ x → x even → suc (suc x) even
+  -- alternative:
+  --   : (x : ℕ) → x even → suc (suc x) even
+
+proof₁ : suc (suc (suc (suc zero))) even
+proof₁ = STEP _ (STEP _ ZERO)
+
+data _∧_ (P : Set) (Q : Set) : Set where
+  ∧-intro : P → Q → (P ∧ Q)
+
+proof₃ : {P Q : Set} → (P ∧ Q) → P
+proof₃ (∧-intro p q) = p
+
+_⇔_ : (P : Set) → (Q : Set) → Set
+a ⇔ b = (a → b) ∧ (b → a)
+
+∧-comm′ : {P Q : Set} → (P ∧ Q) → (Q ∧ P)
+∧-comm′ (∧-intro p q) = ∧-intro q p
+
+--∧-comm : {P Q : Set} → (P ∧ Q) ⇔ (Q ∧ P)
+--∧-comm = ∧-intro (∧-comm′ {P} {Q}) (∧-comm′ {Q} {P})
+
+∧-assoc₁ : {P Q R : Set} → ((P ∧ Q) ∧ R) → (P ∧ (Q ∧ R))
+∧-assoc₁ (∧-intro (∧-intro p q) r) = ∧-intro p (∧-intro q r)
+
+∧-assoc₂ : {P Q R : Set} → (P ∧ (Q ∧ R)) → ((P ∧ Q) ∧ R)
+∧-assoc₂ (∧-intro p (∧-intro q r)) = ∧-intro (∧-intro p q) r
+
+∧-assoc : {P Q R : Set} → ((P ∧ Q) ∧ R) ⇔  (P ∧ (Q ∧ R))
+∧-assoc = ∧-intro ∧-assoc₁ ∧-assoc₂
+
+data _∨_ (P Q : Set) : Set where
+  ∨-intro₁ : P → P ∨ Q
+  ∨-intro₂ : Q → P ∨ Q
+
+∨-elim : {A B C : Set} → (A → C) → (B → C) → (A ∨ B) → C
+∨-elim ac bc (∨-intro₁ a) = ac a
+∨-elim ac bc (∨-intro₂ b) = bc b
+
+∨-comm′ : {P Q : Set} → (P ∨ Q) → (Q ∨ P)
+∨-comm′ (∨-intro₁ p) = ∨-intro₂ p
+∨-comm′ (∨-intro₂ q) = ∨-intro₁ q
+
+∨-comm : {P Q : Set} → (P ∨ Q) ⇔ (Q ∨ P)
+∨-comm = ∧-intro ∨-comm′ ∨-comm′
+
+
+-- this is my first own proof! The associativity of disjunction
+
+∨-assoc₁ : {P Q R : Set} → ((P ∨ Q) ∨ R) → (P ∨ (Q ∨ R))
+∨-assoc₁ (∨-intro₁ (∨-intro₁ p)) = ∨-intro₁ p
+∨-assoc₁ (∨-intro₁ (∨-intro₂ q)) = ∨-intro₂ (∨-intro₁ q)
+∨-assoc₁ (∨-intro₂ r) = ∨-intro₂ (∨-intro₂ r)
+
+∨-assoc₂ : {P Q R : Set} → (P ∨ (Q ∨ R)) → ((P ∨ Q) ∨ R)
+∨-assoc₂ (∨-intro₁ p) = ∨-intro₁ (∨-intro₁ p)
+∨-assoc₂ (∨-intro₂ (∨-intro₁ q)) = ∨-intro₁ (∨-intro₂ q)
+∨-assoc₂ (∨-intro₂ (∨-intro₂ r)) = ∨-intro₂ r
+
+∨-assoc : {P Q R : Set} → ((P ∨ Q) ∨ R) ⇔  (P ∨ (Q ∨ R))
+∨-assoc = ∧-intro ∨-assoc₁ ∨-assoc₂
+
+--
+
+data ⊥ : Set where -- nothing
+
+¬ : Set → Set
+¬ A = A → ⊥