open import Relation.Nullary
open import Data.List
open import Data.Product
open import Data.Empty
open import Data.Sum
open import Data.Unit hiding (_≟_)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.PropositionalEquality as PEq hiding ([_])
open import Data.List.Relation.Unary.Any
open import Data.List.Membership.Propositional
open import Relation.Binary.Construct.Closure.Equivalence as Eq
open import Relation.Binary.Construct.Union
open import Data.List.Relation.Binary.Pointwise as Pw hiding (refl)

open import Stoughton.Var

module ConsistencyImpred {𝒞 𝒱 : Set} (enum : Enum 𝒱) (𝒜 : 𝒞 → 𝒞 → Set) (ℛ : 𝒞 → 𝒞 → 𝒞 → Set) where

  open Enum enum

  open import Stoughton.Chi encode decode inverse
  open import Stoughton.Syntax 𝒞 𝒱 _≟_
  open import Stoughton.Substitution 𝒞 enum
  open import Stoughton.SubstitutionLemmas 𝒞 enum  
  open import Stoughton.Alpha 𝒞 enum
  open import Stoughton.Renaming 𝒞 enum
  
  open import PTSs enum 𝒜 ℛ
  open import PTSs.Metatheory enum 𝒜 ℛ
  open import Beta 𝒞 enum  
  open import BetaReduction 𝒞 enum
  open import BetaConversion 𝒞 enum
  open import Context 𝒱 Λ _≟_
  open import Utils

  open import ChurchRosser 𝒞 enum
  open import InjectivityProducts 𝒞 enum 
  open import SubjectReduction enum 𝒜 ℛ
  
  open import NormalForm enum 𝒜 ℛ
  open import Normalizing enum 𝒜 ℛ
  
  -- Consistency lemmas:
  
  consistencyNf₀ : ∀ {z s M} → Nf M → ¬([(z , c s)] ⊢ₛ M ∶ v z)
  consistencyNf₀ sort z:s⊢M:z with genSort z:s⊢M:z
  ... | s' , _ , _ , z≃s' = absurd₂ z≃s'
  consistencyNf₀ (abs _ _) z:s⊢λ[x:A]M':z with genAbs z:s⊢λ[x:A]M':z
  ... | _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , z≃Π[y:A]B = absurd₃ z≃Π[y:A]B
  consistencyNf₀ (prod _ _) z:s⊢Π[x:A]B:z with genProd z:s⊢Π[x:A]B:z
  ... | _ , _ , _ , _ , _ , _ , _ , _ , z≃s' = absurd₂ z≃s'
  consistencyNf₀ (neu {x} var) z:s⊢x:z with genVar z:s⊢x:z
  consistencyNf₀ {z} {s} (neu {.z} var) z:s⊢z:z | .(c s) , _ , here refl , z≃s = absurd₂ z≃s
  consistencyNf₀ (neu {x} (app NeM _)) z:s⊢MN:z with headFunctional NeM z:s⊢MN:z
  consistencyNf₀ {z} {s} (neu {.z} (app NeM _)) z:s⊢MN:z | _ , .(c s) , _ , _ , here refl , s≃Π[y:A]B =
    absurd₁ (Eq.symmetric (_∼α_ ∪ _→β_) s≃Π[y:A]B)  
  
  consistencyNe : ∀ {M y A} → Ne y M → ¬([] ⊢ₛ M ∶ A)
  consistencyNe var ⊢x:A with genVar ⊢x:A
  ... | _ , _ , () , _
  consistencyNe (app NeM _) ⊢MN:A with genApp ⊢MN:A
  ... | _ , _ , _ , ⊢M:B , _ = consistencyNe NeM ⊢M:B
  
  consistencyNf : ∀ {M x s} → Nf M → ¬([] ⊢ₛ M ∶ Π[ x ∶ c s ](v x))
  consistencyNf sort ⊢t:Π[x:s]x with genSort ⊢t:Π[x:s]x
  ... | u , _ , _ , Π[x:s]x≃u = absurd₁ Π[x:s]x≃u
  consistencyNf {_} {x} {s} (abs {y} {A} {N} NfA NfN) ⊢λ[y:A]N:Π[x:s]x with genAbs ⊢λ[y:A]N:Π[x:s]x
  ... | _ , _ , _ , y' , z , B , _ , _ , _ , _ , z:A⊢N[y=z]:B[y'=z] , _ , Π[x:s]x≃Π[y':A]B with injProdGen Π[x:s]x≃Π[y':A]B
  ... | s≃A , ∀z'→x[x=z']≃B[y'=z'] = consistencyNf₀ NfN[y=z] z:s⊢N[y=z]:z
    where
    ∀z'→z'≃B[y'=z'] : ∀ z' → v z' ≃β B [ y' := v z' ]
    ∀z'→z'≃B[y'=z'] z' with x ≟ x
    ... | yes _ = ∀z'→x[x=z']≃B[y'=z'] z'
    ... | no x≢x = ⊥-elim (x≢x PEq.refl)    
    B[y'=z]≃z : B [ y' := v z ] ≃β v z
    B[y'=z]≃z = Eq.symmetric (_∼α_ ∪ _→β_) (∀z'→z'≃B[y'=z'] z)    
    nfA : nf A
    nfA = soundNf NfA
    A≡s : A ≡ c s
    A≡s = NfConvSort nfA (Eq.symmetric (_∼α_ ∪ _→β_) s≃A)
    z:s⊢N[y=z]:B[y'=z] : [(z , c s)] ⊢ₛ N [ y := v z ] ∶ B [ y' := v z ]
    z:s⊢N[y=z]:B[y'=z] = subst (λ X → [(z , X)] ⊢ₛ N [ y := v z ] ∶ B [ y' := v z ]) A≡s z:A⊢N[y=z]:B[y'=z]     
    NfN[y=z] : Nf (N [ y := v z ])
    NfN[y=z] = renameNf (updRen identRen) NfN    
    z:sok : [(z , c s)] okₛ
    z:sok = validCxt z:s⊢N[y=z]:B[y'=z]
    z:s⊢z:s : [(z , c s)] ⊢ₛ v z ∶ c s
    z:s⊢z:s = ⊢var z:sok (here PEq.refl)
    z:s⊢N[y=z]:z : [(z , c s)] ⊢ₛ N [ y := v z ] ∶ v z
    z:s⊢N[y=z]:z = ⊢conv z:s⊢N[y=z]:B[y'=z] B[y'=z]≃z z:s⊢z:s
  consistencyNf (prod NfA NfB) ⊢Π[y:A]B:Π[x:s]x with genProd ⊢Π[y:A]B:Π[x:s]x
  ... | _ , _ , s₃ , _ , _ , _ , _ , _ , Π[x:s]x≃s₃ = absurd₁ Π[x:s]x≃s₃
  consistencyNf (neu NeM) = consistencyNe NeM

  -- consistency theorem

  module _ (norm : Normalizing) where
  
    consistencyImpred : ∀ {x s} → ¬(∃ λ M → [] ⊢ₛ M ∶ Π[ x ∶ c s ](v x))
    consistencyImpred {x} {s} (M , ⊢M:Π[x:s]x) with norm ⊢M:Π[x:s]x
    ... | (N , nfM , M→*N) , _ = consistencyNf NfN ⊢N:Π[x:s]x
      where
      ⊢N:Π[x:s]x : [] ⊢ₛ N ∶ Π[ x ∶ c s ](v x)
      ⊢N:Π[x:s]x = manyStepSR ⊢M:Π[x:s]x M→*N
      NfN : Nf N
      NfN = completeNf ⊢N:Π[x:s]x nfM

  -- validity falsehood

  module _ where
  
    sufficient : ∀ {x s₁ s₂ s₃} → 𝒜 s₂ s₁ → ℛ s₁ s₂ s₃ → [] ⊢ₛ Π[ x ∶ c s₂ ](v x) ∶ c s₃
    sufficient {x} {s₁} {s₂} {s₃} 𝒜s₂s₁ ℛs₁s₂s₃ =
      ⊢prod {y = x} ℛs₁s₂s₃ (⊢sort ⊢nil 𝒜s₂s₁) (∉- [ x ]) x:s₂⊢x:s₂
      where
      x:s₂⊢x:s₂ : [(x , c s₂)] ⊢ₛ v x [ x := v x ] ∶ c s₂
      x:s₂⊢x:s₂ with x ≟ x
      ... | yes _ = ⊢var (⊢cons ⊢nil (λ()) (⊢sort ⊢nil 𝒜s₂s₁)) (here refl)
      ... | no x≢x = ⊥-elim (x≢x refl)

    nfs : ∀ {s} → nf (c s)
    nfs (→cxt ()) 

    necessary : ∀ {x s s′} → [] ⊢ₛ Π[ x ∶ c s ](v x) ∶ c s′ → ∃ λ s₁ → 𝒜 s s₁ × ℛ s₁ s s′ -- 𝒜 * □ × ℛ □ * s
    necessary {x} {s} {s′} 𝒟 with genProd 𝒟 
    ... | s₁ , s₂ , s₃ , y , ℛs₁s₂s₃ , ⊢s:s₁ , _ , y:s⊢x[x=y]:s₂ , s′≃s₃ with x ≟ x
    ... | no x≢x = ⊥-elim (x≢x refl)
    ... | yes _ with NfConvSort nfs s′≃s₃
    necessary {x} {s} {s′} 𝒟 | s₁ , s₂ , s′ , y , ℛs₁s₂s′ , ⊢s:s₁ , _ , y:s⊢y:s₂ , _ | yes _ | refl
      with genSort ⊢s:s₁ | genVar y:s⊢y:s₂
    ... | s₁′ , _ , 𝒜ss₁′ , s₁≃s₁′ | .(c s) , _ , here refl , s₂≃s with NfConvSort nfs s₁≃s₁′ | NfConvSort nfs s₂≃s
    necessary {x} {s} {s′} 𝒟
      | s₁ , .s , s′ , y , ℛs₁ss′ , _ | yes _ | refl | .s₁ , _ , 𝒜ss₁ , _ | _ | refl | refl = s₁ , 𝒜ss₁ , ℛs₁ss′

    validityFalsehood : ∀ {x s t} → [] ⊢ₛ Π[ x ∶ c s ](v x) ∶ c t ↔ ∃ λ u → 𝒜 s u × ℛ u s t
    validityFalsehood = necessary , λ (u , 𝒜su , ℛust) → sufficient 𝒜su ℛust