Add a Dtree for extensionality of codomain for Pis and Sigmas, and ex…

…tensionality of functions. Through to SimpleArr.v
CoqHott · Jan 21, 2025 · 4fe006f · 4fe006f
1 parent e8e2191
commit 4fe006f
Show file tree

Hide file tree

Showing 12 changed files with 998 additions and 242 deletions.
diff --git a/theories/LogicalRelation.v b/theories/LogicalRelation.v
@@ -292,14 +292,24 @@ Module PolyRedPack.
              (ha : [ shpRed ρ f Hd |  Δ ||- a : shp⟨ρ⟩]< k' >),
         forall {k''} (Ho : over_tree k' k'' (posTree ρ f Hd ha)),
           LRPack@{i} k'' Δ (pos[a .: (ρ >> tRel)]) ;
+    posExtTree {Δ a b k'} (ρ : Δ ≤ Γ) :
+      forall (f : k' ≤ε k)
+             (Hd : [ |-[ ta ] Δ ]< k' >)
+             (ha : [ shpRed ρ f Hd |  Δ ||- a : shp⟨ρ⟩]< k' >)
+             (hb : [ shpRed ρ f Hd |  Δ ||- b : shp⟨ρ⟩]< k' >)
+             (heq : [ shpRed ρ f Hd | Δ ||- a ≅ b : shp⟨ρ⟩ ]< k' >),
+        DTree k' ;
     posExt {Δ a b k'} (ρ : Δ ≤ Γ) :
       forall (f : k' ≤ε k)
              (Hd : [ |-[ ta ] Δ ]< k' >)
              (ha : [ shpRed ρ f Hd |  Δ ||- a : shp⟨ρ⟩]< k' >)
              (hb : [ shpRed ρ f Hd |  Δ ||- b : shp⟨ρ⟩]< k' >)
              (heq : [ shpRed ρ f Hd | Δ ||- a ≅ b : shp⟨ρ⟩ ]< k' >),
-      forall {k''} (Ho : over_tree k' k'' (posTree ρ f Hd ha)),
-        [ (posRed ρ f Hd ha Ho) | Δ ||- (pos[a .: (ρ >> tRel)]) ≅ (pos[b .: (ρ >> tRel)]) ]< k'' > ;
+      forall {k''}
+             (Hoa : over_tree k' k'' (posTree ρ f Hd ha))
+             (Hob : over_tree k' k'' (posTree ρ f Hd hb))
+             (Hoeq : over_tree k' k'' (posExtTree ρ f Hd ha hb heq)),
+        [ (posRed ρ f Hd ha Hoa) | Δ ||- (pos[a .: (ρ >> tRel)]) ≅ (pos[b .: (ρ >> tRel)]) ]< k'' > ;
       }.
 
   Arguments PolyRedPack {_ _ _ _}.
@@ -439,15 +449,15 @@ Inductive isLRFun `{ta : tag} `{WfContext ta}
     (funTree : forall {Δ k'} {a} (ρ : Δ ≤ Γ) (f : k' ≤ε k)
                       (Hd : [ |-[ ta ] Δ ]< k' >)
                       (ha : [ ΠA.(PolyRedPack.shpRed) ρ f Hd | Δ ||- a : ΠA.(PiRedTy.dom)⟨ρ⟩]< k' >),
-        DTree k'),
-    (forall {Δ k'} (ρ : Δ ≤ Γ) (f : k' ≤ε k) (h : [ |- Δ ]< k' >)
-            (domRed:= ΠA.(PolyRedPack.shpRed) ρ f h),
-        [domRed | Δ ||- (PiRedTy.dom ΠA)⟨ρ⟩ ≅ A'⟨ρ⟩]< k' >) ->
-    (forall {Δ k' a} (ρ : Δ ≤ Γ) (f : k' ≤ε k) (h : [ |- Δ ]< k' >)
-            (ha : [ ΠA.(PolyRedPack.shpRed) ρ f h | Δ ||- a : ΠA.(PiRedTy.dom)⟨ρ⟩ ]< k' >),
+        DTree k')
+    (HeqA : forall {Δ k'} (ρ : Δ ≤ Γ) (f : k' ≤ε k) (h : [ |- Δ ]< k' >)
+                   (domRed:= ΠA.(PolyRedPack.shpRed) ρ f h),
+        [domRed | Δ ||- (PiRedTy.dom ΠA)⟨ρ⟩ ≅ A'⟨ρ⟩]< k' >)
+    (Hred: forall {Δ k' a} (ρ : Δ ≤ Γ) (f : k' ≤ε k) (h : [ |- Δ ]< k' >)
+                  (ha : [ ΠA.(PolyRedPack.shpRed) ρ f h | Δ ||- a : ΠA.(PiRedTy.dom)⟨ρ⟩ ]< k' >),
       forall {k''} (Ho : over_tree k' k'' (ΠA.(PolyRedPack.posTree) ρ f h ha))
              (Ho' : over_tree k' k'' (funTree ρ f h ha)),
-        [ΠA.(PolyRedPack.posRed) ρ f h ha Ho | Δ ||- t[a .: (ρ >> tRel)] : ΠA.(PiRedTy.cod)[a .: (ρ >> tRel)]]< k'' >) ->
+        [ΠA.(PolyRedPack.posRed) ρ f h ha Ho | Δ ||- t[a .: (ρ >> tRel)] : ΠA.(PiRedTy.cod)[a .: (ρ >> tRel)]]< k'' >),
     isLRFun ΠA (tLambda A' t)
 | NeLRFun : forall f : term, [Γ |- f ~ f : tProd (PiRedTy.dom ΠA) (PiRedTy.cod ΠA)]< k > -> isLRFun ΠA f.
 
@@ -474,14 +484,23 @@ Module PiRedTm.
       forall {k''} (Ho : over_tree k' k'' (ΠA.(PolyRedPack.posTree) ρ f Hd ha))
              (Ho' : over_tree k' k'' (appTree ρ f Hd ha)),
         [ ΠA.(PolyRedPack.posRed) ρ f Hd ha Ho | Δ ||- tApp nf⟨ρ⟩ a : ΠA.(PiRedTy.cod)[a .: (ρ >> tRel)]]< k'' > ;
+    eqTree {Δ a b k'} (ρ : Δ ≤ Γ) :
+      forall (f : k' ≤ε k) (Hd : [ |-[ ta ] Δ ]< k' >)
+             (ha : [ ΠA.(PolyRedPack.shpRed) ρ f Hd |  Δ ||- a : ΠA.(PiRedTy.dom)⟨ρ⟩]< k' >)
+             (hb : [ ΠA.(PolyRedPack.shpRed) ρ f Hd |  Δ ||- b : ΠA.(PiRedTy.dom)⟨ρ⟩]< k' >)
+             (eq : [ ΠA.(PolyRedPack.shpRed) ρ f Hd | Δ ||- a ≅ b : ΠA.(PiRedTy.dom)⟨ρ⟩ ]< k' >),
+        DTree k' ;
     eq {Δ a b k'} (ρ : Δ ≤ Γ) :
-        forall (f : k' ≤ε k) (Hd : [ |-[ ta ] Δ ]< k' >)
-               (ha : [ ΠA.(PolyRedPack.shpRed) ρ f Hd |  Δ ||- a : ΠA.(PiRedTy.dom)⟨ρ⟩]< k' >)
-               (hb : [ ΠA.(PolyRedPack.shpRed) ρ f Hd |  Δ ||- b : ΠA.(PiRedTy.dom)⟨ρ⟩]< k' >)
-               (eq : [ ΠA.(PolyRedPack.shpRed) ρ f Hd | Δ ||- a ≅ b : ΠA.(PiRedTy.dom)⟨ρ⟩ ]< k' >),
-        forall {k''} (Ho : over_tree k' k'' (ΠA.(PolyRedPack.posTree) ρ f Hd ha))
-               (Ho' : over_tree k' k'' (appTree ρ f Hd ha)),
-          [ ΠA.(PolyRedPack.posRed) ρ f Hd ha Ho | Δ ||- tApp nf⟨ρ⟩ a ≅ tApp nf⟨ρ⟩ b : ΠA.(PiRedTy.cod)[a .: (ρ >> tRel)] ]< k'' > ;
+      forall (f : k' ≤ε k) (Hd : [ |-[ ta ] Δ ]< k' >)
+             (ha : [ ΠA.(PolyRedPack.shpRed) ρ f Hd |  Δ ||- a : ΠA.(PiRedTy.dom)⟨ρ⟩]< k' >)
+             (hb : [ ΠA.(PolyRedPack.shpRed) ρ f Hd |  Δ ||- b : ΠA.(PiRedTy.dom)⟨ρ⟩]< k' >)
+             (eq : [ ΠA.(PolyRedPack.shpRed) ρ f Hd | Δ ||- a ≅ b : ΠA.(PiRedTy.dom)⟨ρ⟩ ]< k' >),
+      forall {k''}
+             (HoPi : over_tree k' k'' (ΠA.(PolyRedPack.posTree) ρ f Hd ha))
+             (Hoa : over_tree k' k'' (appTree ρ f Hd ha))
+             (Hob : over_tree k' k'' (appTree ρ f Hd hb))
+             (Hoeq : over_tree k' k'' (eqTree ρ f Hd ha hb eq)),
+        [ ΠA.(PolyRedPack.posRed) ρ f Hd ha HoPi | Δ ||- tApp nf⟨ρ⟩ a ≅ tApp nf⟨ρ⟩ b : ΠA.(PiRedTy.cod)[a .: (ρ >> tRel)] ]< k'' > ;
     }.
 
   Arguments PiRedTm {_ _ _ _ _ _ _ _ _}.
@@ -1455,15 +1474,25 @@ Section PolyRed.
                 (ha : [ shpRed ρ f Hd |  Δ ||- a : shp⟨ρ⟩]< k' >),
          forall {k''} (Ho : over_tree k' k'' (posTree ρ f Hd ha)),
            [ LogRel@{i j k l} l | Δ ||- pos[a .: (ρ >> tRel)]]< k'' > ;
+      posExtTree {Δ k' a b}
+        (ρ : Δ ≤ Γ) (f : k' ≤ε k)
+        (Hd :  [ |- Δ ]< k' >)
+        (ha : [ (shpRed ρ f Hd) | Δ ||- a : shp⟨ρ⟩ ]< k' >)
+        (hb : [ (shpRed ρ f Hd) | Δ ||- b : shp⟨ρ⟩]< k' >)
+        (hab : [ (shpRed ρ f Hd) | Δ ||- a ≅ b : shp⟨ρ⟩]< k' >) :
+      DTree k' ;
       posExt
         {Δ k' a b}
         (ρ : Δ ≤ Γ) (f : k' ≤ε k)
         (Hd :  [ |- Δ ]< k' >)
-        (ha : [ (shpRed ρ f Hd) | Δ ||- a : shp⟨ρ⟩ ]< k' >) :
-        [ (shpRed ρ f Hd) | Δ ||- b : shp⟨ρ⟩]< k' > ->
-        [ (shpRed ρ f Hd) | Δ ||- a ≅ b : shp⟨ρ⟩]< k' > ->
-        forall {k''} (Ho : over_tree k' k'' (posTree ρ f Hd ha)),
-        [ (posRed ρ f Hd ha Ho) | Δ ||- (pos[a .: (ρ >> tRel)]) ≅ (pos[b .: (ρ >> tRel)]) ]< k'' > ;
+        (ha : [ (shpRed ρ f Hd) | Δ ||- a : shp⟨ρ⟩ ]< k' >)
+        (hb : [ (shpRed ρ f Hd) | Δ ||- b : shp⟨ρ⟩]< k' >)
+        (hab : [ (shpRed ρ f Hd) | Δ ||- a ≅ b : shp⟨ρ⟩]< k' >) :
+      forall {k''}
+             (Hoa : over_tree k' k'' (posTree ρ f Hd ha))
+             (Hob : over_tree k' k'' (posTree ρ f Hd hb))
+             (Hoeq : over_tree k' k'' (posExtTree ρ f Hd ha hb hab)),
+        [ (posRed ρ f Hd ha Hoa) | Δ ||- (pos[a .: (ρ >> tRel)]) ≅ (pos[b .: (ρ >> tRel)]) ]< k'' > ;
     }.
 
   Definition from@{i j k l} {PA : PolyRedPack@{k} k Γ shp pos} 
@@ -1474,6 +1503,7 @@ Section PolyRed.
     - econstructor ; unshelve eapply PolyRedPack.shpAd. 4: eassumption. all: eauto.
     - eapply PolyRedPack.posTree ; eauto.
     - econstructor. unshelve eapply PolyRedPack.posAd. 8: exact Ho. tea.
+    - eapply (PolyRedPack.posExtTree PA (a := a) (b := b)) ; eassumption.
     - now eapply PolyRedPack.shpTy.
     - now eapply PolyRedPack.posTy.
     - now eapply PolyRedPack.posExt.
@@ -1485,6 +1515,7 @@ Section PolyRed.
     - now eapply shpRed.
     - intros ; now eapply posTree.
     - intros; now eapply posRed.
+    - intros ; now eapply (posExtTree PA (a := a) (b := b)).
     - now eapply shpTy. 
     - now eapply posTy.
     - intros; now eapply posExt.

diff --git a/theories/LogicalRelation/Application.v b/theories/LogicalRelation/Application.v
@@ -158,7 +158,7 @@ Proof.
   set (h := invLRΠ _) in hΠ.
   epose proof (e := redtywf_whnf (PiRedTyPack.red h) whnf_tProd); 
   symmetry in e; injection e; clear e; 
-  destruct h as [?????? [?? domRed ? codRed codExt]] ; clear RΠ Rtt'; 
+  destruct h as [?????? [?? domRed ? codRed codExtTree codExt]] ; clear RΠ Rtt'; 
   intros; cbn in *; subst. 
   assert (wfΓ : [|-Γ]< wl >) by gen_typing.
   assert [Γ ||-<l> u' : F⟨@wk_id Γ⟩ | domRed _ _ (@wk_id Γ) (idε _) wfΓ]< wl > by irrelevance.
@@ -175,18 +175,22 @@ Proof.
   1:{
     replace G[u..] with G[u .: @wk_id Γ >> tRel] by now bsimpl.
     unshelve eapply WLRTyEqIrrelevant'.
-    5: exists (posTree _ _ u' (@wk_id Γ) (idε _) wfΓ X) ; intros wl' f Hover.
-    5: irrelevance0 ; [ reflexivity | ].
-    5: unshelve eapply codExt.
-    11: eapply LRTmEqSym; irrelevance.
-    4-8: tea.
+    5:{ unshelve eexists ; [eapply DTree_fusion ; [eapply DTree_fusion | ] | ].
+        + exact (posTree _ _ u' (@wk_id Γ) (idε _) wfΓ X).
+        + exact (posTree _ _ u (@wk_id Γ) (idε _) wfΓ X0).
+        + eapply (codExtTree Γ wl u' u wk_id ((idε) wl) wfΓ) ; eauto.
+          now eapply LRTmEqSym; irrelevance.
+        + intros.
+          irrelevance0 ; [reflexivity | unshelve eapply codExt].
+          9: eapply over_tree_fusion_r, over_tree_fusion_l ; eassumption.
+          2: do 2 (eapply over_tree_fusion_l) ; eassumption.
+          1: now eapply LRTmEqSym; irrelevance.
+          eapply over_tree_fusion_r ; exact Hover'.
+    }
     3: now bsimpl.
     2: now replace G[u' .: @wk_id Γ >> tRel] with G[u'..] by now bsimpl.
   }
-  pose (fez:= (snd (appTerm0 hΠ Rt Ru RGu))).
-  pose (zef := (snd (appTerm0 hΠ Rt' Ru' RGu'))).
   unshelve epose  proof (eqApp _ u _ (@wk_id Γ) (idε _) wfΓ _).  1: irrelevance.
-  cbn in *.
   eapply WtransEqTerm; eapply WtransEqTerm.
   - unshelve eapply (snd (appTerm0 hΠ Rt Ru RGu)).
   - unshelve epose  proof (eqApp _ u _ (@wk_id Γ) (idε _) wfΓ _).  1: irrelevance.
@@ -201,8 +205,10 @@ Proof.
     5: unshelve eapply Hyp.
     4: now bsimpl.
     1,2,5: irrelevance.
-    2: eapply over_tree_fusion_l ; exact Hover'. 
-    eapply over_tree_fusion_r ; exact Hover'.
+    2: do 2 (eapply over_tree_fusion_l) ; exact Hover'. 
+    + eapply over_tree_fusion_r, over_tree_fusion_l ; exact Hover'.
+    + eapply over_tree_fusion_l, over_tree_fusion_r ; exact Hover'.
+    + do 2 (eapply over_tree_fusion_r) ; exact Hover'.
   - replace (_)⟨_⟩ with (PiRedTm.nf Rt') by now bsimpl.
     eapply WLRTmEqRedConv; tea.
     eapply WLRTmEqSym.

diff --git a/theories/LogicalRelation/Irrelevance.v b/theories/LogicalRelation/Irrelevance.v
@@ -129,6 +129,9 @@ Proof.
       * eapply (PolyRed.posTree ΠA) ; now eapply eqv.(eqvShp).
       * eapply eqv.(eqvTree) ; eauto. now eapply eqv.(eqvShp).
     + eapply appTree ; now eapply eqv.(eqvShp).
+  - intros ; eapply DTree_fusion.
+    + eapply (PolyRed.posExtTree ΠA (a := a) (b := b)) ; now eapply eqv.(eqvShp).
+    + eapply (eqTree _ a b) ; now eapply eqv.(eqvShp).
   - now eapply redtmwf_conv.
   - eapply (convtm_conv refl).
     now apply eqPi.
@@ -150,9 +153,9 @@ Proof.
     + eapply over_tree_fusion_r ; eassumption.
   - intros; unshelve eapply eqv.(eqvPos), eq.
     all: try now eapply eqv.(eqvShp).
+    3-5: eapply over_tree_fusion_r ; eassumption.
     + do 2 (eapply over_tree_fusion_l) ; eassumption.
     + eapply over_tree_fusion_r, over_tree_fusion_l ; eassumption.
-    + eapply over_tree_fusion_r ; eassumption.
 Defined.
 
 Lemma ΠIrrelevanceTmEq t u : [Γ ||-<lA> t ≅ u : A | RA]< wl > -> [Γ ||-<lA'> t ≅ u : A' | RA']< wl >.
@@ -731,22 +734,31 @@ Proof.
   + intros Δ wl' a ρ f tΔ ra wl'' Hover ; cbn in *.
     eapply IHpos.
     eapply over_tree_fusion_l ; eassumption.
+  + intros.
+    eapply (PA.(PolyRed.posExtTree) (a := a) (b := b)).
+    all: pose (shpRed := PA.(PolyRed.shpRed) ρ f Hd).
+    all: destruct (LRIrrelevantPreds IH _ _ _ _
+                  (LRAd.adequate shpRed)
+                  (LRAd.adequate (IHshp Δ _ ρ f Hd))
+                  (reflLRTyEq shpRed)) as [_ irrTmRed irrTmEq].
+    * now eapply (snd (irrTmRed a)).
+    * now eapply (snd (irrTmRed b)).
+    * now eapply (snd (irrTmEq a b)).
   + now destruct PA.
   + now destruct PA.
   + cbn. intros Δ wl' a b ρ f tΔ ra rb rab wl''.
     set (p := LRIrrelevantPreds _ _ _ _ _ _ _ _).
     destruct p as [_ irrTmRed irrTmEq].
     pose (ra' := snd (irrTmRed a) ra) ; cbn in *.
-    intros Hover.
-    pose (posRed := PA.(PolyRed.posRed) ρ f tΔ ra' (over_tree_fusion_r Hover)).
+    intros Hoa Hob Hoab.
+    pose (posRed := PA.(PolyRed.posRed) ρ f tΔ ra' (over_tree_fusion_r Hoa)).
     destruct (LRIrrelevantPreds IH _ _ _ _
                 (LRAd.adequate posRed)
-                (LRAd.adequate (IHpos Δ _ a ρ f tΔ ra' wl'' (over_tree_fusion_l Hover)))
+                (LRAd.adequate (IHpos Δ _ a ρ f tΔ ra' wl'' (over_tree_fusion_l Hoa)))
                 (reflLRTyEq posRed)) as [irrTyEq _ _].
     eapply (fst (irrTyEq (pos[b .: ρ >> tRel]))).
-    eapply PolyRed.posExt.
-    1: exact (snd (irrTmRed b) rb).
-    exact (snd (irrTmEq a b) rab).
+    eapply PolyRed.posExt ; [ | eassumption].
+    now eapply over_tree_fusion_r.
 Qed.
 
 
@@ -1182,6 +1194,15 @@ Proof.
   intros ?? []; split; [eapply LRTmRedIrrelevant'| eapply LRTmEqIrrelevant']; tea.
 Qed.
 
+Corollary WLRTmTmEqIrrelevant' lA lA' wl Γ A A' (e : A = A')
+  (lrA : W[Γ ||-< lA > A]< wl >) (lrA' : W[Γ ||-< lA'> A']< wl >) :
+  forall t u, 
+  W[Γ ||-<lA> t : A | lrA]< wl > × W[Γ ||-< lA > t ≅ u : A | lrA]< wl > -> 
+  W[Γ ||-<lA'> t : A' | lrA']< wl > × W[Γ ||-< lA' > t ≅ u : A' | lrA']< wl >.
+Proof.
+  intros ?? []; split; [eapply WLRTmRedIrrelevant'| eapply WLRTmEqIrrelevant']; tea.
+Qed.  
+
 Set Printing Primitive Projection Parameters.
 
 Lemma NeNfEqSym {wl Γ k k' A} : [Γ ||-NeNf k ≅ k' : A]< wl > -> [Γ ||-NeNf k' ≅ k : A]< wl >.
@@ -1225,15 +1246,22 @@ Proof.
     1,2: tea.
     2: now symmetry.
     + intros ; eapply DTree_fusion.
-      * now eapply eqTree.
-      * exact (PolyRed.posTree ΠA _ _ _ (SigRedTm.fstRed redL ρ f Hd)).
+      * eapply DTree_fusion.
+        -- now eapply eqTree.
+        -- exact (PolyRed.posTree ΠA _ _ _ (SigRedTm.fstRed redL ρ f Hd)).
+      * eapply (PolyRed.posExtTree ΠA ρ f Hd).
+        -- eapply (SigRedTm.fstRed redL ρ f Hd).
+        -- eapply (SigRedTm.fstRed redR ρ f Hd).
+        -- now eapply eqFst.
     + intros; now eapply ihshp.
     + intros; unshelve eapply ihpos.
       eapply LRTmEqRedConv.
       2: unshelve eapply (eqSnd _ k') ; eauto ; cbn in *.
-      * now eapply PolyRed.posExt.
-      * now eapply over_tree_fusion_r. 
-      * now eapply over_tree_fusion_l. 
+      * eapply PolyRed.posExt.
+        -- eassumption.
+        -- now eapply over_tree_fusion_r. 
+      * now eapply over_tree_fusion_r, over_tree_fusion_l. 
+      * now do 2 (eapply over_tree_fusion_l). 
   - intros ???? [] ???? [????? hprop]; unshelve econstructor; unfold_id_outTy; cbn in *.
     3,4: tea.
     1: now symmetry.