From 7f4c31b14e454b6b4eee0c038d11ebb98a78a37c Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 27 Dec 2024 12:12:19 -0500 Subject: [PATCH] Generalize Pi to TBind so we have both sigma and pi --- syntax.sig | 5 +- theories/Autosubst2/syntax.v | 88 ++++++++++++++++++++++-------------- theories/fp_red.v | 38 ++++++++-------- 3 files changed, 77 insertions(+), 54 deletions(-) diff --git a/syntax.sig b/syntax.sig index 00ef8ec..aee89b0 100644 --- a/syntax.sig +++ b/syntax.sig @@ -1,13 +1,16 @@ nat : Type Tm(VarTm) : Type PTag : Type +TTag : Type +TPi : TTag +TSig : TTag PL : PTag PR : PTag Abs : (bind Tm in Tm) -> Tm App : Tm -> Tm -> Tm Pair : Tm -> Tm -> Tm Proj : PTag -> Tm -> Tm -Pi : Tm -> (bind Tm in Tm) -> Tm +TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm Bot : Tm Univ : nat -> Tm \ No newline at end of file diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v index 285bc2c..b972476 100644 --- a/theories/Autosubst2/syntax.v +++ b/theories/Autosubst2/syntax.v @@ -19,13 +19,27 @@ Proof. exact (eq_refl). Qed. +Inductive TTag : Type := + | TPi : TTag + | TSig : TTag. + +Lemma congr_TPi : TPi = TPi. +Proof. +exact (eq_refl). +Qed. + +Lemma congr_TSig : TSig = TSig. +Proof. +exact (eq_refl). +Qed. + Inductive Tm (n_Tm : nat) : Type := | VarTm : fin n_Tm -> Tm n_Tm | Abs : Tm (S n_Tm) -> Tm n_Tm | App : Tm n_Tm -> Tm n_Tm -> Tm n_Tm | Pair : Tm n_Tm -> Tm n_Tm -> Tm n_Tm | Proj : PTag -> Tm n_Tm -> Tm n_Tm - | Pi : Tm n_Tm -> Tm (S n_Tm) -> Tm n_Tm + | TBind : TTag -> Tm n_Tm -> Tm (S n_Tm) -> Tm n_Tm | Bot : Tm n_Tm | Univ : nat -> Tm n_Tm. @@ -59,12 +73,14 @@ exact (eq_trans (eq_trans eq_refl (ap (fun x => Proj m_Tm x s1) H0)) (ap (fun x => Proj m_Tm t0 x) H1)). Qed. -Lemma congr_Pi {m_Tm : nat} {s0 : Tm m_Tm} {s1 : Tm (S m_Tm)} {t0 : Tm m_Tm} - {t1 : Tm (S m_Tm)} (H0 : s0 = t0) (H1 : s1 = t1) : - Pi m_Tm s0 s1 = Pi m_Tm t0 t1. +Lemma congr_TBind {m_Tm : nat} {s0 : TTag} {s1 : Tm m_Tm} {s2 : Tm (S m_Tm)} + {t0 : TTag} {t1 : Tm m_Tm} {t2 : Tm (S m_Tm)} (H0 : s0 = t0) (H1 : s1 = t1) + (H2 : s2 = t2) : TBind m_Tm s0 s1 s2 = TBind m_Tm t0 t1 t2. Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => Pi m_Tm x s1) H0)) - (ap (fun x => Pi m_Tm t0 x) H1)). +exact (eq_trans + (eq_trans (eq_trans eq_refl (ap (fun x => TBind m_Tm x s1 s2) H0)) + (ap (fun x => TBind m_Tm t0 x s2) H1)) + (ap (fun x => TBind m_Tm t0 t1 x) H2)). Qed. Lemma congr_Bot {m_Tm : nat} : Bot m_Tm = Bot m_Tm. @@ -98,7 +114,8 @@ Fixpoint ren_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm) | App _ s0 s1 => App n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1) | Pair _ s0 s1 => Pair n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1) | Proj _ s0 s1 => Proj n_Tm s0 (ren_Tm xi_Tm s1) - | Pi _ s0 s1 => Pi n_Tm (ren_Tm xi_Tm s0) (ren_Tm (upRen_Tm_Tm xi_Tm) s1) + | TBind _ s0 s1 s2 => + TBind n_Tm s0 (ren_Tm xi_Tm s1) (ren_Tm (upRen_Tm_Tm xi_Tm) s2) | Bot _ => Bot n_Tm | Univ _ s0 => Univ n_Tm s0 end. @@ -124,8 +141,8 @@ Fixpoint subst_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm) | App _ s0 s1 => App n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1) | Pair _ s0 s1 => Pair n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1) | Proj _ s0 s1 => Proj n_Tm s0 (subst_Tm sigma_Tm s1) - | Pi _ s0 s1 => - Pi n_Tm (subst_Tm sigma_Tm s0) (subst_Tm (up_Tm_Tm sigma_Tm) s1) + | TBind _ s0 s1 s2 => + TBind n_Tm s0 (subst_Tm sigma_Tm s1) (subst_Tm (up_Tm_Tm sigma_Tm) s2) | Bot _ => Bot n_Tm | Univ _ s0 => Univ n_Tm s0 end. @@ -163,9 +180,9 @@ subst_Tm sigma_Tm s = s := congr_Pair (idSubst_Tm sigma_Tm Eq_Tm s0) (idSubst_Tm sigma_Tm Eq_Tm s1) | Proj _ s0 s1 => congr_Proj (eq_refl s0) (idSubst_Tm sigma_Tm Eq_Tm s1) - | Pi _ s0 s1 => - congr_Pi (idSubst_Tm sigma_Tm Eq_Tm s0) - (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s1) + | TBind _ s0 s1 s2 => + congr_TBind (eq_refl s0) (idSubst_Tm sigma_Tm Eq_Tm s1) + (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) end. @@ -206,10 +223,10 @@ Fixpoint extRen_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) | Proj _ s0 s1 => congr_Proj (eq_refl s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) - | Pi _ s0 s1 => - congr_Pi (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0) + | TBind _ s0 s1 s2 => + congr_TBind (eq_refl s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) (extRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm) - (upExtRen_Tm_Tm _ _ Eq_Tm) s1) + (upExtRen_Tm_Tm _ _ Eq_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) end. @@ -251,10 +268,10 @@ Fixpoint ext_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm) congr_Pair (ext_Tm sigma_Tm tau_Tm Eq_Tm s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) | Proj _ s0 s1 => congr_Proj (eq_refl s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) - | Pi _ s0 s1 => - congr_Pi (ext_Tm sigma_Tm tau_Tm Eq_Tm s0) + | TBind _ s0 s1 s2 => + congr_TBind (eq_refl s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) (ext_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (upExt_Tm_Tm _ _ Eq_Tm) - s1) + s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) end. @@ -296,10 +313,10 @@ Fixpoint compRenRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1) | Proj _ s0 s1 => congr_Proj (eq_refl s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1) - | Pi _ s0 s1 => - congr_Pi (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0) + | TBind _ s0 s1 s2 => + congr_TBind (eq_refl s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1) (compRenRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm) - (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s1) + (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) end. @@ -351,10 +368,11 @@ Fixpoint compRenSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} | Proj _ s0 s1 => congr_Proj (eq_refl s0) (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1) - | Pi _ s0 s1 => - congr_Pi (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0) + | TBind _ s0 s1 s2 => + congr_TBind (eq_refl s0) + (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1) (compRenSubst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm tau_Tm) - (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s1) + (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) end. @@ -427,10 +445,11 @@ ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s := | Proj _ s0 s1 => congr_Proj (eq_refl s0) (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1) - | Pi _ s0 s1 => - congr_Pi (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0) + | TBind _ s0 s1 s2 => + congr_TBind (eq_refl s0) + (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1) (compSubstRen_Tm (up_Tm_Tm sigma_Tm) (upRen_Tm_Tm zeta_Tm) - (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s1) + (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) end. @@ -504,10 +523,11 @@ subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s := | Proj _ s0 s1 => congr_Proj (eq_refl s0) (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1) - | Pi _ s0 s1 => - congr_Pi (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0) + | TBind _ s0 s1 s2 => + congr_TBind (eq_refl s0) + (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1) (compSubstSubst_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) - (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s1) + (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) end. @@ -620,10 +640,10 @@ Fixpoint rinst_inst_Tm {m_Tm : nat} {n_Tm : nat} (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1) | Proj _ s0 s1 => congr_Proj (eq_refl s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1) - | Pi _ s0 s1 => - congr_Pi (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0) + | TBind _ s0 s1 s2 => + congr_TBind (eq_refl s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1) (rinst_inst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm sigma_Tm) - (rinstInst_up_Tm_Tm _ _ Eq_Tm) s1) + (rinstInst_up_Tm_Tm _ _ Eq_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) end. @@ -828,7 +848,7 @@ Arguments Univ {n_Tm}. Arguments Bot {n_Tm}. -Arguments Pi {n_Tm}. +Arguments TBind {n_Tm}. Arguments Proj {n_Tm}. diff --git a/theories/fp_red.v b/theories/fp_red.v index a110d51..b3d73bb 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -68,10 +68,10 @@ Module Par. | ProjCong p a0 a1 : R a0 a1 -> R (Proj p a0) (Proj p a1) - | PiCong A0 A1 B0 B1: + | BindCong p A0 A1 B0 B1: R A0 A1 -> R B0 B1 -> - R (Pi A0 B0) (Pi A1 B1) + R (TBind p A0 B0) (TBind p A1 B1) (* Bot is useful for making the prov function computable *) | BotCong : R Bot Bot @@ -209,11 +209,11 @@ Module Par. move : iha => [b0 [? ?]]. subst. eexists. split. by apply ProjCong; eauto. by asimpl. - - move => n A0 A1 B0 B1 ha iha hB ihB m ξ []//= t t0 [*]. subst. + - move => n p A0 A1 B0 B1 ha iha hB ihB m ξ []//= ? t t0 [*]. subst. spec_refl. move : iha => [b0 [? ?]]. move : ihB => [c0 [? ?]]. subst. - eexists. split. by apply PiCong; eauto. + eexists. split. by apply BindCong; eauto. by asimpl. - move => n n0 ξ []//=. hauto l:on. - move => n i n0 ξ []//=. hauto l:on. @@ -286,7 +286,7 @@ Module RPar. | ProjCong p a0 a1 : R a0 a1 -> R (Proj p a0) (Proj p a1) - | PiCong A0 A1 B0 B1: + | BindCong A0 A1 B0 B1: R A0 A1 -> R B0 B1 -> R (Pi A0 B0) (Pi A1 B1) @@ -404,7 +404,7 @@ Module EPar. | ProjCong p a0 a1 : R a0 a1 -> R (Proj p a0) (Proj p a1) - | PiCong A0 A1 B0 B1: + | BindCong A0 A1 B0 B1: R A0 A1 -> R B0 B1 -> R (Pi A0 B0) (Pi A1 B1) @@ -533,7 +533,7 @@ Module RPars. rtc RPar.R (App a0 b0) (App a1 b1). Proof. solve_s. Qed. - Lemma PiCong n (a0 a1 : Tm n) b0 b1 : + Lemma BindCong n (a0 a1 : Tm n) b0 b1 : rtc RPar.R a0 a1 -> rtc RPar.R b0 b1 -> rtc RPar.R (Pi a0 b0) (Pi a1 b1). @@ -754,7 +754,7 @@ Proof. exists d. split => //. hauto lq:on use:RPars.ProjCong, relations.rtc_transitive. + hauto lq:on ctrs:EPar.R use:RPars.ProjCong. - - hauto lq:on inv:RPar.R ctrs:EPar.R, rtc use:RPars.PiCong. + - hauto lq:on inv:RPar.R ctrs:EPar.R, rtc use:RPars.BindCong. - hauto l:on ctrs:EPar.R inv:RPar.R. - hauto l:on ctrs:EPar.R inv:RPar.R. Qed. @@ -927,7 +927,7 @@ Proof. - move => n a0 a1 b0 b1 ha iha hb ihb c. move /Pi_EPar' => [a2][b2][/iha [a3 h0]][/ihb [b3 h1]]h2 {iha ihb}. have : EPar.R (Pi a2 b2)(Pi a3 b3) - by hauto l:on use:EPar.PiCong. + by hauto l:on use:EPar.BindCong. move : OExp.commutativity0 h2; repeat move/[apply]. move => [d h]. exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge. @@ -1375,24 +1375,24 @@ Module ERPar. - sfirstorder use:EPar.AppCong, @rtc_once. Qed. - Lemma PiCong n (a0 a1 : Tm n) b0 b1: + Lemma BindCong n (a0 a1 : Tm n) b0 b1: R a0 a1 -> R b0 b1 -> rtc R (Pi a0 b0) (Pi a1 b1). Proof. move => [] + []. - - sfirstorder use:RPar.PiCong, @rtc_once. + - sfirstorder use:RPar.BindCong, @rtc_once. - move => h0 h1. apply : rtc_l. - left. apply RPar.PiCong; eauto; apply RPar.refl. + left. apply RPar.BindCong; eauto; apply RPar.refl. apply rtc_once. - hauto l:on use:EPar.PiCong, EPar.refl. + hauto l:on use:EPar.BindCong, EPar.refl. - move => h0 h1. apply : rtc_l. - left. apply RPar.PiCong; eauto; apply RPar.refl. + left. apply RPar.BindCong; eauto; apply RPar.refl. apply rtc_once. - hauto l:on use:EPar.PiCong, EPar.refl. - - sfirstorder use:EPar.PiCong, @rtc_once. + hauto l:on use:EPar.BindCong, EPar.refl. + - sfirstorder use:EPar.BindCong, @rtc_once. Qed. Lemma PairCong n (a0 a1 b0 b1 : Tm n) : @@ -1423,7 +1423,7 @@ Module ERPar. End ERPar. -Hint Resolve ERPar.AppCong ERPar.refl ERPar.AbsCong ERPar.PairCong ERPar.ProjCong ERPar.PiCong : erpar. +Hint Resolve ERPar.AppCong ERPar.refl ERPar.AbsCong ERPar.PairCong ERPar.ProjCong ERPar.BindCong : erpar. Module ERPars. #[local]Ltac solve_s_rec := @@ -1454,7 +1454,7 @@ Module ERPars. rtc ERPar.R (Proj p a0) (Proj p a1). Proof. solve_s. Qed. - Lemma PiCong n (a0 a1 : Tm n) b0 b1: + Lemma BindCong n (a0 a1 : Tm n) b0 b1: rtc ERPar.R a0 a1 -> rtc ERPar.R b0 b1 -> rtc ERPar.R (Pi a0 b0) (Pi a1 b1). @@ -1512,7 +1512,7 @@ Proof. - sfirstorder use:ERPars.AppCong. - sfirstorder use:ERPars.PairCong. - sfirstorder use:ERPars.ProjCong. - - sfirstorder use:ERPars.PiCong. + - sfirstorder use:ERPars.BindCong. - sfirstorder. - sfirstorder. Qed.