Stoughton.SubstitutionLemmas

open import Relation.Binary hiding (Rel)
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; _≢_; refl; sym; cong; cong₂; trans; setoid)
open import Stoughton.Var

module Stoughton.SubstitutionLemmas (𝒞 : Set) {𝒱 : Set} (var : Enum 𝒱) where

  private 
    _≟_ = Enum._≟_ var

  open import Stoughton.Chi (Enum.encode var) (Enum.decode var) (Enum.inverse var)
  open import Stoughton.Syntax 𝒞 𝒱 _≟_
  open import Stoughton.Substitution 𝒞 var
  open import Stoughton.Alpha 𝒞 var

  open import Relation.Binary using (Decidable)
  open import Relation.Binary.PropositionalEquality using (_≡_; subst)

  open import Data.Empty
  open import Data.Nat hiding (_*_; _≟_)
  open import Data.Nat.Properties hiding (_≟_)
  open import Relation.Nullary
  open import Function renaming (_∘_ to _∘f_)
  open import Data.Product renaming (Σ to Σₓ)
  
  open PropEq.≡-Reasoning renaming (begin_ to begin≡_;_∎ to _◻)
  open import Data.List as List hiding (any) renaming (length to length') 
  open import Data.List.Properties
  open import Data.List.Relation.Unary.Any as Any hiding (map)
  open import Data.List.Membership.Propositional
  open import Data.List.Membership.Propositional.Properties

  ++-injʳ : {xs xs' ys ys' : List 𝒱} → xs ≡ xs' → xs ++ ys ≡ xs' ++ ys' → ys ≡ ys'
  ++-injʳ {[]} .{[]} {ys} {ys'} refl ys=ys' = ys=ys'
  ++-injʳ {x ∷ xs} .{x ∷ xs} {ys} {ys'} refl x:xs++ys=x:xs++ys' = ++-injʳ refl (∷-injectiveʳ x:xs++ys=x:xs++ys')

  fvλ∼ : ∀ {x x' A A' M M'} → λ[ x ∶ A ] M ∼α λ[ x' ∶ A' ] M' → fv M - x ≡ fv M' - x'
  fvλ∼ e@(∼λ A∼A' _ _ _) = ++-injʳ (M∼M'→fvM≡fvM' A∼A') (M∼M'→fvM≡fvM' e)

  fvΠ∼ : ∀ {x x' A A' M M'} → Π[ x ∶ A ] M ∼α Π[ x' ∶ A' ] M' → fv M - x ≡ fv M' - x'
  fvΠ∼ e@(∼Π A∼A' _ _ _) = ++-injʳ (M∼M'→fvM≡fvM' A∼A') (M∼M'→fvM≡fvM' e)

  compatSubAlpha : ∀ {M M' σ} → M ∼α M' → M ∙ σ ≡ M' ∙ σ
  compatSubAlpha ∼c              = refl
  compatSubAlpha ∼v              = refl
  compatSubAlpha (∼· M∼M' N∼N') = cong₂ _·_ (compatSubAlpha M∼M') (compatSubAlpha N∼N')
  compatSubAlpha {σ = σ} λxAM∼λx'A'M'@(∼λ {x} {x'} {z} {A} {A'} {M} {M'} A∼A' z#λxM z#λx'M' Mι≺+xz∼M'ι≺+x'z) rewrite fvλ∼ λxAM∼λx'A'M' =
    cong₂ (λ[_∶_]_ y) (compatSubAlpha A∼A') Mσx,y=M'σx'y
    where
    y : 𝒱
    y = X(σ , fv M' - x')
    Mσx,y=M'σx'y : M ∙ (σ ‚ x := v y) ≡ M' ∙ (σ ‚ x' := v y)
    Mσx,y=M'σx'y =
      begin≡
      M ∙ (σ ‚ x := v y)
      ≡⟨ composRenUpd {x} {z} {M} z#λxM ⟩
      (M ∙ (ι ‚ x := v z)) ∙ (σ ‚ z := v y)
      ≡⟨ cong₂ _∙_ Mι≺+xz∼M'ι≺+x'z refl ⟩
      (M' ∙ (ι ‚ x' := v z)) ∙ (σ ‚ z := v y)
      ≡⟨ sym (composRenUpd {x'} {z} {M'} z#λx'M') ⟩
      M' ∙ (σ ‚ x' := v y)
      ◻    
  compatSubAlpha {σ = σ} ΠxAM∼Πx'A'M'@(∼Π {x} {x'} {z} {A} {A'} {M} {M'} A∼A' z#λxM z#λx'M' Mι≺+xz∼M'ι≺+x'z) rewrite fvΠ∼ ΠxAM∼Πx'A'M' =
    cong₂ (Π[_∶_]_ y) (compatSubAlpha A∼A') Mσx,y=M'σx'y
    where
    y : 𝒱
    y = X(σ , fv M' - x')
    Mσx,y=M'σx'y : M ∙ (σ ‚ x := v y) ≡ M' ∙ (σ ‚ x' := v y)
    Mσx,y=M'σx'y =
      begin≡
      M ∙ (σ ‚ x := v y)
      ≡⟨ composRenUpd {x} {z} {M} z#λxM ⟩
      (M ∙ (ι ‚ x := v z)) ∙ (σ ‚ z := v y)
      ≡⟨ cong₂ _∙_ Mι≺+xz∼M'ι≺+x'z refl ⟩
      (M' ∙ (ι ‚ x' := v z)) ∙ (σ ‚ z := v y)
      ≡⟨ sym (composRenUpd {x'} {z} {M'} z#λx'M') ⟩
      M' ∙ (σ ‚ x' := v y)
      ◻       

  ∼σ : Symmetric _∼α_
  ∼σ {M} {N} M∼N 
    = iotaAlpha 
            (sym (compatSubAlpha M∼N))

  ∼τ : Transitive _∼α_
  ∼τ {M} {N} {P} M∼N N∼P 
    = iotaAlpha 
           (trans (compatSubAlpha M∼N) 
                  (compatSubAlpha N∼P))

  ≈-preorder∼ : Preorder _ _ _
  ≈-preorder∼ =  
      record { 
        Carrier = Λ;
        _≈_ = _≡_;
        _∼_ = _∼α_;
        isPreorder =  record {
          isEquivalence = Relation.Binary.Setoid.isEquivalence (setoid Λ) ;
          reflexive = λ { {M} {.M} refl → ∼ρ {M}};
          trans = ∼τ } }

  import Relation.Binary.Reasoning.Preorder as PreR

  lemma-σ⇂ : {M : List 𝒱}{σ σ' : Sub} → σ ∼α σ' ⇂ M → ((ι ⊙ σ) , M) ≅⇂ₗ ((ι ⊙ σ') , M)
  lemma-σ⇂ σ∼σ'⇂M  = ∼*ρ , (λ x xfreeM → compatSubAlpha (σ∼σ'⇂M  x xfreeM))

  subAlpha : ∀ {M σ σ'} → σ ∼α σ' ⇂ fv M → M ∙ σ ∼α M ∙ σ'
  subAlpha {M} {σ} {σ'} σ∼ασ'⇂M = iotaAlpha aux
    where
      aux : (M ∙ σ) ∙ ι ≡ (M ∙ σ') ∙ ι
      aux = begin≡
        (M ∙ σ) ∙ ι
        ≡⟨ subComp {M} {σ} {ι} ⟩
        M ∙ (ι ⊙ σ)
        ≡⟨  subEqRes {M} {ι ⊙ σ} {ι ⊙ σ'} (lemma-σ⇂ σ∼ασ'⇂M) ⟩
        M ∙ (ι ⊙ σ')
        ≡⟨ sym (subComp {M} {σ'} {ι}) ⟩
        (M ∙ σ') ∙ ι                                               ◻ 

  lemma-subst : ∀ {M M' σ σ'} → M ∼α M' → σ ∼α σ' ⇂ fv M → M ∙ σ ∼α M' ∙ σ'
  lemma-subst {M} {M'} {σ} {σ'} M∼M' σ∼σ'⇂M 
    =  begin
         M ∙ σ
         ∼⟨ subAlpha {M} σ∼σ'⇂M ⟩
         M ∙ σ'
         ≈⟨ compatSubAlpha M∼M'  ⟩
         M' ∙ σ'
       ∎
    where open PreR ≈-preorder∼ 

  lemma∙ι : ∀ {M} → M ∼α M ∙ ι
  lemma∙ι {M} = iotaAlpha ( begin≡
                                      M ∙ ι
                                    ≡⟨ subEqRes {M} {ι} {ι ⊙ ι} (∼*ρ , (λ _ _ → refl) ) ⟩
                                      M ∙ (ι ⊙ ι)
                                    ≡⟨  sym (subComp {M} {ι} {ι}) ⟩
                                      (M ∙ ι) ∙ ι
                                    ◻) 

  lemma∼λ : {M N A B : Λ}{x : 𝒱} → A ∼α B → M ∼α N → λ[ x ∶ A ] M ∼α λ[ x ∶ B ] N
  lemma∼λ {M} {N} {A} {B} {x} A∼B M∼N = ∼λ A∼B (∉- (fv M)) (∉- (fv N)) lemma∼ƛaux
    where
    lemma∼ƛaux : M ∙ ι ‚ x := v x ≡ N ∙ ι ‚ x := v x
    lemma∼ƛaux = compatSubAlpha {σ = ι ‚ x := v x} M∼N 

  lemma∼Π : {M N A B : Λ}{x : 𝒱} → A ∼α B → M ∼α N → Π[ x ∶ A ] M ∼α Π[ x ∶ B ] N
  lemma∼Π {M} {N} {A} {B} {x} A∼B M∼N = ∼Π A∼B (∉- (fv M)) (∉- (fv N)) lemma∼ƛaux
    where
    lemma∼ƛaux : M ∙ ι ‚ x := v x ≡ N ∙ ι ‚ x := v x
    lemma∼ƛaux = compatSubAlpha {σ = ι ‚ x := v x} M∼N 

  infix 1 _∼ασ_
  _∼ασ_ : Sub → Sub → Set
  σ ∼ασ σ' = (x : 𝒱) → σ x ∼α σ' x

  lemma∼ασ : {σ σ' : Sub}{M : List 𝒱} → σ ∼ασ σ' → σ ∼α σ' ⇂ M
  lemma∼ασ σ∼ασ' x x*M = σ∼ασ' x

  lemmaι∘σ : {σ : Sub} → ι ⊙ σ ∼ασ σ 
  lemmaι∘σ {σ} x = begin
                     σ x ∙ ι
                   ∼⟨ ∼σ (lemma∙ι) ⟩
                     σ x
                   ∎
                   where open PreR ≈-preorder∼ 

  lemma∼≺+ : {x : 𝒱}{N : Λ}{σ σ' : Sub} → σ ∼ασ σ' → σ ‚ x := N ∼ασ σ' ‚ x := N
  lemma∼≺+ {x} σ∼σ' y with x ≟ y
  ... | yes  _ = ∼ρ
  ... | no   _ = σ∼σ' y

  prop8 : {x y : 𝒱}{σ : Sub}{M N : Λ} → y #⇂ (σ , fv M - x) → (ι ‚ y := N ⊙ σ ‚ x := v y) ∼α σ ‚ x := N ⇂ fv M
  prop8 {x} {y} {σ} {M} {N} y#⇂λxM z z*M =
                  begin
                    (ι ‚ y := N ⊙ σ ‚ x := v y) z
                  ≈⟨ lemmaσ∘≺+ M N σ ι x y y#⇂λxM z z*M ⟩
                    ((ι ⊙ σ) ‚ x := N) z
                  ∼⟨ (lemma∼≺+ {x} {N} (lemmaι∘σ {σ})) z ⟩
                    (σ ‚ x := N) z
                  ∎
                  where open PreR ≈-preorder∼ 

  composRenUnary : ∀ {x y σ M N} → y #⇂ (σ , fv M - x) → (M ∙ (σ ‚ x := v y)) [ y := N ] ∼α M ∙ (σ ‚ x := N)
  composRenUnary {x} {y} {σ} {M} {N} y#⇂σ,λxM 
    =  begin
         (M ∙ σ ‚ x := v y) ∙ ι ‚ y := N
       ≈⟨ subComp {M} ⟩
         M ∙ (ι ‚ y := N ⊙ σ ‚ x := v y)
       ∼⟨ subAlpha {M} (prop8 {x} {M = M} y#⇂σ,λxM) ⟩
         M ∙ σ ‚ x := N
       ∎
       where open PreR ≈-preorder∼ 

  corollary4-2 : {x y : 𝒱}{M A : Λ}{σ : Sub} → y #⇂ (σ , fv M - x) → λ[ x ∶ A ] M ∙ σ ∼α λ[ y ∶ A ∙ σ ] (M ∙ σ ‚ x := v y)
  corollary4-2 {x} {y} {M} {A} {σ} y#⇂σ,λxM =
    begin
    λ[ x ∶ A ] M ∙ σ
    ≈⟨ refl ⟩
    λ[ z ∶ A ∙ σ ](M ∙ σ ‚ x := v z)
    ∼⟨ ∼λ ∼ρ w#ƛzM∙σ≺+x,z w#ƛyM∙σ≺+x,y e ⟩
    λ[ y ∶ A ∙ σ ](M ∙ σ ‚ x := v y)
    ∎
    where
    z w : 𝒱
    z = X (σ , fv M - x)
    w = X' ((fv (M ∙ σ ‚ x := v z) - z) ++ (fv (M ∙ σ ‚ x := v y)) - y)
    z#⇂σ,λxM : z #⇂ (σ , fv M - x)
    z#⇂σ,λxM = Xfresh σ (fv M - x)
    aux : ∀ u → u * M → (ι ‚ z := v w ⊙ σ ‚ x := v z) u ≡ (ι ‚ y := v w ⊙ σ ‚ x := v y) u
    aux u u*M with x ≟ u
    aux .x x*M | yes refl with z ≟ z
    aux .x x*M | yes refl | yes refl with y ≟ y
    aux .x x*M | yes refl | yes refl | yes refl = refl
    aux .x x*M | yes refl | yes refl | no y≢y = ⊥-elim (y≢y refl)
    aux .x x*M | yes refl | no z≢z = ⊥-elim (z≢z refl)
    aux u u*M  | no x≢u = trans aux1 (sym aux2)
      where
      aux1 : (σ u) [ z := v w ] ≡ σ u ∙ ι 
      aux1 = updFresh {z} {σ u} (z#⇂σ,λxM u (proj₂ delList (sym≢ x≢u , u*M)))
      aux2 : (σ u) [ y := v w ] ≡ σ u ∙ ι
      aux2 = updFresh {y} {σ u} (y#⇂σ,λxM u (proj₂ delList (sym≢ x≢u , u*M)))
    e : M ∙ σ ‚ x := v z ∙ ι ‚ z := v w ≡ M ∙ σ ‚ x := v y ∙ ι ‚ y := v w
    e = 
      begin≡ 
      M ∙ σ ‚ x := v z ∙ ι ‚ z := v w
      ≡⟨ subComp {M} {σ ‚ x := v z} {ι ‚ z := v w} ⟩
      M ∙ ι ‚ z := v w ⊙ σ ‚ x := v z
      ≡⟨ subEqRes {M} (∼*ρ , aux) ⟩
      M ∙ ι ‚ y := v w ⊙ σ ‚ x := v y      
      ≡⟨ sym (subComp {M} {σ ‚ x := v y} {ι ‚ y := v w}) ⟩
      M ∙ σ ‚ x := v y ∙ ι ‚ y := v w
      ◻
    w#ƛzM∙σ≺+x,z : w ∉ fv (M ∙ σ ‚ x := v z) - z
    w#ƛzM∙σ≺+x,z = c∉xs++ys→c∉xs  {w} {fv ((M ∙ σ ‚ x := v z)) - z} (Xpfresh (((fv (M ∙ σ ‚ x := v z)) - z) ++ (fv (M ∙ σ ‚ x := v y) - y)))
    w#ƛyM∙σ≺+x,y : w ∉ fv (M ∙ σ ‚ x := v y) - y
    w#ƛyM∙σ≺+x,y = c∉xs++ys→c∉ys  {w} {fv ((M ∙ σ ‚ x := v z)) - z} {fv ((M ∙ σ ‚ x := v y)) - y} (Xpfresh ((fv (M ∙ σ ‚ x := v z) - z) ++ (fv (M ∙ σ ‚ x := v y) - y)))
    open PreR ≈-preorder∼ 

  corollary4-2Π : {x y : 𝒱}{M A : Λ}{σ : Sub} → y #⇂ (σ , fv M - x) → Π[ x ∶ A ] M ∙ σ ∼α Π[ y ∶ A ∙ σ ] (M ∙ σ ‚ x := v y)
  corollary4-2Π {x} {y} {M} {A} {σ} y#⇂σ,ΠxM = 
    begin
    Π[ x ∶ A ] M ∙ σ
    ≈⟨ refl ⟩
    Π[ z ∶ A ∙ σ ](M ∙ σ ‚ x := v z)
    ∼⟨ ∼Π ∼ρ w#ƛzM∙σ≺+x,z w#ƛyM∙σ≺+x,y e ⟩
    Π[ y ∶ A ∙ σ ](M ∙ σ ‚ x := v y)
    ∎
    where
    z w : 𝒱
    z = X (σ , fv M - x)
    w = X' ((fv (M ∙ σ ‚ x := v z) - z) ++ (fv (M ∙ σ ‚ x := v y)) - y)
    z#⇂σ,ΠxM : z #⇂ (σ , fv M - x)
    z#⇂σ,ΠxM = Xfresh σ (fv M - x)
    aux : ∀ u → u * M → (ι ‚ z := v w ⊙ σ ‚ x := v z) u ≡ (ι ‚ y := v w ⊙ σ ‚ x := v y) u
    aux u u*M with x ≟ u
    aux .x x*M | yes refl with z ≟ z
    aux .x x*M | yes refl | yes refl with y ≟ y
    aux .x x*M | yes refl | yes refl | yes refl = refl
    aux .x x*M | yes refl | yes refl | no y≢y = ⊥-elim (y≢y refl)
    aux .x x*M | yes refl | no z≢z = ⊥-elim (z≢z refl)
    aux u u*M  | no x≢u = trans aux1 (sym aux2)
      where
      aux1 : (σ u) [ z := v w ] ≡ σ u ∙ ι 
      aux1 = updFresh {z} {σ u} (z#⇂σ,ΠxM u (proj₂ delList (sym≢ x≢u , u*M)))
      aux2 : (σ u) [ y := v w ] ≡ σ u ∙ ι
      aux2 = updFresh {y} {σ u} (y#⇂σ,ΠxM u (proj₂ delList (sym≢ x≢u , u*M)))
    e : M ∙ σ ‚ x := v z ∙ ι ‚ z := v w ≡ M ∙ σ ‚ x := v y ∙ ι ‚ y := v w
    e = 
      begin≡ 
      M ∙ σ ‚ x := v z ∙ ι ‚ z := v w
      ≡⟨ subComp {M} {σ ‚ x := v z} {ι ‚ z := v w} ⟩
      M ∙ ι ‚ z := v w ⊙ σ ‚ x := v z
      ≡⟨ subEqRes {M} (∼*ρ , aux) ⟩
      M ∙ ι ‚ y := v w ⊙ σ ‚ x := v y      
      ≡⟨ sym (subComp {M} {σ ‚ x := v y} {ι ‚ y := v w}) ⟩
      M ∙ σ ‚ x := v y ∙ ι ‚ y := v w
      ◻
    w#ƛzM∙σ≺+x,z : w ∉ fv (M ∙ σ ‚ x := v z) - z
    w#ƛzM∙σ≺+x,z = c∉xs++ys→c∉xs  {w} {fv ((M ∙ σ ‚ x := v z)) - z} (Xpfresh (((fv (M ∙ σ ‚ x := v z)) - z) ++ (fv (M ∙ σ ‚ x := v y) - y)))
    w#ƛyM∙σ≺+x,y : w ∉ fv (M ∙ σ ‚ x := v y) - y
    w#ƛyM∙σ≺+x,y = c∉xs++ys→c∉ys  {w} {fv ((M ∙ σ ‚ x := v z)) - z} {fv ((M ∙ σ ‚ x := v y)) - y} (Xpfresh ((fv (M ∙ σ ‚ x := v z) - z) ++ (fv (M ∙ σ ‚ x := v y) - y)))
    open PreR ≈-preorder∼ 
      
  corollary4-2' : {x y : 𝒱}{M A : Λ} → y ∉ fv M - x → λ[ x ∶ A ] M ∼α λ[ y ∶ A ] (M ∙ ι ‚ x := v y)
  corollary4-2' {x} {y} {M} {A} y#λxM
    =  begin
          λ[ x ∶ A ] M
        ∼⟨ lemma∙ι ⟩
          λ[ x ∶ A ] M ∙ ι
        ∼⟨ corollary4-2 {x} {y} {M} {A} (lemma#→ι#⇂ {y} {x} {fv M} y#λxM)  ⟩
          λ[ y ∶ A ∙ ι ](M ∙ ι ‚ x := v y)
        ∼⟨ lemma∼λ (∼σ lemma∙ι) ∼ρ ⟩
          λ[ y ∶ A ](M ∙ ι ‚ x := v y)
        ∎
        where open PreR ≈-preorder∼

  corollary4-2'Π : {x y : 𝒱}{M A : Λ} → y ∉ fv M - x → Π[ x ∶ A ] M ∼α Π[ y ∶ A ] (M ∙ ι ‚ x := v y)
  corollary4-2'Π {x} {y} {M} {A} y#ΠxM
    =  begin
          Π[ x ∶ A ] M
        ∼⟨ lemma∙ι ⟩
          Π[ x ∶ A ] M ∙ ι
        ∼⟨ corollary4-2Π {x} {y} {M} {A} (lemma#→ι#⇂ {y} {x} {fv M} y#ΠxM)  ⟩
          Π[ y ∶ A ∙ ι ](M ∙ ι ‚ x := v y)
        ∼⟨ lemma∼Π (∼σ lemma∙ι) ∼ρ ⟩
          Π[ y ∶ A ](M ∙ ι ‚ x := v y)
        ∎
        where open PreR ≈-preorder∼

  iotaIdem : ∀ {x y M} → (ι ‚ x := v y) ≅ ι ⊙ ι ‚ x := v y ⇂ fv M
  iotaIdem {x} {y} {M} = ∼*ρ , aux
    where
    aux : ∀ z → z ∈ fv M → (ι ‚ x := v y) z ≡ (ι ⊙ ι ‚ x := v y) z
    aux z _ with x ≟ z
    ... | yes _ = refl
    ... | no _  = refl

  eqSubSym : ∀ {σ σ' M} → σ ≅ σ' ⇂ fv M → σ' ≅ σ ⇂ fv M
  eqSubSym (_ , h) = ∼*ρ , λ x x∈fvM → sym (h x x∈fvM)

  lemma∼⇒≡ : ∀ {M M' x x' y} → M [ x := v y ] ∼α M' [ x' := v y ] → M [ x := v y ] ≡ M' [ x' := v y ]
  lemma∼⇒≡ {M} {M'} {x} {x'} {y} M[x=y]∼M'[x'=y] = begin≡
    M [ x := v y ]
    ≡⟨ subEqRes {M} (iotaIdem {x} {y} {M}) ⟩
    M ∙ ι ⊙ ι ‚ x := v y
    ≡⟨ sym (subComp {M}) ⟩
    M [ x := v y ] ∙ ι
    ≡⟨ compatSubAlpha M[x=y]∼M'[x'=y] ⟩
    M' [ x' := v y ] ∙ ι
    ≡⟨ subComp {M'} ⟩                
    M' ∙ ι ⊙ ι ‚ x' := v y
    ≡⟨ subEqRes {M'} (eqSubSym {M = M'} (iotaIdem {x'} {y} {M'}))  ⟩
    M' [ x' := v y ]
    ◻

  soundAlpha : ∀ {M N} → M ∼α N → M ∼αₛ N
  soundAlpha M∼N = iotaAlphaSt (compatSubAlpha M∼N)

  completeAlpha : ∀ {M N} → M ∼αₛ N → M ∼α N
  completeAlpha ∼c = ∼c
  completeAlpha ∼v = ∼v
  completeAlpha (∼· e f) = ∼· (completeAlpha e) (completeAlpha f)
  completeAlpha (∼λ {M} {M'} {x} {x'} {y} {A} {A'} e f g h) = ∼λ (completeAlpha e) f g (lemma∼⇒≡ {M} {M'} {x} {x'} {y} (completeAlpha h))
  completeAlpha (∼Π {M} {M'} {x} {x'} {y} {A} {A'} e f g h) = ∼Π (completeAlpha e) f g (lemma∼⇒≡ {M} {M'} {x} {x'} {y} (completeAlpha h))