Skip to content

Commit

Permalink
Added proof that substitution commutes with weakening
Browse files Browse the repository at this point in the history
  • Loading branch information
Alan Jeffrey committed Nov 4, 2011
1 parent db5d8b1 commit ed37751
Show file tree
Hide file tree
Showing 2 changed files with 87 additions and 6 deletions.
88 changes: 82 additions & 6 deletions src/agda/FRP/JS/Model/STLambdaC/Exp.agda
View file
@@ -1,7 +1,7 @@
import FRP.JS.Model.STLambdaC.Typ

open import FRP.JS.Model.Util using
( _≡_ ; refl ; sym ; cong ; cong₂ ; subst ; begin_ ; _≡⟨_⟩_ ; _∎ ; _∘_ ; ⊥ )
( _≡_ ; refl ; sym ; cong ; cong₂ ; subst ; subst-natural ; begin_ ; _≡⟨_⟩_ ; _∎ ; _∘_ ; ⊥ )

module FRP.JS.Model.STLambdaC.Exp
(TConst : Set)
Expand Down Expand Up @@ -204,11 +204,16 @@ mutual

xsubstn+-∙ : ∀ {k l} B Γ Δ E (σ : Substn k Γ Δ) (ρ : Substn l Δ E) {T} (x : Case T B E) →
(substn+ B Γ Δ σ (expr (xsubstn+ B Δ E ρ x)) ≡ expr (xsubstn+ B Γ E (σ ∙ ρ) x))
xsubstn+-∙ {k} {var} B Γ Δ E σ ρ (inj₁ x) = cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≪ x Δ)
xsubstn+-∙ {var} {exp var} B Γ Δ E σ ρ (inj₁ x) = cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≪ x Δ)
xsubstn+-∙ {exp var} {exp var} B Γ Δ E σ ρ (inj₁ x) = cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≪ x Δ)
xsubstn+-∙ {var} {var} B Γ Δ E σ ρ (inj₂ x) = cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≫ B (ρ x))
xsubstn+-∙ {exp var} {var} B Γ Δ E σ ρ (inj₂ x) = cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≫ B (ρ x))
xsubstn+-∙ {k} {var} B Γ Δ E σ ρ (inj₁ x) =
cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≪ x Δ)
xsubstn+-∙ {var} {exp var} B Γ Δ E σ ρ (inj₁ x) =
cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≪ x Δ)
xsubstn+-∙ {exp var} {exp var} B Γ Δ E σ ρ (inj₁ x) =
cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≪ x Δ)
xsubstn+-∙ {var} {var} B Γ Δ E σ ρ (inj₂ x) =
cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≫ B (ρ x))
xsubstn+-∙ {exp var} {var} B Γ Δ E σ ρ (inj₂ x) =
cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≫ B (ρ x))
xsubstn+-∙ {var} {exp var} B Γ Δ E σ ρ (inj₂ x) =
begin
substn+ B Γ Δ σ (weaken* B (ρ x))
Expand Down Expand Up @@ -324,3 +329,74 @@ weaken*-comm A B Γ Δ M =
≡⟨ cong (par (id (A ++ B)) (snd Γ Δ)) (case-⋙ A B Δ x) ⟩
par (id (A ++ B)) (snd Γ Δ) (case (A ++ B) Δ (A ≫ x))
∎

weaken-comm : ∀ T B Γ Δ {U} (M : Exp (B ++ Δ) U) →
weaken T (weaken+ B Γ Δ M)
≡ weaken+ (T ∷ B) Γ Δ (weaken T M)
weaken-comm T = weaken*-comm [ T ]

-- Weakening distributes through susbtn

weaken-substn : ∀ B Γ Δ {T U} (M : Exp (B ++ Δ) T) (N : Exp (T ∷ B ++ Δ) U) →
substn (weaken+ B Γ Δ M) (weaken+ (T ∷ B) Γ Δ N)
≡ weaken+ B Γ Δ (substn M N)
weaken-substn B Γ Δ {T} M N = begin
substn (weaken+ B Γ Δ M) (weaken+ (T ∷ B) Γ Δ N)
≡⟨ cong₂ substn (substn+* B (Γ ++ Δ) Δ (snd Γ Δ) M) (substn+* (T ∷ B) (Γ ++ Δ) Δ (snd Γ Δ) N) ⟩
substn (substn* (id B +++ snd Γ Δ) M) (substn* (id (T ∷ B) +++ snd Γ Δ) N)
≡⟨ substn*-∙ (substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ)) (id (T ∷ B) +++ snd Γ Δ) N ⟩
substn* ((substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ)) ∙ (id (T ∷ B) +++ snd Γ Δ)) N
≡⟨ substn*-cong lemma₂ N ⟩
substn* ((id B +++ snd Γ Δ) ∙ (M ◁ id (B ++ Δ))) N
≡⟨ sym (substn*-∙ (id B +++ snd Γ Δ) (M ◁ id (B ++ Δ)) N) ⟩
substn* (id B +++ snd Γ Δ) (substn M N)
≡⟨ sym (substn+* B (Γ ++ Δ) Δ (snd Γ Δ) (substn M N)) ⟩
weaken+ B Γ Δ (substn M N)
∎ where

lemma₁ : ∀ {S} (x : Case₃ S [ T ] B Δ) →
(substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ))
(par (id (T ∷ B)) (snd Γ Δ) (caseˡ x))
≡ substn* (id B +++ snd Γ Δ)
(choose ⟨ M ⟩ (id (B ++ Δ)) (caseʳ x))
lemma₁ (inj₁ x) = begin
(substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ)) (x ≪ B ≪ Γ ≪ Δ)
≡⟨ cong (choose ⟨ substn* (id B +++ snd Γ Δ) M ⟩ (id (B ++ Γ ++ Δ))) (case-≪ x (B ++ Γ ++ Δ)) ⟩
⟨ substn* (id B +++ snd Γ Δ) M ⟩ x
≡⟨ subst-natural (uniq x) (substn* (id B +++ snd Γ Δ)) M ⟩
substn* (id B +++ snd Γ Δ) (⟨ M ⟩ x)
∎
lemma₁ (inj₂ x) = begin
(substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ)) ([ T ] ≫ x ≪ Γ ≪ Δ)
≡⟨ cong (choose ⟨ substn* (id B +++ snd Γ Δ) M ⟩ (id (B ++ Γ ++ Δ))) (case-≫ [ T ] (x ≪ Γ ≪ Δ)) ⟩
var (x ≪ Γ ≪ Δ)
≡⟨ cong (var ∘ par (id B) (snd Γ Δ)) (sym (case-≪ x Δ)) ⟩
var ((id B +++ snd Γ Δ) (x ≪ Δ))
≡⟨ cong (var ∘ xsubstn+ [] (B ++ Γ ++ Δ) (B ++ Δ) (id B +++ snd Γ Δ)) (sym (case-≫ [] (x ≪ Δ))) ⟩
substn* (id B +++ snd Γ Δ) (var (x ≪ Δ))
∎
lemma₁ (inj₃ x) = begin
(substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ)) ([ T ] ≫ B ≫ Γ ≫ x)
≡⟨ cong (choose ⟨ substn* (id B +++ snd Γ Δ) M ⟩ (id (B ++ Γ ++ Δ))) (case-≫ [ T ] (B ≫ Γ ≫ x)) ⟩
var (B ≫ Γ ≫ x)
≡⟨ cong (var ∘ par (id B) (snd Γ Δ)) (sym (case-≫ B x)) ⟩
var ((id B +++ snd Γ Δ) (B ≫ x))
≡⟨ cong (var ∘ xsubstn+ [] (B ++ Γ ++ Δ) (B ++ Δ) (id B +++ snd Γ Δ)) (sym (case-≫ [] (B ≫ x))) ⟩
substn* (id B +++ snd Γ Δ) (var (B ≫ x))
∎

lemma₂ : ((substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ)) ∙ (id (T ∷ B) +++ snd Γ Δ))
≈ ((id B +++ snd Γ Δ) ∙ (M ◁ id (B ++ Δ)))
lemma₂ {S} x = begin
((substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ)) ∙ (id (T ∷ B) +++ snd Γ Δ)) x
≡⟨ cong (substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ) ∘ par (id (T ∷ B)) (snd Γ Δ))
(sym (caseˡ₃ [ T ] B Δ x)) ⟩
(substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ))
(par (id (T ∷ B)) (snd Γ Δ) (caseˡ (case₃ [ T ] B Δ x)))
≡⟨ lemma₁ (case₃ [ T ] B Δ x) ⟩
substn* (id B +++ snd Γ Δ)
(choose ⟨ M ⟩ (id (B ++ Δ)) (caseʳ (case₃ [ T ] B Δ x)))
≡⟨ cong (substn* (id B +++ snd Γ Δ) ∘ choose ⟨ M ⟩ (id (B ++ Δ)))
(caseʳ₃ [ T ] B Δ x) ⟩
((id B +++ snd Γ Δ) ∙ (M ◁ id (B ++ Δ))) x
∎
5 changes: 5 additions & 0 deletions src/agda/FRP/JS/Model/Util.agda
View file
Expand Up @@ -58,6 +58,11 @@ cong₂ f refl refl = refl
(a≡b : a ≡ b) → (subst B a≡b c ≡ d) → (f a c ≡ f b d)
δcong₂ f refl refl = refl

subst-natural : {A : Set} {B C : A → Set} {a₁ a₂ : A} (p : a₁ ≡ a₂)
(f : ∀ {a} → B a → C a) (b : B a₁) →
subst C p (f b) ≡ f (subst B p b)
subst-natural refl f b = refl

private
primitive
primTrustMe : ∀ {α} {A : Set α} {a b : A} → (a ≡ b)
Expand Down

0 comments on commit ed37751

Please sign in to comment.