From fbc44a0f78e3b9657fabb7a49b38f3efa8886e29 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sat, 16 Oct 2021 03:26:07 -0500
Subject: [PATCH] homework 3 start

---
 .vscode/settings.json          |   4 +-
 src/Homework3.agda             |  48 +++++++
 src/Homework3Prelude.agda      | 240 +++++++++++++++++++++++++++++++++
 src/LambdaTest.agda            |  27 ++++
 src/plfa/part2/Lambda.lagda.md |   2 +-
 5 files changed, 318 insertions(+), 3 deletions(-)
 create mode 100644 src/Homework3.agda
 create mode 100644 src/Homework3Prelude.agda
 create mode 100644 src/LambdaTest.agda

diff --git a/.vscode/settings.json b/.vscode/settings.json
index 0e558f80..c641a404 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -1,7 +1,7 @@
 {
-  "editor.fontFamily": "'Roboto Mono', 'Droid Sans Mono', 'monospace', monospace, 'Droid Sans Fallback'",
   "editor.fontSize": 15,
   "vim.insertModeKeyBindings": [
     { "before": ["k", "j"], "after": ["<Esc>"] }
-  ]
+  ],
+  "editor.fontFamily": "\"PragmataPro Mono Liga\", \"Roboto Mono\", 'Droid Sans Mono', 'monospace', monospace, 'Droid Sans Fallback'"
 }
\ No newline at end of file
diff --git a/src/Homework3.agda b/src/Homework3.agda
new file mode 100644
index 00000000..0875f495
--- /dev/null
+++ b/src/Homework3.agda
@@ -0,0 +1,48 @@
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s)
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Decidable using (True; toWitness)
+open import Homework3Prelude
+
+module Homework3 where
+
+---------------------------------------------------------
+-- task 1
+---------------------------------------------------------
+
+V¬—→ : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ ⊢ A}
+  → Value M
+  → ¬ (M —→ N)
+V¬—→ V-ƛ ()
+V¬—→ V-zero ()
+V¬—→ (V-suc v) (ξ-suc m) = V¬—→ v m
+
+---------------------------------------------------------
+-- task 2
+---------------------------------------------------------
+
+mul : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
+mul = μ -- *
+  ƛ -- m
+  ƛ -- n
+  (case (# 1)
+    -- case `zero
+    (# 0)
+
+    -- case `suc
+    (plus · # 0 · (# 3 · # 1 · # 0))
+  )
+
+task2 : mul {∅} · one · one —↠ one
+task2 =
+  begin
+    mul {∅} · (`suc `zero) · (`suc `zero)
+  —→⟨ {!   !} ⟩
+    mul [ μ mul ] · (`suc `zero) · (`suc `zero)
+  —→⟨ {!   !} ⟩
+    mul [ μ mul ] [ `suc `zero ] · (`suc `zero)
+  —→⟨ {!   !} ⟩
+    one
+  ∎
diff --git a/src/Homework3Prelude.agda b/src/Homework3Prelude.agda
new file mode 100644
index 00000000..1df80524
--- /dev/null
+++ b/src/Homework3Prelude.agda
@@ -0,0 +1,240 @@
+-- This file contains the code extracted from the DeBruijn chapter in PLFA
+
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s)
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Decidable using (True; toWitness)
+
+module Homework3Prelude where
+
+infix  4 _⊢_
+infix  4 _∋_
+infixl 5 _,_
+
+infixr 7 _⇒_
+
+infix  5 ƛ_
+infix  5 μ_
+infixl 7 _·_
+infix  8 `suc_
+infix  9 `_
+infix  9 S_
+infix  9 #_
+
+data Type : Set where
+  _⇒_ : Type → Type → Type
+  `ℕ  : Type
+
+data Context : Set where
+  ∅   : Context
+  _,_ : Context → Type → Context
+
+data _∋_ : Context → Type → Set where
+
+  Z : ∀ {Γ A}
+      ---------
+    → Γ , A ∋ A
+
+  S_ : ∀ {Γ A B}
+    → Γ ∋ A
+      ---------
+    → Γ , B ∋ A
+
+data _⊢_ : Context → Type → Set where
+
+  `_ : ∀ {Γ A}
+    → Γ ∋ A
+      -----
+    → Γ ⊢ A
+
+  ƛ_  : ∀ {Γ A B}
+    → Γ , A ⊢ B
+      ---------
+    → Γ ⊢ A ⇒ B
+
+  _·_ : ∀ {Γ A B}
+    → Γ ⊢ A ⇒ B
+    → Γ ⊢ A
+      ---------
+    → Γ ⊢ B
+
+  `zero : ∀ {Γ}
+      ---------
+    → Γ ⊢ `ℕ
+
+  `suc_ : ∀ {Γ}
+    → Γ ⊢ `ℕ
+      ------
+    → Γ ⊢ `ℕ
+
+  case : ∀ {Γ A}
+    → Γ ⊢ `ℕ
+    → Γ ⊢ A
+    → Γ , `ℕ ⊢ A
+      ----------
+    → Γ ⊢ A
+
+  μ_ : ∀ {Γ A}
+    → Γ , A ⊢ A
+      ---------
+    → Γ ⊢ A
+
+length : Context → ℕ
+length ∅        =  zero
+length (Γ , _)  =  suc (length Γ)
+
+lookup : {Γ : Context} → {n : ℕ} → (p : n < length Γ) → Type
+lookup {(_ , A)} {zero}    (s≤s z≤n)  =  A
+lookup {(Γ , _)} {(suc n)} (s≤s p)    =  lookup p
+
+count : ∀ {Γ} → {n : ℕ} → (p : n < length Γ) → Γ ∋ lookup p
+count {_ , _} {zero}    (s≤s z≤n)  =  Z
+count {Γ , _} {(suc n)} (s≤s p)    =  S (count p)
+
+#_ : ∀ {Γ}
+  → (n : ℕ)
+  → {n∈Γ : True (suc n ≤? length Γ)}
+    --------------------------------
+  → Γ ⊢ lookup (toWitness n∈Γ)
+#_ n {n∈Γ}  =  ` count (toWitness n∈Γ)
+
+one : ∀ {Γ} → Γ ⊢ `ℕ
+one = `suc `zero
+
+two : ∀ {Γ} → Γ ⊢ `ℕ
+two = `suc `suc `zero
+
+plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
+plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
+
+ext : ∀ {Γ Δ}
+  → (∀ {A} →       Γ ∋ A →     Δ ∋ A)
+    ---------------------------------
+  → (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
+ext ρ Z      =  Z
+ext ρ (S x)  =  S (ρ x)
+
+rename : ∀ {Γ Δ}
+  → (∀ {A} → Γ ∋ A → Δ ∋ A)
+    -----------------------
+  → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
+rename ρ (` x)          =  ` (ρ x)
+rename ρ (ƛ N)          =  ƛ (rename (ext ρ) N)
+rename ρ (L · M)        =  (rename ρ L) · (rename ρ M)
+rename ρ (`zero)        =  `zero
+rename ρ (`suc M)       =  `suc (rename ρ M)
+rename ρ (case L M N)   =  case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
+rename ρ (μ N)          =  μ (rename (ext ρ) N)
+
+exts : ∀ {Γ Δ}
+  → (∀ {A} →       Γ ∋ A →     Δ ⊢ A)
+    ---------------------------------
+  → (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A)
+exts σ Z      =  ` Z
+exts σ (S x)  =  rename S_ (σ x)
+
+subst : ∀ {Γ Δ}
+  → (∀ {A} → Γ ∋ A → Δ ⊢ A)
+    -----------------------
+  → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
+subst σ (` k)          =  σ k
+subst σ (ƛ N)          =  ƛ (subst (exts σ) N)
+subst σ (L · M)        =  (subst σ L) · (subst σ M)
+subst σ (`zero)        =  `zero
+subst σ (`suc M)       =  `suc (subst σ M)
+subst σ (case L M N)   =  case (subst σ L) (subst σ M) (subst (exts σ) N)
+subst σ (μ N)          =  μ (subst (exts σ) N)
+
+_[_] : ∀ {Γ A B}
+  → Γ , B ⊢ A
+  → Γ ⊢ B
+    ---------
+  → Γ ⊢ A
+_[_] {Γ} {A} {B} N M =  subst {Γ , B} {Γ} σ {A} N
+  where
+  σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A
+  σ Z      =  M
+  σ (S x)  =  ` x
+
+data Value : ∀ {Γ A} → Γ ⊢ A → Set where
+
+  V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
+      ---------------------------
+    → Value (ƛ N)
+
+  V-zero : ∀ {Γ}
+      -----------------
+    → Value (`zero {Γ})
+
+  V-suc : ∀ {Γ} {V : Γ ⊢ `ℕ}
+    → Value V
+      --------------
+    → Value (`suc V)
+
+infix 2 _—→_
+
+data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+
+  ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
+    → L —→ L′
+      ---------------
+    → L · M —→ L′ · M
+
+  ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
+    → Value V
+    → M —→ M′
+      ---------------
+    → V · M —→ V · M′
+
+  β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
+    → Value W
+      --------------------
+    → (ƛ N) · W —→ N [ W ]
+
+  ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
+    → M —→ M′
+      -----------------
+    → `suc M —→ `suc M′
+
+  ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+    → L —→ L′
+      -------------------------
+    → case L M N —→ case L′ M N
+
+  β-zero :  ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+      -------------------
+    → case `zero M N —→ M
+
+  β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+    → Value V
+      ----------------------------
+    → case (`suc V) M N —→ N [ V ]
+
+  β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
+      ----------------
+    → μ N —→ N [ μ N ]
+
+infix  2 _—↠_
+infix  1 begin_
+infixr 2 _—→⟨_⟩_
+infix  3 _∎
+
+data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where
+
+  _∎ : (M : Γ ⊢ A)
+      ------
+    → M —↠ M
+
+  _—→⟨_⟩_ : (L : Γ ⊢ A) {M N : Γ ⊢ A}
+    → L —→ M
+    → M —↠ N
+      ------
+    → L —↠ N
+
+begin_ : ∀ {Γ A} {M N : Γ ⊢ A}
+  → M —↠ N
+    ------
+  → M —↠ N
+begin M—↠N = M—↠N
diff --git a/src/LambdaTest.agda b/src/LambdaTest.agda
new file mode 100644
index 00000000..69ce60e0
--- /dev/null
+++ b/src/LambdaTest.agda
@@ -0,0 +1,27 @@
+module LambdaTest where
+
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; _≢_; refl; sym; cong; cong₂)
+open import Data.String using (String; _≟_)
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Product
+  using (_×_; proj₁; proj₂; ∃; ∃-syntax)
+  renaming (_,_ to ⟨_,_⟩)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Function using (_∘_)
+V¬—→ V-ƛ = ?
+V¬—→ V-zero = ?
+V¬—→ (V-suc v) (ξ-suc m) = ?
+V¬—→ V-zero = ?
+V¬—→ (V-suc v) = ?
+open import plfa.part2.Lambda
+
+V¬—→ : ∀ {M N}
+  → Value M
+    ----------
+  → ¬ (M —→ N)
+V¬—→ V-ƛ ()
+V¬—→ V-zero ()
+V¬—→ (V-suc v) (ξ-suc m) = V¬—→ v m
diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md
index 1ccc9494..1f249c1a 100644
--- a/src/plfa/part2/Lambda.lagda.md
+++ b/src/plfa/part2/Lambda.lagda.md
@@ -1082,7 +1082,7 @@ Context≃List = record
   { from = contextOfList
   ; to = listOfContext
   ; from∘to = contextListIso
-  ; to∘from = ?
+  ; to∘from = listContextIso
   }
 ```