diff --git a/src/DeBruijn.lagda b/src/DeBruijn.lagda index 8ee91bee..e63a3030 100644 --- a/src/DeBruijn.lagda +++ b/src/DeBruijn.lagda @@ -143,11 +143,17 @@ Simultaneous substitution, a la McBride ## Renaming \begin{code} -ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B) +ext : ∀ {Γ Δ} + → (∀ {B} → Γ ∋ B → Δ ∋ B) + ---------------------------------- + → (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B) ext σ Z = Z ext σ (S x) = S (σ x) -rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A} → Γ ⊢ A → Δ ⊢ A) +rename : ∀ {Γ Δ} + → (∀ {A} → Γ ∋ A → Δ ∋ A) + ------------------------ + → (∀ {A} → Γ ⊢ A → Δ ⊢ A) rename σ (⌊ n ⌋) = ⌊ σ n ⌋ rename σ (ƛ N) = ƛ (rename (ext σ) N) rename σ (L · M) = (rename σ L) · (rename σ M) @@ -160,11 +166,17 @@ rename σ (μ N) = μ (rename (ext σ) N) ## Substitution \begin{code} -exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ⊢ B) +exts : ∀ {Γ Δ} + → (∀ {B} → Γ ∋ B → Δ ⊢ B) + ---------------------------------- + → (∀ {A B} → Γ , A ∋ B → Δ , A ⊢ B) exts ρ Z = ⌊ Z ⌋ exts ρ (S x) = rename S_ (ρ x) -subst : ∀ {Γ Δ} → (∀ {C} → Γ ∋ C → Δ ⊢ C) → (∀ {C} → Γ ⊢ C → Δ ⊢ C) +subst : ∀ {Γ Δ} + → (∀ {A} → Γ ∋ A → Δ ⊢ A) + ------------------------ + → (∀ {A} → Γ ⊢ A → Δ ⊢ A) subst ρ (⌊ k ⌋) = ρ k subst ρ (ƛ N) = ƛ (subst (exts ρ) N) subst ρ (L · M) = (subst ρ L) · (subst ρ M) diff --git a/src/Maps.lagda b/src/Maps.lagda index 723c16da..79652b37 100644 --- a/src/Maps.lagda +++ b/src/Maps.lagda @@ -293,7 +293,8 @@ updates. ... | 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)) + ... | 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. @@ -305,7 +306,8 @@ And a slightly different version of the same proof. ... | yes x≡z | yes y≡z = ⊥-elim (x≢y (trans x≡z (sym y≡z))) ... | no x≢z | yes y≡z rewrite y≡z = sym (update-eq′ ρ z w) ... | yes x≡z | no y≢z rewrite x≡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)) + ... | no x≢z | no y≢z = trans (update-neq ρ x v z x≢z) + (sym (update-neq ρ y w z y≢z)) \end{code} diff --git a/src/StlcPropNew.lagda b/src/StlcPropNew.lagda index 1ecdc3ac..8ecb54f9 100644 --- a/src/StlcPropNew.lagda +++ b/src/StlcPropNew.lagda @@ -337,79 +337,32 @@ as the two contexts agree on those variables, one can be exchanged for the other. \begin{code} -context-lemma : ∀ {Γ Δ M A} - → (∀ {w B} → w ∈ M → Γ ∋ w ⦂ B → Δ ∋ w ⦂ B) - → Γ ⊢ M ⦂ A - → Δ ⊢ M ⦂ A -\end{code} +ext : ∀ {Γ Δ} + → (∀ {w B} → Γ ∋ w ⦂ B → Δ ∋ w ⦂ B) + ----------------------------------------------------- + → (∀ {w x A B} → Γ , x ⦂ A ∋ w ⦂ B → Δ , x ⦂ A ∋ w ⦂ B) +ext σ Z = Z +ext σ (S w≢ ∋w) = S w≢ (σ ∋w) -_Proof_: By induction on the derivation of `Γ ⊢ M ⦂ A`. - - - If the last rule in the derivation was `Ax`, then `M = x` - and `Γ x ≡ just A`. By assumption, `Γ′ x = just A` as well, and - hence `Γ′ ⊢ M : A` by `Ax`. - - - If the last rule was `⇒-I`, then `M = λ[ y : A] N`, with - `A = A ⇒ B` and `Γ , y ⦂ A ⊢ N ⦂ B`. The - induction hypothesis is that, for any context `Γ″`, if - `Γ , y : A` and `Γ″` assign the same types to all the - free variables in `N`, then `N` has type `B` under - `Γ″`. Let `Γ′` be a context which agrees with - `Γ` on the free variables in `N`; we must show - `Γ′ ⊢ λ[ y ⦂ A] N ⦂ A ⇒ B`. - - By `⇒-I`, it suffices to show that `Γ′ , y:A ⊢ N ⦂ B`. - By the IH (setting `Γ″ = Γ′ , y : A`), it suffices to show - that `Γ , y : A` and `Γ′ , y : A` agree on all the variables - that appear free in `N`. - - Any variable occurring free in `N` must be either `y` or - some other variable. Clearly, `Γ , y : A` and `Γ′ , y : A` - agree on `y`. Otherwise, any variable other - than `y` that occurs free in `N` also occurs free in - `λ[ y : A] N`, and by assumption `Γ` and - `Γ′` agree on all such variables; hence so do - `Γ , y : A` and `Γ′ , y : A`. - - - If the last rule was `⇒-E`, then `M = L · M`, with `Γ ⊢ L ⦂ A ⇒ B` - and `Γ ⊢ M ⦂ B`. One induction hypothesis states that for all - contexts `Γ′`, if `Γ′` agrees with `Γ` on the free variables in - `L` then `L` has type `A ⇒ B` under `Γ′`; there is a similar IH - for `M`. We must show that `L · M` also has type `B` under `Γ′`, - given the assumption that `Γ′` agrees with `Γ` on all the free - variables in `L · M`. By `⇒-E`, it suffices to show that `L` and - `M` each have the same type under `Γ′` as under `Γ`. But all free - variables in `L` are also free in `L · M`; in the proof, this is - expressed by composing `free-·₁ : ∀ {x} → x ∈ L → x ∈ L · M` with - `Γ~Γ′ : (∀ {x} → x ∈ L · M → Γ x ≡ Γ′ x)` to yield `Γ~Γ′ ∘ free-·₁ - : ∀ {x} → x ∈ L → Γ x ≡ Γ′ x`. Similarly for `M`; hence the - desired result follows from the induction hypotheses. - - - The remaining cases are similar to `⇒-E`. - -\begin{code} -context-lemma Γ⊆Δ (Ax ∋w) = Ax (Γ⊆Δ free-# ∋w) -context-lemma {Γ} {Δ} {ƛ x ⇒ N} Γ⊆Δ (⇒-I ⊢N) = ⇒-I (context-lemma Γ′⊆Δ′ ⊢N) - where - Γ′⊆Δ′ : ∀ {w A B} → w ∈ N → Γ , x ⦂ A ∋ w ⦂ B → Δ , x ⦂ A ∋ w ⦂ B - Γ′⊆Δ′ ∈N Z = Z - Γ′⊆Δ′ ∈N (S w≢ ∋w) = S w≢ (Γ⊆Δ (free-ƛ w≢ ∈N) ∋w) -context-lemma Γ⊆Δ (⇒-E ⊢L ⊢M) = ⇒-E (context-lemma (Γ⊆Δ ∘ free-·₁) ⊢L) - (context-lemma (Γ⊆Δ ∘ free-·₂) ⊢M) -context-lemma Γ⊆Δ 𝔹-I₁ = 𝔹-I₁ -context-lemma Γ⊆Δ 𝔹-I₂ = 𝔹-I₂ -context-lemma Γ⊆Δ (𝔹-E ⊢L ⊢M ⊢N) = 𝔹-E (context-lemma (Γ⊆Δ ∘ free-if₁) ⊢L) - (context-lemma (Γ⊆Δ ∘ free-if₂) ⊢M) - (context-lemma (Γ⊆Δ ∘ free-if₃) ⊢N) +rename : ∀ {Γ Δ} + → (∀ {w B} → Γ ∋ w ⦂ B → Δ ∋ w ⦂ B) + ---------------------------------- + → (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A) +rename σ (Ax ∋w) = Ax (σ ∋w) +rename σ (⇒-I ⊢N) = ⇒-I (rename (ext σ) ⊢N) +rename σ (⇒-E ⊢L ⊢M) = ⇒-E (rename σ ⊢L) (rename σ ⊢M) +rename σ 𝔹-I₁ = 𝔹-I₁ +rename σ 𝔹-I₂ = 𝔹-I₂ +rename σ (𝔹-E ⊢L ⊢M ⊢N) = 𝔹-E (rename σ ⊢L) (rename σ ⊢M) (rename σ ⊢N) \end{code} As a corollary, any closed term can be weakened to any context. \begin{code} -weaken-closed : ∀ {M A Γ} → ∅ ⊢ M ⦂ A → Γ ⊢ M ⦂ A -weaken-closed {M} {A} {Γ} ⊢M = context-lemma ∅⊆Δ ⊢M +rename₀ : ∀ {Γ M A} → ∅ ⊢ M ⦂ A → Γ ⊢ M ⦂ A +rename₀ {Γ} ⊢M = rename σ₀ ⊢M where - ∅⊆Δ : ∀ {w B} → w ∈ M → ∅ ∋ w ⦂ B → Γ ∋ w ⦂ B - ∅⊆Δ _ () + σ₀ : ∀ {w B} → ∅ ∋ w ⦂ B → Γ ∋ w ⦂ B + σ₀ () \end{code} Now we come to the conceptual heart of the proof that reduction @@ -428,16 +381,6 @@ and obtain a new term that still has type `B`. _Lemma_: If `Γ , x ⦂ A ⊢ N ⦂ B` and `∅ ⊢ V ⦂ A`, then `Γ ⊢ (N [ x := V ]) ⦂ B`. -\begin{code} -{- -preservation-[:=] : ∀ {Γ w A N B V} - → Γ , w ⦂ A ⊢ N ⦂ B - → ∅ ⊢ V ⦂ A - ----------------------- - → Γ ⊢ N [ w := V ] ⦂ B --} -\end{code} - One technical subtlety in the statement of the lemma is that we assume `V` is closed; it has type `A` in the _empty_ context. This assumption simplifies the `λ` case of the proof because the context @@ -456,62 +399,30 @@ assign a type to `N [ x := V ]`---the result is the same either way. --> -_Proof_: By induction on the derivation of `Γ , x ⦂ A ⊢ N ⦂ B`, -we show that if `∅ ⊢ V ⦂ A` then `Γ ⊢ N [ x := V ] ⦂ B`. - - - If `N` is a variable there are two cases to consider, - depending on whether `N` is `x` or some other variable. - - - If `N = `` `x ``, then from `Γ , x ⦂ A ⊢ x ⦂ B` - we know that looking up `x` in `Γ , x : A` gives - `just B`, but we already know it gives `just A`; - applying injectivity for `just` we conclude that `A ≡ B`. - We must show that `x [ x := V] = V` - has type `A` under `Γ`, given the assumption that - `V` has type `A` under the empty context. This - follows from context invariance: if a closed term has type - `A` in the empty context, it has that type in any context. - - - If `N` is some variable `x′` different from `x`, then - we need only note that `x′` has the same type under `Γ , x ⦂ A` - as under `Γ`. - - - If `N` is an abstraction `λ[ x′ ⦂ A′ ] N′`, then the IH tells us, - for all `Γ′`́ and `B′`, that if `Γ′ , x ⦂ A ⊢ N′ ⦂ B′` - and `∅ ⊢ V ⦂ A`, then `Γ′ ⊢ N′ [ x := V ] ⦂ B′`. - - The substitution in the conclusion behaves differently - depending on whether `x` and `x′` are the same variable. - - First, suppose `x ≡ x′`. Then, by the definition of - substitution, `N [ x := V] = N`, so we just need to show `Γ ⊢ N ⦂ B`. - But we know `Γ , x ⦂ A ⊢ N ⦂ B` and, since `x ≡ x′` - does not appear free in `λ[ x′ ⦂ A′ ] N′`, the context invariance - lemma yields `Γ ⊢ N ⦂ B`. - - Second, suppose `x ≢ x′`. We know `Γ , x ⦂ A , x′ ⦂ A′ ⊢ N′ ⦂ B′` - by inversion of the typing relation, from which - `Γ , x′ ⦂ A′ , x ⦂ A ⊢ N′ ⦂ B′` follows by update permute, - so the IH applies, giving us `Γ , x′ ⦂ A′ ⊢ N′ [ x := V ] ⦂ B′` - By `⇒-I`, we have `Γ ⊢ λ[ x′ ⦂ A′ ] (N′ [ x := V ]) ⦂ A′ ⇒ B′` - and the definition of substitution (noting `x ≢ x′`) gives - `Γ ⊢ (λ[ x′ ⦂ A′ ] N′) [ x := V ] ⦂ A′ ⇒ B′` as required. - - - If `N` is an application `L′ · M′`, the result follows - straightforwardly from the definition of substitution and the - induction hypotheses. - - - The remaining cases are similar to application. - \begin{code} +permute : ∀ {Γ x y z A B C} + → x ≢ y + → Γ , x ⦂ A , y ⦂ B ∋ z ⦂ C + -------------------------- + → Γ , y ⦂ B , x ⦂ A ∋ z ⦂ C +permute x≢y Z = S (λ{refl → x≢y refl}) Z +permute x≢y (S z≢y Z) = Z +permute x≢y (S z≢y (S z≢x ∋w)) = S z≢x (S z≢y ∋w) + +substitution : ∀ {Γ w A N B V} + → Γ , w ⦂ A ⊢ N ⦂ B + → ∅ ⊢ V ⦂ A + ----------------------- + → Γ ⊢ N [ w := V ] ⦂ B +substitution ⊢N ⊢V = {!!} {- -preservation-[:=] {Γ} {w} {A} (Ax {.(Γ , w ⦂ A)} {x} ∋x) ⊢V with w ≟ x -...| yes refl = weaken-closed ⊢V +substitution {Γ} {w} {A} (Ax {.(Γ , w ⦂ A)} {x} ∋x) ⊢V with w ≟ x +...| yes refl = rename₀ ⊢V ...| no w≢ with ∋x ... | Z = ⊥-elim (w≢ refl) ... | S _ ∋x′ = Ax ∋x′ -preservation-[:=] {Γ} {w} {A} {ƛ x ⦂ A′ ] N′} {.A′ ⇒ B′} {V} (⇒-I ⊢N′) ⊢V with x ≟ x′ -...| yes x≡x′ rewrite x≡x′ = context-lemma Γ′~Γ (⇒-I ⊢N′) +substitution {Γ} {w} {A} {ƛ x ⦂ A′ ] N′} {.A′ ⇒ B′} {V} (⇒-I ⊢N′) ⊢V with x ≟ x′ +...| yes x≡x′ rewrite x≡x′ = rename Γ′~Γ (⇒-I ⊢N′) where Γ′~Γ : ∀ {y} → y ∈ (λ[ x′ ⦂ A′ ] N′) → (Γ , x′ ⦂ A) y ≡ Γ y Γ′~Γ {y} (free-λ x′≢y y∈N′) with x′ ≟ y @@ -522,12 +433,12 @@ preservation-[:=] {Γ} {w} {A} {ƛ x ⦂ A′ ] N′} {.A′ ⇒ B′} {V} (⇒- x′x⊢N′ : Γ , x′ ⦂ A′ , x ⦂ A ⊢ N′ ⦂ B′ x′x⊢N′ rewrite update-permute Γ x A x′ A′ x≢x′ = ⊢N′ ⊢N′V : (Γ , x′ ⦂ A′) ⊢ N′ [ x := V ] ⦂ B′ - ⊢N′V = preservation-[:=] x′x⊢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) + ⊢N′V = substitution x′x⊢N′ ⊢V +substitution (⇒-E ⊢L ⊢M) ⊢V = ⇒-E (substitution ⊢L ⊢V) (substitution ⊢M ⊢V) +substitution 𝔹-I₁ ⊢V = 𝔹-I₁ +substitution 𝔹-I₂ ⊢V = 𝔹-I₂ +substitution (𝔹-E ⊢L ⊢M ⊢N) ⊢V = + 𝔹-E (substitution ⊢L ⊢V) (substitution ⊢M ⊢V) (substitution ⊢N ⊢V) -} \end{code} @@ -579,7 +490,7 @@ _Proof_: By induction on the derivation of `∅ ⊢ M ⦂ A`. {- preservation (Ax Γx≡A) () preservation (⇒-I ⊢N) () -preservation (⇒-E (⇒-I ⊢N) ⊢V) (βλ· valueV) = preservation-[:=] ⊢N ⊢V +preservation (⇒-E (⇒-I ⊢N) ⊢V) (βλ· valueV) = substitution ⊢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′