improved substitution

src/plta/Lambda.lagda

@@ -400,19 +400,19 @@ Here is the formal definition of substitution by closed terms in Agda.
 
 \begin{code}
 infix 9 _[_:=_]
-infix 9 _[[_][_:=_]]
+infix 9 _⟨_⟩[_:=_]
 
 _[_:=_]   : Term → Id → Term → Term
 
-_[[_][_:=_]] : Term → Id → Id → Term → Term
-N [[ x ][ y := V ]] with x ≟ y
+_⟨_⟩[_:=_] : Term → Id → Id → Term → Term
+N ⟨ x ⟩[ y := V ] with x ≟ y
 ... | yes _                  =  N
 ... | no  _                  =  N [ y := V ]
 
 (` x) [ y := V ] with x ≟ y
 ... | yes _                  =  V
 ... | no  _                  =  ` x
-(ƛ x ⇒ N) [ y := V ]         =  ƛ x ⇒ N [[ x ][ y := V ]]
+(ƛ x ⇒ N) [ y := V ]         =  ƛ x ⇒ N ⟨ x ⟩[ y := V ]
 (L · M) [ y := V ]           =  (L [ y := V ]) · (M [ y := V ])
 (`zero) [ y := V ]           =  `zero
 (`suc M) [ y := V ]          =  `suc (M [ y := V ])
@@ -420,8 +420,8 @@ N [[ x ][ y := V ]] with x ≟ y
   [zero⇒ M
   |suc x ⇒ N ]) [ y := V ]   =  `case L [ y := V ]
                                    [zero⇒ M [ y := V ]
-                                   |suc x ⇒ N [[ x ][ y := V ]] ]
-(μ x ⇒ N) [ y := V ]         =  μ x ⇒ (N [[ x ][ y := V ]])
+                                   |suc x ⇒ N ⟨ x ⟩[ y := V ] ]
+(μ x ⇒ N) [ y := V ]         =  μ x ⇒ (N ⟨ x ⟩[ y := V ])
 
 
 {-
@@ -979,7 +979,7 @@ data _⊢_⦂_ : Context → Term → Type → Set where
 
   Ax : ∀ {Γ x A}
     → Γ ∋ x ⦂ A
-      -------------
+       -------------
     → Γ ⊢ ` x ⦂ A
 
   -- ⇒-I

src/plta/Properties.lagda

@@ -667,41 +667,54 @@ we require an arbitrary context `Γ`, as in the statement of the lemma.
 
 Here is the formal statement and proof that substitution preserves types.
 \begin{code}
-subst : ∀ {Γ x N V A B}
-  → ∅ ⊢ V ⦂ A
-  → Γ , x ⦂ A ⊢ N ⦂ B
+subst : ∀ {Γ y N V A B}
+  → ∅ ⊢ V ⦂ B
+  → Γ , y ⦂ B ⊢ N ⦂ A
     --------------------
-  → Γ ⊢ N [ x := V ] ⦂ B
+  → Γ ⊢ N [ y := V ] ⦂ A
+
+substvar : ∀ {Γ x y V A B}
+  → ∅ ⊢ V ⦂ B
+  → Γ , y ⦂ B ∋ x ⦂ A
+    ------------------------
+  → Γ ⊢ (` x) [ y := V ] ⦂ A 
 
-{-
 substbind : ∀ {Γ x y N V A B C}
   → ∅ ⊢ V ⦂ B
-  → Γ , x ⦂ A , y ⦂ B ⊢ N ⦂ C
-    -----------------------------------
-  → Γ , x ⦂ A ⊢ N [[ x ][ y := V ]] ⦂ C
-substbind {x = x} {y = y} ⊢V ⊢N with x ≟ y
-... | yes refl     =  drop ⊢N
-... | no  x≢y      =  subst ⊢V (swap x≢y ⊢N)
--}
+  → Γ , y ⦂ B , x ⦂ A ⊢ N ⦂ C
+    ---------------------------------
+  → Γ , x ⦂ A ⊢ N ⟨ x ⟩[ y := V ] ⦂ C
 
-subst {x = y} ⊢V (Ax {x = x} Z) with x ≟ y
-... | yes refl     =  weaken ⊢V
-... | no  x≢y      =  ⊥-elim (x≢y refl)
-subst {x = y} ⊢V (Ax {x = x} (S x≢y ∋x)) with x ≟ y
-... | yes refl     =  ⊥-elim (x≢y refl)
-... | no  _        =  Ax ∋x
+subst ⊢V (Ax ∋x)           =  substvar ⊢V ∋x
+subst ⊢V (⊢ƛ ⊢N)           =  ⊢ƛ (substbind ⊢V ⊢N)
+subst ⊢V (⊢L · ⊢M)         =  subst ⊢V ⊢L · subst ⊢V ⊢M
+subst ⊢V ⊢zero             =  ⊢zero
+subst ⊢V (⊢suc ⊢M)         =  ⊢suc (subst ⊢V ⊢M)
+subst ⊢V (⊢case ⊢L ⊢M ⊢N)  =  ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (substbind ⊢V ⊢N)
+subst ⊢V (⊢μ ⊢N)           =  ⊢μ (substbind ⊢V ⊢N)
+
+substvar {x = x} {y = y} ⊢V Z with x ≟ y
+... | yes refl             =  weaken ⊢V
+... | no  x≢y              =  ⊥-elim (x≢y refl)
+substvar {x = x} {y = y} ⊢V (S x≢y ∋x) with x ≟ y
+... | yes refl             =  ⊥-elim (x≢y refl)
+... | no  _                =  Ax ∋x
+
+substbind {x = x} {y = y} ⊢V ⊢N with x ≟ y
+... | yes refl             =  drop ⊢N
+... | no  x≢y              =  subst ⊢V (swap x≢y ⊢N)
+
+{-
 subst {x = y} ⊢V (⊢ƛ {x = x} ⊢N) with x ≟ y
 ... | yes refl     =  ⊢ƛ (drop ⊢N)
 ... | no  x≢y      =  ⊢ƛ (subst ⊢V (swap x≢y ⊢N))
-subst ⊢V (⊢L · ⊢M) = subst ⊢V ⊢L · subst ⊢V ⊢M
-subst ⊢V ⊢zero     =  ⊢zero
-subst ⊢V (⊢suc ⊢M) =  ⊢suc (subst ⊢V ⊢M)
 subst {x = y} ⊢V (⊢case {x = x} ⊢L ⊢M ⊢N) with x ≟ y
 ... | yes refl     =  ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (drop ⊢N)
 ... | no  x≢y      =  ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (subst ⊢V (swap x≢y ⊢N))
 subst {x = y} ⊢V (⊢μ {x = x} ⊢M) with x ≟ y
 ... | yes refl     =  ⊢μ (drop ⊢M)
 ... | no  x≢y      =  ⊢μ (subst ⊢V (swap x≢y ⊢M))
+-}
 
 
 {-