Merge pull request #55 from CoqHott/uniformize-validity-lemma-names

Uniformize some lemma names for validity.
CoqHott · Sep 27, 2023 · 1f16171 · 1f16171
2 parents e6330aa + d397c56
commit 1f16171
Show file tree

Hide file tree

Showing 10 changed files with 69 additions and 69 deletions.
diff --git a/theories/Fundamental.v b/theories/Fundamental.v
@@ -150,7 +150,7 @@ Section Fundamental.
     econstructor.
     unshelve eapply (PiValid VΓ).
     - assumption.
-    - now eapply irrelevanceValidity.
+    - now eapply irrelevanceTy.
   Qed.
 
   Lemma FundTyUniv (Γ : context) (A : term)
@@ -236,7 +236,7 @@ Section Fundamental.
     FundTyEq Γ A B -> FundTyEq Γ B A.
   Proof.
     intros * [];  unshelve econstructor; tea.
-    now eapply symValidEq.
+    now eapply symValidTyEq.
   Qed.
 
   Lemma FundTyEqTrans : forall (Γ : context) (A B C : term),
@@ -245,7 +245,7 @@ Section Fundamental.
     FundTyEq Γ A C.
   Proof.
     intros * [] []; unshelve econstructor; tea. 1:irrValid.
-    eapply transValidEq; irrValid.
+    eapply transValidTyEq; irrValid.
     Unshelve. tea.
   Qed.
 
@@ -332,13 +332,13 @@ Section Fundamental.
     { eapply irrelevanceLift; [tea|]; irrValid. }
     assert (Vλt : [Γ ||-v< one > tLambda A' t : tProd A B | VΓ | VΠAB ]).
     { eapply conv; [|eapply lamValid].
-      + eapply symValidEq, PiCong; tea; try irrValid.
+      + eapply symValidTyEq, PiCong; tea; try irrValid.
         eapply reflValidTy.
       + eapply irrelevanceTmLift; irrValid.
     }
     assert (Vλu : [Γ ||-v< one > tLambda A'' u : tProd A B | VΓ | VΠAB ]).
     { eapply conv; [|eapply lamValid].
-      + eapply symValidEq, PiCong; tea; try irrValid.
+      + eapply symValidTyEq, PiCong; tea; try irrValid.
         eapply reflValidTy.
       + eapply irrelevanceTmLift; irrValid.
     }
@@ -363,7 +363,7 @@ Section Fundamental.
     + eapply irrelevanceTmEq'; [eapply eq0|].
       eapply transValidTmEq; [eapply betaValid|]; refold.
       - eapply irrelevanceTm'.
-        2: eapply (wkTmValid  (A := B)) with (ρ := wk_up A' (@wk1 Γ A)).
+        2: eapply (wkValidTm  (A := B)) with (ρ := wk_up A' (@wk1 Γ A)).
         * now bsimpl.
         * eapply irrelevanceTmLift; irrValid.
       - eapply irrelevanceTmEq'; [symmetry; eapply eq0|].
@@ -374,7 +374,7 @@ Section Fundamental.
     + apply symValidTmEq; eapply irrelevanceTmEq'; [eapply eq0|].
       eapply transValidTmEq; [eapply betaValid|]; refold.
       - eapply irrelevanceTm'.
-        2: eapply (wkTmValid  (A := B)) with (ρ := wk_up A'' (@wk1 Γ A)).
+        2: eapply (wkValidTm  (A := B)) with (ρ := wk_up A'' (@wk1 Γ A)).
         * now bsimpl.
         * eapply irrelevanceTmLift; irrValid.
       - eapply irrelevanceTmEq'; [symmetry; eapply eq0|].
@@ -384,16 +384,16 @@ Section Fundamental.
         apply reflValidTm; tea.
     Unshelve.
     all: refold; try irrValid.
-    * unshelve eapply irrelevanceValidity; tea.
+    * unshelve eapply irrelevanceTy; tea.
       rewrite <- (wk_up_wk1_ren_on Γ A' A).
-      eapply wkValid, irrelevanceLift; irrValid.
-    * eapply conv; [now eapply irrelevanceEq, wk1ValidTyEq|].
+      eapply wkValidTy, irrelevanceLift; irrValid.
+    * eapply conv; [now eapply irrelevanceTyEq, wk1ValidTyEq|].
       eapply irrelevanceTm'; [symmetry; eapply wk1_ren_on|].
       eapply var0Valid'.
-    * eapply irrelevanceValidity.
+    * eapply irrelevanceTy.
       rewrite <- (wk_up_wk1_ren_on Γ A'' A).
-      eapply wkValid, irrelevanceLift; irrValid.
-    * eapply conv; [now eapply irrelevanceEq, wk1ValidTyEq|].
+      eapply wkValidTy, irrelevanceLift; irrValid.
+    * eapply conv; [now eapply irrelevanceTyEq, wk1ValidTyEq|].
       eapply irrelevanceTm'; [symmetry; eapply wk1_ren_on|].
       eapply var0Valid'.
   Unshelve.
@@ -411,29 +411,29 @@ Section Fundamental.
   { now eapply PiValidDom. }
   assert (VΓA := validSnoc VΓ VA).
   assert (VΓAA : [Γ,, A ||-v< one > A⟨@wk1 Γ A⟩ | VΓA]).
-  { now eapply irrelevanceValidity, wk1ValidTy. }
+  { now eapply irrelevanceTy, wk1ValidTy. }
   assert (VΓAA0 : VAdequate (ta := ta) (Γ,, A,, A⟨@wk1 Γ A⟩) VR).
   { now eapply validSnoc. }
   assert (VΓAA' : [Γ,, A ||-v< one > A⟨↑⟩ | VΓA]).
   { now rewrite wk1_ren_on in VΓAA. }
   assert [Γ,, A ||-v< one > B | VΓA].
-  { eapply irrelevanceValidity, PiValidCod. }
+  { eapply irrelevanceTy, PiValidCod. }
   assert ([Γ,, A ||-v< one > tProd A⟨@wk1 Γ A⟩ B⟨upRen_term_term ↑⟩ | VΓA]).
   { rewrite <- (wk_up_wk1_ren_on Γ A A).
-    now eapply irrelevanceValidity, (wk1ValidTy (A := tProd A B)). }
+    now eapply irrelevanceTy, (wk1ValidTy (A := tProd A B)). }
   assert ([Γ,, A ||-v< one > tRel 0 : A⟨wk1 A⟩ | VΓA | VΓAA]).
   { eapply irrelevanceTm'; [rewrite wk1_ren_on; reflexivity|].
     unshelve apply var0Valid'. }
   assert ([(Γ,, A),, A⟨wk1 A⟩ ||-v< one > tProd A⟨↑⟩⟨↑⟩ B⟨upRen_term_term ↑⟩⟨upRen_term_term ↑⟩ | VΓAA0]).
   { assert (eq1 : (tProd A B)⟨@wk1 Γ A⟩⟨@wk1 (Γ,, A) A⟨@wk1 Γ A⟩⟩ = tProd (A⟨↑⟩⟨↑⟩) (B⟨upRen_term_term ↑⟩⟨upRen_term_term ↑⟩)).
     { rewrite wk1_ren_on, wk1_ren_on; reflexivity. }
-    eapply irrelevanceValidity'; [|eapply eq1|reflexivity].
-    now eapply wkValid, wkValid. }
+    eapply irrelevanceTy'; [|eapply eq1|reflexivity].
+    now eapply wkValidTy, wkValidTy. }
   assert ([Γ ||-v< one > tLambda A (tApp f⟨↑⟩ (tRel 0)) : tProd A B | VΓ | VΠ]).
   { eapply irrelevanceTm, lamValid.
     eapply irrelevanceTm'; [apply eq0|eapply (appValid (F := A⟨@wk1 Γ A⟩))].
     rewrite <- (wk1_ren_on Γ A).
-    eapply irrelevanceTm'; [|now eapply wkTmValid].
+    eapply irrelevanceTm'; [|now eapply wkValidTm].
     rewrite <- (wk_up_wk1_ren_on Γ A A).
     reflexivity. }
   Unshelve. all: try irrValid.
@@ -449,7 +449,7 @@ Section Fundamental.
     { rewrite wk1_ren_on, wk1_ren_on; reflexivity. }
     eapply irrelevanceTm'; [eapply eq1|].
     rewrite <- (wk1_ren_on (Γ,, A)  A⟨@wk1 Γ A⟩).
-    now eapply wkTmValid, wkTmValid.
+    now eapply wkValidTm, wkValidTm.
   + refold.
     match goal with |- [_ ||-v< _ > ?t ≅ ?u : _ | _ | _ ] => assert (Hrw : t = u) end.
     { rewrite <- eq0; now bsimpl. }
@@ -461,18 +461,18 @@ Section Fundamental.
     now rewrite <- (wk_up_wk1_ren_on Γ A A).
   Unshelve.
   all: refold; try irrValid.
-  { unshelve eapply irrelevanceValidity; [tea|].
+  { unshelve eapply irrelevanceTy; [tea|].
     rewrite <- (wk_up_wk1_ren_on Γ A A).
-    now eapply wkValid. }
-  { eapply (irrelevanceValidity' (A := A⟨↑⟩⟨@wk1 (Γ,, A) A⟨@wk1 Γ A⟩⟩)); [|now rewrite wk1_ren_on|reflexivity].
-    now eapply wkValid. }
+    now eapply wkValidTy. }
+  { eapply (irrelevanceTy' (A := A⟨↑⟩⟨@wk1 (Γ,, A) A⟨@wk1 Γ A⟩⟩)); [|now rewrite wk1_ren_on|reflexivity].
+    now eapply wkValidTy. }
   { eapply (irrelevanceTm' (A := A⟨@wk1 Γ A⟩⟨↑⟩)); [now rewrite wk1_ren_on|].
     apply var0Valid'. }
   Unshelve.
   all: try irrValid.
   { shelve. }
   { rewrite <- (wk1_ren_on (Γ,, A)  A⟨@wk1 Γ A⟩).
-    now eapply wkValid. }
+    now eapply wkValidTy. }
   Qed.
 
   Lemma FundTmEqFunExt : forall (Γ : context) (f g A B : term),
@@ -487,7 +487,7 @@ Section Fundamental.
     1:{
       eapply conv. 
       2: irrValid.
-      eapply symValidEq. eapply PiCong.
+      eapply symValidTyEq. eapply PiCong.
       eapply irrelevanceLift. 
       1,3,4: eapply reflValidTy.
       irrValid.
@@ -624,7 +624,7 @@ Section Fundamental.
     2: eapply natElimValid; irrValid.
     + eapply conv.
       2: eapply irrelevanceTm; now eapply natElimValid.
-      eapply symValidEq. 
+      eapply symValidTyEq. 
       eapply substSEq; tea. 
       2,3: irrValid.
       eapply reflValidTy.
@@ -682,7 +682,7 @@ Section Fundamental.
     2: eapply emptyElimValid; irrValid.
     + eapply conv.
       2: eapply irrelevanceTm; now eapply emptyElimValid.
-      eapply symValidEq.
+      eapply symValidTyEq.
       eapply substSEq; tea.
       2,3: irrValid.
       eapply reflValidTy.
@@ -837,7 +837,7 @@ Section Fundamental.
     3,5: unshelve eapply pairSndValid; irrValid.
     + tea.
     + eapply conv; tea.
-      eapply irrelevanceEq.
+      eapply irrelevanceTyEq.
       eapply substSEq.
       1,3: eapply reflValidTy.
       1: irrValid.
@@ -916,7 +916,7 @@ Section Fundamental.
     3: eapply conv.
     2,4: eapply reflValid; try irrValid.
     2: eapply conv; irrValid.
-    2: eapply symValidEq; eapply IdCongValid; tea; try irrValid.
+    2: eapply symValidTyEq; eapply IdCongValid; tea; try irrValid.
     eapply IdValid; irrValid.
     Unshelve. all: try eapply IdValid; try irrValid; eapply conv; irrValid.
     Unshelve. all: irrValid.
@@ -956,7 +956,7 @@ Section Fundamental.
     3,4: eapply IdValid; irrValid.
     1: eapply validSnoc; now eapply idElimMotiveCtxIdValid.
     eapply convCtx2'; tea.
-    1: eapply convCtx1; tea; [eapply symValidEq; irrValid| ].
+    1: eapply convCtx1; tea; [eapply symValidTyEq; irrValid| ].
     1,3: now eapply idElimMotiveCtxIdValid.
     eapply idElimMotiveCtxIdCongValid; tea; irrValid.
     Unshelve.

diff --git a/theories/Substitution/Conversion.v b/theories/Substitution/Conversion.v
@@ -125,11 +125,11 @@ Lemma convCtx1 {Γ A B P l}
   [_ ||-v<l> P | VΓB].
 Proof.
   opector; intros.
-  - eapply validTy; tea; eapply convSubstCtx1; tea; now eapply symValidEq.
+  - eapply validTy; tea; eapply convSubstCtx1; tea; now eapply symValidTyEq.
   - irrelevanceRefl; unshelve eapply validTyExt.
     3,4: tea. 
-    1,2:  eapply convSubstCtx1; tea; now eapply symValidEq.
-    eapply convSubstEqCtx1; cycle 2; tea; now eapply symValidEq.
+    1,2:  eapply convSubstCtx1; tea; now eapply symValidTyEq.
+    eapply convSubstEqCtx1; cycle 2; tea; now eapply symValidTyEq.
     Unshelve. all: tea.
 Qed.
 
@@ -148,7 +148,7 @@ Proof.
   constructor; intros; irrelevanceRefl.
   eapply validTyEq; tea.
   Unshelve. 1: tea. 
-  unshelve eapply convSubstCtx1; cycle 5; tea; now eapply symValidEq.
+  unshelve eapply convSubstCtx1; cycle 5; tea; now eapply symValidTyEq.
 Qed.
 
 Lemma convSubstCtx2 {Γ Δ A1 B1 A2 B2 l σ} 
@@ -288,8 +288,8 @@ Lemma convCtx2 {Γ A1 B1 A2 B2 P l}
   [_ ||-v<l> P | VΓB12].
 Proof.
   assert [_ ||-v<l> A2 | VΓB1] by now eapply convCtx1.
-  assert [_ ||-v<l> B1 ≅ A1 | _ | VB1] by now eapply symValidEq.
-  assert [_ ||-v<l> B2 ≅ A2 | _ | VB2'] by (eapply convEqCtx1; tea; now eapply symValidEq).
+  assert [_ ||-v<l> B1 ≅ A1 | _ | VB1] by now eapply symValidTyEq.
+  assert [_ ||-v<l> B2 ≅ A2 | _ | VB2'] by (eapply convEqCtx1; tea; now eapply symValidTyEq).
   opector; intros.
   - eapply validTy; tea; now eapply convSubstCtx2'.
   - irrelevanceRefl; unshelve eapply validTyExt.
@@ -315,7 +315,7 @@ Lemma convCtx2' {Γ A1 A2 B1 B2 P l}
   (VP : [_ ||-v<l> P | VΓA12]) :
   [_ ||-v<l> P | VΓB12].
 Proof.
-  eapply irrelevanceValidity; eapply convCtx2; irrValid.
+  eapply irrelevanceTy; eapply convCtx2; irrValid.
   Unshelve. all: tea; irrValid.
 Qed.
 

diff --git a/theories/Substitution/Introductions/Id.v b/theories/Substitution/Introductions/Id.v
@@ -547,7 +547,7 @@ Context `{GenericTypingProperties}.
       1: eapply reflValidTy.
       now eapply reflValidTm.
     }
-    eapply transValidEq.
+    eapply transValidTyEq.
     - eapply substExtIdElimMotive.
       2: tea. all: tea.
       Unshelve. eapply substIdElimMotive; cycle 1; tea.
@@ -655,7 +655,7 @@ Context `{GenericTypingProperties}.
     assert (VPalt' : [_ ||-v<l> P' | VΓext']).
     1:{
       eapply convCtx2'; tea.
-      1: eapply convCtx1; tea; [now eapply symValidEq| ].
+      1: eapply convCtx1; tea; [now eapply symValidTyEq| ].
       1,3: now eapply idElimMotiveCtxIdValid.
       eapply idElimMotiveCtxIdCongValid; tea.
       Unshelve. 1: now eapply idElimMotiveCtxIdValid. tea.
@@ -696,7 +696,7 @@ Context `{GenericTypingProperties}.
       6,7: tea.  5-8: tea. 2-4: tea. 1: tea.
       2: eapply conv.
       1,3: now eapply reflValid.
-      1: eapply symValidEq; now eapply IdCongValid.
+      1: eapply symValidTyEq; now eapply IdCongValid.
       now eapply reflCongValid.
       Unshelve. all: now eapply IdValid.
     + eapply LRTmRedConv; tea.
@@ -730,7 +730,7 @@ Context `{GenericTypingProperties}.
       1: now eapply reflValid.
       eapply reflCongValid; tea.
       eapply conv; tea.
-      now eapply symValidEq.
+      now eapply symValidTyEq.
       Unshelve. now eapply IdValid.
     }
     eapply redwfSubstValid; cycle 1.

diff --git a/theories/Substitution/Introductions/Nat.v b/theories/Substitution/Introductions/Nat.v
@@ -544,7 +544,7 @@ Lemma elimSuccHypTyCongValid {Γ l P P'}
     [Γ ||-v<l> elimSuccHypTy P ≅ elimSuccHypTy P' | VΓ | elimSuccHypTyValid VΓ VP].
   Proof.
     unfold elimSuccHypTy.
-    eapply irrelevanceEq.
+    eapply irrelevanceTyEq.
     assert [Γ,, tNat ||-v< l > P'[tSucc (tRel 0)]⇑ | validSnoc VΓ VN]. 1:{
       eapply substLiftS; tea.
       eapply irrelevanceTm.

diff --git a/theories/Substitution/Introductions/Pi.v b/theories/Substitution/Introductions/Pi.v
@@ -280,7 +280,7 @@ Section PiTmValidity.
       exact (PiRedU tΔ Vσ).
     - intros Δ σ σ' tΔ Vσ Vσ' Vσσ'.
       pose proof (univValid (l' := zero) _ _ VFU) as VF0.
-      pose proof (irrelevanceValidity (validSnoc VΓ VF)
+      pose proof (irrelevanceTy (validSnoc VΓ VF)
                     (validSnoc (l := zero) VΓ VF0)
                     (univValid (l' := zero) _ _ VGU)) as VG0.
       unshelve econstructor ; cbn.
@@ -322,10 +322,10 @@ Section PiTmCongruence.
     pose proof (Vuσ := liftSubstS' vF Vσ).
     pose proof (Vuσσ := liftSubstSEq' vF Vσσ).
     instAllValid Vσ Vσ Vσσ; instAllValid Vuσ Vuσ Vuσσ; escape.
-    pose proof (irrelevanceValidity (validSnoc vΓ vF)
+    pose proof (irrelevanceTy (validSnoc vΓ vF)
                   (validSnoc (l := zero) vΓ vF0)
                   (univValid (l' := zero) _ _ vGU)) as vG0.
-    pose proof (irrelevanceValidity (validSnoc vΓ vF')
+    pose proof (irrelevanceTy (validSnoc vΓ vF')
                   (validSnoc (l := zero) vΓ vF'0)
                   (univValid (l' := zero) _ _ vG'U)) as vG'0.
     unshelve econstructor ; cbn.
@@ -338,7 +338,7 @@ Section PiTmCongruence.
       refine (PiEqRed2 vΓ vF0 vG0 vF'0 vG'0 _ _ tΔ Vσ).
       + exact (univEqValid vΓ (UValid vΓ) vF0 vFF').
       + pose proof (univEqValid (validSnoc vΓ vF) vU (univValid (l' := zero) _ _ vGU) vGG') as vGG'0.
-        refine (irrelevanceEq _ _ _ _ vGG'0).
+        refine (irrelevanceTyEq _ _ _ _ vGG'0).
   Qed.
 
 End PiTmCongruence.

diff --git a/theories/Substitution/Introductions/Sigma.v b/theories/Substitution/Introductions/Sigma.v
@@ -185,7 +185,7 @@ Section SigTmValidity.
       exact (SigRedU tΔ Vσ).
     - intros Δ σ σ' tΔ Vσ Vσ' Vσσ'.
       pose proof (univValid (l' := zero) _ _ VFU) as VF0.
-      pose proof (irrelevanceValidity (validSnoc VΓ VF)
+      pose proof (irrelevanceTy (validSnoc VΓ VF)
                     (validSnoc (l := zero) VΓ VF0)
                     (univValid (l' := zero) _ _ VGU)) as VG0.
       unshelve econstructor ; cbn.
@@ -227,10 +227,10 @@ Section SigTmCongruence.
     pose proof (Vuσ := liftSubstS' VF Vσ).
     pose proof (Vuσσ := liftSubstSEq' VF Vσσ).
     instAllValid Vσ Vσ Vσσ; instAllValid Vuσ Vuσ Vuσσ; escape.
-    pose proof (irrelevanceValidity (validSnoc VΓ VF)
+    pose proof (irrelevanceTy (validSnoc VΓ VF)
                   (validSnoc (l := zero) VΓ VF0)
                   (univValid (l' := zero) _ _ VGU)) as VG0.
-    pose proof (irrelevanceValidity (validSnoc VΓ VF')
+    pose proof (irrelevanceTy (validSnoc VΓ VF')
                   (validSnoc (l := zero) VΓ VF'0)
                   (univValid (l' := zero) _ _ VG'U)) as VG'0.
     unshelve econstructor ; cbn.
@@ -243,7 +243,7 @@ Section SigTmCongruence.
       refine (SigCongRed VΓ VF0 VG0 VF'0 VG'0 _ _ tΔ Vσ).
       + exact (univEqValid VΓ (UValid VΓ) VF0 VFF').
       + pose proof (univEqValid (validSnoc VΓ VF) VU (univValid (l' := zero) _ _ VGU) VGG') as VGG'0.
-        refine (irrelevanceEq _ _ _ _ VGG'0).
+        refine (irrelevanceTyEq _ _ _ _ VGG'0).
   Qed.
 
 End SigTmCongruence.

diff --git a/theories/Substitution/Introductions/SimpleArr.v b/theories/Substitution/Introductions/SimpleArr.v
@@ -30,14 +30,14 @@ Section SimpleArrValidity.
     (VeqG : [Γ ||-v< l > G ≅ G' | VΓ | VG]) :
     [Γ ||-v<l> arr F G ≅ arr F' G' | VΓ | simpleArrValid _ VF VG].
   Proof.
-    eapply irrelevanceEq.
+    eapply irrelevanceTyEq.
     unshelve eapply PiCong; tea.
     + replace G⟨↑⟩ with G⟨@wk1 Γ F⟩ by now bsimpl.
       now eapply wk1ValidTy.
     + replace G'⟨↑⟩ with G'⟨@wk1 Γ F'⟩ by now bsimpl.
       now eapply wk1ValidTy.
     + replace G'⟨↑⟩ with G'⟨@wk1 Γ F⟩ by now bsimpl.
-      eapply irrelevanceEq'.
+      eapply irrelevanceTyEq'.
       2: now eapply wk1ValidTyEq.
       now bsimpl.
     Unshelve. 2: tea.