From 3da3cdb23576683864bf68960b70367d4916385a Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Mon, 26 Jun 2017 13:16:13 +0100
Subject: [PATCH] updated Maps with extensionality

---
 src/Maps.lagda     | 85 +++++++++++++++++++++++++++-------------------
 src/StlcProp.lagda | 43 ++++++++++++-----------
 2 files changed, 74 insertions(+), 54 deletions(-)

diff --git a/src/Maps.lagda b/src/Maps.lagda
index 4e292d41..7d4eebd1 100644
--- a/src/Maps.lagda
+++ b/src/Maps.lagda
@@ -86,6 +86,8 @@ y = id "y"
 z = id "z"
 \end{code}
 
+## Extensionality
+
 ## Total Maps
 
 Our main job in this chapter will be to build a definition of
@@ -219,8 +221,8 @@ back $$v$$:
   update-eq′ : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A)
              → (ρ , x ↦ v) x ≡ v
   update-eq′ ρ x v with x ≟ x
-  ... | yes x=x = refl
-  ... | no  x≠x = ⊥-elim (x≠x refl)
+  ... | yes x≡x = refl
+  ... | no  x≢x = ⊥-elim (x≢x refl)
 \end{code}
 </div>
 
@@ -237,6 +239,14 @@ the same result that $$m$$ would have given:
   ... | no  _   = refl
 \end{code}
 
+For the following lemmas, since maps are represented by functions, to
+show two maps equal we will need to postulate extensionality.
+
+\begin{code}
+  postulate
+    extensionality : ∀ {A : Set} {ρ ρ′ : TotalMap A} → (∀ x → ρ x ≡ ρ′ x) → ρ ≡ ρ′
+\end{code}
+
 #### Exercise: 2 stars, optional (update-shadow)
 If we update a map $$ρ$$ at a key $$x$$ with a value $$v$$ and then
 update again with the same key $$x$$ and another value $$w$$, the
@@ -246,18 +256,20 @@ the second update on $$ρ$$:
 
 \begin{code}
   postulate
-    update-shadow : ∀ {A} (ρ : TotalMap A) (x : Id) (v w : A) (y : Id)
-                  → (ρ , x ↦ v , x ↦ w) y ≡ (ρ , x ↦ w) y
+    update-shadow : ∀ {A} (ρ : TotalMap A) (x : Id) (v w : A) 
+                  → (ρ , x ↦ v , x ↦ w) ≡ (ρ , x ↦ w)
 \end{code}
 
 <div class="hidden">
 \begin{code}
-  update-shadow′ :  ∀ {A} (ρ : TotalMap A) (x : Id) (v w : A) (y : Id)
-                  → ((ρ , x ↦ v) , x ↦ w) y ≡ (ρ , x ↦ w) y
-  update-shadow′ ρ x v w y
-      with x ≟ y
-  ... | yes x≡y = refl
-  ... | no  x≢y = update-neq ρ x v y x≢y
+  update-shadow′ :  ∀ {A} (ρ : TotalMap A) (x : Id) (v w : A) 
+                  → ((ρ , x ↦ v) , x ↦ w) ≡ (ρ , x ↦ w)
+  update-shadow′ ρ x v w = extensionality lemma
+    where
+    lemma : ∀ y → ((ρ , x ↦ v) , x ↦ w) y ≡ (ρ , x ↦ w) y
+    lemma y with x ≟ y
+    ... | yes refl = refl
+    ... | no  x≢y  = update-neq ρ x v y x≢y
 \end{code}
 </div>
 
@@ -268,16 +280,18 @@ result is equal to $$ρ$$:
 
 \begin{code}
   postulate
-    update-same : ∀ {A} (ρ : TotalMap A) (x y : Id) → (ρ , x ↦ ρ x) y ≡ ρ y
+    update-same : ∀ {A} (ρ : TotalMap A) (x : Id) → (ρ , x ↦ ρ x) ≡ ρ
 \end{code}
 
 <div class="hidden">
 \begin{code}
-  update-same′ : ∀ {A} (ρ : TotalMap A) (x y : Id) → (ρ , x ↦ ρ x) y ≡ ρ y
-  update-same′ ρ x y
-    with x ≟ y
-  ... | yes refl = refl
-  ... | no  x≢y  = refl
+  update-same′ : ∀ {A} (ρ : TotalMap A) (x : Id) → (ρ , x ↦ ρ x) ≡ ρ
+  update-same′ ρ x  =  extensionality lemma
+    where
+    lemma : ∀ y → (ρ , x ↦ ρ x) y ≡ ρ y
+    lemma y with x ≟ y
+    ... | yes refl = refl
+    ... | no  x≢y  = refl
 \end{code}
 </div>
 
@@ -288,19 +302,22 @@ updates.
 
 \begin{code}
   postulate
-    update-permute : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A) (z : Id)
-                   → x ≢ y → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z
+    update-permute : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A)
+                   → x ≢ y → (ρ , x ↦ v , y ↦ w) ≡ (ρ , y ↦ w , x ↦ v)
 \end{code}
 
 <div class="hidden">
 \begin{code}
-  update-permute′ : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A) (z : Id)
-                   → x ≢ y → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z
-  update-permute′ {A} ρ x v y w z x≢y with x ≟ z | y ≟ z
-  ... | yes refl | yes refl  =  ⊥-elim (x≢y refl)
-  ... | no  x≢z  | yes refl  =  sym (update-eq′ ρ z w)
-  ... | yes refl | no  y≢z   =  update-eq′ ρ z v
-  ... | no  x≢z  | no  y≢z   =  trans (update-neq ρ x v z x≢z) (sym (update-neq ρ y w z y≢z))  
+  update-permute′ : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A)
+                   → x ≢ y → (ρ , x ↦ v , y ↦ w) ≡ (ρ , y ↦ w , x ↦ v)
+  update-permute′ {A} ρ x v y w x≢y  =  extensionality lemma
+    where
+    lemma : ∀ z → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z
+    lemma z with x ≟ z | y ≟ z
+    ... | yes refl | yes refl  =  ⊥-elim (x≢y refl)
+    ... | no  x≢z  | yes refl  =  sym (update-eq′ ρ z w)
+    ... | yes refl | no  y≢z   =  update-eq′ ρ z v
+    ... | no  x≢z  | no  y≢z   =  trans (update-neq ρ x v z x≢z) (sym (update-neq ρ y w z y≢z))  
 \end{code}
 
 And a slightly different version of the same proof.
@@ -373,20 +390,20 @@ We now lift all of the basic lemmas about total maps to partial maps.
 \end{code}
 
 \begin{code}
-  update-shadow : ∀ {A} (ρ : PartialMap A) (x : Id) (v w : A) (y : Id)
-                → (ρ , x ↦ v , x ↦ w) y ≡ (ρ , x ↦ w) y
-  update-shadow ρ x v w y = TotalMap.update-shadow ρ x (just v) (just w) y
+  update-shadow : ∀ {A} (ρ : PartialMap A) (x : Id) (v w : A) 
+                → (ρ , x ↦ v , x ↦ w) ≡ (ρ , x ↦ w)
+  update-shadow ρ x v w = TotalMap.update-shadow ρ x (just v) (just w)
 \end{code}
 
 \begin{code}
-  update-same : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) (y : Id)
+  update-same : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) 
               → ρ x ≡ just v
-              → (ρ , x ↦ v) y ≡ ρ y
-  update-same ρ x v y ρx≡v rewrite sym ρx≡v = TotalMap.update-same ρ x y
+              → (ρ , x ↦ v) ≡ ρ
+  update-same ρ x v ρx≡v rewrite sym ρx≡v = TotalMap.update-same ρ x
 \end{code}
 
 \begin{code}
-  update-permute : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) (y : Id) (w : A) (z : Id)
-                 → x ≢ y → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z
-  update-permute ρ x v y w z x≢y = TotalMap.update-permute ρ x (just v) y (just w) z x≢y
+  update-permute : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) (y : Id) (w : A) 
+                 → x ≢ y → (ρ , x ↦ v , y ↦ w) ≡ (ρ , y ↦ w , x ↦ v)
+  update-permute ρ x v y w x≢y = TotalMap.update-permute ρ x (just v) y (just w) x≢y
 \end{code}
diff --git a/src/StlcProp.lagda b/src/StlcProp.lagda
index e4760f06..f5eabe7c 100644
--- a/src/StlcProp.lagda
+++ b/src/StlcProp.lagda
@@ -277,7 +277,7 @@ postulate
 
 <div class="hidden">
 \begin{code}
-contradiction : ∀ {A : Set} → ∀ {v : A} → ¬ (_≡_ {A = Maybe A} (just v) nothing)
+contradiction : ∀ {X : Set} → ∀ {x : X} → ¬ (_≡_ {A = Maybe X} (just x) nothing)
 contradiction ()
 
 ∅⊢-closed′ : ∀ {M A} → ∅ ⊢ M ∈ A → closed M
@@ -396,8 +396,8 @@ $$Γ ⊢ (N [ x := V ]) ∈ B$$.
 
 \begin{code}
 preservation-[:=] : ∀ {Γ x A N B V}
-                 → ∅ ⊢ V ∈ A
                  → (Γ , x ↦ A) ⊢ N ∈ B
+                 → ∅ ⊢ V ∈ A
                  → Γ ⊢ (N [ x := V ]) ∈ B
 \end{code}
 
@@ -464,29 +464,32 @@ $$Γ \vdash N [ x := V ] ∈ B$$.
 
   - The remaining cases are similar to the application case.
 
-For one case, we need to know that weakening applies to any closed term.
+We need a couple of lemmas. A closed term can be weakened to any context, and just is injective.
 \begin{code}
-weaken-closed : ∀ {P A Γ} → ∅ ⊢ P ∈ A → Γ ⊢ P ∈ A
-weaken-closed {P} {A} {Γ} ⊢P = weaken Γ~Γ′ ⊢P
+weaken-closed : ∀ {V A Γ} → ∅ ⊢ V ∈ A → Γ ⊢ V ∈ A
+weaken-closed {V} {A} {Γ} ⊢V = weaken Γ~Γ′ ⊢V
   where
-  Γ~Γ′ : ∀ {x} → x FreeIn P → ∅ x ≡ Γ x
-  Γ~Γ′ {x} x∈P = ⊥-elim (x∉P x∈P)
+  Γ~Γ′ : ∀ {x} → x FreeIn V → ∅ x ≡ Γ x
+  Γ~Γ′ {x} x∈V = ⊥-elim (x∉V x∈V)
     where
-    x∉P : ¬ (x FreeIn P)
-    x∉P = ∅⊢-closed ⊢P {x}
+    x∉V : ¬ (x FreeIn V)
+    x∉V = ∅⊢-closed ⊢V {x}
+
+just-injective : ∀ {X : Set} {x y : X} → _≡_ {A = Maybe X} (just x) (just y) → x ≡ y
+just-injective refl = refl
 \end{code}
 
 \begin{code}
-preservation-[:=] {Γ} {y} {A} ⊢P (Ax {_} {x} {B} Γx≡justB) with x ≟ y
-...| yes x≡y  =  {!!}  -- weaken-closed ⊢P
-...| no  x≢y  =  {!!} -- Ax {_} {x} Γx≡justB
-preservation-[:=] {Γ} {y} {A} ⊢P (⇒-I {_} {x} ⊢N) with x ≟ y
-...| yes x≡y  =  {!!} -- ⇒-I {_} {x} ⊢N
-...| no  x≢y  =  {!!}  -- ⇒-I {_} {x} (preservation-[:=] {_} {y} {A} ⊢P ⊢N)
-preservation-[:=] ⊢P (⇒-E ⊢L ⊢M) = ⇒-E (preservation-[:=] ⊢P ⊢L) (preservation-[:=] ⊢P ⊢M)
-preservation-[:=] ⊢P 𝔹-I₁ = 𝔹-I₁
-preservation-[:=] ⊢P 𝔹-I₂ = 𝔹-I₂
-preservation-[:=] ⊢P (𝔹-E ⊢L ⊢M ⊢N) = 𝔹-E (preservation-[:=] ⊢P ⊢L) (preservation-[:=] ⊢P ⊢M) (preservation-[:=] ⊢P ⊢N)
+preservation-[:=] {Γ} {x} {A} {varᵀ x′} {B} {V} (Ax {.(Γ , x ↦ A)} {.x′} {.B} Γx′≡B) ⊢V with x ≟ x′
+...| yes x≡x′ rewrite just-injective Γx′≡B  =  weaken-closed ⊢V
+...| no  x≢x′  =  Ax {Γ} {x′} {B} Γx′≡B
+preservation-[:=] {Γ} {x} {A} {λᵀ x′ ∈ A′ ⇒ N′} {.A′ ⇒ B′} {V} (⇒-I {.(Γ , x ↦ A)} {.x′} {.N′} {.A′} {.B′} ⊢N′) ⊢V with x ≟ x′
+...| yes x≡x′  =  {!!}  -- rewrite x≡x′ | update-shadow Γ x A A′  =  ⇒-I ⊢N′
+...| no  x≢x′ rewrite update-permute Γ x A x′ A′ x≢x′ =  ⇒-I {Γ} {x′} {N′} {A′} {B′} (preservation-[:=] {(Γ , x′ ↦ A′)} {x} {A} ⊢N′ ⊢V)
+preservation-[:=] (⇒-E ⊢L ⊢M) ⊢V = ⇒-E (preservation-[:=] ⊢L ⊢V) (preservation-[:=] ⊢M ⊢V)
+preservation-[:=] 𝔹-I₁ ⊢V = 𝔹-I₁
+preservation-[:=] 𝔹-I₂ ⊢V = 𝔹-I₂
+preservation-[:=] (𝔹-E ⊢L ⊢M ⊢N) ⊢V = 𝔹-E (preservation-[:=] ⊢L ⊢V) (preservation-[:=] ⊢M ⊢V) (preservation-[:=] ⊢N ⊢V)
 
 
 {-
@@ -551,7 +554,7 @@ _Proof_: By induction on the derivation of $$\vdash t : T$$.
 \begin{code}
 preservation (Ax x₁) ()
 preservation (⇒-I ⊢N) ()
-preservation (⇒-E (⇒-I ⊢N) ⊢V) (β⇒ valueV) = preservation-[:=] ⊢V ⊢N
+preservation (⇒-E (⇒-I ⊢N) ⊢V) (β⇒ valueV) = preservation-[:=] ⊢N ⊢V
 preservation (⇒-E ⊢L ⊢M) (γ⇒₁ L⟹L′) with preservation ⊢L L⟹L′
 ...| ⊢L′ = ⇒-E ⊢L′ ⊢M
 preservation (⇒-E ⊢L ⊢M) (γ⇒₂ valueL M⟹M′) with preservation ⊢M M⟹M′