open import Data.Empty
open import Data.Product
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
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 InjectivityProducts (𝒞 : 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 ChurchRosser 𝒞 var  
    
  fvUpToAlpha : ∀ {y x x' z B B'} → y ∉ fv B - x → {- z ∉ fv B - x → -} z ∉ fv B' - x' → B [ x := v z ] ≡ B' [ x' := v z ] → y ∉ fv B' - x'
  fvUpToAlpha {y} {x} {x'} {z} {B} {B'} y∉fvB-x {- z∉fvB-x-} z∉fvB'-x' B[x=z]=B'[x'=z] y∈fvB'-x'
    with proj₁ (delList {y} {x'} {fv B'}) y∈fvB'-x'
  ... | y≠x' , y∈fvB' = ⊥-elim (y∉fvB-x ((proj₂ delList) y∈fvB×y≠x))
    where
    y∈y[x'=z] : y ∈ fv ((ι ‚ x' := v z) y)
    y∈y[x'=z] with (Enum._≟_ var) x' y
    ... | yes x'=y = ⊥-elim (y≠x' (sym x'=y))
    ... | no _ = here refl
    y∈fvB'[x'=z] : y ∈ fv (B' [ x' := v z ]) 
    y∈fvB'[x'=z] = lemmafreeσ←ₗ {y} {B'} (y , y∈fvB' , y∈y[x'=z])
    y∈fvB[x=z] : y ∈ fv (B [ x := v z ]) -- iif ex w . w * fv B & y * (w [ x = z ]) 
    y∈fvB[x=z] = subst (λ C → y ∈ fv C) (sym B[x=z]=B'[x'=z]) y∈fvB'[x'=z]
    y∈fvB×y≠x : y ≢ x × y ∈ fv B
    y∈fvB×y≠x with lemmafreeσ→ₗ {y} {B} y∈fvB[x=z]
    ... | w , w∈fvB , y∈w[x=z] with (Enum._≟_ var) x w
    y∈fvB×y≠x | .x , x∈fvB , here y=z | yes refl = ⊥-elim (z∉fvB'-x' (subst (λ u → u ∈ fv B' - x') y=z y∈fvB'-x'))
    y∈fvB×y≠x | y , y∈fvB , here refl | no x≠y = sym≢ x≠y , y∈fvB       
    
  rednInConv : _→β*₀_ ⇒ _≃β_
  rednInConv ε = ε
  rednInConv (M→N ◅ N→*P) = inj₁ (inj₂ M→N) ◅ rednInConv N→*P

  alphaInConv : _∼α_ ⇒ _≃β_
  alphaInConv M∼N = inj₁ (inj₁ M∼N) ◅ ε
  
  injProdGen : ∀ {x₁ x₂ A₁ A₂ B₁ B₂}
        → Π[ x₁ ∶ A₁ ] B₁ ≃β Π[ x₂ ∶ A₂ ] B₂
        → A₁ ≃β A₂
        × ∀ y → B₁ [ x₁ := v y ] ≃β B₂ [ x₂ := v y ]
  injProdGen {x₁} {x₂} {A₁} {A₂} {B₁} {B₂} Π[x₁:A₁]B₁=Π[x₂:A₂]B₂ with CR2 Π[x₁:A₁]B₁=Π[x₂:A₂]B₂
  ... | C₁ , C₂ , Π[x₁:A₁]B₁→*C₁ , Π[x₂:A₂]B₂→*C₂ , C₁∼C₂ with genRedProd Π[x₁:A₁]B₁→*C₁ | genRedProd Π[x₂:A₂]B₂→*C₂
  injProdGen {x₁} {x₂} {A₁} {A₂} {B₁} {B₂} _
    | .(Π[ x₁ ∶ A₁' ] B₁') , .(Π[ x₂ ∶ A₂' ] B₂') , _ , _ , ∼Π {y = y'} A₁'∼A₂' y'∉fvB₁'-x₁ y'∉fvB₂'-x₂ B₁'[x₁=y']=B₂'[x₂=y']
    | A₁' , B₁' , refl , A₁→*A₁' , B₁→*B₁' | A₂' , B₂' , refl , A₂→*A₂' , B₂→*B₂' = A₁≃A₂ , goal₂
    where
    open PreR convPreorder   
    A₁≃A₂ : A₁ ≃β A₂
    A₁≃A₂ = rednInConv A₁→*A₁' ◅◅ alphaInConv A₁'∼A₂' ◅◅ Eq.symmetric (_∼α_ ∪ _→β_)  (rednInConv A₂→*A₂')    
    goal₂ : ∀ y → B₁ [ x₁ := v y ] ≃β B₂ [ x₂ := v y ]
    goal₂ y = B₁[x₁=y]≃B₂[x₂=y]
      where   
      symm : ∀ {M N} → M ≃β N → N ≃β M
      symm = Eq.symmetric (_∼α_ ∪ _→β_)      
      B₁[x₁=y]≃B₂[x₂=y] : B₁ [ x₁ := v y ] ≃β B₂ [ x₂ := v y ]
      B₁[x₁=y]≃B₂[x₂=y] = begin
        B₁ [ x₁ := v y ]                 ∼⟨ compatConvSub (rednInConv B₁→*B₁') ⟩
        B₁' [ x₁ := v y ]                ≡⟨ composRenUpd {x₁} {y'} {B₁'} y'∉fvB₁'-x₁ ⟩
        B₁' [ x₁ := v y' ] [ y' := v y ] ≡⟨ cong₂ _∙_ B₁'[x₁=y']=B₂'[x₂=y'] refl ⟩ 
        B₂' [ x₂ := v y' ] [ y' := v y ] ≡⟨ sym (composRenUpd {x₂} {y'} {B₂'} y'∉fvB₂'-x₂) ⟩
        B₂' [ x₂ := v y ]                ∼⟨ symm (compatConvSub (rednInConv B₂→*B₂')) ⟩      
        B₂ [ x₂ := v y ]                 ∎