From bde73ef7b2528d2faae68ef0d3ed7496cdd15d8a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 27 Sep 2023 14:42:02 +0200 Subject: [PATCH] =?UTF-8?q?Split=20the=20declarative=20conversion=20rules?= =?UTF-8?q?=20for=20=CE=A3-types=20into=20congruence=20+=20=CE=B7.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- theories/BundledAlgorithmicTyping.v | 5 +- theories/DeclarativeInstance.v | 18 ++- theories/DeclarativeTyping.v | 16 +- theories/Fundamental.v | 168 ++++++++++++++++++-- theories/Substitution/Introductions/Sigma.v | 2 - 5 files changed, 185 insertions(+), 24 deletions(-) diff --git a/theories/BundledAlgorithmicTyping.v b/theories/BundledAlgorithmicTyping.v index d5a8093..8321353 100644 --- a/theories/BundledAlgorithmicTyping.v +++ b/theories/BundledAlgorithmicTyping.v @@ -691,7 +691,10 @@ Section BundledConv. pose proof hp as []%boundary%sig_ty_inv. edestruct ihsnd as []; tea. 1: now econstructor. - 2: split; [eauto|now econstructor]. + 2:{ split; [eauto|]. + eapply TermTrans; [|now constructor]. + eapply TermTrans; [eapply TermSym; now constructor|]. + constructor; tea; now apply TypeRefl. } eapply wfTermConv; [now econstructor|]. eapply typing_subst1; [now symmetry|]. now eapply TypeRefl. diff --git a/theories/DeclarativeInstance.v b/theories/DeclarativeInstance.v index 5e19279..668dca2 100644 --- a/theories/DeclarativeInstance.v +++ b/theories/DeclarativeInstance.v @@ -227,11 +227,16 @@ Section TypingWk. - intros * ????? ih ** ; do 2 rewrite <- wk_sig. constructor; eauto. eapply ih; constructor; tea; constructor; eauto. - - intros * ??? ihB **. rewrite <- wk_sig. + - intros * ? ihA₀ ? ihA ? ihA' ? ihB ? ihB' ? iha ? ihb Δ ρ **. + rewrite <- wk_sig, <- !wk_pair. + assert [|-[de] Δ,, A⟨ρ⟩] by now constructor. constructor; eauto. - 1: eapply ihB; constructor; eauto. - 1,2: rewrite wk_sig; eauto. - rewrite wk_fst, <- subst_ren_wk_up; eauto. + * now apply ihB. + * now apply ihB'. + * rewrite <- subst_ren_wk_up; now apply ihb. + - intros * ? ihp Δ ρ **. + rewrite <- wk_sig, <- wk_pair. + constructor; rewrite wk_sig; eauto. - intros * ? ih **. econstructor; now eapply ih. - intros * ??? ihB ** ; rewrite <- wk_fst; rewrite <- wk_pair; constructor; eauto. 1: eapply ihB; constructor; eauto. @@ -531,7 +536,10 @@ Module DeclarativeTypingProperties. - now do 2 econstructor. - now do 2 econstructor. - now econstructor. - - intros. econstructor; tea. + - intros. + eapply TermTrans; [|now constructor]. + eapply TermTrans; [eapply TermSym; now constructor|]. + constructor; tea; now apply TypeRefl. - now do 2 econstructor. - now econstructor. - now econstructor. diff --git a/theories/DeclarativeTyping.v b/theories/DeclarativeTyping.v index 1bb5091..a8f9309 100644 --- a/theories/DeclarativeTyping.v +++ b/theories/DeclarativeTyping.v @@ -217,14 +217,18 @@ Section Definitions. [ Γ |- A ≅ A' : U ] -> [ Γ ,, A |- B ≅ B' : U ] -> [ Γ |- tSig A B ≅ tSig A' B' : U ] - | TermPairEta {Γ} {A B p q} : + | TermPairCong {Γ A A' A'' B B' B'' a a' b b'} : [Γ |- A] -> - [Γ ,, A |- B] -> + [Γ |- A ≅ A'] -> + [Γ |- A ≅ A''] -> + [Γ,, A |- B ≅ B'] -> + [Γ,, A |- B ≅ B''] -> + [Γ |- a ≅ a' : A] -> + [Γ |- b ≅ b' : B[a..]] -> + [Γ |- tPair A' B' a b ≅ tPair A'' B'' a' b' : tSig A B] + | TermPairEta {Γ} {A B p} : [Γ |- p : tSig A B] -> - [Γ |- q : tSig A B] -> - [Γ |- tFst p ≅ tFst q : A] -> - [Γ |- tSnd p ≅ tSnd q : B[(tFst p)..]] -> - [Γ |- p ≅ q : tSig A B] + [Γ |- tPair A B (tFst p) (tSnd p) ≅ p : tSig A B] | TermFstCong {Γ A B p p'} : [Γ |- p ≅ p' : tSig A B] -> [Γ |- tFst p ≅ tFst p' : A] diff --git a/theories/Fundamental.v b/theories/Fundamental.v index b344c07..73719d1 100644 --- a/theories/Fundamental.v +++ b/theories/Fundamental.v @@ -768,20 +768,167 @@ Section Fundamental. Unshelve. all: solve [ eapply UValid | now eapply univValid | irrValid]. Qed. - Lemma FundTmEqSigEta : forall (Γ : context) (A B p q : term), + Lemma FundTmEqPairCong : forall (Γ : context) (A A' A'' B B' B'' a a' b b' : term), FundTy Γ A -> - FundTy (Γ,, A) B -> - FundTm Γ (tSig A B) p -> - FundTm Γ (tSig A B) q -> - FundTmEq Γ A (tFst p) (tFst q) -> - FundTmEq Γ B[(tFst p)..] (tSnd p) (tSnd q) -> FundTmEq Γ (tSig A B) p q. + FundTyEq Γ A A' -> + FundTyEq Γ A A'' -> + FundTyEq (Γ,, A) B B' -> + FundTyEq (Γ,, A) B B'' -> + FundTmEq Γ A a a' -> + FundTmEq Γ B[a..] b b' -> FundTmEq Γ (tSig A B) (tPair A' B' a b) (tPair A'' B'' a' b'). Proof. - intros * [] [] [] [] [] []; unshelve econstructor. - 5: eapply sigEtaValid; tea; irrValid. - all: irrValid. - Unshelve. all: irrValid. + intros * [VΓ VA] [] [] [] [] [] []. + assert (VΣ : [Γ ||-v< one > tSig A B | VΓ]). + { unshelve eapply SigValid; irrValid. } + assert (VA' : [Γ ||-v< one > A' | VΓ]) by irrValid. + assert (VA'' : [Γ ||-v< one > A'' | VΓ]) by irrValid. + assert ([Γ ||-v< one > a : A' | VΓ | VA']). + { eapply conv; [|irrValid]; irrValid. Unshelve. tea. } + assert ([Γ ||-v< one > a : A'' | VΓ | VA'']). + { eapply conv; [irrValid|]; irrValid. Unshelve. tea. } + assert ([Γ ||-v< one > a' : A'' | VΓ | VA'']). + { eapply conv; [irrValid|]; irrValid. Unshelve. tea. } + assert (VΓA' : VAdequate (ta := ta) (Γ,, A') VR) by now eapply validSnoc. + assert (VΓA'' : VAdequate (ta := ta) (Γ,, A'') VR) by now eapply validSnoc. + assert (VA'B : [Γ,, A' ||-v< one > B | VΓA']). + { eapply irrelevanceTy, irrelevanceLift; irrValid. + Unshelve. all: irrValid. } + assert (VA''B : [Γ,, A'' ||-v< one > B | VΓA'']). + { eapply irrelevanceTy, irrelevanceLift; irrValid. + Unshelve. all: irrValid. } + assert (VA'B' : [Γ,, A' ||-v< one > B' | VΓA']). + { eapply irrelevanceTy, irrelevanceLift; try irrValid. + Unshelve. all: irrValid. } + assert (VA''B' : [Γ,, A'' ||-v< one > B' | VΓA'']). + { eapply irrelevanceTy, irrelevanceLift; try irrValid. + Unshelve. all: irrValid. } + assert (VA''B'' : [Γ,, A'' ||-v< one > B'' | VΓA'']). + { eapply irrelevanceTy, irrelevanceLift; try irrValid. + Unshelve. all: irrValid. } + assert (VBa : [Γ ||-v< one > B[a..] | VΓ]). + { irrValid. } + assert (VB'a : [Γ ||-v< one > B'[a..] | VΓ]). + { eapply substS; irrValid. Unshelve. all: irrValid. } + assert (VB''a : [Γ ||-v< one > B''[a..] | VΓ]). + { eapply substS; irrValid. Unshelve. all: irrValid. } + assert (VB''a' : [Γ ||-v< one > B''[a'..] | VΓ]). + { eapply substS; irrValid. Unshelve. all: irrValid. } + assert [Γ ||-v< one > B[a..] ≅ B'[a..] | VΓ | VBa]. + { eapply irrelevanceTyEq, substSEq; try irrValid. + apply reflValidTm. irrValid. Unshelve. all: irrValid. } + assert [Γ ||-v< one > B[a..] ≅ B''[a'..] | VΓ | VBa]. + { eapply irrelevanceTyEq, substSEq; [..|irrValid|irrValid]. + all: irrValid. Unshelve. all: irrValid. } + assert (VΣA'B' : [Γ ||-v< one > tSig A' B' | VΓ]). + { unshelve eapply SigValid; try irrValid. } + assert (VΣA''B'' : [Γ ||-v< one > tSig A'' B'' | VΓ]). + { unshelve eapply SigValid; try irrValid. } + assert ([Γ ||-v< one > tSig A B ≅ tSig A' B' | VΓ | VΣ]). + { unshelve eapply irrelevanceTyEq, SigCong; try irrValid. } + assert ([Γ ||-v< one > tSig A B ≅ tSig A'' B'' | VΓ | VΣ]). + { unshelve eapply irrelevanceTyEq, SigCong; try irrValid. } + assert [Γ ||-v< one > tPair A' B' a b : tSig A B | _ | VΣ ]. + { eapply conv; [|unshelve eapply pairValid]; try irrValid. + - unshelve eapply symValidTyEq; irrValid. + - eapply conv; irrValid. Unshelve. all: irrValid. } + assert [Γ ||-v< one > tPair A'' B'' a' b' : tSig A B | _ | VΣ ]. + { eapply conv; [|unshelve eapply pairValid]; try irrValid. + - unshelve eapply symValidTyEq; irrValid. + - eapply conv; irrValid. + Unshelve. all: irrValid. } + assert [Γ ||-v< one > b : B'[a..] | VΓ | VB'a]. + { eapply conv; irrValid. Unshelve. all: irrValid. } + assert [Γ ||-v< one > b' : B''[a'..] | VΓ | VB''a']. + { eapply conv; irrValid. Unshelve. all: irrValid. } + assert ([Γ ||-v< one > tFst (tPair A' B' a b) ≅ a : A | VΓ | VA]). + { eapply (convEq (A := A')); [eapply symValidTyEq; irrValid|]. + eapply pairFstValid. Unshelve. all: try irrValid. } + assert ([Γ ||-v< one > tFst (tPair A'' B'' a' b') ≅ a' : A | VΓ | VA]). + { eapply (convEq (A := A'')); [eapply symValidTyEq; irrValid|]. + eapply pairFstValid. Unshelve. all: irrValid. } + assert ([Γ ||-v< one > tFst (tPair A' B' a b) ≅ tFst (tPair A'' B'' a' b') : A | VΓ | VA]). + { eapply transValidTmEq; [irrValid|]. + eapply transValidTmEq; [irrValid|]. + eapply symValidTmEq; irrValid. } + assert ([Γ ||-v< one > tFst (tPair A' B' a b) : A | VΓ | VA]). + { eapply fstValid. Unshelve. all: try irrValid. } + assert ([Γ ||-v< one > tFst (tPair A'' B'' a' b') : A | VΓ | VA]). + { eapply fstValid. Unshelve. all: try irrValid. } + assert (VBfst : [Γ ||-v< one > B[(tFst (tPair A' B' a b))..] | VΓ]). + { eapply (substS (F := A)). Unshelve. all: try irrValid. } + assert (VB'fst : [Γ ||-v< one > B'[(tFst (tPair A' B' a b))..] | VΓ]). + { eapply (substS (F := A)). Unshelve. all: try irrValid. } + assert (VB''fst' : [Γ ||-v< one > B''[(tFst (tPair A'' B'' a' b'))..] | VΓ]). + { eapply (substS (F := A)). Unshelve. all: try irrValid. } + assert ([Γ ||-v< one > B[(tFst (tPair A' B' a b))..] ≅ B[a..] | VΓ | VBfst]). + { eapply irrelevanceTyEq, substSEq; [..|irrValid|irrValid]. + Unshelve. all: try irrValid. eapply reflValidTy. } + assert ([Γ ||-v< one > B'[(tFst (tPair A' B' a b))..] ≅ B[a..] | VΓ | VB'fst]). + { eapply irrelevanceTyEq, substSEq; [..|irrValid|irrValid]. + Unshelve. all: try irrValid. + eapply symValidTyEq; irrValid. Unshelve. all: try irrValid. } + assert ([Γ ||-v< one > B''[(tFst (tPair A'' B'' a' b'))..] ≅ B[a'..] | VΓ | VB''fst']). + { eapply irrelevanceTyEq, substSEq; [..|irrValid|]. + Unshelve. all: try irrValid. + eapply symValidTyEq; irrValid. Unshelve. all: try irrValid. } + assert ([Γ ||-v< one > B''[(tFst (tPair A'' B'' a' b'))..] ≅ B[a..] | VΓ | VB''fst']). + { eapply irrelevanceTyEq, substSEq; [..|irrValid|]. + Unshelve. all: try irrValid. + eapply symValidTyEq; irrValid. Unshelve. all: try irrValid. + eapply transValidTmEq; [irrValid|]. + eapply symValidTmEq; irrValid. + } + assert ([Γ ||-v< one > tSnd (tPair A' B' a b) ≅ b : B[(tFst (tPair A' B' a b))..] | VΓ | VBfst]). + { eapply (convEq (A := B'[(tFst (tPair A' B' a b))..])). + shelve. eapply pairSndValid. + Unshelve. all: try irrValid. + eapply irrelevanceTyEq, substSEq; [..|irrValid|apply reflValidTm; irrValid]. + all: try irrValid. + - unshelve apply reflValidTy. + - unshelve eapply symValidTyEq; irrValid. } + assert ([Γ ||-v< one > tSnd (tPair A'' B'' a' b') ≅ b' : B[a..] | VΓ | VBa]). + { eapply (convEq (A := B''[(tFst (tPair A'' B'' a' b'))..])). + shelve. eapply pairSndValid. + Unshelve. all: try irrValid. } + unshelve econstructor. 1-4: irrValid. + eapply irrelevanceTmEq, sigEtaValid; try irrValid. + eapply transValidTmEq; [irrValid|]. + eapply transValidTmEq. + - eapply convEq; [|irrValid]. + eapply symValidTyEq; try irrValid. + - eapply symValidTmEq; try irrValid. + eapply convEq; [|irrValid]. + eapply symValidTyEq; try irrValid. + Unshelve. all: try irrValid. Qed. + Lemma FundTmEqSigEta : forall (Γ : context) (A B p : term), + FundTm Γ (tSig A B) p -> FundTmEq Γ (tSig A B) (tPair A B (tFst p) (tSnd p)) p. + Proof. + intros * [VΓ VΣ Vp]. + assert (VA := domSigValid _ VΣ). + assert (VB := codSigValid _ VΣ). + assert (Vfst : [Γ ||-v< one > tFst p : A | _ | VA]). + { unshelve eapply irrelevanceTm, fstValid; try irrValid. } + assert (VBfst : [Γ ||-v< one > B[(tFst p)..] | VΓ]). + { unshelve eapply substS; try irrValid. } + assert (Vsnd : [Γ ||-v< one > tSnd p : B[(tFst p)..] | _ | VBfst]). + { unshelve eapply irrelevanceTm, sndValid. + 5: irrValid. all: irrValid. } + assert (Vηp : [Γ ||-v< one > tPair A B (tFst p) (tSnd p) : tSig A B | VΓ | VΣ]). + { unshelve eapply irrelevanceTm, pairValid; try irrValid. } + unshelve econstructor; try irrValid. + eapply irrelevanceTmEq, sigEtaValid; try irrValid. + - eapply transValidTmEq; [eapply pairFstValid|eapply reflValidTm]. + Unshelve. all: try irrValid. + - eapply transValidTmEq; [unshelve eapply irrelevanceTmEq, pairSndValid|unshelve eapply reflValidTm]; try irrValid. + unshelve eapply conv; try irrValid. + eapply irrelevanceTyEq, substSEq; try irrValid. + 1,2: unshelve apply reflValidTy. + { unshelve eapply fstValid; try irrValid. } + { unshelve eapply symValidTmEq, pairFstValid; try irrValid. } + Unshelve. all: try irrValid. + Qed. Lemma FundTmEqFstCong : forall (Γ : context) (A B p p' : term), FundTmEq Γ (tSig A B) p p' -> FundTmEq Γ A (tFst p) (tFst p'). @@ -1055,6 +1202,7 @@ Lemma Fundamental : (forall Γ : context, [ |-[ de ] Γ ] -> FundCon (ta := ta) + intros; now apply FundTmEqNatElimSucc. + intros; now apply FundTmEqEmptyElimCong. + intros; now apply FundTmEqSigCong. + + intros; now apply FundTmEqPairCong. + intros; now apply FundTmEqSigEta. + intros; now eapply FundTmEqFstCong. + intros; now apply FundTmEqFstBeta. diff --git a/theories/Substitution/Introductions/Sigma.v b/theories/Substitution/Introductions/Sigma.v index b974ca1..cf5c624 100644 --- a/theories/Substitution/Introductions/Sigma.v +++ b/theories/Substitution/Introductions/Sigma.v @@ -977,8 +977,6 @@ Section PairRed. + irrelevance0. 1: now rewrite <- subst_fst, <- singleSubstComm'. tea. Qed. - - End PairRed.