From 1033a2b3c3f136efcf850f8235bc385b72585e1e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Tue, 28 Jan 2025 21:26:19 +0100 Subject: [PATCH 1/4] Move proofs of reducibility to theories/LogicalRelation/Introductions. This parallels the organization of the Validity folder. --- _CoqProject | 10 +++++----- .../LogicalRelation/{ => Introductions}/Application.v | 0 theories/LogicalRelation/{ => Introductions}/Id.v | 0 .../LogicalRelation/{ => Introductions}/SimpleArr.v | 0 .../LogicalRelation/{ => Introductions}/Universe.v | 0 5 files changed, 5 insertions(+), 5 deletions(-) rename theories/LogicalRelation/{ => Introductions}/Application.v (100%) rename theories/LogicalRelation/{ => Introductions}/Id.v (100%) rename theories/LogicalRelation/{ => Introductions}/SimpleArr.v (100%) rename theories/LogicalRelation/{ => Introductions}/Universe.v (100%) diff --git a/_CoqProject b/_CoqProject index c4c2f315..db53d184 100644 --- a/_CoqProject +++ b/_CoqProject @@ -37,16 +37,16 @@ theories/LogicalRelation/ShapeView.v theories/LogicalRelation/Reflexivity.v theories/LogicalRelation/Irrelevance.v theories/LogicalRelation/Weakening.v -theories/LogicalRelation/Universe.v theories/LogicalRelation/Neutral.v theories/LogicalRelation/Transitivity.v theories/LogicalRelation/InstKripke.v theories/LogicalRelation/EqRedRight.v theories/LogicalRelation/Reduction.v theories/LogicalRelation/NormalRed.v -theories/LogicalRelation/Application.v -theories/LogicalRelation/SimpleArr.v -theories/LogicalRelation/Id.v +theories/LogicalRelation/Introductions/Universe.v +theories/LogicalRelation/Introductions/Application.v +theories/LogicalRelation/Introductions/SimpleArr.v +theories/LogicalRelation/Introductions/Id.v theories/Validity/Validity.v theories/Validity/Irrelevance.v @@ -85,4 +85,4 @@ theories/Decidability/UntypedSoundness.v theories/Decidability/UntypedCompleteness.v theories/Decidability.v -theories/Decidability/Execution.v \ No newline at end of file +theories/Decidability/Execution.v diff --git a/theories/LogicalRelation/Application.v b/theories/LogicalRelation/Introductions/Application.v similarity index 100% rename from theories/LogicalRelation/Application.v rename to theories/LogicalRelation/Introductions/Application.v diff --git a/theories/LogicalRelation/Id.v b/theories/LogicalRelation/Introductions/Id.v similarity index 100% rename from theories/LogicalRelation/Id.v rename to theories/LogicalRelation/Introductions/Id.v diff --git a/theories/LogicalRelation/SimpleArr.v b/theories/LogicalRelation/Introductions/SimpleArr.v similarity index 100% rename from theories/LogicalRelation/SimpleArr.v rename to theories/LogicalRelation/Introductions/SimpleArr.v diff --git a/theories/LogicalRelation/Universe.v b/theories/LogicalRelation/Introductions/Universe.v similarity index 100% rename from theories/LogicalRelation/Universe.v rename to theories/LogicalRelation/Introductions/Universe.v From 9450c7e34b5fda87d219bd9c1335a357949b0790 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Tue, 28 Jan 2025 21:39:52 +0100 Subject: [PATCH 2/4] Remove a spurious dependency in InstKripke. This ensures a clean delineation of dependencies in LogicalRelation.Introductions. --- theories/LogicalRelation/InstKripke.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/LogicalRelation/InstKripke.v b/theories/LogicalRelation/InstKripke.v index ede13be9..ade78f56 100644 --- a/theories/LogicalRelation/InstKripke.v +++ b/theories/LogicalRelation/InstKripke.v @@ -1,7 +1,7 @@ (** * LogRel.LogicalRelation.InstKripke: combinators to instantiate Kripke-style quantifications *) From Coq Require Import CRelationClasses. From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation. -From LogRel.LogicalRelation Require Import Induction Escape Reflexivity Neutral Weakening Irrelevance Application Reduction Transitivity NormalRed EqRedRight. +From LogRel.LogicalRelation Require Import Induction Escape Reflexivity Neutral Weakening Irrelevance Reduction Transitivity NormalRed EqRedRight. Set Universe Polymorphism. Set Printing Primitive Projection Parameters. From 38e9b620f1f0ba9024a9d218bfddbb74f36e9b6a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Tue, 28 Jan 2025 21:44:50 +0100 Subject: [PATCH 3/4] Split some reducibility-only parts of Validity into LogicalRelation. This effectively moves the reducibility-only parts of Poly and Pi from Validity to LogicalRelation. --- _CoqProject | 2 + theories/LogicalRelation/Introductions/Pi.v | 47 ++++++ theories/LogicalRelation/Introductions/Poly.v | 134 ++++++++++++++++++ .../TypingProperties/LogRelConsequences.v | 1 + theories/Validity/Introductions/Pi.v | 44 +----- theories/Validity/Introductions/Poly.v | 122 +--------------- theories/Validity/Introductions/Sigma.v | 1 + 7 files changed, 187 insertions(+), 164 deletions(-) create mode 100644 theories/LogicalRelation/Introductions/Pi.v create mode 100644 theories/LogicalRelation/Introductions/Poly.v diff --git a/_CoqProject b/_CoqProject index db53d184..8a1b4d9a 100644 --- a/_CoqProject +++ b/_CoqProject @@ -44,6 +44,8 @@ theories/LogicalRelation/EqRedRight.v theories/LogicalRelation/Reduction.v theories/LogicalRelation/NormalRed.v theories/LogicalRelation/Introductions/Universe.v +theories/LogicalRelation/Introductions/Poly.v +theories/LogicalRelation/Introductions/Pi.v theories/LogicalRelation/Introductions/Application.v theories/LogicalRelation/Introductions/SimpleArr.v theories/LogicalRelation/Introductions/Id.v diff --git a/theories/LogicalRelation/Introductions/Pi.v b/theories/LogicalRelation/Introductions/Pi.v new file mode 100644 index 00000000..6a86be81 --- /dev/null +++ b/theories/LogicalRelation/Introductions/Pi.v @@ -0,0 +1,47 @@ +From Coq Require Import ssrbool. +From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation. +From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Induction NormalRed EqRedRight. +From LogRel.LogicalRelation.Introductions Require Import Poly. + +Set Universe Polymorphism. + +Section PolyRedPi. + Context `{GenericTypingProperties}. + + Lemma LRPiPoly0 {Γ l A B} (PAB : PolyRed Γ l A B) : [Γ ||-Π tProd A B]. + Proof. + econstructor; tea; pose proof (polyRedId PAB) as []; escape. + + eapply redtywf_refl; gen_typing. + + unshelve eapply escapeEq; tea; eapply reflLRTyEq. + + eapply convty_prod; tea; unshelve eapply escapeEq; tea; eapply reflLRTyEq. + Defined. + + Definition LRPiPoly {Γ l A B} (PAB : PolyRed Γ l A B) : [Γ ||- tProd A B] := LRPi' (LRPiPoly0 PAB). + + Lemma LRPiPolyEq0 {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') : + [Γ |- A'] -> [Γ ,, A' |- B'] -> + [Γ ||-Π tProd A B ≅ tProd A' B' | LRPiPoly0 PAB]. + Proof. + econstructor; cbn; tea. + + eapply redtywf_refl; gen_typing. + + pose proof (polyRedEqId PAB Peq) as []; now escape. + + pose proof (polyRedEqId PAB Peq) as []; escape. + eapply convty_prod; tea. + eapply escape; now apply (polyRedId PAB). + Qed. + + Lemma LRPiPolyEq {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') : + [Γ |- A'] -> [Γ ,, A' |- B'] -> + [Γ ||- tProd A B ≅ tProd A' B' | LRPiPoly PAB]. + Proof. + now eapply LRPiPolyEq0. + Qed. + + Lemma LRPiPolyEq' {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') (RAB : [Γ ||- tProd A B]): + [Γ |- A'] -> [Γ ,, A' |- B'] -> + [Γ ||- tProd A B ≅ tProd A' B' | RAB]. + Proof. + intros; irrelevanceRefl; now eapply LRPiPolyEq. + Qed. + +End PolyRedPi. diff --git a/theories/LogicalRelation/Introductions/Poly.v b/theories/LogicalRelation/Introductions/Poly.v new file mode 100644 index 00000000..5848ffcc --- /dev/null +++ b/theories/LogicalRelation/Introductions/Poly.v @@ -0,0 +1,134 @@ +From Coq Require Import ssrbool. +From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation. +From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Transitivity EqRedRight InstKripke. + +Set Universe Polymorphism. + +Lemma subst_wk_id_tail Γ P t : P[t .: @wk_id Γ >> tRel] = P[t..]. +Proof. setoid_rewrite id_ren; now bsimpl. Qed. + +Set Printing Primitive Projection Parameters. + +Section PolyValidity. + + Context `{GenericTypingProperties}. + + Lemma mkPolyRed {Γ l A B} (wfΓ : [|-Γ]) + (RA : forall Δ (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||- A⟨ρ⟩]) + (RB : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||- a ≅ b : _ | RA Δ ρ wfΔ] -> [Δ ||- B[a .: ρ >> tRel]]) + (RBext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) (Rab : [Δ ||- a ≅ b : _ | RA Δ ρ wfΔ]), + [Δ ||- B[a .: ρ >> tRel] ≅ B[b .: ρ >> tRel] | RB Δ a b ρ wfΔ Rab]) : + PolyRed Γ l A B. + Proof. + assert [Γ |- A] by (eapply escape; now eapply instKripke). + unshelve econstructor; tea. + unshelve epose proof (h := RB _ (tRel 0) (tRel 0) (@wk1 Γ A) _ _). + + gen_typing. + + eapply var0; tea; now rewrite wk1_ren_on. + + escape. now rewrite <- eq_id_subst_scons in Esch. + Qed. + + Lemma mkPolyRed' {Γ l A B} (RA : [Γ ||- A]) + (RB : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||- a ≅ b : _ | wk ρ wfΔ RA] -> [Δ ||- B[a .: ρ >> tRel]]) + (RBext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) (Rab : [Δ ||- a ≅ b : _ | wk ρ wfΔ RA]), + [Δ ||- B[a .: ρ >> tRel] ≅ B[b .: ρ >> tRel] | RB Δ a b ρ wfΔ Rab]) : + PolyRed Γ l A B. + Proof. + unshelve eapply mkPolyRed; tea. + escape; gen_typing. + Qed. + + + Lemma polyCodSubstRed {Γ l F G} (RF : [Γ ||- F]) : + PolyRed Γ l F G -> forall t u, [Γ ||- t ≅ u : _ | RF] -> [Γ ||- G[t..]]. + Proof. + intros PFG ???. + assert (wfΓ : [|- Γ]) by (escape ; gen_typing). + erewrite <- subst_wk_id_tail. + eapply (PolyRed.posRed PFG wk_id wfΓ ). + irrelevance. + Qed. + + Lemma polyCodSubstExtRed {Γ l F G} (RF : [Γ ||- F]) (PFG : PolyRed Γ l F G) (RG := polyCodSubstRed RF PFG) : + forall t u (Rt : [Γ ||- t ≅ u : _ | RF]), + [Γ ||- G[t..] ≅ G[u..]| RG t u Rt]. + Proof. + intros. assert (wfΓ : [|- Γ]) by (escape; gen_typing). + irrelevance0; erewrite <- subst_wk_id_tail; [reflexivity|]. + unshelve eapply (PolyRed.posExt PFG wk_id wfΓ); irrelevance. + Qed. + + Lemma polyRedId {Γ l F G} : PolyRed Γ l F G -> [Γ ||- F] × [Γ ,, F ||- G]. + Proof. + intros PFG; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing). + split; [exact (instKripke wfΓ (PolyRed.shpRed PFG))| exact (instKripkeSubst wfΓ (PolyRed.posRed PFG))]. + Qed. + + Lemma polyRedEqId {Γ l F F' G G'} (PFG : PolyRed Γ l F G) (RFG := polyRedId PFG) : + PolyRedEq PFG F' G' -> [Γ ||- F ≅ F' | fst RFG] × [Γ ,, F ||- G ≅ G' | snd RFG]. + Proof. + intros PFGeq; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing). + split. + - pose (instKripkeEq wfΓ (PolyRedEq.shpRed PFGeq)); irrelevance. + - unshelve epose proof (instKripkeSubstEq wfΓ _). + 7: intros; eapply LRTransEq; [|unshelve eapply (PolyRedEq.posRed PFGeq _ _ (urefl hab))]; + try (unshelve eapply (PolyRed.posExt PFG); tea). + irrelevance. + Qed. + + Lemma polyRedEqCodSubstExt {Γ l F F' G G'} (RF : [Γ ||- F]) (PFG : PolyRed Γ l F G) (RG := polyCodSubstRed RF PFG) : + PolyRedEq PFG F' G' -> + forall t u (Rt : [Γ ||- t ≅ u : _ | RF]), + [Γ ||- G[t..] ≅ G'[u..]| RG t u Rt]. + Proof. + intros Peq *; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing). + unshelve epose proof (h := posRedExt Peq wk_id wfΓ _). + 3: irrelevance. + rewrite subst_wk_id_tail in h; irrelevance. + Qed. + + Lemma polyRedSubst {Γ l A B t} (PAB : PolyRed Γ l A B) + (Rt : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]), + [Δ ||- a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] -> + [Δ ||- t[a .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ]) + (Rtext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]), + [Δ ||- a : _ | PolyRed.shpRed PAB ρ wfΔ] -> + [Δ ||- b : _ | PolyRed.shpRed PAB ρ wfΔ] -> + [Δ ||- a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] -> + [Δ ||- t[a .: ρ >> tRel] ≅ t[b .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ]) + : PolyRed Γ l A B[t]⇑. + Proof. + destruct PAB; opector; tea. + + intros; rewrite liftSubst_scons_eq. + unshelve eapply posRed; [..| eapply Rt]; tea ; now irrelevanceRefl. + + unshelve epose proof (posRed _ t t (@wk1 Γ A) _ _). + - escape; gen_typing. + - replace t with t[tRel 0 .: @wk1 Γ A >> tRel]. + 2:{ bsimpl; rewrite scons_eta'; now asimpl. } + eapply Rt. + eapply var0; tea; now rewrite wk1_ren_on. + - escape. + replace (B[_]) with B[t .: @wk1 Γ A >> tRel]; tea. + now setoid_rewrite wk1_ren. + + intros; irrelevance0; rewrite liftSubst_scons_eq;[reflexivity|]. + unshelve eapply posExt; tea; eapply Rt + eapply Rtext; cbn; irrelevanceRefl. + 1: now eapply lrefl. + 1: now eapply urefl. + eassumption. + Qed. + + Lemma polyRedEqSubst {Γ l A B t u} (PAB : PolyRed Γ l A B) + (Rtu : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]), + [Δ ||- a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] -> + [Δ ||- t[a .: ρ >> tRel] ≅ u[b .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ]) + (PABt : PolyRed Γ l A B[t]⇑) + : PolyRedEq PABt A B[u]⇑. + Proof. + constructor. + - intros; eapply reflLRTyEq. + - intros; irrelevance0; rewrite liftSubst_scons_eq; [reflexivity|]. + unshelve eapply PolyRed.posExt; cycle 1; tea. + eapply Rtu; irrelevanceRefl; now eapply lrefl. + Qed. + +End PolyValidity. diff --git a/theories/TypingProperties/LogRelConsequences.v b/theories/TypingProperties/LogRelConsequences.v index e6df5606..2392c412 100644 --- a/theories/TypingProperties/LogRelConsequences.v +++ b/theories/TypingProperties/LogRelConsequences.v @@ -4,6 +4,7 @@ From LogRel.TypingProperties Require Import PropertiesDefinition DeclarativeProp From LogRel Require Import LogicalRelation Fundamental. From LogRel.LogicalRelation Require Import Escape Irrelevance Transitivity Neutral Induction NormalRed. +From LogRel.LogicalRelation.Introductions Require Import Poly. From LogRel.Validity Require Import Validity Escape Poly Irrelevance. (** ** Stability of typing under substitution *) diff --git a/theories/Validity/Introductions/Pi.v b/theories/Validity/Introductions/Pi.v index 206e3a12..94dc0b6b 100644 --- a/theories/Validity/Introductions/Pi.v +++ b/theories/Validity/Introductions/Pi.v @@ -1,53 +1,11 @@ From Coq Require Import ssrbool. From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation. From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Induction NormalRed EqRedRight. +From LogRel.LogicalRelation.Introductions Require Import Poly Pi. From LogRel.Validity Require Import Validity Irrelevance Properties SingleSubst Reflexivity Universe Poly. Set Universe Polymorphism. - -Section PolyRedPi. - Context `{GenericTypingProperties}. - - Lemma LRPiPoly0 {Γ l A B} (PAB : PolyRed Γ l A B) : [Γ ||-Π tProd A B]. - Proof. - econstructor; tea; pose proof (polyRedId PAB) as []; escape. - + eapply redtywf_refl; gen_typing. - + unshelve eapply escapeEq; tea; eapply reflLRTyEq. - + eapply convty_prod; tea; unshelve eapply escapeEq; tea; eapply reflLRTyEq. - Defined. - - Definition LRPiPoly {Γ l A B} (PAB : PolyRed Γ l A B) : [Γ ||- tProd A B] := LRPi' (LRPiPoly0 PAB). - - Lemma LRPiPolyEq0 {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') : - [Γ |- A'] -> [Γ ,, A' |- B'] -> - [Γ ||-Π tProd A B ≅ tProd A' B' | LRPiPoly0 PAB]. - Proof. - econstructor; cbn; tea. - + eapply redtywf_refl; gen_typing. - + pose proof (polyRedEqId PAB Peq) as []; now escape. - + pose proof (polyRedEqId PAB Peq) as []; escape. - eapply convty_prod; tea. - eapply escape; now apply (polyRedId PAB). - Qed. - - Lemma LRPiPolyEq {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') : - [Γ |- A'] -> [Γ ,, A' |- B'] -> - [Γ ||- tProd A B ≅ tProd A' B' | LRPiPoly PAB]. - Proof. - now eapply LRPiPolyEq0. - Qed. - - Lemma LRPiPolyEq' {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') (RAB : [Γ ||- tProd A B]): - [Γ |- A'] -> [Γ ,, A' |- B'] -> - [Γ ||- tProd A B ≅ tProd A' B' | RAB]. - Proof. - intros; irrelevanceRefl; now eapply LRPiPolyEq. - Qed. - -End PolyRedPi. - - Section PiTyValidity. Context `{GenericTypingProperties}. diff --git a/theories/Validity/Introductions/Poly.v b/theories/Validity/Introductions/Poly.v index f32b33d1..f9e71e73 100644 --- a/theories/Validity/Introductions/Poly.v +++ b/theories/Validity/Introductions/Poly.v @@ -1,6 +1,7 @@ From Coq Require Import ssrbool. From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation. From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Transitivity EqRedRight InstKripke. +From LogRel.LogicalRelation.Introductions Require Import Poly. From LogRel.Validity Require Import Validity Irrelevance Properties Reflexivity Universe. Set Universe Polymorphism. @@ -15,133 +16,12 @@ Proof. bsimpl ; now substify. Qed. -Lemma subst_wk_id_tail Γ P t : P[t .: @wk_id Γ >> tRel] = P[t..]. -Proof. setoid_rewrite id_ren; now bsimpl. Qed. - Set Printing Primitive Projection Parameters. Section PolyValidity. Context `{GenericTypingProperties}. - Lemma mkPolyRed {Γ l A B} (wfΓ : [|-Γ]) - (RA : forall Δ (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||- A⟨ρ⟩]) - (RB : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||- a ≅ b : _ | RA Δ ρ wfΔ] -> [Δ ||- B[a .: ρ >> tRel]]) - (RBext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) (Rab : [Δ ||- a ≅ b : _ | RA Δ ρ wfΔ]), - [Δ ||- B[a .: ρ >> tRel] ≅ B[b .: ρ >> tRel] | RB Δ a b ρ wfΔ Rab]) : - PolyRed Γ l A B. - Proof. - assert [Γ |- A] by (eapply escape; now eapply instKripke). - unshelve econstructor; tea. - unshelve epose proof (h := RB _ (tRel 0) (tRel 0) (@wk1 Γ A) _ _). - + gen_typing. - + eapply var0; tea; now rewrite wk1_ren_on. - + escape. now rewrite <- eq_id_subst_scons in Esch. - Qed. - - Lemma mkPolyRed' {Γ l A B} (RA : [Γ ||- A]) - (RB : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||- a ≅ b : _ | wk ρ wfΔ RA] -> [Δ ||- B[a .: ρ >> tRel]]) - (RBext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) (Rab : [Δ ||- a ≅ b : _ | wk ρ wfΔ RA]), - [Δ ||- B[a .: ρ >> tRel] ≅ B[b .: ρ >> tRel] | RB Δ a b ρ wfΔ Rab]) : - PolyRed Γ l A B. - Proof. - unshelve eapply mkPolyRed; tea. - escape; gen_typing. - Qed. - - - Lemma polyCodSubstRed {Γ l F G} (RF : [Γ ||- F]) : - PolyRed Γ l F G -> forall t u, [Γ ||- t ≅ u : _ | RF] -> [Γ ||- G[t..]]. - Proof. - intros PFG ???. - assert (wfΓ : [|- Γ]) by (escape ; gen_typing). - erewrite <- subst_wk_id_tail. - eapply (PolyRed.posRed PFG wk_id wfΓ ). - irrelevance. - Qed. - - Lemma polyCodSubstExtRed {Γ l F G} (RF : [Γ ||- F]) (PFG : PolyRed Γ l F G) (RG := polyCodSubstRed RF PFG) : - forall t u (Rt : [Γ ||- t ≅ u : _ | RF]), - [Γ ||- G[t..] ≅ G[u..]| RG t u Rt]. - Proof. - intros. assert (wfΓ : [|- Γ]) by (escape; gen_typing). - irrelevance0; erewrite <- subst_wk_id_tail; [reflexivity|]. - unshelve eapply (PolyRed.posExt PFG wk_id wfΓ); irrelevance. - Qed. - - Lemma polyRedId {Γ l F G} : PolyRed Γ l F G -> [Γ ||- F] × [Γ ,, F ||- G]. - Proof. - intros PFG; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing). - split; [exact (instKripke wfΓ (PolyRed.shpRed PFG))| exact (instKripkeSubst wfΓ (PolyRed.posRed PFG))]. - Qed. - - Lemma polyRedEqId {Γ l F F' G G'} (PFG : PolyRed Γ l F G) (RFG := polyRedId PFG) : - PolyRedEq PFG F' G' -> [Γ ||- F ≅ F' | fst RFG] × [Γ ,, F ||- G ≅ G' | snd RFG]. - Proof. - intros PFGeq; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing). - split. - - pose (instKripkeEq wfΓ (PolyRedEq.shpRed PFGeq)); irrelevance. - - unshelve epose proof (instKripkeSubstEq wfΓ _). - 7: intros; eapply LRTransEq; [|unshelve eapply (PolyRedEq.posRed PFGeq _ _ (urefl hab))]; - try (unshelve eapply (PolyRed.posExt PFG); tea). - irrelevance. - Qed. - - Lemma polyRedEqCodSubstExt {Γ l F F' G G'} (RF : [Γ ||- F]) (PFG : PolyRed Γ l F G) (RG := polyCodSubstRed RF PFG) : - PolyRedEq PFG F' G' -> - forall t u (Rt : [Γ ||- t ≅ u : _ | RF]), - [Γ ||- G[t..] ≅ G'[u..]| RG t u Rt]. - Proof. - intros Peq *; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing). - unshelve epose proof (h := posRedExt Peq wk_id wfΓ _). - 3: irrelevance. - rewrite subst_wk_id_tail in h; irrelevance. - Qed. - - Lemma polyRedSubst {Γ l A B t} (PAB : PolyRed Γ l A B) - (Rt : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]), - [Δ ||- a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] -> - [Δ ||- t[a .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ]) - (Rtext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]), - [Δ ||- a : _ | PolyRed.shpRed PAB ρ wfΔ] -> - [Δ ||- b : _ | PolyRed.shpRed PAB ρ wfΔ] -> - [Δ ||- a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] -> - [Δ ||- t[a .: ρ >> tRel] ≅ t[b .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ]) - : PolyRed Γ l A B[t]⇑. - Proof. - destruct PAB; opector; tea. - + intros; rewrite liftSubst_scons_eq. - unshelve eapply posRed; [..| eapply Rt]; tea ; now irrelevanceRefl. - + unshelve epose proof (posRed _ t t (@wk1 Γ A) _ _). - - escape; gen_typing. - - replace t with t[tRel 0 .: @wk1 Γ A >> tRel]. - 2:{ bsimpl; rewrite scons_eta'; now asimpl. } - eapply Rt. - eapply var0; tea; now rewrite wk1_ren_on. - - escape. - replace (B[_]) with B[t .: @wk1 Γ A >> tRel]; tea. - now setoid_rewrite wk1_ren. - + intros; irrelevance0; rewrite liftSubst_scons_eq;[reflexivity|]. - unshelve eapply posExt; tea; eapply Rt + eapply Rtext; cbn; irrelevanceRefl. - 1: now eapply lrefl. - 1: now eapply urefl. - eassumption. - Qed. - - Lemma polyRedEqSubst {Γ l A B t u} (PAB : PolyRed Γ l A B) - (Rtu : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]), - [Δ ||- a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] -> - [Δ ||- t[a .: ρ >> tRel] ≅ u[b .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ]) - (PABt : PolyRed Γ l A B[t]⇑) - : PolyRedEq PABt A B[u]⇑. - Proof. - constructor. - - intros; eapply reflLRTyEq. - - intros; irrelevance0; rewrite liftSubst_scons_eq; [reflexivity|]. - unshelve eapply PolyRed.posExt; cycle 1; tea. - eapply Rtu; irrelevanceRefl; now eapply lrefl. - Qed. - Context {l Γ F G} (VΓ : [||-v Γ]) (VF : [Γ ||-v< l > F | VΓ ]) (VG : [Γ ,, F ||-v< l > G | validSnoc VΓ VF]). diff --git a/theories/Validity/Introductions/Sigma.v b/theories/Validity/Introductions/Sigma.v index e860c78d..475da557 100644 --- a/theories/Validity/Introductions/Sigma.v +++ b/theories/Validity/Introductions/Sigma.v @@ -1,6 +1,7 @@ From Coq Require Import ssrbool CRelationClasses. From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation. From LogRel.LogicalRelation Require Import Induction Escape Reflexivity Irrelevance Weakening Neutral Transitivity Reduction Application Universe EqRedRight SimpleArr NormalRed InstKripke. +From LogRel.LogicalRelation.Introductions Require Import Poly. From LogRel.Validity Require Import Validity Irrelevance Properties Conversion SingleSubst Reflexivity Reduction Universe Poly. From e52df5256d20c6f335051f080be8a98306ff9624 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Tue, 28 Jan 2025 22:05:23 +0100 Subject: [PATCH 4/4] Factorize poly-related proofs in LogicalRelations. --- theories/LogicalRelation/Introductions/SimpleArr.v | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/theories/LogicalRelation/Introductions/SimpleArr.v b/theories/LogicalRelation/Introductions/SimpleArr.v index 0e1a7853..c784570b 100644 --- a/theories/LogicalRelation/Introductions/SimpleArr.v +++ b/theories/LogicalRelation/Introductions/SimpleArr.v @@ -1,5 +1,6 @@ From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation. From LogRel.LogicalRelation Require Import Induction Irrelevance Weakening Neutral Escape Reflexivity NormalRed Reduction Transitivity Application. +From LogRel.LogicalRelation.Introductions Require Import Poly Pi. Set Universe Polymorphism. Set Printing Primitive Projection Parameters. @@ -24,14 +25,8 @@ Section SimpleArrow. Lemma ArrRedTy0 {Γ l A B} : [Γ ||- A] -> [Γ ||- B] -> [Γ ||-Π arr A B]. Proof. - intros RA RB; escape. - unshelve econstructor; [exact A| exact B⟨↑⟩|..]; tea. - - eapply redtywf_refl. - now eapply wft_simple_arr. - - now unshelve eapply escapeEq, reflLRTyEq. - - eapply convty_simple_arr; tea. - all: now unshelve eapply escapeEq, reflLRTyEq. - - now eapply shiftPolyRed. + intros RA RB. + now apply LRPiPoly0, shiftPolyRed. Qed. Lemma ArrRedTy {Γ l A B} : [Γ ||- A] -> [Γ ||- B] -> [Γ ||- arr A B].