Through to Poly.v

Author: Martin Baillon

theories/LogicalRelation.v

@@ -1437,11 +1437,20 @@ Notation "W[ Γ ||-< l > A ≅ B | RA ]< wl >" := (WLogRelEq l wl Γ A B RA).
 Notation "W[ Γ ||-< l > t : A | RA ]< wl >" := (WLogRelTm l wl Γ t A RA).
 Notation "W[ Γ ||-< l > t ≅ u : A | RA ]< wl >" := (WLogRelTmEq l wl Γ t u A RA).
 
-Lemma instKripke `{GenericTypingProperties} {k Γ A l} (wfΓ : [|-Γ]< k >) (h : forall Δ (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]< k >), [Δ ||-<l> A⟨ρ⟩]< k >) : [Γ ||-<l> A]< k >.
+Lemma instKripke `{GenericTypingProperties} {k Γ A l} (wfΓ : [|-Γ]< k >)
+  (h : forall Δ (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]< k >), [Δ ||-<l> A⟨ρ⟩]< k >) :
+  [Γ ||-<l> A]< k >.
 Proof.
   specialize (h Γ wk_id wfΓ); now rewrite wk_id_ren_on in h.
 Qed.
 
+Lemma instKripke' `{GenericTypingProperties} {wl Γ A l} (wfΓ : [|-Γ]< wl >)
+  (h : forall Δ wl' (ρ : Δ ≤ Γ) (f : wl' ≤ε wl) (wfΔ : [|-Δ]< wl' >), [Δ ||-<l> A⟨ρ⟩]< wl' >) :
+  [Γ ||-<l> A]< wl >.
+Proof.
+  specialize (h Γ wl wk_id (wfLCon_le_id _) wfΓ); now rewrite wk_id_ren_on in h.
+Qed.
+
 (** ** Rebundling reducibility of Polynomial *)
 
 (** The definition of reducibility of product types in the logical relation, which separates
@@ -1541,11 +1550,13 @@ Section PolyRed.
     : toAd (from PAad) = PAad.
   Proof. destruct PA, PAad; reflexivity. Qed.
 
+
 End PolyRed.
 
 Arguments PolyRed : clear implicits.
 Arguments PolyRed {_ _ _ _ _ _ _ _ _} _ _ _.
 
+
 End PolyRed.
 
 Export PolyRed(PolyRed,Build_PolyRed).
@@ -1637,6 +1648,25 @@ Section EvenMoreDefs.
     : [ LogRel@{i j k l} l | Γ ||- A ]< k > :=
     LRbuild (LRSig (LogRelRec l) _ (ParamRedTy.toAd ΠA)).
 
+  
+  Record WPolyRed@{i j k l} (k : wfLCon) (Γ : context) (l : TypeLevel) (shp pos : term) :=
+    { WPol : DTree k  ;
+      WRedPol {k'} (Ho : over_tree k k' WPol) :
+      PolyRed@{i j k l} k' Γ l shp pos ;
+    }.
+  Arguments WPol [_ _ _ _ _ ] _.
+  Arguments WRedPol [_ _ _ _ _] _ [_] _.
+
+  Record WPolyRedEq@{i j k l} {k : wfLCon} {Γ : context} {l : TypeLevel} {shp pos : term} (Hyp : WPolyRed@{i j k l} k Γ l shp pos)
+    (shp' pos' : term) :=
+    { WPolEq : DTree k  ;
+      WRedPolEq {k'} (Ho : over_tree k k' (WPol Hyp))
+        (Ho' : over_tree k k' WPolEq) :
+      PolyRedEq@{k} (PolyRed.toPack (WRedPol Hyp Ho)) shp' pos' ;
+    }.
+  Arguments WPolEq [_ _ _ _ _] _.
+  Arguments WRedPolEq [_ _ _ _ _ _] _.
+  
 End EvenMoreDefs.
 
 

theories/LogicalRelation/Irrelevance.v

@@ -917,6 +917,16 @@ Corollary LRCumulative' @{i j k l i' j' k' l'} {lA}
 Proof.
   intros ->; apply LRCumulative.
 Qed.
+
+Theorem WLRCumulative@{i j k l i' j' k' l'} {lA}
+  {wl : wfLCon} {Γ : context} {A : term}
+  : WLogRel@{i j k l} lA wl Γ A ->
+    WLogRel@{i' j' k' l'} lA wl Γ A.
+Proof.
+  intros [d Hd] ; exists d.
+  intros wl' f ; now eapply LRCumulative, Hd.
+Qed.
+
 End LRIrrelevant.
 
 

theories/LogicalRelation/Monotonicity.v

@@ -856,3 +856,89 @@ Proof.
 Defined.
 
 End Injection.
+
+Section Weakening_Ltrans.
+  Context `{GenericTypingProperties}.
+
+  Lemma wk_Ltrans@{h i j k l} {wl Γ Δ wl' A l}
+    (ρ : Δ ≤ Γ) 
+    (f : wl' ≤ε wl)
+    (wfΔ : [|- Δ]< wl' >) :
+    [LogRel@{i j k l} l | Γ ||- A]< wl > ->
+    [LogRel@{i j k l} l | Δ ||- A⟨ρ⟩]< wl' >.
+  Proof.
+    intros ; now eapply (wk@{i j k l}), (Ltrans@{h i j k l}).
+  Defined.
+
+  Lemma Wwk_Ltrans@{h i j k l} {wl Γ Δ wl' A l}
+    (ρ : Δ ≤ Γ) 
+    (f : wl' ≤ε wl)
+    (wfΔ : [|- Δ]< wl' >) :
+    WLogRel@{i j k l} l wl Γ A ->
+    WLogRel@{i j k l} l wl' Δ A⟨ρ⟩.
+  Proof.
+    intros ; now eapply (Wwk@{i j k l}), (WLtrans@{h i j k l}).
+  Defined.
+
+  Lemma wkEq_Ltrans@{h i j k l} {wl Γ Δ wl' A B l} (ρ : Δ ≤ Γ) (f : wl' ≤ε wl)
+    (wfΔ : [|- Δ]< wl' >)
+    (lrA : [Γ ||-<l> A]< wl >) : 
+    [LogRel@{i j k l} l | Γ ||- A ≅ B | lrA]< wl > ->
+    [LogRel@{i j k l} l | Δ ||- A⟨ρ⟩ ≅ B⟨ρ⟩ | wk_Ltrans@{h i j k l} ρ f wfΔ lrA]< wl' >.
+  Proof.
+    intros ; now eapply (wkEq@{i j k l}), (Eq_Ltrans@{h i j k l}).
+  Defined.
+
+  Lemma WwkEq_Ltrans@{h i j k l} {wl Γ Δ wl' A B l}
+    (ρ : Δ ≤ Γ) 
+    (f : wl' ≤ε wl)
+    (wfΔ : [|- Δ]< wl' >)
+    (lrA : W[Γ ||-<l> A]< wl >) :
+    WLogRelEq@{i j k l} l wl Γ A B lrA ->
+    WLogRelEq@{i j k l} l wl' Δ A⟨ρ⟩ B⟨ρ⟩ (Wwk_Ltrans@{h i j k l} ρ f wfΔ lrA).
+  Proof.
+    intros ; now eapply (WwkEq@{i j k l}), (WEq_Ltrans@{h i j k l}).
+  Defined.
+
+  Lemma wkTm_Ltrans@{h i j k l} {wl Γ Δ wl' t A l} (ρ : Δ ≤ Γ) (f : wl' ≤ε wl)
+    (wfΔ : [|- Δ]< wl' >)
+    (lrA : [Γ ||-<l> A]< wl >) : 
+    [LogRel@{i j k l} l | Γ ||- t : A | lrA]< wl > ->
+    [LogRel@{i j k l} l | Δ ||- t⟨ρ⟩ : A⟨ρ⟩ | wk_Ltrans@{h i j k l} ρ f wfΔ lrA]< wl' >.
+  Proof.
+    intros ; now eapply (wkTerm@{i j k l}), (Tm_Ltrans@{h i j k l}).
+  Defined.
+    
+  Lemma WwkTm_Ltrans@{h i j k l} {wl Γ Δ wl' t A l}
+    (ρ : Δ ≤ Γ) 
+    (f : wl' ≤ε wl)
+    (wfΔ : [|- Δ]< wl' >)
+    (lrA : W[Γ ||-<l> A]< wl >) :
+    WLogRelTm@{i j k l} l wl Γ t A lrA ->
+    WLogRelTm@{i j k l} l wl' Δ t⟨ρ⟩ A⟨ρ⟩ (Wwk_Ltrans@{h i j k l} ρ f wfΔ lrA).
+  Proof.
+    intros ; now eapply (WwkTerm@{i j k l}), (WTm_Ltrans@{h i j k l}).
+  Defined.
+
+  Lemma wkTmEq_Ltrans@{h i j k l} {wl Γ Δ wl' t u A l} (ρ : Δ ≤ Γ) (f : wl' ≤ε wl)
+    (wfΔ : [|- Δ]< wl' >)
+    (lrA : [Γ ||-<l> A]< wl >) : 
+    [LogRel@{i j k l} l | Γ ||- t ≅ u : A | lrA]< wl > ->
+    [LogRel@{i j k l} l | Δ ||- t⟨ρ⟩ ≅ u⟨ρ⟩ : A⟨ρ⟩ | wk_Ltrans@{h i j k l} ρ f wfΔ lrA]< wl' >.
+  Proof.
+    intros ; now eapply (wkTermEq@{i j k l}), (TmEq_Ltrans@{h i j k l}).
+  Defined.
+    
+  Lemma WwkEqTm_Ltrans@{h i j k l} {wl Γ Δ wl' t u A l}
+    (ρ : Δ ≤ Γ) 
+    (f : wl' ≤ε wl)
+    (wfΔ : [|- Δ]< wl' >)
+    (lrA : W[Γ ||-<l> A]< wl >) :
+    WLogRelTmEq@{i j k l} l wl Γ t u A lrA ->
+    WLogRelTmEq@{i j k l} l wl' Δ t⟨ρ⟩ u⟨ρ⟩ A⟨ρ⟩ (Wwk_Ltrans@{h i j k l} ρ f wfΔ lrA).
+  Proof.
+    intros ; now eapply (WwkTermEq@{i j k l}), (WTmEq_Ltrans@{h i j k l}).
+  Defined.
+
+  
+End Weakening_Ltrans.

theories/LogicalRelation/Reduction.v

@@ -203,6 +203,13 @@ Proof.
   intros ? []; now eapply redSubstTerm.
 Qed.
 
+Lemma WredwfSubstTerm {wl Γ A t u l} (RA : W[Γ ||-<l> A]< wl >) :
+  W[Γ ||-<l> u : A | RA]< wl > ->
+  [Γ |- t :⤳*: u : A ]< wl > ->
+  W[Γ ||-<l> t : A | RA]< wl > × W[Γ ||-<l> t ≅ u : A | RA]< wl >.
+Proof.
+  intros ? []; now eapply WredSubstTerm.
+Qed.
 
 Lemma redFwd {wl Γ l A B} :
   [Γ ||-<l> A]< wl > ->

theories/LogicalRelation/Reflexivity.v

@@ -9,16 +9,24 @@ Set Universe Polymorphism.
 Section Reflexivities.
   Context `{GenericTypingProperties}.
 
-  Definition reflLRTyEq {l wl Γ A} (lr : [ Γ ||-< l > A ]< wl > ) : [ Γ ||-< l > A ≅ A | lr ]< wl >.
+  Definition reflLRTyEq {l wl Γ A} (lr : [ Γ ||-< l > A ]< wl > ) :
+    [ Γ ||-< l > A ≅ A | lr ]< wl >.
   Proof.
     pattern l, wl, Γ, A, lr; eapply LR_rect_TyUr; intros ???? [] **.
     all: try match goal with H : PolyRed _ _ _ _ _ |- _ => destruct H; econstructor; tea end.
     all: try now econstructor.
     Unshelve.
-    all: cbn in * ; try eassumption.
+    all: cbn in * ; eassumption.
     (* econstructor; tea; now eapply escapeEqTerm. *)
   Qed.
 
+  Definition WreflLRTyEq {l wl Γ A} (lr : W[ Γ ||-< l > A ]< wl > ) :
+    W[ Γ ||-< l > A ≅ A | lr ]< wl >.
+  Proof.
+    exists (WT _ lr).
+    intros ; now eapply reflLRTyEq.
+  Defined.
+
   (* Deprecated *)
   Corollary LRTyEqRefl {l wl Γ A eqTy redTm eqTm}
     (lr : LogRel l wl Γ A eqTy redTm eqTm) : eqTy A.

theories/LogicalRelation/Universe.v

@@ -1,5 +1,5 @@
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening GenericTyping LogicalRelation.
+From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening GenericTyping Monad LogicalRelation.
 From LogRel.LogicalRelation Require Import Induction Escape Irrelevance.
 
 Set Universe Polymorphism.
@@ -31,13 +31,38 @@ Section UniverseReducibility.
       + apply (UnivEq' rU rA).
   Qed.
 
-  Lemma UnivEqEq@{i j k l} {wl Γ A B l l'} (rU : [ LogRel@{i j k l} l | Γ ||- U ]< wl >) (rA : [LogRel@{i j k l} l' | Γ ||- A ]< wl >) (rAB : [ LogRel@{i j k l} l | Γ ||- A ≅ B : U | rU ]< wl >)
+  Lemma WUnivEq@{i j k l} {wl Γ A l} l' (rU : WLogRel@{i j k l} l wl Γ U) (rA : WLogRelTm@{i j k l} l wl Γ A U rU)
+    : WLogRel@{i j k l} l' wl Γ A.
+  Proof.
+    unshelve eexists (DTree_fusion _ _ _).
+    + exact (WTTm _ rA).
+    + exact (WT _ rU).
+    + intros ; now eapply UnivEq, rA, over_tree_fusion_l.
+      Unshelve.
+      now eapply over_tree_fusion_r.
+  Qed.
+
+  Lemma UnivEqEq@{i j k l} {wl Γ A B l l'} (rU : [ LogRel@{i j k l} l | Γ ||- U ]< wl >)
+    (rA : [LogRel@{i j k l} l' | Γ ||- A ]< wl >)
+    (rAB : [ LogRel@{i j k l} l | Γ ||- A ≅ B : U | rU ]< wl >)
     : [ LogRel@{i j k l} l' | Γ ||- A ≅ B | rA ]< wl >.
   Proof.
     assert [ LogRel@{i j k l} one | Γ ||- A ≅ B : U | LRU_@{i j k l} (redUOne rU) ]< wl > as [ _ _ _ hA _ hAB ] by irrelevance.
     eapply LRTyEqIrrelevantCum. exact hAB.
   Qed.
 
+  Lemma WUnivEqEq@{i j k l} {wl Γ A B l l'} (rU : WLogRel@{i j k l} l wl Γ U)
+    (rA : WLogRel@{i j k l} l' wl Γ A)
+    (rAB : WLogRelTmEq@{i j k l} l wl Γ A B U rU)
+    : WLogRelEq@{i j k l} l' wl Γ A B rA.
+  Proof.
+    unshelve eexists (DTree_fusion _ _ _).
+    + exact (WTTmEq _ rAB).
+    + exact (WT _ rU).
+    + intros ; now eapply UnivEqEq, rAB, over_tree_fusion_l.
+      Unshelve.
+      now eapply over_tree_fusion_r.
+  Qed.
 
   (* The lemmas below does not seem to be
      at the right levels for fundamental lemma ! *)

theories/Substitution/Introductions/Application.v

@@ -1,5 +1,5 @@
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening GenericTyping LogicalRelation Validity.
+From LogRel Require Import Utils BasicAst Notations LContexts Context NormalForms Weakening GenericTyping LogicalRelation Validity.
 From LogRel.LogicalRelation Require Import Induction Irrelevance Escape Reflexivity Weakening Neutral Transitivity Reduction Application.
 From LogRel.Substitution Require Import Irrelevance Properties Conversion SingleSubst Reflexivity.
 
@@ -12,41 +12,44 @@ Set Printing Primitive Projection Parameters.
 
 Set Printing Universes.
 
-Lemma appValid {Γ F G t u l}
-  {VΓ : [||-v Γ]}
-  {VF : [Γ ||-v<l> F | VΓ]}
-  {VΠFG : [Γ ||-v<l> tProd F G | VΓ]}
-  (Vt : [Γ ||-v<l> t : tProd F G | VΓ | VΠFG])
-  (Vu : [Γ ||-v<l> u : F | VΓ | VF])
+Lemma appValid {Γ wl F G t u l}
+  {VΓ : [||-v Γ]< wl >}
+  {VF : [Γ ||-v<l> F | VΓ]< wl >}
+  {VΠFG : [Γ ||-v<l> tProd F G | VΓ]< wl >}
+  (Vt : [Γ ||-v<l> t : tProd F G | VΓ | VΠFG]< wl >)
+  (Vu : [Γ ||-v<l> u : F | VΓ | VF]< wl >)
   (VGu := substSΠ VΠFG Vu) :
-  [Γ ||-v<l> tApp t u : G[u..] | VΓ | VGu].
+  [Γ ||-v<l> tApp t u : G[u..] | VΓ | VGu]< wl >.
 Proof.
   opector; intros.
   - instValid Vσ.
-    epose (appTerm RVΠFG RVt RVu (substSΠaux VΠFG Vu _ _ wfΔ Vσ)).
-    irrelevance.
+    epose (WappTerm RVΠFG RVt RVu (substSΠaux VΠFG Vu _ _ _ f wfΔ Vσ)).
+    Wirrelevance. 
+    fold subst_term ; now bsimpl.
   - instAllValid Vσ Vσ' Vσσ'. 
-    unshelve epose (appcongTerm _ REVt RVu _ REVu (substSΠaux VΠFG Vu _ _ wfΔ Vσ)).
-    2: irrelevance.
-    eapply LRTmRedConv; tea.
-    unshelve eapply LRTyEqSym. 2,3: tea.
+    unshelve epose (WappcongTerm _ REVt RVu _ REVu (substSΠaux VΠFG Vu _ _ _ f wfΔ Vσ)).
+    2: Wirrelevance.
+    eapply WLRTmRedConv; tea.
+    unshelve eapply WLRTyEqSym. 2,3: tea.
+    fold subst_term ; now bsimpl.
 Qed.
 
-Lemma appcongValid {Γ F G t u a b l}
-  {VΓ : [||-v Γ]}
-  {VF : [Γ ||-v<l> F | VΓ]}
-  {VΠFG : [Γ ||-v<l> tProd F G | VΓ]}
-  (Vtu : [Γ ||-v<l> t ≅ u : tProd F G | VΓ | VΠFG])
-  (Va : [Γ ||-v<l> a : F | VΓ | VF])
-  (Vb : [Γ ||-v<l> b : F | VΓ | VF])
-  (Vab : [Γ ||-v<l> a ≅ b : F | VΓ | VF])
+Lemma appcongValid {Γ wl F G t u a b l}
+  {VΓ : [||-v Γ]< wl >}
+  {VF : [Γ ||-v<l> F | VΓ]< wl >}
+  {VΠFG : [Γ ||-v<l> tProd F G | VΓ]< wl >}
+  (Vtu : [Γ ||-v<l> t ≅ u : tProd F G | VΓ | VΠFG]< wl >)
+  (Va : [Γ ||-v<l> a : F | VΓ | VF]< wl >)
+  (Vb : [Γ ||-v<l> b : F | VΓ | VF]< wl >)
+  (Vab : [Γ ||-v<l> a ≅ b : F | VΓ | VF]< wl >)
   (VGa := substSΠ VΠFG Va) :
-  [Γ ||-v<l> tApp t a ≅ tApp u b : G[a..] | VΓ | VGa].
+  [Γ ||-v<l> tApp t a ≅ tApp u b : G[a..] | VΓ | VGa]< wl >.
 Proof.
   constructor; intros; instValid Vσ.
-  unshelve epose proof (appcongTerm _ RVtu _ _ _ (substSΠaux VΠFG Va _ _ wfΔ Vσ)); fold subst_term; cycle 5.
-  all: try irrelevance.
-  now eapply LRCumulative.
+  unshelve epose proof (WappcongTerm _ RVtu _ _ _ (substSΠaux VΠFG Va _ _ _ f wfΔ Vσ)); fold subst_term; cycle 5.
+  all: try Wirrelevance.
+  1: fold subst_term ; now bsimpl.  
+  now eapply WLRCumulative.
 Qed.
 
 End Application.