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

further improvements to StlcProp, only two holes left

Browse source
This commit is contained in:
wadler 2017-06-26 13:38:08 +01:00
parent 3da3cdb235
commit cb27a230c8
1 changed files with 10 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/StlcProp.lagda
View file

@ -480,18 +480,24 @@ just-injective refl = refl
\end{code}
\begin{code}
preservation-[:=] {_} {x} (Ax {_} {x′} Γx′≡B) ⊢V with x ≟ x′
...| yes x≡x′ rewrite just-injective Γx′≡B = weaken-closed ⊢V
...| no x≢x′ = Ax Γx′≡B
{-
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-[:=] {Γ} {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)
{-
[:=]-preserves-⊢ {Γ} {x} v∶A (var y y∈Γ) with x ≟ y
... | yes x=y = {!!}