LogRel.Substitution.Introductions.Pi

From Coq Require Import ssrbool.
From LogRel.AutoSubst Require Import core unscoped Ast Extra.
From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening
  GenericTyping LogicalRelation Validity.
From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance.
From LogRel.Substitution Require Import Irrelevance Properties.
From LogRel.Substitution.Introductions Require Import Universe Poly.

Set Universe Polymorphism.

(* Lemma eq_subst_1 F G Δ σ : Gup_term_term σ = GtRel 0 .: σ⟨ @wk1 Δ F[σ] .
Proof.
  now bsimpl.
Qed.

Lemma eq_subst_2 G a ρ σ : Gup_term_term σa .: ρ >> tRel = Ga .: σ⟨ρ⟩.
Proof.
  bsimpl ; now substify.
Qed. *)


Section PolyRedPi.
  Context `{GenericTypingProperties}.

  Lemma LRPiPoly0 {Γ l A B} (PAB : PolyRed Γ l A B) : [Γ ||-Π<l> tProd A B].
  Proof.
    econstructor; tea; pose proof (polyRedId PAB) as []; escape.
    + eapply redtywf_refl; gen_typing.
    + unshelve eapply escapeEq; tea; eapply reflLRTyEq.
    + eapply convty_prod; tea; unshelve eapply escapeEq; tea; eapply reflLRTyEq.
  Defined.

  Definition LRPiPoly {Γ l A B} (PAB : PolyRed Γ l A B) : [Γ ||-<l> tProd A B] := LRPi' (LRPiPoly0 PAB).

  Lemma LRPiPolyEq0 {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') :
    [Γ |- A'] -> [Γ ,, A' |- B'] ->
    [Γ ||-Π tProd A B tProd A' B' | LRPiPoly0 PAB].
  Proof.
    econstructor; cbn; tea.
    + eapply redtywf_refl; gen_typing.
    + pose proof (polyRedEqId PAB Peq) as []; now escape.
    + pose proof (polyRedEqId PAB Peq) as []; escape.
      eapply convty_prod; tea.
      eapply escape; now apply (polyRedId PAB).
  Qed.

  Lemma LRPiPolyEq {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') :
    [Γ |- A'] -> [Γ ,, A' |- B'] ->
    [Γ ||-<l> tProd A B tProd A' B' | LRPiPoly PAB].
  Proof.
    now eapply LRPiPolyEq0.
  Qed.

  Lemma LRPiPolyEq' {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') (RAB : [Γ ||-<l> tProd A B]):
    [Γ |- A'] -> [Γ ,, A' |- B'] ->
    [Γ ||-<l> tProd A B tProd A' B' | RAB].
  Proof.
    intros; irrelevanceRefl; now eapply LRPiPolyEq.
  Qed.

End PolyRedPi.

Section PiTyValidity.

  Context `{GenericTypingProperties}.
  Context {l Γ F G} ( : [||-v Γ])
    (vF : [Γ ||-v< l > F | ])
    (vG : [Γ ,, F ||-v< l > G | validSnoc vF]).

  Lemma PiRed {Δ σ} ( : [ |-[ ta ] Δ])
    (vσ : [ | Δ ||-v σ : _ | ])
    : [ Δ ||-< l > (tProd F G)[σ] ].
  Proof.
    eapply LRPi'.
    pose (p := substPolyRed vF vG _ vσ).
    escape; cbn; econstructor; tea;
    destruct (polyRedId p);
    destruct (polyRedEqId p (substPolyRedEq vF vG _ vσ vσ (reflSubst _ _ vσ))); escape.
    - apply redtywf_refl; gen_typing.
    - gen_typing.
    - gen_typing.
  Defined.

  Lemma PiEqRed1 {Δ σ σ'} ( : [ |-[ ta ] Δ])
    (vσ : [ | Δ ||-v σ : _ | ])
    (vσ' : [ | Δ ||-v σ' : _ | ])
    (vσσ' : [ | Δ ||-v σ σ' : _ | | vσ])
    : [ Δ ||-< l > (tProd F G)[σ] (tProd F G)[σ'] | PiRed vσ ].
  Proof.
    pose (p := substPolyRed vF vG _ vσ).
    pose (p' := substPolyRed vF vG _ vσ').
    pose (peq := substPolyRedEq vF vG _ vσ vσ' vσσ').
    destruct (polyRedId p); destruct (polyRedId p'); destruct (polyRedEqId p peq).
    escape; econstructor; cbn; tea.
    - apply redtywf_refl; gen_typing.
    - gen_typing.
  Defined.

  Lemma PiValid : [Γ ||-v< l > tProd F G | ].
  Proof.
    unshelve econstructor.
    - intros Δ σ. eapply PiRed.
    - intros Δ σ σ'. eapply PiEqRed1.
  Defined.

End PiTyValidity.

Section PiTyDomValidity.

  Context `{GenericTypingProperties}.
  Context {l Γ F G} ( : [||-v Γ])
    (vΠFG : [Γ ||-v< l > tProd F G | ]).

  Lemma PiValidDom : [Γ ||-v< l > F | ].
  Proof.
  unshelve econstructor.
  - intros Δ σ vσ; instValid vσ.
    cbn in RvΠFG; apply Induction.invLRΠ in RvΠFG.
    destruct RvΠFG as [dom ? red ? ? ? [? ? Hdom]].
    assert (Hrw : F[σ] = dom); [|subst dom].
    { eapply redtywf_whnf in red as [=]; [tea|constructor]. }
    rewrite <- (wk_id_ren_on Δ F[σ]).
    now eapply Hdom.
  - cbn; refold.
    intros Δ σ σ' vσ vσ' vσσ'.
    match goal with |- [ LRAd.pack ?P | _ ||- _ _] => set (vF := P); clearbody vF end.
    instValid vσ.
    cbn in RvΠFG; apply Induction.invLRΠ in RvΠFG.
    assert ( := validTyExt vΠFG _ vσ vσ' vσσ').
    eapply LRTyEqIrrelevant' with (lrA' := LRPi' RvΠFG) in ; [|reflexivity].
    destruct RvΠFG as [dom ? red ? ? ? []].
    destruct as [dom' ? red' ? ? [Heq _]]; simpl in *.
    specialize (Heq Δ wk_id ).
    assert (Hrw : F[σ] = dom).
    { eapply redtywf_whnf in red as [=]; [tea|constructor]. }
    assert (Hrw' : F[σ'] = dom').
    { eapply redtywf_whnf in red' as [=]; [tea|constructor]. }
    rewrite wk_id_ren_on, <- Hrw' in Heq.
    eapply Transitivity.transEq; [|eapply Heq].
    rewrite <- (wk_id_ren_on Δ dom) in Hrw; rewrite <- Hrw.
    eapply LRTyEqIrrelevant' with (lrA := vF); [reflexivity|].
    eapply reflLRTyEq.
  Qed.

  Lemma PiValidCod : [Γ,, F ||-v< l > G | validSnoc PiValidDom].
  Proof.
  unshelve econstructor.
  - intros Δ σ [vσ v0].
    instValid vσ; cbn in *.
    apply Induction.invLRΠ in RvΠFG.
    destruct RvΠFG as [dom cod red ? ? ? [? ? Hdom Hcod _]].
    specialize (Hcod Δ (σ 0) wk_id ).
    assert (HF : F[ >> σ] = dom).
    { eapply redtywf_whnf in red as [=]; [tea|constructor]. }
    assert (HG0 : G[up_term_term ( >> σ)] = cod).
    { eapply redtywf_whnf in red as [=]; [tea|constructor]. }
    assert (HG : G[σ] = cod[σ 0 .: @wk_id Δ >> tRel]).
    { rewrite <- HG0; bsimpl; apply ext_term; intros []; reflexivity. }
    rewrite HG; apply Hcod.
    irrelevance0; [|eapply v0].
    now rewrite wk_id_ren_on.
  - cbn; refold.
    intros Δ σ σ' [vσ v0] [vσ' v0'] [vσσ' v00'].
    match goal with |- [ LRAd.pack ?P | _ ||- _ _] => set (vG := P); clearbody vG end.
    instValid vσ.
    cbn in RvΠFG; apply Induction.invLRΠ in RvΠFG.
    assert ( := validTyExt vΠFG _ vσ vσ' vσσ').
    eapply LRTyEqIrrelevant' with (lrA' := LRPi' RvΠFG) in ; [|reflexivity].
    destruct RvΠFG as [dom cod red ? ? ? [? ? ? ? Hcod]].
    destruct as [dom' cod' red' ? ? [Hdom' Hcod']]; simpl in *.
    specialize (Hcod' Δ (σ' 0) wk_id ).
    assert (HF : F[ >> σ] = dom).
    { eapply redtywf_whnf in red as [=]; [tea|constructor]. }
    assert (HF' : F[ >> σ'] = dom').
    { eapply redtywf_whnf in red' as [=]; [tea|constructor]. }
    assert (HG0 : G[up_term_term ( >> σ)] = cod).
    { eapply redtywf_whnf in red as [=]; [tea|constructor]. }
    assert (HG : G[σ] = cod[σ 0 .: @wk_id Δ >> tRel]).
    { rewrite <- HG0; bsimpl; apply ext_term; intros []; reflexivity. }
    assert (HG0' : G[up_term_term ( >> σ')] = cod').
    { eapply redtywf_whnf in red' as [=]; [tea|constructor]. }
    assert (HG' : G[σ'] = cod'[σ' 0 .: @wk_id Δ >> tRel]).
    { rewrite <- HG0'; bsimpl; apply ext_term; intros []; reflexivity. }
    rewrite HG'.
    assert (Hσ0 : [shpRed Δ wk_id | _ ||- σ 0 : _]).
    { irrelevance0; [|eapply v0].
      now rewrite wk_id_ren_on. }
    assert (Hσ0' : [shpRed Δ wk_id | _ ||- σ' 0 : _]).
    { eapply LRTmRedConv; [|eapply v0'].
      eapply LRTyEqSym; rewrite HF'.
      rewrite <- (wk_id_ren_on Δ dom').
      apply (Hdom' _ _ ). }
    eassert (Hcod0 := Hcod Δ (σ 0) (σ' 0) wk_id Hσ0 Hσ0').
    eapply Transitivity.transEq; [|now unshelve eapply Hcod'].
    eapply Transitivity.transEq; [|unshelve eapply Hcod0].
    + unshelve (irrelevance0; [|eapply reflLRTyEq]); try now symmetry.
      shelve.
      now eauto.
    + irrelevance0; [|eapply v00'].
      now rewrite wk_id_ren_on.
  Qed.

End PiTyDomValidity.

Section PiTyCongruence.

  Context `{GenericTypingProperties}.
  Context {Γ F G F' G' l}
    ( : [||-v Γ])
    (vF : [ Γ ||-v< l > F | ])
    (vG : [ Γ ,, F ||-v< l > G | validSnoc vF ])
    (vF' : [ Γ ||-v< l > F' | ])
    (vG' : [ Γ ,, F' ||-v< l > G' | validSnoc vF' ])
    (vFF' : [ Γ ||-v< l > F F' | | vF ])
    (vGG' : [ Γ ,, F ||-v< l > G G' | validSnoc vF | vG ]).

  Lemma PiEqRed2 {Δ σ} ( : [ |-[ ta ] Δ]) (vσ : [ | Δ ||-v σ : _ | ])
    : [ Δ ||-< l > (tProd F G)[σ] (tProd F' G')[σ] | validTy (PiValid vF vG) vσ ].
  Proof.
    pose (p := substPolyRed vF vG _ vσ).
    pose (p' := substPolyRed vF' vG' _ vσ).
    pose (peq := substEqPolyRedEq vF vG _ vσ vF' vG' vFF' vGG').
    destruct (polyRedId p); destruct (polyRedId p'); destruct (polyRedEqId p peq).
    escape; econstructor; cbn; tea.
    - apply redtywf_refl; gen_typing.
    - gen_typing.
  Qed.

  Lemma PiCong : [ Γ ||-v< l > tProd F G tProd F' G' | | PiValid vF vG ].
  Proof.
    econstructor. intros Δ σ. eapply PiEqRed2.
  Qed.

End PiTyCongruence.

Section PiTmValidity.

  Context `{GenericTypingProperties}.
  Context {Γ F G} ( : [||-v Γ])
    (VF : [ Γ ||-v< one > F | ])
    (VU : [ Γ ,, F ||-v< one > U | validSnoc VF ])
    (VFU : [ Γ ||-v< one > F : U | | UValid ])
    (VGU : [ Γ ,, F ||-v< one > G : U | validSnoc VF | VU ]) .
    (* (VF := univValid (l':=zero) _ _ vFU)
    (VG := univValid (l':=zero) _ _ vGU). *)


  Lemma prodTyEqU {Δ σ σ'} ( : [ |-[ ta ] Δ])
    (Vσ : [ | Δ ||-v σ : _ | ])
    (Vσ' : [ | Δ ||-v σ' : _ | ])
    (Vσσ' : [ | Δ ||-v σ σ' : _ | | Vσ ])
    : [Δ |-[ ta ] tProd F[σ] G[up_term_term σ] tProd F[σ'] G[up_term_term σ'] : U].
  Proof.
    pose proof (Vuσ := liftSubstS' VF Vσ).
    pose proof (Vureaσ' := liftSubstSrealign' VF Vσσ' Vσ').
    pose proof (Vuσσ' := liftSubstSEq' VF Vσσ').
    instAllValid Vσ Vσ' Vσσ'; instAllValid Vuσ Vureaσ' Vuσσ'; escape.
    eapply convtm_prod; tea.
  Qed.

  Lemma PiRedU {Δ σ} ( : [ |-[ ta ] Δ]) (Vσ : [ | Δ ||-v σ : _ | ])
    : [ Δ ||-< one > (tProd F G)[σ] : U | validTy (UValid ) Vσ ].
  Proof.
    pose proof (Vσσ := reflSubst _ _ Vσ).
    pose proof (Vuσ := liftSubstS' VF Vσ).
    pose proof (Vuσσ := liftSubstSEq' VF Vσσ).
    instAllValid Vσ Vσ Vσσ; instAllValid Vuσ Vuσ Vuσσ; escape.
    econstructor; cbn.
    - apply redtmwf_refl; cbn in *; now eapply ty_prod.
    - constructor.
    - now eapply convtm_prod.
    - cbn. unshelve refine (LRCumulative (PiRed _ _ _ Vσ));
      unshelve eapply univValid; tea; try irrValid.
  Defined.

  Lemma PiValidU : [ Γ ||-v< one > tProd F G : U | | UValid ].
  Proof.
    econstructor.
    - intros Δ σ Vσ.
      exact (PiRedU Vσ).
    - intros Δ σ σ' Vσ Vσ' Vσσ'.
      pose proof (univValid (l' := zero) _ _ VFU) as VF0.
      pose proof (irrelevanceTy (validSnoc VF)
                    (validSnoc (l := zero) VF0)
                    (univValid (l' := zero) _ _ VGU)) as VG0.
      unshelve econstructor ; cbn.
      + exact (PiRedU Vσ).
      + exact (PiRedU Vσ').
      + exact (LRCumulative (PiRed VF0 VG0 Vσ)).
      + exact (prodTyEqU Vσ Vσ' Vσσ').
      + exact (LRCumulative (PiRed VF0 VG0 Vσ')).
      + pose proof (PiEqRed1 VF0 VG0 Vσ Vσ' Vσσ').
        irrelevanceCum.
  Qed.

End PiTmValidity.

Section PiTmCongruence.

  Context `{GenericTypingProperties}.
  Context {Γ F G F' G'}
    ( : [||-v Γ])
    (vF : [ Γ ||-v< one > F | ])
    (vU : [ Γ ,, F ||-v< one > U | validSnoc vF ])
    (vFU : [ Γ ||-v< one > F : U | | UValid ])
    (vGU : [ Γ ,, F ||-v< one > G : U | validSnoc vF | vU ])
    (vF' : [ Γ ||-v< one > F' | ])
    (vU' : [ Γ ,, F' ||-v< one > U | validSnoc vF' ])
    (vF'U : [ Γ ||-v< one > F' : U | | UValid ])
    (vG'U : [ Γ ,, F' ||-v< one > G' : U | validSnoc vF' | vU' ])
    (vFF' : [ Γ ||-v< one > F F' : U | | UValid ])
    (vGG' : [ Γ ,, F ||-v< one > G G' : U | validSnoc vF | vU ]).

  Lemma PiCongTm : [ Γ ||-v< one > tProd F G tProd F' G' : U | | UValid ].
  Proof.
    econstructor.
    intros Δ σ Vσ.
    pose proof (univValid (l' := zero) _ _ vFU) as vF0.
    pose proof (univValid (l' := zero) _ _ vF'U) as vF'0.
    pose proof (Vσσ := reflSubst _ _ Vσ).
    pose proof (Vuσ := liftSubstS' vF Vσ).
    pose proof (Vuσσ := liftSubstSEq' vF Vσσ).
    instAllValid Vσ Vσ Vσσ; instAllValid Vuσ Vuσ Vuσσ; escape.
    pose proof (irrelevanceTy (validSnoc vF)
                  (validSnoc (l := zero) vF0)
                  (univValid (l' := zero) _ _ vGU)) as vG0.
    pose proof (irrelevanceTy (validSnoc vF')
                  (validSnoc (l := zero) vF'0)
                  (univValid (l' := zero) _ _ vG'U)) as vG'0.
    unshelve econstructor ; cbn.
    - exact (PiRedU vF vU vFU vGU Vσ).
    - exact (PiRedU vF' vU' vF'U vG'U Vσ).
    - exact (LRCumulative (PiRed vF0 vG0 Vσ)).
    - now eapply convtm_prod.
    - exact (LRCumulative (PiRed vF'0 vG'0 Vσ)).
    - enough ([ Δ ||-< zero > (tProd F G)[σ] (tProd F' G')[σ] | PiRed vF0 vG0 Vσ]) by irrelevanceCum.
      refine (PiEqRed2 vF0 vG0 vF'0 vG'0 _ _ Vσ).
      + exact (univEqValid (UValid ) vF0 vFF').
      + pose proof (univEqValid (validSnoc vF) vU (univValid (l' := zero) _ _ vGU) vGG') as vGG'0.
        refine (irrelevanceTyEq _ _ _ _ vGG'0).
  Qed.

End PiTmCongruence.