From a67cd02e557f0819255443da4f270d65673fc8d3 Mon Sep 17 00:00:00 2001
From: hellerve <veit@veitheller.de>
Date: Thu, 28 Mar 2019 21:45:04 +0100
Subject: [PATCH] initial

---
 .gitignore   |  2 ++
 Dep.agda     | 30 ++++++++++++++++++
 Distrib.agda | 26 ++++++++++++++++
 Peano.agda   | 86 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 README.md    | 18 +++++++++++
 5 files changed, 162 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 Dep.agda
 create mode 100644 Distrib.agda
 create mode 100644 Peano.agda
 create mode 100644 README.md

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..502124e
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+*.agdai
+*.agda~
diff --git a/Dep.agda b/Dep.agda
new file mode 100644
index 0000000..5d13539
--- /dev/null
+++ b/Dep.agda
@@ -0,0 +1,30 @@
+module dep where
+
+data Nat : Set where
+  zero : Nat
+  suc  : Nat → Nat
+
+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
+
+
diff --git a/Distrib.agda b/Distrib.agda
new file mode 100644
index 0000000..f15ab34
--- /dev/null
+++ b/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)
diff --git a/Peano.agda b/Peano.agda
new file mode 100644
index 0000000..8e36fd2
--- /dev/null
+++ b/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 → ⊥
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..121e3f4
--- /dev/null
+++ b/README.md
@@ -0,0 +1,18 @@
+# agda doodles
+
+Some Agda programs that I’ve doodled with to get a feel for the language.
+The usual stuff, Peano arithmetic, basic proofs, et al. Nothing new, and
+mostly derived from various tutorials and blog posts, most notably:
+
+- [Learn You an Agda](http://learnyouanagda.liamoc.net/)
+- [Logic Proofs with Coq, Agda, and Idris](https://queertypes.com/posts/48-logic-proofs-with-agda-coq-idris.html)
+- [An Introduction to Dependent Types and Agda](http://www2.tcs.ifi.lmu.de/~abel/lehre/SS09/Fun/DepTypes.pdf)
+
+A single proof was done by myself without help—well, except for Agda’s: the
+associativity of disjunction (found in Peano). It might well be that it’s
+complete and utter bollocks, but it seems to check out, so it’s good enough
+for me?
+
+<hr/>
+
+Have fun!