From 46ec21b763084482c72e108ed7e580e266ea3e26 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Tue, 24 Dec 2024 01:09:02 -0500 Subject: [PATCH] Add pi type --- syntax.sig | 1 + theories/Autosubst2/syntax.v | 47 ++++++++++++++++++++++++++++++++- theories/fp_red.v | 51 +++++++++++++++++++++++++++++++++--- 3 files changed, 95 insertions(+), 4 deletions(-) diff --git a/syntax.sig b/syntax.sig index 68be421..a0e461d 100644 --- a/syntax.sig +++ b/syntax.sig @@ -7,3 +7,4 @@ 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 \ No newline at end of file diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v index ed66e97..bc4e559 100644 --- a/theories/Autosubst2/syntax.v +++ b/theories/Autosubst2/syntax.v @@ -24,7 +24,8 @@ Inductive Tm (n_Tm : nat) : Type := | 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. + | Proj : PTag -> Tm n_Tm -> Tm n_Tm + | Pi : Tm n_Tm -> Tm (S n_Tm) -> Tm n_Tm. Lemma congr_Abs {m_Tm : nat} {s0 : Tm (S m_Tm)} {t0 : Tm (S m_Tm)} (H0 : s0 = t0) : Abs m_Tm s0 = Abs m_Tm t0. @@ -56,6 +57,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. +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)). +Qed. + Lemma upRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) : fin (S m) -> fin (S n). Proof. @@ -76,6 +85,7 @@ 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) end. Lemma up_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) : @@ -99,6 +109,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) end. Lemma upId_Tm_Tm {m_Tm : nat} (sigma : fin m_Tm -> Tm m_Tm) @@ -134,6 +146,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) end. Lemma upExtRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) @@ -172,6 +187,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) + (extRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm) + (upExtRen_Tm_Tm _ _ Eq_Tm) s1) end. Lemma upExt_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) @@ -211,6 +230,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) + (ext_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (upExt_Tm_Tm _ _ Eq_Tm) + s1) end. Lemma up_ren_ren_Tm_Tm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l) @@ -250,6 +273,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) + (compRenRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm) + (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s1) end. Lemma up_ren_subst_Tm_Tm {k : nat} {l : nat} {m_Tm : nat} @@ -299,6 +326,10 @@ 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) + (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) end. Lemma up_subst_ren_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat} @@ -369,6 +400,10 @@ 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) + (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) end. Lemma up_subst_subst_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat} @@ -440,6 +475,10 @@ 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) + (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) end. Lemma renRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} @@ -550,6 +589,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) + (rinst_inst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm sigma_Tm) + (rinstInst_up_Tm_Tm _ _ Eq_Tm) s1) end. Lemma rinstInst'_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm) @@ -748,6 +791,8 @@ Core. Arguments VarTm {n_Tm}. +Arguments Pi {n_Tm}. + Arguments Proj {n_Tm}. Arguments Pair {n_Tm}. diff --git a/theories/fp_red.v b/theories/fp_red.v index 44b7d16..e04d509 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -49,7 +49,11 @@ Module Par. R (Pair a0 b0) (Pair a1 b1) | ProjCong p a0 a1 : R a0 a1 -> - R (Proj p a0) (Proj p a1). + R (Proj p a0) (Proj p a1) + | PiCong A0 A1 B0 B1: + R A0 A1 -> + R B0 B1 -> + R (Pi A0 B0) (Pi A1 B1). End Par. (***************** Beta rules only ***********************) @@ -89,7 +93,11 @@ Module RPar. R (Pair a0 b0) (Pair a1 b1) | ProjCong p a0 a1 : R a0 a1 -> - R (Proj p a0) (Proj p a1). + R (Proj p a0) (Proj p a1) + | PiCong A0 A1 B0 B1: + R A0 A1 -> + R B0 B1 -> + R (Pi A0 B0) (Pi A1 B1). Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. @@ -154,6 +162,7 @@ Module RPar. - hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R use:morphing_up. Qed. Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : @@ -196,7 +205,11 @@ Module EPar. R (Pair a0 b0) (Pair a1 b1) | ProjCong p a0 a1 : R a0 a1 -> - R (Proj p a0) (Proj p a1). + R (Proj p a0) (Proj p a1) + | PiCong A0 A1 B0 B1: + R A0 A1 -> + R B0 B1 -> + R (Pi A0 B0) (Pi A1 B1). Lemma refl n (a : Tm n) : EPar.R a a. Proof. @@ -238,6 +251,7 @@ Module EPar. - hauto q:on ctrs:R. - hauto q:on ctrs:R. - hauto q:on ctrs:R. + - hauto l:on ctrs:R use:renaming inv:option. Qed. Lemma substing n a0 a1 (b0 b1 : Tm n) : @@ -315,6 +329,12 @@ Module RPars. rtc RPar.R (App a0 b0) (App a1 b1). Proof. solve_s. Qed. + Lemma PiCong 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). + Proof. solve_s. Qed. + Lemma PairCong n (a0 a1 b0 b1 : Tm n) : rtc RPar.R a0 a1 -> rtc RPar.R b0 b1 -> @@ -530,6 +550,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. Qed. Lemma commutativity1 n (a b0 b1 : Tm n) : @@ -599,6 +620,21 @@ Proof. - hauto l:on ctrs:OExp.R. Qed. +Lemma Pi_EPar' n (a : Tm n) b u : + EPar.R (Pi a b) u -> + (exists a0 b0, EPar.R a a0 /\ EPar.R b b0 /\ rtc OExp.R (Pi a0 b0) u). +Proof. + move E : (Pi a b) => t h. + move : a b E. elim : n t u /h => //=. + - move => n a0 a1 ha iha a b ?. subst. + specialize iha with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - move => n a0 a1 ha iha a b ?. subst. + specialize iha with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - hauto l:on ctrs:OExp.R. +Qed. + Lemma Pair_EPar' n (a b u : Tm n) : EPar.R (Pair a b) u -> exists a0 b0, EPar.R a a0 /\ EPar.R b b0 /\ rtc OExp.R (Pair a0 b0) u. @@ -654,6 +690,13 @@ Proof. move : OExp.commutativity0 h1; repeat move/[apply]. move => [d1 h1]. exists d1. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge. + - 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. + move : OExp.commutativity0 h2; repeat move/[apply]. + move => [d h]. + exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge. Qed. Function tstar {n} (a : Tm n) := @@ -668,6 +711,7 @@ Function tstar {n} (a : Tm n) := | Proj p (Pair a b) => if p is PL then (tstar a) else (tstar b) | Proj p (Abs a) => (Abs (Proj p (tstar a))) | Proj p a => Proj p (tstar a) + | Pi a b => Pi (tstar a) (tstar b) end. Lemma RPar_triangle n (a : Tm n) : forall b, RPar.R a b -> RPar.R b (tstar a). @@ -683,6 +727,7 @@ Proof. - hauto drew:off inv:RPar.R use:RPar.refl, RPar.ProjPair'. - hauto lq:on inv:RPar.R ctrs:RPar.R. - hauto lq:on inv:RPar.R ctrs:RPar.R. + - hauto lq:on inv:RPar.R ctrs:RPar.R. Qed. Lemma RPar_diamond n (c a1 b1 : Tm n) :