michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

improved subst

Browse source
This commit is contained in:
wadler 2018-07-01 06:16:39 -03:00
parent deeb5269f6
commit aefe4ba95c
2 changed files with 87 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

62
src/plta/Lambda.lagda
View file

@ -400,23 +400,57 @@ Here is the formal definition of substitution by closed terms in Agda.
\begin{code}
infix 9 _[_:=_]
infix 9 _[[_][_:=_]]
_[_:=_] : Term → Id → Term → Term
_[[_][_:=_]] : 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 ]]
(L · M) [ y := V ] = (L [ y := V ]) · (M [ y := V ])
(`zero) [ y := V ] = `zero
(`suc M) [ y := V ] = `suc (M [ y := V ])
(`case L
[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 ]])
{-
infix 9 _[_:=_]
_[_:=_] : Term → Id → Term → Term
(` x) [ y := V ] with x ≟ y
... | yes _ = V
... | no _ = ` x
... | yes _ = V
... | no _ = ` x
(ƛ x ⇒ N) [ y := V ] with x ≟ y
... | yes _ = ƛ x ⇒ N
... | no _ = ƛ x ⇒ (N [ y := V ])
(L · M) [ y := V ] = (L [ y := V ]) · (M [ y := V ])
(`zero) [ y := V ] = `zero
(`suc M) [ y := V ] = `suc (M [ y := V ])
(`case L [zero⇒ M |suc x ⇒ N ]) [ y := V ] with x ≟ y
... | yes _ = `case L [ y := V ] [zero⇒ M [ y := V ] |suc x ⇒ N ]
... | no _ = `case L [ y := V ] [zero⇒ M [ y := V ] |suc x ⇒ N [ y := V ] ]
... | yes _ = ƛ x ⇒ N
... | no _ = ƛ x ⇒ (N [ y := V ])
(L · M) [ y := V ] = (L [ y := V ]) · (M [ y := V ])
(`zero) [ y := V ] = `zero
(`suc M) [ y := V ] = `suc (M [ y := V ])
(`case L
[zero⇒ M
|suc x ⇒ N ])
[ y := V ] with x ≟ y
... | yes _ = `case L [ y := V ]
[zero⇒ M [ y := V ]
|suc x ⇒ N ]
... | no _ = `case L [ y := V ]
[zero⇒ M [ y := V ]
|suc x ⇒ N [ y := V ] ]
(μ x ⇒ N) [ y := V ] with x ≟ y
... | yes _ = μ x ⇒ N
... | no _ = μ x ⇒ (N [ y := V ])
... | yes _ = μ x ⇒ N
... | no _ = μ x ⇒ (N [ y := V ])
-}
\end{code}
Let's unpack the first three cases.
@ -442,10 +476,10 @@ simply push substitution recursively into the subterms.
Here is confirmation that the examples above are correct.
\begin{code}
_ : (sucᶜ · sucᶜ · ` "z") [ "z" := `zero ] ≡ sucᶜ · sucᶜ · `zero
_ : (sucᶜ · (sucᶜ · ` "z")) [ "z" := `zero ] ≡ sucᶜ · (sucᶜ · `zero)
_ = refl
_ : (ƛ "z" ⇒ ` "s" · ` "s" · ` "z") [ "s" := sucᶜ ] ≡ ƛ "z" ⇒ sucᶜ · sucᶜ · ` "z"
_ : (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) [ "s" := sucᶜ ] ≡ ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")
_ = refl
_ : (ƛ "x" ⇒ ` "y") [ "y" := `zero ] ≡ ƛ "x" ⇒ `zero

39
src/plta/Properties.lagda
View file

@ -672,6 +672,18 @@ subst : ∀ {Γ x N V A B}
→ Γ , x ⦂ A ⊢ N ⦂ B
--------------------
→ Γ ⊢ N [ x := V ] ⦂ B
{-
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)
-}
subst {x = y} ⊢V (Ax {x = x} Z) with x ≟ y
... | yes refl = weaken ⊢V
... | no x≢y = ⊥-elim (x≢y refl)
@ -690,6 +702,33 @@ subst {x = y} ⊢V (⊢case {x = x} ⊢L ⊢M ⊢N) with x ≟ y
subst {x = y} ⊢V (⊢μ {x = x} ⊢M) with x ≟ y
... | yes refl = ⊢μ (drop ⊢M)
... | no x≢y = ⊢μ (subst ⊢V (swap x≢y ⊢M))
{-
subst : ∀ {Γ x N V A B}
→ ∅ ⊢ V ⦂ A
→ Γ , x ⦂ A ⊢ N ⦂ B
--------------------
→ Γ ⊢ N [ x := V ] ⦂ B
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 {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))
-}
\end{code}
We induct on the evidence that `N` is well-typed in the
context `Γ` extended by `x`.