ParallelReduction.Properties

open import Data.Empty
open import Data.Product
open import Relation.Binary.Construct.Closure.ReflexiveTransitive hiding (_⋆)
open import Relation.Binary.Construct.Closure.Equivalence as Eq
open import Relation.Binary.Construct.Union
open import Level
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.Construct.Composition
import Relation.Binary.Reasoning.Preorder as PreR
open import Relation.Binary.PropositionalEquality as PropEq hiding (trans)
open import Data.List
open import Data.List.Membership.Propositional
open import Data.Sum
open import Data.List.Relation.Unary.Any 

open import Stoughton.Var

module ParallelReduction.Properties (𝒞 : Set) {𝒱 : Set} (var : Enum 𝒱) where

  open import Stoughton.Syntax 𝒞 𝒱 (Enum._≟_ var)  
  open import Stoughton.Alpha 𝒞 var
  open import Stoughton.Chi (Enum.encode var) (Enum.decode var) (Enum.inverse var)
  open import Stoughton.Substitution 𝒞 var      
  open import Stoughton.SubstitutionLemmas 𝒞 var
  open import Beta 𝒞 var  
  open import BetaReduction 𝒞 var
  open import BetaConversion 𝒞 var  
  open import Relation 𝒞 var
  open import ParallelReduction 𝒞 var

  private
    _≟_ = Enum._≟_ var
    
  infixl 3 _⇉ₛ_
  _⇉ₛ_ : Sub → Sub → Set
  σ ⇉ₛ σ' = ∀ x → σ x ⇉ σ' x

  lemma⇉s : {σ σ' : Sub}(x y : 𝒱) → σ ⇉ₛ σ' → σ ‚ x := v y ⇉ₛ σ' ‚ x := v y
  lemma⇉s {σ} {σ'} x y σ⇉σ' z with x ≟ z 
  ... | yes  _ = ⇉v
  ... | no   _ = σ⇉σ' z

  lemma⇉# : {x : 𝒱}{M N : Λ} → x # M → M ⇉ N → x # N
  lemma⇉# x#M M⇉N = lemma→α*# x#M (manyStepBetaContainsPar M⇉N) 

  lemma⇉* : {x : 𝒱}{M N : Λ} → x * N → M ⇉ N → x * M
  lemma⇉* x*N M⇉N = lemma→α** x*N (manyStepBetaContainsPar M⇉N) 

  lemma⇉#⇂ : {x y : 𝒱}{M M' : Λ}{σ σ' : Sub} → M ⇉ M' → σ ⇉ₛ σ' → y #⇂ (σ , fv M - x) → y #⇂ (σ' , fv M' - x)
  lemma⇉#⇂ {x} {y} {M} {M'} {σ} {σ'} M⇉M' σ⇉σ' y#σ⇂fvM-x z z∈fvM'-x = y#σ'z
    where
    z≢x : z ≢ x
    z≢x = ∈-→≢ {xs = fv M'} z∈fvM'-x
    z∈fvM' : z ∈ fv M' 
    z∈fvM' = ∈-→∈ z∈fvM'-x
    z∈fvM : z ∈ fv M
    z∈fvM = lemma⇉* z∈fvM' M⇉M' 
    z∈fvM-x : z ∈ fv M - x
    z∈fvM-x = lemma∈-≢ z∈fvM (sym≢ z≢x)
    y#σz : y # σ z
    y#σz = y#σ⇂fvM-x z z∈fvM-x
    y#σ'z : y # σ' z
    y#σ'z = lemma⇉# y#σz (σ⇉σ' z)

  compatParSub : ∀ {M M' σ σ'} → M ⇉ M' → σ ⇉ₛ σ' → ∃ λ N → M ∙ σ ⇉ N × N ∼α M' ∙ σ'
  compatParSub {σ' = σ'} (⇉v {x}) σ⇉σ' = σ' x , σ⇉σ' x , ∼ρ
  compatParSub (⇉c {k}) _ = c k , ⇉c , ∼c
  compatParSub {λ[ .x ∶ .A ] M} {λ[ .x ∶ .A' ] M'} {σ} {σ'} (⇉λ {x} {A} {A'} A⇉A' M⇉M') σ⇉σ'
    with compatParSub A⇉A' σ⇉σ' | compatParSub M⇉M' (lemma⇉s x (X (σ , fv M - x)) σ⇉σ')
  ... | B , Aσ⇉B , B∼A'σ' | N , Mσ,x=y⇉N , N∼M'σ',x=y =
    λ[ y ∶ B ] N , ⇉λ {y} Aσ⇉B Mσ,x=y⇉N , ∼σ (∼τ λ[x:A']M'σ'∼λ[y:A'σ']M'σ',x=y λ[y:A'σ']M'σ',x=y∼λ[y:B]N)
    where
    y : 𝒱 
    y = X (σ , fv M - x)
    y#⇂σ,ƛxM : y #⇂ (σ , fv M - x)
    y#⇂σ,ƛxM = Xfresh σ (fv M - x)
    y#⇂σ',ƛxM' : y #⇂ (σ' , fv M' - x)
    y#⇂σ',ƛxM' = lemma⇉#⇂ {x} {y} {M} M⇉M' σ⇉σ' y#⇂σ,ƛxM
    λ[x:A']M'σ'∼λ[y:A'σ']M'σ',x=y : (λ[ x ∶ A' ] M') ∙ σ' ∼α λ[ y ∶ A' ∙ σ' ] (M' ∙ σ' ‚ x := v y)
    λ[x:A']M'σ'∼λ[y:A'σ']M'σ',x=y = corollary4-2  {x} {y} {M'} {A'} y#⇂σ',ƛxM'
    λ[y:A'σ']M'σ',x=y∼λ[y:B]N : λ[ y ∶ A' ∙ σ' ] (M' ∙ σ' ‚ x := v y) ∼α λ[ y ∶ B ] N
    λ[y:A'σ']M'σ',x=y∼λ[y:B]N = lemma∼λ (∼σ B∼A'σ') (∼σ N∼M'σ',x=y)      
  compatParSub {Π[ .x ∶ .A ] M} {Π[ .x ∶ .A' ] M'} {σ} {σ'} (⇉Π {x} {A} {A'} A⇉A' M⇉M') σ⇉σ'
    with compatParSub A⇉A' σ⇉σ' | compatParSub M⇉M' (lemma⇉s x (X (σ , fv M - x)) σ⇉σ')
  ... | B , Aσ⇉B , B∼A'σ' | N , Mσ,x=y⇉N , N∼M'σ',x=y =
    Π[ y ∶ B ] N , ⇉Π {y} Aσ⇉B Mσ,x=y⇉N , ∼σ (∼τ Π[x:A']M'σ'∼Π[y:A'σ']M'σ',x=y Π[y:A'σ']M'σ',x=y∼Π[y:B]N)
    where
    y : 𝒱 
    y = X (σ , fv M - x)
    y#⇂σ,ƛxM : y #⇂ (σ , fv M - x)
    y#⇂σ,ƛxM = Xfresh σ (fv M - x)
    y#⇂σ',ƛxM' : y #⇂ (σ' , fv M' - x)
    y#⇂σ',ƛxM' = lemma⇉#⇂ {x} {y} {M} M⇉M' σ⇉σ' y#⇂σ,ƛxM
    Π[x:A']M'σ'∼Π[y:A'σ']M'σ',x=y : (Π[ x ∶ A' ] M') ∙ σ' ∼α Π[ y ∶ A' ∙ σ' ] (M' ∙ σ' ‚ x := v y)
    Π[x:A']M'σ'∼Π[y:A'σ']M'σ',x=y = corollary4-2Π  {x} {y} {M'} {A'} y#⇂σ',ƛxM'
    Π[y:A'σ']M'σ',x=y∼Π[y:B]N : Π[ y ∶ A' ∙ σ' ] (M' ∙ σ' ‚ x := v y) ∼α Π[ y ∶ B ] N
    Π[y:A'σ']M'σ',x=y∼Π[y:B]N = lemma∼Π (∼σ B∼A'σ') (∼σ N∼M'σ',x=y)     
  compatParSub (⇉· M⇉M' N⇉N') σ⇉σ' with compatParSub M⇉M' σ⇉σ' | compatParSub N⇉N' σ⇉σ'
  ... | P' , M⇉P , P∼M'σ' | Q' , N⇉P , P∼N'σ' = (P' · Q') , ⇉· M⇉P N⇉P , ∼· P∼M'σ' P∼N'σ'
  compatParSub {.((λ[ x ∶ A ] M) · N)} {.(M' ∙ ι ‚ x := N')} {σ} {σ'} (⇉β {x} {A} {M} {M'} {N} {N'} M⇉M' N⇉N') σ⇉σ'
    with compatParSub M⇉M' (lemma⇉s x (X (σ , fv M - x)) σ⇉σ') | compatParSub N⇉N' σ⇉σ'
  ... | P , Mσ,x=y⇉P , P∼M'σ,x=y | Q , Nσ⇉Q , Q∼N'σ = P [ y := Q ] , ⇉β {y} {M' = P} {N' = Q} Mσ,x=y⇉P Nσ⇉Q , ∼τ lemma∼2 lemma∼
    where    
    y : 𝒱
    y = X (σ , fv M - x)
    y#⇂σ,ƛxM : y #⇂ (σ , fv M - x)
    y#⇂σ,ƛxM = Xfresh σ (fv M - x)
    open PreR ≈-preorder∼
    lemma∼ : (M' ∙ σ' ‚ x := v y) ∙ (ι ‚ y := (N' ∙ σ')) ∼α (M' ∙ ι ‚ x := N') ∙ σ'
    lemma∼ = 
      begin
      (M' ∙ σ' ‚ x := v y) ∙ (ι ‚ y := (N' ∙ σ'))
      ∼⟨ composRenUnary {x} {y} {σ'} {M'} (lemma⇉#⇂ M⇉M' σ⇉σ' y#⇂σ,ƛxM) ⟩
      (M' ∙ (σ' ‚ x := (N' ∙ σ')))
      ≈⟨ subDistribUpd {M'} {N'} {σ'} {x} ⟩
      (M' ∙ ι ‚ x := N') ∙ σ'
      ∎        
    lemma∼2 : P ∙ (ι ‚ y := Q) ∼α (M' ∙ σ' ‚ x := v y) ∙ (ι ‚ y := (N' ∙ σ'))
    lemma∼2 = lemma-subst P∼M'σ,x=y (lemma≺+∼α⇂ {x = y} lemmaι∼α⇂ Q∼N'σ)

  lemma∼α⇂ρ : ∀ {σ M} → σ ∼α σ ⇂ M
  lemma∼α⇂ρ x _ =  ∼ρ

  lemma⇉ₛρ : ∀ {σ} → σ ⇉ₛ σ
  lemma⇉ₛρ {σ} x = ⇉ρ

  lemma⇉ₛ≺+ : (x : 𝒱) {M N : Λ} {σ σ' : Sub} → M ⇉ N → σ ⇉ₛ σ' → σ ‚ x := M ⇉ₛ σ' ‚ x := N
  lemma⇉ₛ≺+ x {M} {N} {σ} {σ'} red red' y with x ≟ y
  lemma⇉ₛ≺+ x red red' .x | yes refl = red
  ... | no ¬p = red' y

  corollary⇉ₛ≺+ : (x : 𝒱) {M N : Λ} → M ⇉ N → ι ‚ x := M ⇉ₛ ι ‚ x := N
  corollary⇉ₛ≺+ x M⇉N = lemma⇉ₛ≺+ x M⇉N lemma⇉ₛρ

  lemma⇉#- : {x y : 𝒱}{M M' : Λ} → M ⇉ M' → y ∉ fv M - x → y ∉ fv M' - x
  lemma⇉#- {x} {y} {M} {N} M⇉N y∉fvM-x = lemma→β*#- M→β*N y∉fvM-x
    where
    M→β*N : M →β*₀ N
    M→β*N = manyStepBetaContainsPar M⇉N
    
  parComm : CommAlpha _⇉_ 
  parComm ∼c (⇉c {k}) = c k , ⇉c , ∼c
  parComm ∼v (⇉v {x}) = v x , ⇉v , ∼v
  parComm λ[x:A]M∼λ[x':A']M'@(∼λ {x}{x'}{y}{A}{A'}{M}{M'} A∼A' y∉fvM-x y∉fvM'-x' M[x=y]=M'[x'=y]) (⇉λ {_}{_}{_}{_}{M″} A'⇉A″ M'⇉M″)
    with compatParSub M'⇉M″ (lemma⇉ₛ≺+ x' {σ = ι} ⇉v lemma⇉ₛρ)
  ... | N , M'[x'=x]⇉N , N∼M″[x'=x] with parComm A∼A' A'⇉A″ | parComm M∼M'[x'=x] M'[x'=x]⇉N
    where
    M∼M'[x'=x] : M ∼α M' [ x' := v x ]
    M∼M'[x'=x] =
      begin 
      M                             ∼⟨ lemma∙ι ⟩
      M ∙ ι                         ≈⟨ sym (lemma≺+ι {x} {y} {M} y∉fvM-x) ⟩ 
      M [ x := v y ] [ y := v x ]   ≈⟨ cong₂ _∙_ M[x=y]=M'[x'=y] refl ⟩ 
      M' [ x' := v y ] [ y := v x ] ≈⟨ sym (composRenUpd {x'} {y} {M'} y∉fvM'-x') ⟩ 
      M' [ x' := v x ]              ∎
      where open PreR ≈-preorder∼
  ... | B , A⇉B , B∼A″ | P , M⇉P , P∼N = λ[ x ∶ B ] P , ⇉λ A⇉B M⇉P , ∼λ B∼A″ y∉fvP-x y∉fvM″-x' P[x=y]=M″[x'=y]
    where
    x∉fvM'-x' : x ∉ fv M' - x'
    x∉fvM'-x' = ∼α⇒∉- λ[x:A]M∼λ[x':A']M'
    x∉fvM″-x' : x ∉ fv M″ - x'
    x∉fvM″-x' = lemma⇉#- M'⇉M″ x∉fvM'-x'
    P[x=y]=M″[x'=y] : P [ x := v y ] ≡ M″ [ x' := v y ]
    P[x=y]=M″[x'=y] =
      begin
      P [ x := v y ]                ≡⟨ compatSubAlpha (∼τ P∼N N∼M″[x'=x]) ⟩
      M″ [ x' := v x ] [ x := v y ] ≡⟨ sym (composRenUpd {x'} {x} {M″} x∉fvM″-x') ⟩                  
      M″ [ x' := v y ]              ∎
      where open PropEq.≡-Reasoning
    y∉fvP-x : y ∉ fv P - x
    y∉fvP-x = lemma⇉#- M⇉P y∉fvM-x
    y∉fvM″-x' : y ∉ fv M″ - x'
    y∉fvM″-x' = lemma⇉#- M'⇉M″ y∉fvM'-x'
  parComm Π[x:A]M∼Π[x':A']M'@(∼Π {x} {x'} {y} {A} {A'} {M} {M'} A∼A' y∉fvM-x y∉fvM'-x' M[x=y]=M'[x'=y]) (⇉Π {_}{_}{_}{_}{M″} A'⇉A″ M'⇉M″)
    with compatParSub M'⇉M″ (lemma⇉ₛ≺+ x' {σ = ι} ⇉v lemma⇉ₛρ)
  ... | N , M'[x'=x]⇉N , N∼M″[x'=x] with parComm A∼A' A'⇉A″ | parComm M∼M'[x'=x] M'[x'=x]⇉N
    where
    M∼M'[x'=x] : M ∼α M' [ x' := v x ]
    M∼M'[x'=x] =
      begin 
      M                             ∼⟨ lemma∙ι ⟩
      M ∙ ι                         ≈⟨ sym (lemma≺+ι {x} {y} {M} y∉fvM-x) ⟩ 
      M [ x := v y ] [ y := v x ]   ≈⟨ cong₂ _∙_ M[x=y]=M'[x'=y] refl ⟩ 
      M' [ x' := v y ] [ y := v x ] ≈⟨ sym (composRenUpd {x'} {y} {M'} y∉fvM'-x') ⟩ 
      M' [ x' := v x ]              ∎
      where open PreR ≈-preorder∼
  ... | B , A⇉B , B∼A″ | P , M⇉P , P∼N = Π[ x ∶ B ] P , ⇉Π A⇉B M⇉P , ∼Π B∼A″ y∉fvP-x y∉fvM″-x' P[x=y]=M″[x'=y]
    where
    x∉fvM'-x' : x ∉ fv M' - x'
    x∉fvM'-x' = ∼α⇒∉-Π Π[x:A]M∼Π[x':A']M'
    x∉fvM″-x' : x ∉ fv M″ - x'
    x∉fvM″-x' = lemma⇉#- M'⇉M″ x∉fvM'-x'
    P[x=y]=M″[x'=y] : P [ x := v y ] ≡ M″ [ x' := v y ]
    P[x=y]=M″[x'=y] =
      begin
      P [ x := v y ]                ≡⟨ compatSubAlpha (∼τ P∼N N∼M″[x'=x]) ⟩
      M″ [ x' := v x ] [ x := v y ] ≡⟨ sym (composRenUpd {x'} {x} {M″} x∉fvM″-x') ⟩                  
      M″ [ x' := v y ]              ∎
      where open PropEq.≡-Reasoning
    y∉fvP-x : y ∉ fv P - x
    y∉fvP-x = lemma⇉#- M⇉P y∉fvM-x
    y∉fvM″-x' : y ∉ fv M″ - x'
    y∉fvM″-x' = lemma⇉#- M'⇉M″ y∉fvM'-x'
  parComm (∼· M∼M' N∼N') (⇉· M'⇉M″ N'⇉N″) with parComm M∼M' M'⇉M″ | parComm N∼N' N'⇉N″
  ... | P , M⇉P , P∼M″ | Q , N⇉Q , Q∼N″ = P · Q , ⇉· M⇉P N⇉Q , ∼· P∼M″ Q∼N″
  parComm (∼· λ[x:A]M∼λ[x':A']M'@(∼λ{x}{x'}{y}{A}{A'}{M}{M'}A∼A' y∉fvM-x y∉fvM'-x' M[x=y]=M'[x'=y])N∼N')(⇉β{M' = M″}{N'}{N″}M'⇉M″ N'⇉N″)
    with compatParSub M'⇉M″(lemma⇉ₛ≺+ x' {σ = ι} ⇉v lemma⇉ₛρ)
  ... | P , M'[x'=x]⇉P , P∼M″[x'=x] with parComm M∼M'[x'=x] M'[x'=x]⇉P | parComm N∼N' N'⇉N″
    where
    M∼M'[x'=x] : M ∼α M' [ x' := v x ]
    M∼M'[x'=x] =
      begin 
      M                             ∼⟨ lemma∙ι ⟩
      M ∙ ι                         ≈⟨ sym (lemma≺+ι {x} {y} {M} y∉fvM-x) ⟩ 
      M [ x := v y ] [ y := v x ]   ≈⟨ cong₂ _∙_ M[x=y]=M'[x'=y] refl ⟩ 
      M' [ x' := v y ] [ y := v x ] ≈⟨ sym (composRenUpd {x'} {y} {M'} y∉fvM'-x') ⟩ 
      M' [ x' := v x ]              ∎
      where open PreR ≈-preorder∼    
  ... | Q , M⇉Q , Q∼P | R , N⇉R , R∼N″ = Q [ x := R ] , ⇉β M⇉Q N⇉R , Q[x=R]∼M″[x'=N″] 
    where
    x∉fvM'-x' : x ∉ fv M' - x'
    x∉fvM'-x' = ∼α⇒∉- λ[x:A]M∼λ[x':A']M'
    x∉fvM″-x' : x ∉ fv M″ - x'
    x∉fvM″-x' = lemma⇉#- M'⇉M″ x∉fvM'-x'
    Q[x=R]∼M″[x'=N″] : Q [ x := R ] ∼α M″ [ x' := N″ ]
    Q[x=R]∼M″[x'=N″] =
      begin 
      Q [ x := R ]                 ≈⟨ compatSubAlpha Q∼P ⟩
      P [ x := R ]                 ∼⟨ lemma-subst P∼M″[x'=x] (lemma≺+∼α⇂ {x = x} lemmaι∼α⇂ R∼N″) ⟩      
      M″ [ x' := v x ] [ x := N″ ] ≈⟨ sym (composRenUpd {x'} {x} {M″} x∉fvM″-x') ⟩ 
      M″ [ x' := N″ ]              ∎
      where open PreR ≈-preorder∼