From d397c56a5d33034abc6f03d6d1da1709ae30fd65 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Tue, 26 Sep 2023 11:29:14 +0200 Subject: [PATCH] Uniformize some lemma names for validity. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We follow the scheme that lemmas about types (resp. type convertibility) end with Ty (resp. TyEq). - irrelevanceValidity → irrelevanceTy - irrelevanceEq → irrelevanceTyEq - symValidEq → symValidTyEq - transValidEq → transValidTyEq - wkValid → wkValidTy - wkEqValid → wkValidTyEq - wkTmValid → wkValidTm --- theories/Fundamental.v | 62 +++++++++---------- theories/Substitution/Conversion.v | 14 ++--- theories/Substitution/Introductions/Id.v | 8 +-- theories/Substitution/Introductions/Nat.v | 2 +- theories/Substitution/Introductions/Pi.v | 8 +-- theories/Substitution/Introductions/Sigma.v | 8 +-- .../Substitution/Introductions/SimpleArr.v | 4 +- theories/Substitution/Irrelevance.v | 20 +++--- theories/Substitution/Properties.v | 10 +-- theories/Substitution/SingleSubst.v | 2 +- 10 files changed, 69 insertions(+), 69 deletions(-) diff --git a/theories/Fundamental.v b/theories/Fundamental.v index cc8653ee..b344c079 100644 --- 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 index 07f5a2e8..20948219 100644 --- a/theories/Substitution/Conversion.v +++ b/theories/Substitution/Conversion.v @@ -125,11 +125,11 @@ Lemma convCtx1 {Γ A B P l} [_ ||-v 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 P | VΓB12]. Proof. assert [_ ||-v A2 | VΓB1] by now eapply convCtx1. - assert [_ ||-v B1 ≅ A1 | _ | VB1] by now eapply symValidEq. - assert [_ ||-v B2 ≅ A2 | _ | VB2'] by (eapply convEqCtx1; tea; now eapply symValidEq). + assert [_ ||-v B1 ≅ A1 | _ | VB1] by now eapply symValidTyEq. + assert [_ ||-v 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 P | VΓA12]) : [_ ||-v 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 index db61d0ec..1c173249 100644 --- 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 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 index d6fa627b..9b78283e 100644 --- a/theories/Substitution/Introductions/Nat.v +++ b/theories/Substitution/Introductions/Nat.v @@ -544,7 +544,7 @@ Lemma elimSuccHypTyCongValid {Γ l P P'} [Γ ||-v 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 index 2babc95f..db0bd22c 100644 --- 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 index 9a3643df..e34f8f71 100644 --- 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 index fc39971f..8240dee8 100644 --- 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 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. diff --git a/theories/Substitution/Irrelevance.v b/theories/Substitution/Irrelevance.v index a78a4cfc..55158376 100644 --- a/theories/Substitution/Irrelevance.v +++ b/theories/Substitution/Irrelevance.v @@ -92,7 +92,7 @@ Proof. now eapply validTail. Qed. -Lemma irrelevanceValidity {Γ} : forall (VΓ VΓ' : [||-v Γ]) {l A}, +Lemma irrelevanceTy {Γ} : forall (VΓ VΓ' : [||-v Γ]) {l A}, [Γ ||-v A | VΓ] -> [Γ ||-v A | VΓ']. Proof. intros VΓ VΓ' l A [VA VAext]; unshelve econstructor; intros. @@ -100,10 +100,10 @@ Proof. - eapply VAext; [eapply irrelevanceSubst| eapply irrelevanceSubstEq]; eassumption. Qed. -Lemma irrelevanceValidity' {Γ Γ' A A' l} (VΓ : [||-v Γ]) (VΓ' : [||-v Γ']) (VA : [Γ ||-v A | VΓ]) : +Lemma irrelevanceTy' {Γ Γ' A A' l} (VΓ : [||-v Γ]) (VΓ' : [||-v Γ']) (VA : [Γ ||-v A | VΓ]) : A = A' -> Γ = Γ' -> [Γ' ||-v A' | VΓ']. Proof. - intros eqA eqΓ; subst; now eapply irrelevanceValidity. + intros eqA eqΓ; subst; now eapply irrelevanceTy. Qed. Lemma irrelevanceLift {l A F G Γ} (VΓ : [||-v Γ]) @@ -126,7 +126,7 @@ Proof. eapply LRTyEqSym; unshelve eapply VFeqG; eassumption. Qed. -Lemma irrelevanceEq {Γ l A B} (VΓ VΓ' : [||-v Γ]) (VA : [Γ ||-v A | VΓ]) (VA' : [Γ||-v A | VΓ']) : +Lemma irrelevanceTyEq {Γ l A B} (VΓ VΓ' : [||-v Γ]) (VA : [Γ ||-v A | VΓ]) (VA' : [Γ||-v A | VΓ']) : [Γ ||-v< l > A ≅ B | VΓ | VA] -> [Γ ||-v< l > A ≅ B | VΓ' | VA']. Proof. intros [h]; constructor; intros. @@ -135,13 +135,13 @@ Proof. eapply irrelevanceSubst; eassumption. Qed. -Lemma irrelevanceEq' {Γ l A A' B} (VΓ VΓ' : [||-v Γ]) (VA : [Γ ||-v A | VΓ]) (VA' : [Γ||-v A' | VΓ']) : A = A' -> +Lemma irrelevanceTyEq' {Γ l A A' B} (VΓ VΓ' : [||-v Γ]) (VA : [Γ ||-v A | VΓ]) (VA' : [Γ||-v A' | VΓ']) : A = A' -> [Γ ||-v< l > A ≅ B | VΓ | VA] -> [Γ ||-v< l > A' ≅ B | VΓ' | VA']. Proof. - intros ->; now eapply irrelevanceEq. + intros ->; now eapply irrelevanceTyEq. Qed. -Lemma symValidEq {Γ l A B} {VΓ : [||-v Γ]} {VA : [Γ ||-v A | VΓ]} (VB : [Γ ||-v B | VΓ]) : +Lemma symValidTyEq {Γ l A B} {VΓ : [||-v Γ]} {VA : [Γ ||-v A | VΓ]} (VB : [Γ ||-v B | VΓ]) : [Γ ||-v A ≅ B | VΓ | VA] -> [Γ ||-v B ≅ A | VΓ | VB]. Proof. intros; constructor; intros. @@ -149,7 +149,7 @@ Proof. Unshelve. all: tea. Qed. -Lemma transValidEq {Γ l A B C} {VΓ : [||-v Γ]} +Lemma transValidTyEq {Γ l A B C} {VΓ : [||-v Γ]} {VA : [Γ ||-v A | VΓ]} {VB : [Γ ||-v B | VΓ]} : [Γ ||-v A ≅ B | VΓ | VA] -> [Γ ||-v B ≅ C | VΓ | VB] -> [Γ ||-v A ≅ C | VΓ | VA]. Proof. @@ -280,8 +280,8 @@ Ltac irrValid := | [_ : _ |- [||-v _]] => idtac | [_ : _ |- [ _ ||-v _ : _ | _ | _]] => eapply irrelevanceSubst | [_ : _ |- [ _ ||-v _ ≅ _ : _ | _ | _ | _]] => eapply irrelevanceSubstEq - | [_ : _ |- [_ ||-v<_> _ | _]] => eapply irrelevanceValidity - | [_ : _ |- [_ ||-v<_> _ ≅ _ | _ | _]] => eapply irrelevanceEq + | [_ : _ |- [_ ||-v<_> _ | _]] => eapply irrelevanceTy + | [_ : _ |- [_ ||-v<_> _ ≅ _ | _ | _]] => eapply irrelevanceTyEq | [_ : _ |- [_ ||-v<_> _ : _ | _ | _]] => eapply irrelevanceTm | [_ : _ |- [_ ||-v<_> _ ≅ _ : _ | _ | _]] => eapply irrelevanceTmEq end; eassumption. \ No newline at end of file diff --git a/theories/Substitution/Properties.v b/theories/Substitution/Properties.v index 2cefbf74..89ff10ab 100644 --- a/theories/Substitution/Properties.v +++ b/theories/Substitution/Properties.v @@ -417,7 +417,7 @@ Proof. eapply (validHead v). Qed. -Lemma wkValid {l Γ Δ A} (ρ : Δ ≤ Γ) +Lemma wkValidTy {l Γ Δ A} (ρ : Δ ≤ Γ) (VΓ : [||-v Γ]) (VΔ : [||-v Δ]) (VA : [Γ ||-v A | VΓ]) : @@ -435,12 +435,12 @@ Proof. Unshelve. 2,3: tea. Qed. -Lemma wkTmValid {l Γ Δ A t} (ρ : Δ ≤ Γ) +Lemma wkValidTm {l Γ Δ A t} (ρ : Δ ≤ Γ) (VΓ : [||-v Γ]) (VΔ : [||-v Δ]) (VA : [Γ ||-v A | VΓ]) (Vt : [Γ ||-v t : A | VΓ | VA]) : - [Δ ||-v t⟨ρ⟩ : A⟨ρ⟩ | VΔ | wkValid ρ VΓ VΔ VA]. + [Δ ||-v t⟨ρ⟩ : A⟨ρ⟩ | VΔ | wkValidTy ρ VΓ VΔ VA]. Proof. assert (hA : forall σ, A⟨ρ⟩[σ] = A[ρ >> σ]) by (intros; now asimpl). assert (ht : forall σ, t⟨ρ⟩[σ] = t[ρ >> σ]) by (intros; now asimpl). @@ -456,12 +456,12 @@ Proof. now eapply substS_wk. Qed. -Lemma wkEqValid {l Γ Δ A B} (ρ : Δ ≤ Γ) +Lemma wkValidTyEq {l Γ Δ A B} (ρ : Δ ≤ Γ) (VΓ : [||-v Γ]) (VΔ : [||-v Δ]) (VA : [Γ ||-v A | VΓ]) (VAB : [Γ ||-v A ≅ B | VΓ | VA]) : - [Δ ||-v A⟨ρ⟩ ≅ B⟨ρ⟩ | VΔ | wkValid ρ VΓ VΔ VA]. + [Δ ||-v A⟨ρ⟩ ≅ B⟨ρ⟩ | VΔ | wkValidTy ρ VΓ VΔ VA]. Proof. assert (h : forall A σ, A⟨ρ⟩[σ] = A[ ρ >> σ]) by (intros; now asimpl). unshelve econstructor; intros; irrelevance0; rewrite h; [reflexivity|]. diff --git a/theories/Substitution/SingleSubst.v b/theories/Substitution/SingleSubst.v index 858f6fb0..69cda664 100644 --- a/theories/Substitution/SingleSubst.v +++ b/theories/Substitution/SingleSubst.v @@ -194,7 +194,7 @@ Lemma substLiftSEq' {Γ F G G' t t' l} (VΓ : [||-v Γ]) (Vtt' : [Γ,, F ||-v t ≅ t' : F⟨@wk1 Γ F⟩ | VΓF | VF']) : [Γ ,, F ||-v G[t]⇑ ≅ G'[t']⇑ | VΓF | substLiftS _ VF VG Vt]. Proof. - eapply transValidEq. + eapply transValidTyEq. 1: eapply substLiftSEq; [| exact VGeq]; tea. constructor; intros; irrelevance0; rewrite liftSubstComm ; [reflexivity|]. instValid Vσ.