From cb27a230c8150e09f87c996179e8e80db6009b6e Mon Sep 17 00:00:00 2001 From: wadler Date: Mon, 26 Jun 2017 13:38:08 +0100 Subject: [PATCH] further improvements to StlcProp, only two holes left --- src/StlcProp.lagda | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/StlcProp.lagda b/src/StlcProp.lagda index f5eabe7c..04af9e38 100644 --- a/src/StlcProp.lagda +++ b/src/StlcProp.lagda @@ -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 = {!!}