hwk3

src/Homework3.agda

@@ -27,22 +27,51 @@ mul : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
 mul = μ -- *
   ƛ -- m
   ƛ -- n
-  (case (# 1)
+  (case (# 1) -- match on m
-    -- case `zero
+    -- case `zero → return 0
-    (# 0)
+    (`zero)
 
-    -- case `suc
+    -- case `suc m₁ → return n + (m₁ * n)
-    (plus · # 0 · (# 3 · # 1 · # 0))
+    (plus · # 1 · (# 3 · # 0 · # 1))
   )
 
 task2 : mul {∅} · one · one —↠ one
 task2 =
   begin
-    mul {∅} · (`suc `zero) · (`suc `zero)
+    mul · one · one
-  —→⟨ {!   !} ⟩
+  —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
-    mul [ μ mul ] · (`suc `zero) · (`suc `zero)
+    (ƛ ƛ (case (# 1) `zero (plus · # 1 · (mul · # 0 · # 1)))) · one · one
-  —→⟨ {!   !} ⟩
+  —→⟨ ξ-·₁ (β-ƛ (V-suc V-zero)) ⟩
-    mul [ μ mul ] [ `suc `zero ] · (`suc `zero)
+    (ƛ (case one `zero (plus · # 1 · (mul · # 0 · # 1)))) · one
-  —→⟨ {!   !} ⟩
+  —→⟨ β-ƛ (V-suc V-zero) ⟩
+    case one `zero (plus · one · (mul · # 0 · one))
+  —→⟨ β-suc V-zero ⟩
+    plus · one · (mul · `zero · one)
+  —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
+    (ƛ ƛ (case (# 1) (# 0) (`suc (plus · # 0 · # 1)))) · one · (mul · `zero · one)
+  —→⟨ ξ-·₁ (β-ƛ (V-suc V-zero)) ⟩
+    (ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) · (mul · `zero · one)
+  —→⟨ ξ-·₂ V-ƛ (ξ-·₁ (ξ-·₁ β-μ)) ⟩
+    (ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) ·
+      ((ƛ ƛ (case (# 1) `zero (plus · # 1 · (mul · # 0 · # 1)))) · `zero · one)
+  —→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-zero)) ⟩
+    (ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) ·
+      ((ƛ (case `zero `zero (plus · # 1 · (mul · # 0 · # 1)))) · one)
+  —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
+    (ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) ·
+      (case `zero `zero (plus · one · (mul · # 0 · one)))
+  —→⟨ ξ-·₂ V-ƛ β-zero ⟩
+    (ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) · `zero
+  —→⟨ β-ƛ V-zero ⟩
+    case one `zero (`suc (plus · # 0 · `zero))
+  —→⟨ β-suc V-zero ⟩
+    `suc (plus · `zero · `zero)
+  —→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
+    `suc ((ƛ ƛ (case (# 1) (# 0) (`suc (plus · # 0 · # 1)))) · `zero · `zero)
+  —→⟨ ξ-suc (ξ-·₁ (β-ƛ V-zero)) ⟩
+    `suc ((ƛ (case `zero (# 0) (`suc (plus · # 0 · # 1)))) · `zero)
+  —→⟨ ξ-suc (β-ƛ V-zero) ⟩
+    `suc (case `zero `zero (`suc (plus · # 0 · `zero)))
+  —→⟨ ξ-suc β-zero ⟩
     one
   ∎

src/Homework3Prelude.agda

@@ -229,6 +229,7 @@ data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where
 
   _—→⟨_⟩_ : (L : Γ ⊢ A) {M N : Γ ⊢ A}
     → L —→ M
+    -- → L —↠ M
     → M —↠ N
       ------
     → L —↠ N