remove unnecessary reducible conversion in reducibility of list terms

CoqHott · Jul 14, 2023 · b7efd26 · b7efd26
1 parent d2ed98d
commit b7efd26
Show file tree

Hide file tree

Showing 6 changed files with 89 additions and 130 deletions.
diff --git a/coq-partialfun b/coq-partialfun
diff --git a/theories/LogicalRelation.v b/theories/LogicalRelation.v
@@ -910,11 +910,11 @@ Section ListRedTm.
   with ListProp : term -> Type :=
   | nilR {P} (wfΓ : [|- Γ]) :
     [Γ |- P] ->
-    [parRedΓ wfΓ | Γ ||- _ ≅ P] ->
+    [Γ |- par ≅ P] ->
     ListProp (tNil P)
   | consR {P hd tl} (wfΓ : [|- Γ]):
     [Γ |- P] ->
-    [parRedΓ wfΓ | Γ ||- _ ≅ P] ->
+    [Γ |- par ≅ P] ->
     [parRedΓ wfΓ | Γ ||- hd : _] ->
     ListRedTm tl ->
     ListProp (tCons P hd tl)
@@ -1025,15 +1025,15 @@ Section ListRedTmEq.
   (* KM: plugging in the parameter type directly... Is that ok ? *)
   | nilReq {P P'} (wfΓ : [|- Γ]) :
     [Γ |- P] ->
-    [parRedΓ wfΓ | Γ ||- _ ≅ P] ->
+    [Γ |- par ≅ P] ->
     [Γ |- P'] ->
-    [parRedΓ wfΓ | Γ ||- _ ≅ P'] ->
+    [Γ |- par ≅ P'] ->
     ListPropEq (tNil P) (tNil P')
   | consReq {P P' hd hd' tl tl'} (wfΓ : [|- Γ]) :
     [Γ |- P] ->
-    [parRedΓ wfΓ | Γ ||- _ ≅ P] ->
+    [Γ |- par ≅ P] ->
     [Γ |- P'] ->
-    [parRedΓ wfΓ | Γ ||- _ ≅ P'] ->
+    [Γ |- par ≅ P'] ->
     [parRedΓ wfΓ | Γ ||- hd ≅ hd' : _] ->
     ListRedTmEq tl tl' ->
     ListPropEq (tCons P hd tl) (tCons P' hd' tl')

diff --git a/theories/LogicalRelation/Irrelevance.v b/theories/LogicalRelation/Irrelevance.v
@@ -290,8 +290,8 @@ Proof.
   eapply ListRedInduction; intros; econstructor; tea.
   - now eapply redtmwf_conv.
   - now eapply convtm_conv.
-  - now eapply eqvPar.
-  - now eapply eqvPar.
+  - etransitivity ; tea; now symmetry.
+  - etransitivity ; tea; now symmetry.
   - now eapply eqvPar.
   - now eapply ty_conv.
   - now eapply convneulist_conv.
@@ -313,9 +313,10 @@ Proof.
     all: cbn in * ; tea.
     now eapply convtm_conv.
   - econstructor ; tea.
-    all: now eapply eqvPar.
+    all: etransitivity ; tea; now symmetry.
   - econstructor ; tea.
-    all: now eapply eqvPar.
+    3: now eapply eqvPar.
+    all: etransitivity ; tea; now symmetry.
   - econstructor.
     2,3: now eapply ListRedTm_map_inv_irrelevance.
     2: now eapply ListRedTm_map_inv_eq_irrelevance.

diff --git a/theories/LogicalRelation/Transitivity.v b/theories/LogicalRelation/Transitivity.v
@@ -258,14 +258,14 @@ Proof.
     + etransitivity ; tea. etransitivity ; tea.
       rewrite eqR. eapply lrefl ; tea.
     + eapply h. rewrite eqR. eassumption.
-  - intros * ????? uv.
+  - intros * ?????? uv.
     inversion uv ; subst.
     2:{ apply convneulist_whne_list in conv. inv_whne. }
     econstructor; tea; irrelevance.
   - intros * ????? ? h ? uv.
     inversion uv ; subst.
     2:{ apply convneulist_whne_list in conv. inv_whne. }
-    econstructor ; try easy. 1: irrelevance.
+    econstructor ; try easy.
     eapply ih; tea; irrelevance.
   - intros * ????? uv.
     assert (whne_list l').

diff --git a/theories/LogicalRelation/Weakening.v b/theories/LogicalRelation/Weakening.v
@@ -233,20 +233,10 @@ Section Weakenings.
       + assumption.
     - intros. unshelve econstructor; tea.
       + now eapply wft_wk.
-      + irrelevance0.
-        1: now rewrite wk_id_ren_on.
-        unshelve eapply wkEq; tea.
-        2: irrelevance.
-        pose proof (h := ListRedTy.parRed LA wk_id wfΓ); 
-        now rewrite wk_id_ren_on in h.
+      + cbn; now eapply convty_wk.
     - intros. unshelve econstructor; tea.
       + now eapply wft_wk.
-      + irrelevance0.
-        1: now rewrite wk_id_ren_on.
-        unshelve eapply wkEq; tea.
-        2: irrelevance.
-        pose proof (h := ListRedTy.parRed LA wk_id wfΓ); 
-        now rewrite wk_id_ren_on in h.
+      + cbn; now eapply convty_wk.
       + fold ren_term. 
         irrelevance0.
         2: now apply ih.
@@ -393,34 +383,14 @@ Section Weakenings.
         assumption.
     - intros. unshelve econstructor; tea.
       + now eapply wft_wk.
-      + irrelevance0.
-        1: now rewrite wk_id_ren_on.
-        unshelve eapply wkEq; tea.
-        2: irrelevance.
-        pose proof (h := ListRedTy.parRed LA wk_id wfΓ); 
-        now rewrite wk_id_ren_on in h.
+      + cbn; now eapply convty_wk.
       + now eapply wft_wk.
-      + irrelevance0.
-        1: now rewrite wk_id_ren_on.
-        unshelve eapply wkEq; tea.
-        2: irrelevance.
-        pose proof (h := ListRedTy.parRed LA wk_id wfΓ); 
-        now rewrite wk_id_ren_on in h.
+      + cbn; now eapply convty_wk.
     - intros. unshelve econstructor; tea.
       + now eapply wft_wk.
-      + irrelevance0.
-        1: now rewrite wk_id_ren_on.
-        unshelve eapply wkEq; tea.
-        2: irrelevance.
-        pose proof (h := ListRedTy.parRed LA wk_id wfΓ); 
-        now rewrite wk_id_ren_on in h.
+      + cbn; now eapply convty_wk.
       + now eapply wft_wk.
-      + irrelevance0.
-        1: now rewrite wk_id_ren_on.
-        unshelve eapply wkEq; tea.
-        2: irrelevance.
-        pose proof (h := ListRedTy.parRed LA wk_id wfΓ); 
-        now rewrite wk_id_ren_on in h.
+      + cbn; now eapply convty_wk.
       + irrelevance0.
         2: now apply ih.
         now rewrite 2! wk_id_ren_on.