Advent of proof submissions.HEADmaster

Completed all problems save 12, where I had to postulate two lemma.

1 files changed, 69 insertions, 0 deletions

diff --git a/src/Problem11.agda b/src/Problem11.agda
new file mode 100644
index 0000000..686f645
--- /dev/null
+++ b/src/Problem11.agda
@@ -0,0 +1,69 @@
+{-# OPTIONS --safe #-}
+
+module Problem11 where
+
+data Term : Set where
+  Ref : Term
+  Sop : Term
+  Kop : Term
+  App : Term → Term → Term
+
+variable M N P M₁ M₂ M₃ N₁ N₂ : Term
+
+data _↦_ : Term → Term → Set where
+  red-S : (App (App (App Sop M) N) P) ↦ (App (App M P) (App N P))
+  red-K : (App (App Kop M) N) ↦ M
+  red-left : M₁ ↦ M₂ → App M₁ N ↦ App M₂ N
+  red-right : N₁ ↦ N₂ → App M N₁ ↦ App M N₂
+  red-trans : M ↦ N → N ↦ P → M ↦ P
+
+open import Relation.Binary.Reasoning.Base.Partial _↦_ red-trans
+
+ident : Term
+ident = App (App Sop Kop) Kop
+
+ident-red : App ident M ↦ M
+ident-red {M} = begin
+  App (App (App Sop Kop) Kop) M ∼⟨ red-S ⟩
+  App (App Kop M) (App Kop M)   ∼⟨ red-K ⟩
+  M                             ∎
+
+const-sop : Term
+const-sop = App Kop Sop
+
+const-sop-red : App const-sop M ↦ Sop
+const-sop-red = red-K
+
+const-kop : Term
+const-kop = App Kop Kop
+
+const-kop-red : App const-kop M ↦ Kop
+const-kop-red = red-K
+
+app-app : Term → Term → Term
+app-app M N = App (App Sop M) N
+
+app-app-red : App (app-app M₁ M₂) M₃ ↦ App (App M₁ M₃) (App M₂ M₃)
+app-app-red = red-S
+
+lambda : Term → Term
+lambda Ref = ident
+lambda Sop = App Kop Sop
+lambda Kop = App Kop Kop
+lambda (App M N) = app-app (lambda M) (lambda N)
+
+substitution : Term → Term → Term
+substitution Ref N = N
+substitution Sop N = Sop
+substitution Kop N = Kop
+substitution (App M₁ M₂) N = App (substitution M₁ N) (substitution M₂ N)
+
+beta : ∀ M N → (App (lambda M) N) ↦ (substitution M N)
+beta Ref N = ident-red
+beta Sop N = const-sop-red
+beta Kop N = const-kop-red
+beta (App M₁ M₂) N = begin
+  App (app-app (lambda M₁) (lambda M₂)) N     ∼⟨ app-app-red ⟩
+  App (App (lambda M₁) N) (App (lambda M₂) N) ∼⟨ red-left (beta M₁ N) ⟩
+  App (substitution M₁ N) (App (lambda M₂) N) ∼⟨ red-right (beta M₂ N) ⟩
+  App (substitution M₁ N) (substitution M₂ N) ∎