From 9f80013df6683b4e77a2021f714473aa3c5638f2 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 27 Jan 2025 16:44:48 -0500 Subject: [PATCH 01/18] Add tstar to preserve eta normal forms --- syntax.sig | 2 +- theories/Autosubst2/syntax.v | 110 +++++++++++----------- theories/fp_red.v | 178 ++++++++++++++++++++++++++++++----- 3 files changed, 209 insertions(+), 81 deletions(-) diff --git a/syntax.sig b/syntax.sig index d052897..e2bafac 100644 --- a/syntax.sig +++ b/syntax.sig @@ -9,7 +9,7 @@ Void : Ty PL : PTag PR : PTag -PAbs : Ty -> (bind PTm in PTm) -> PTm +PAbs : (bind PTm in PTm) -> PTm PApp : PTm -> PTm -> PTm PPair : PTm -> PTm -> PTm PProj : PTag -> PTm -> PTm diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v index b37b721..b5cbc66 100644 --- a/theories/Autosubst2/syntax.v +++ b/theories/Autosubst2/syntax.v @@ -19,43 +19,17 @@ Proof. exact (eq_refl). Qed. -Inductive Ty : Type := - | Fun : Ty -> Ty -> Ty - | Prod : Ty -> Ty -> Ty - | Void : Ty. - -Lemma congr_Fun {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0) - (H1 : s1 = t1) : Fun s0 s1 = Fun t0 t1. -Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => Fun x s1) H0)) - (ap (fun x => Fun t0 x) H1)). -Qed. - -Lemma congr_Prod {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0) - (H1 : s1 = t1) : Prod s0 s1 = Prod t0 t1. -Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => Prod x s1) H0)) - (ap (fun x => Prod t0 x) H1)). -Qed. - -Lemma congr_Void : Void = Void. -Proof. -exact (eq_refl). -Qed. - Inductive PTm (n_PTm : nat) : Type := | VarPTm : fin n_PTm -> PTm n_PTm - | PAbs : Ty -> PTm (S n_PTm) -> PTm n_PTm + | PAbs : PTm (S n_PTm) -> PTm n_PTm | PApp : PTm n_PTm -> PTm n_PTm -> PTm n_PTm | PPair : PTm n_PTm -> PTm n_PTm -> PTm n_PTm | PProj : PTag -> PTm n_PTm -> PTm n_PTm. -Lemma congr_PAbs {m_PTm : nat} {s0 : Ty} {s1 : PTm (S m_PTm)} {t0 : Ty} - {t1 : PTm (S m_PTm)} (H0 : s0 = t0) (H1 : s1 = t1) : - PAbs m_PTm s0 s1 = PAbs m_PTm t0 t1. +Lemma congr_PAbs {m_PTm : nat} {s0 : PTm (S m_PTm)} {t0 : PTm (S m_PTm)} + (H0 : s0 = t0) : PAbs m_PTm s0 = PAbs m_PTm t0. Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => PAbs m_PTm x s1) H0)) - (ap (fun x => PAbs m_PTm t0 x) H1)). +exact (eq_trans eq_refl (ap (fun x => PAbs m_PTm x) H0)). Qed. Lemma congr_PApp {m_PTm : nat} {s0 : PTm m_PTm} {s1 : PTm m_PTm} @@ -98,7 +72,7 @@ Fixpoint ren_PTm {m_PTm : nat} {n_PTm : nat} (xi_PTm : fin m_PTm -> fin n_PTm) (s : PTm m_PTm) {struct s} : PTm n_PTm := match s with | VarPTm _ s0 => VarPTm n_PTm (xi_PTm s0) - | PAbs _ s0 s1 => PAbs n_PTm s0 (ren_PTm (upRen_PTm_PTm xi_PTm) s1) + | PAbs _ s0 => PAbs n_PTm (ren_PTm (upRen_PTm_PTm xi_PTm) s0) | PApp _ s0 s1 => PApp n_PTm (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) | PPair _ s0 s1 => PPair n_PTm (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) | PProj _ s0 s1 => PProj n_PTm s0 (ren_PTm xi_PTm s1) @@ -122,7 +96,7 @@ Fixpoint subst_PTm {m_PTm : nat} {n_PTm : nat} := match s with | VarPTm _ s0 => sigma_PTm s0 - | PAbs _ s0 s1 => PAbs n_PTm s0 (subst_PTm (up_PTm_PTm sigma_PTm) s1) + | PAbs _ s0 => PAbs n_PTm (subst_PTm (up_PTm_PTm sigma_PTm) s0) | PApp _ s0 s1 => PApp n_PTm (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) | PPair _ s0 s1 => @@ -155,9 +129,9 @@ Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm) : subst_PTm sigma_PTm s = s := match s with | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 s1 => - congr_PAbs (eq_refl s0) - (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s1) + | PAbs _ s0 => + congr_PAbs + (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s0) | PApp _ s0 s1 => congr_PApp (idSubst_PTm sigma_PTm Eq_PTm s0) (idSubst_PTm sigma_PTm Eq_PTm s1) @@ -194,10 +168,10 @@ Fixpoint extRen_PTm {m_PTm : nat} {n_PTm : nat} ren_PTm xi_PTm s = ren_PTm zeta_PTm s := match s with | VarPTm _ s0 => ap (VarPTm n_PTm) (Eq_PTm s0) - | PAbs _ s0 s1 => - congr_PAbs (eq_refl s0) + | PAbs _ s0 => + congr_PAbs (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) - (upExtRen_PTm_PTm _ _ Eq_PTm) s1) + (upExtRen_PTm_PTm _ _ Eq_PTm) s0) | PApp _ s0 s1 => congr_PApp (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) @@ -235,10 +209,10 @@ Fixpoint ext_PTm {m_PTm : nat} {n_PTm : nat} subst_PTm sigma_PTm s = subst_PTm tau_PTm s := match s with | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 s1 => - congr_PAbs (eq_refl s0) + | PAbs _ s0 => + congr_PAbs (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) - (upExt_PTm_PTm _ _ Eq_PTm) s1) + (upExt_PTm_PTm _ _ Eq_PTm) s0) | PApp _ s0 s1 => congr_PApp (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) @@ -275,10 +249,10 @@ Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} {struct s} : ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm rho_PTm s := match s with | VarPTm _ s0 => ap (VarPTm l_PTm) (Eq_PTm s0) - | PAbs _ s0 s1 => - congr_PAbs (eq_refl s0) + | PAbs _ s0 => + congr_PAbs (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) - (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s1) + (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s0) | PApp _ s0 s1 => congr_PApp (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) @@ -325,10 +299,10 @@ Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} {struct s} : subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm theta_PTm s := match s with | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 s1 => - congr_PAbs (eq_refl s0) + | PAbs _ s0 => + congr_PAbs (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm) - (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s1) + (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s0) | PApp _ s0 s1 => congr_PApp (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0) (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) @@ -395,10 +369,10 @@ Fixpoint compSubstRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := match s with | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 s1 => - congr_PAbs (eq_refl s0) + | PAbs _ s0 => + congr_PAbs (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm) - (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s1) + (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s0) | PApp _ s0 s1 => congr_PApp (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0) (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) @@ -467,10 +441,10 @@ Fixpoint compSubstSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := match s with | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 s1 => - congr_PAbs (eq_refl s0) + | PAbs _ s0 => + congr_PAbs (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) - (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s1) + (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s0) | PApp _ s0 s1 => congr_PApp (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0) (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) @@ -580,10 +554,10 @@ Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat} (s : PTm m_PTm) {struct s} : ren_PTm xi_PTm s = subst_PTm sigma_PTm s := match s with | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 s1 => - congr_PAbs (eq_refl s0) + | PAbs _ s0 => + congr_PAbs (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm) - (rinstInst_up_PTm_PTm _ _ Eq_PTm) s1) + (rinstInst_up_PTm_PTm _ _ Eq_PTm) s0) | PApp _ s0 s1 => congr_PApp (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) @@ -663,6 +637,30 @@ Proof. exact (fun x => eq_refl). Qed. +Inductive Ty : Type := + | Fun : Ty -> Ty -> Ty + | Prod : Ty -> Ty -> Ty + | Void : Ty. + +Lemma congr_Fun {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0) + (H1 : s1 = t1) : Fun s0 s1 = Fun t0 t1. +Proof. +exact (eq_trans (eq_trans eq_refl (ap (fun x => Fun x s1) H0)) + (ap (fun x => Fun t0 x) H1)). +Qed. + +Lemma congr_Prod {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0) + (H1 : s1 = t1) : Prod s0 s1 = Prod t0 t1. +Proof. +exact (eq_trans (eq_trans eq_refl (ap (fun x => Prod x s1) H0)) + (ap (fun x => Prod t0 x) H1)). +Qed. + +Lemma congr_Void : Void = Void. +Proof. +exact (eq_refl). +Qed. + Class Up_PTm X Y := up_PTm : X -> Y. diff --git a/theories/fp_red.v b/theories/fp_red.v index babb3c8..288a2b3 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -22,16 +22,17 @@ Ltac spec_refl := ltac2:(spec_refl ()). Module ERed. Inductive R {n} : PTm n -> PTm n -> Prop := (****************** Eta ***********************) - | AppEta A a0 a1 : + | AppEta a0 a1 : R a0 a1 -> - R (PAbs A (PApp (ren_PTm shift a0) (VarPTm var_zero))) a1 - | PairEta a0 a1 : + R (PAbs (PApp (ren_PTm shift a0) (VarPTm var_zero))) a1 + | PairEta a0 b0 a1 : R a0 a1 -> - R (PPair (PProj PL a0) (PProj PR a0)) a1 + R b0 a1 -> + R (PPair (PProj PL a0) (PProj PR b0)) a1 (*************** Congruence ********************) - | AbsCong A a0 a1 : + | AbsCong a0 a1 : R a0 a1 -> - R (PAbs A a0) (PAbs A a1) + R (PAbs a0) (PAbs a1) | AppCong a0 a1 b0 b1 : R a0 a1 -> R b0 b1 -> @@ -53,8 +54,8 @@ Module ERed. Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. - Lemma AppEta' n A a0 a1 (u : PTm n) : - u = (PAbs A (PApp (ren_PTm shift a0) (VarPTm var_zero))) -> + Lemma AppEta' n a0 a1 (u : PTm n) : + u = (PAbs (PApp (ren_PTm shift a0) (VarPTm var_zero))) -> R a0 a1 -> R u a1. Proof. move => ->. apply AppEta. Qed. @@ -65,8 +66,8 @@ Module ERed. move => h. move : m ξ. elim : n a b /h. - move => n A a0 a1 ha iha m ξ /=. - eapply AppEta' with (A := A); eauto. by asimpl. + move => n a0 a1 ha iha m ξ /=. + eapply AppEta'; eauto. by asimpl. all : qauto ctrs:R. Qed. @@ -91,8 +92,8 @@ Module ERed. R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b). Proof. move => + h. move : m ρ0 ρ1. elim : n a b / h => n. - move => A a0 a1 ha iha m ρ0 ρ1 hρ /=. - eapply AppEta' with (A := A); eauto. by asimpl. + move => a0 a1 ha iha m ρ0 ρ1 hρ /=. + eapply AppEta'; eauto. by asimpl. all : hauto lq:on ctrs:R use:morphing_up. Qed. @@ -120,9 +121,9 @@ with SN {n} : PTm n -> Prop := SN a -> SN b -> SN (PPair a b) -| N_Abs A a : +| N_Abs a : SN a -> - SN (PAbs A a) + SN (PAbs a) | N_SNe a : SNe a -> SN a @@ -131,9 +132,9 @@ with SN {n} : PTm n -> Prop := SN b -> SN a with TRedSN {n} : PTm n -> PTm n -> Prop := -| N_β A a b : +| N_β a b : SN b -> - TRedSN (PApp (PAbs A a) b) (subst_PTm (scons b VarPTm) a) + TRedSN (PApp (PAbs a) b) (subst_PTm (scons b VarPTm) a) | N_AppL a0 a1 b : TRedSN a0 a1 -> TRedSN (PApp a0 b) (PApp a1 b) @@ -153,6 +154,27 @@ Scheme sne_ind := Induction for SNe Sort Prop Combined Scheme sn_mutual from sne_ind, sn_ind, sred_ind. + +Fixpoint ne {n} (a : PTm n) := + match a with + | VarPTm i => true + | PApp a b => ne a && nf b + | PAbs a => false + | PPair _ _ => false + | PProj _ a => ne a + end +with nf {n} (a : PTm n) := + match a with + | VarPTm i => true + | PApp a b => ne a && nf b + | PAbs a => nf a + | PPair a b => nf a && nf b + | PProj _ a => ne a +end. + +Lemma ne_nf n a : @ne n a -> nf a. +Proof. elim : a => //=. Qed. + Inductive TRedSN' {n} (a : PTm n) : PTm n -> Prop := | T_Refl : TRedSN' a a @@ -182,7 +204,7 @@ Proof. + have /iha : (ERed.R (PProj PL a0) (PProj PL b0)) by sauto lq:on. sfirstorder use:SN_Proj. + sauto lq:on. - - move => A a ha iha b. + - move => a ha iha b. inversion 1; subst. + have : ERed.R (PApp (ren_PTm shift a0) (VarPTm var_zero)) (PApp (ren_PTm shift b) (VarPTm var_zero)). apply ERed.AppCong; eauto using ERed.refl. @@ -192,7 +214,7 @@ Proof. + sauto lq:on. - sauto lq:on. - sauto lq:on. - - move => A a b ha iha c h0. + - move => a b ha iha c h0. inversion h0; subst. inversion H1; subst. + exists (PApp a1 b1). split. sfirstorder. @@ -208,7 +230,7 @@ Proof. elim /ERed.inv => //= _. move => p a0 a1 ha [*]. subst. elim /ERed.inv : ha => //= _. - + move => a0 a2 ha [*]. subst. + + move => a0 b0 a2 ha ha' [*]. subst. exists (PProj PL a1). split. sauto. sauto lq:on. @@ -217,7 +239,7 @@ Proof. elim /ERed.inv => //=_. move => p a0 a1 + [*]. subst. elim /ERed.inv => //=_. - + move => a0 a2 h [*]. subst. + + move => a0 b0 a2 h0 h1 [*]. subst. exists (PProj PR a1). split. sauto. sauto lq:on. @@ -228,16 +250,16 @@ Admitted. Module RRed. Inductive R {n} : PTm n -> PTm n -> Prop := (****************** Eta ***********************) - | AppAbs A a b : - R (PApp (PAbs A a) b) (subst_PTm (scons b VarPTm) a) + | AppAbs a b : + R (PApp (PAbs a) b) (subst_PTm (scons b VarPTm) a) | ProjPair p a b : R (PProj p (PPair a b)) (if p is PL then a else b) (*************** Congruence ********************) - | AbsCong A a0 a1 : + | AbsCong a0 a1 : R a0 a1 -> - R (PAbs A a0) (PAbs A a1) + R (PAbs a0) (PAbs a1) | AppCong0 a0 a1 b : R a0 a1 -> R (PApp a0 b) (PApp a1 b) @@ -255,4 +277,112 @@ Module RRed. R (PProj p a0) (PProj p a1). Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. + + + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) : + R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b. + Proof. + move E : (ren_PTm ξ a) => u h. + move : n ξ a E. elim : m u b/h. + - move => n a b m ξ []//=. move => []//= t t0 [*]. subst. + eexists. split. apply AppAbs. by asimpl. + - move => n p a b m ξ []//=. + move => p0 []//=. hauto q:on ctrs:R. + - move => n a0 a1 ha iha m ξ []//=. + move => p [*]. subst. + spec_refl. + move : iha => [t [h0 h1]]. subst. + eexists. split. eauto using AbsCong. + by asimpl. + - move => n a0 a1 b ha iha m ξ []//=. + hauto lq:on ctrs:R. + - move => n a b0 b1 h ih m ξ []//=. + hauto lq:on ctrs:R. + - move => n a0 a1 b ha iha m ξ []//=. + hauto lq:on ctrs:R. + - move => n a b0 b1 h ih m ξ []//=. + hauto lq:on ctrs:R. + - move => n p a0 a1 ha iha m ξ []//=. + hauto lq:on ctrs:R. + Qed. + End RRed. + +Function tstar {n} (a : PTm n) := + match a with + | VarPTm i => a + | PAbs a => PAbs (tstar a) + | PApp (PAbs a) b => subst_PTm (scons (tstar b) VarPTm) (tstar a) + | PApp a b => PApp (tstar a) (tstar b) + | PPair a b => PPair (tstar a) (tstar b) + | PProj p (PPair a b) => if p is PL then (tstar a) else (tstar b) + | PProj p a => PProj p (tstar a) + end. + +Lemma η_nf n (a b c : PTm n) : ERed.R a b -> nf b -> + ERed.R c b. + +Lemma η_nf n (a b c : PTm n) : ERed.R a b -> nf b -> RRed.R a c -> + ERed.R c b. +Proof. + move => h. move : c. + elim : n a b /h=>//=n. + - move => a0 a1 ha iha u hu. + elim /RRed.inv => //= _. + move => a2 a3 h [*]. subst. + elim / RRed.inv : h => //_. + + move => a2 b0 [h0 h1 h2]. subst. + case : a0 h0 ha iha =>//=. + move => u [?] ha iha. subst. + by asimpl. + + move => a2 b4 b0 h [*]. subst. + move /RRed.antirenaming : h. + hauto lq:on ctrs:ERed.R. + + move => a2 b0 b1 h [*]. subst. + inversion h. + - move => a0 b0 a1 ha iha hb ihb u hu. + elim /RRed.inv => //=_. + + move => a2 a3 b1 h0 [*]. subst. + elim /RRed.inv : h0 => //=_. + * move => p a2 b1 [*]. subst. + elim /ERed.inv : ha => //=_. + ** sauto lq:on. + ** move => a0 a2 b2 b3 h h' [*]. subst. + + +Lemma η_nf n (a b c : PTm n) : ERed.R a b -> nf b -> RRed.R a c -> + ERed.R a c. +Proof. + move => h. move : c. + elim : n a b /h=>//=. + - move => n A a0 a1 ha iha c ha1. + elim /RRed.inv => //=_. + move => A0 a2 a3 hr [*]. subst. + set u := a0 in hr *. + set q := a3 in hr *. + elim / RRed.inv : hr => //_. + + move => A0 a2 b0 [h0] h1 h2. subst. + subst u q. + rewrite h0. apply ERed.AppEta. + subst. + case : a0 ha iha h0 => //= B a ha iha [*]. subst. + asimpl. + admit. + + subst u q. + move => a2 a4 b0 hr [*]. subst. + move /RRed.antirenaming : hr => [b0 [h0 h1]]. subst. + hauto lq:on ctrs:ERed.R use:ERed.renaming. + + subst u q. + move => a2 b0 b1 h [*]. subst. + inversion h. + - move => n a0 a1 ha iha v hv. + elim /RRed.inv => //=_. + + move => a2 a3 b0 h [*]. subst. + elim /RRed.inv : h => //=_. + * move => p a2 b0 [*]. subst. + elim /ERed.inv : ha=>//= _. + move => a0 a2 h [*]. subst. + best. + apply ERed.PairEta. + + - From b8d7ebfaa267465557da6ab56e679b494d96f4f4 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 27 Jan 2025 16:48:38 -0500 Subject: [PATCH 02/18] Fix the broken pair eta rule --- theories/fp_red.v | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 288a2b3..461e5f3 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -25,10 +25,9 @@ Module ERed. | AppEta a0 a1 : R a0 a1 -> R (PAbs (PApp (ren_PTm shift a0) (VarPTm var_zero))) a1 - | PairEta a0 b0 a1 : + | PairEta a0 a1 : R a0 a1 -> - R b0 a1 -> - R (PPair (PProj PL a0) (PProj PR b0)) a1 + R (PPair (PProj PL a0) (PProj PR a0)) a1 (*************** Congruence ********************) | AbsCong a0 a1 : R a0 a1 -> @@ -230,7 +229,7 @@ Proof. elim /ERed.inv => //= _. move => p a0 a1 ha [*]. subst. elim /ERed.inv : ha => //= _. - + move => a0 b0 a2 ha ha' [*]. subst. + + move => a0 a2 ha' [*]. subst. exists (PProj PL a1). split. sauto. sauto lq:on. @@ -239,7 +238,7 @@ Proof. elim /ERed.inv => //=_. move => p a0 a1 + [*]. subst. elim /ERed.inv => //=_. - + move => a0 b0 a2 h0 h1 [*]. subst. + + move => a0 a2 h1 [*]. subst. exists (PProj PR a1). split. sauto. sauto lq:on. @@ -319,8 +318,17 @@ Function tstar {n} (a : PTm n) := | PProj p a => PProj p (tstar a) end. -Lemma η_nf n (a b c : PTm n) : ERed.R a b -> nf b -> - ERed.R c b. +Lemma η_nf n (a b : PTm n) : ERed.R a b -> nf b -> ERed.R (tstar a) b. +Proof. + move => h. + elim : n a b /h => n. + - move => a0 a1 ha iha. + + move : ha. clear. best. + clear. + - sfirstorder. + - + Lemma η_nf n (a b c : PTm n) : ERed.R a b -> nf b -> RRed.R a c -> ERed.R c b. From 5ea75052a56f85dd60a6560c4a144cffe982cf05 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 27 Jan 2025 22:47:10 -0500 Subject: [PATCH 03/18] Show that eta expansion can be immediately be removed by beta --- theories/fp_red.v | 444 +++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 442 insertions(+), 2 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 461e5f3..dbe7312 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -277,6 +277,12 @@ Module RRed. Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. + Lemma AppAbs' n a (b : PTm n) u : + u = (subst_PTm (scons b VarPTm) a) -> + R (PApp (PAbs a) b) u. + Proof. + move => ->. by apply AppAbs. Qed. + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) : R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b. @@ -307,6 +313,8 @@ Module RRed. End RRed. + + Function tstar {n} (a : PTm n) := match a with | VarPTm i => a @@ -318,12 +326,444 @@ Function tstar {n} (a : PTm n) := | PProj p a => PProj p (tstar a) end. -Lemma η_nf n (a b : PTm n) : ERed.R a b -> nf b -> ERed.R (tstar a) b. +Module TStar. + Lemma renaming n m (ξ : fin n -> fin m) (a : PTm n) : + tstar (ren_PTm ξ a) = ren_PTm ξ (tstar a). + Proof. + move : m ξ. + apply tstar_ind => {}n {}a => //=. + - hauto lq:on. + - scongruence. + - move => a0 b ? h ih m ξ. + rewrite ih. + asimpl; congruence. + - qauto l:on. + - scongruence. + - hauto q:on. + - qauto l:on. + Qed. + + Lemma pair n (a b : PTm n) : + tstar (PPair a b) = PPair (tstar a) (tstar b). + reflexivity. Qed. +End TStar. + +Definition isPair {n} (a : PTm n) := if a is PPair _ _ then true else false. + +Lemma tstar_proj n (a : PTm n) : + ((~~ isPair a) /\ forall p, tstar (PProj p a) = PProj p (tstar a)) \/ + exists a0 b0, a = PPair a0 b0 /\ forall p, tstar (PProj p a) = (if p is PL then (tstar a0) else (tstar b0)). +Proof. sauto lq:on. Qed. + +Module ERed'. + Inductive R {n} : PTm n -> PTm n -> Prop := + (****************** Eta ***********************) + | AppEta a : + R (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) a + | PairEta a : + R (PPair (PProj PL a) (PProj PR a)) a + (*************** Congruence ********************) + | AbsCong a0 a1 : + R a0 a1 -> + R (PAbs a0) (PAbs a1) + | AppCong0 a0 a1 b : + R a0 a1 -> + R (PApp a0 b) (PApp a1 b) + | AppCong1 a b0 b1 : + R b0 b1 -> + R (PApp a b0) (PApp a b1) + | PairCong0 a0 a1 b : + R a0 a1 -> + R (PPair a0 b) (PPair a1 b) + | PairCong1 a b0 b1 : + R b0 b1 -> + R (PPair a b0) (PPair a b1) + | ProjCong p a0 a1 : + R a0 a1 -> + R (PProj p a0) (PProj p a1). + + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. + + Lemma AppEta' n a (u : PTm n) : + u = (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) -> + R u a. + Proof. move => ->. apply AppEta. Qed. + + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). + Proof. + move => h. move : m ξ. + elim : n a b /h. + + move => n a m ξ /=. + eapply AppEta'; eauto. by asimpl. + all : qauto ctrs:R. + Qed. + + Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> PTm m) (ξ : fin m -> fin p) : + (forall i, R (ρ0 i) (ρ1 i)) -> + (forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ1) i)). + Proof. eauto using renaming. Qed. + + (* Lemma morphing_ext n m (ρ0 ρ1 : fin n -> PTm m) a b : *) + (* R a b -> *) + (* (forall i, R (ρ0 i) (ρ1 i)) -> *) + (* (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)). *) + (* Proof. hauto q:on inv:option. Qed. *) + + (* Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) : *) + (* (forall i, R (ρ0 i) (ρ1 i)) -> *) + (* (forall i, R (up_PTm_PTm ρ0 i) (up_PTm_PTm ρ1 i)). *) + (* Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_PTm_PTm. Qed. *) + + (* Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) : *) + (* (forall i, R (ρ0 i) (ρ1 i)) -> *) + (* R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b). *) + (* Proof. *) + (* move => + h. move : m ρ0 ρ1. elim : n a b / h => n. *) + (* move => a0 a1 ha iha m ρ0 ρ1 hρ /=. *) + (* eapply AppEta'; eauto. by asimpl. *) + (* all : hauto lq:on ctrs:R use:morphing_up. *) + (* Qed. *) + + (* Lemma substing n m (a : PTm n) b (ρ : fin n -> PTm m) : *) + (* R a b -> *) + (* R (subst_PTm ρ a) (subst_PTm ρ b). *) + (* Proof. *) + (* hauto l:on use:morphing, refl. *) + (* Qed. *) + +End ERed'. + +Module EReds. + + #[local]Ltac solve_s_rec := + move => *; eapply rtc_l; eauto; + hauto lq:on ctrs:ERed'.R. + + #[local]Ltac solve_s := + repeat (induction 1; last by solve_s_rec); apply rtc_refl. + + Lemma AbsCong n (a b : PTm (S n)) : + rtc ERed'.R a b -> + rtc ERed'.R (PAbs a) (PAbs b). + Proof. solve_s. Qed. + + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : + rtc ERed'.R a0 a1 -> + rtc ERed'.R b0 b1 -> + rtc ERed'.R (PApp a0 b0) (PApp a1 b1). + Proof. solve_s. Qed. + + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : + rtc ERed'.R a0 a1 -> + rtc ERed'.R b0 b1 -> + rtc ERed'.R (PPair a0 b0) (PPair a1 b1). + Proof. solve_s. Qed. + + Lemma ProjCong n p (a0 a1 : PTm n) : + rtc ERed'.R a0 a1 -> + rtc ERed'.R (PProj p a0) (PProj p a1). + Proof. solve_s. Qed. +End EReds. + +Module RReds. + + #[local]Ltac solve_s_rec := + move => *; eapply rtc_l; eauto; + hauto lq:on ctrs:RRed.R. + + #[local]Ltac solve_s := + repeat (induction 1; last by solve_s_rec); apply rtc_refl. + + Lemma AbsCong n (a b : PTm (S n)) : + rtc RRed.R a b -> + rtc RRed.R (PAbs a) (PAbs b). + Proof. solve_s. Qed. + + Lemma AppCong n (a0 a1 b0 b1 : PTm n) : + rtc RRed.R a0 a1 -> + rtc RRed.R b0 b1 -> + rtc RRed.R (PApp a0 b0) (PApp a1 b1). + Proof. solve_s. Qed. + + Lemma PairCong n (a0 a1 b0 b1 : PTm n) : + rtc RRed.R a0 a1 -> + rtc RRed.R b0 b1 -> + rtc RRed.R (PPair a0 b0) (PPair a1 b1). + Proof. solve_s. Qed. + + Lemma ProjCong n p (a0 a1 : PTm n) : + rtc RRed.R a0 a1 -> + rtc RRed.R (PProj p a0) (PProj p a1). + Proof. solve_s. Qed. +End RReds. + + +Lemma ne_nf_ren n m (a : PTm n) (ξ : fin n -> fin m) : + (ne a <-> ne (ren_PTm ξ a)) /\ (nf a <-> nf (ren_PTm ξ a)). Proof. + move : m ξ. elim : n / a => //=; solve [hauto b:on]. +Qed. + +Lemma ne_ered n (a b : PTm n) (h : ERed'.R a b ) : + (ne a -> ne b) /\ (nf a -> nf b). +Proof. + elim : n a b /h=>//=; hauto qb:on use:ne_nf_ren, ne_nf. +Qed. + +Lemma η_nf_to_ne n (a0 a1 : PTm n) : + ERed'.R a0 a1 -> nf a0 -> ~~ ne a0 -> ne a1 -> + (a0 = PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) \/ + (a0 = PPair (PProj PL a1) (PProj PR a1)). +Proof. + move => h. + elim : n a0 a1 /h => n /=. + - sfirstorder use:ne_ered. + - hauto l:on use:ne_ered. + - scongruence use:ne_ered. + - hauto qb:on use:ne_ered, ne_nf. + - move => a b0 b1 h0 ih0 /andP [h1 h2] h3 /andP [h4 h5]. + have {h3} : ~~ ne a by sfirstorder b:on. + by move /negP. + - hauto lqb:on. + - sfirstorder b:on. + - scongruence b:on. +Qed. + +Lemma η_nf'' n (a b : PTm n) : ERed'.R a b -> nf b -> nf a \/ rtc RRed.R a b. +Proof. + move => h. + elim : n a b / h. + - move => n a. + case : a => //=. + * tauto. + * move => p hp. right. + apply rtc_once. + apply RRed.AbsCong. + apply RRed.AppAbs'. by asimpl. + * hauto lb:on use:ne_nf_ren. + * move => p p0 /andP [h0 h1]. + right. + (* violates SN *) + admit. + * move => p u h. + hauto lb:on use:ne_nf_ren. + - move => n a ha. + case : a ha => //=. + * tauto. + * move => p hp. right. + (* violates SN *) + admit. + * sfirstorder b:on. + * hauto lq:on ctrs:rtc,RRed.R. + * qauto b:on. + - move => n a0 a1 ha h0 /= h1. + specialize h0 with (1 := h1). + case : h0. tauto. + eauto using RReds.AbsCong. + - move => n a0 a1 b ha h /= /andP [h0 h1]. + have h2 : nf a1 by sfirstorder use:ne_nf. + have {}h := h h2. + case : h => h. + + have : ne a0 \/ ~~ ne a0 by sauto lq:on. + case; first by sfirstorder b:on. + move : η_nf_to_ne (ha) h h0; repeat move/[apply]. + case => ?; subst. + * simpl. + right. + apply rtc_once. + apply : RRed.AppAbs'. + by asimpl. + * simpl. + (* violates SN *) + admit. + + right. + hauto lq:on ctrs:rtc use:RReds.AppCong. + - move => n a b0 b1 h h0 /=. + move /andP => [h1 h2]. + have {h0} := h0 h2. + case => h3. + + sfirstorder b:on. + + right. + hauto lq:on ctrs:rtc use:RReds.AppCong. + - hauto lqb:on drew:off use:RReds.PairCong. + - hauto lqb:on drew:off use:RReds.PairCong. + - move => n p a0 a1 h0 h1 h2. + simpl in h2. + have : nf a1 by sfirstorder use:ne_nf. + move : h1 => /[apply]. + case=> h. + + have : ne a0 \/ ~~ ne a0 by sauto lq:on. + case;first by tauto. + move : η_nf_to_ne (h0) h h2; repeat move/[apply]. + case => ?. subst => //=. + * right. + (* violates SN *) + admit. + * right. + subst. + apply rtc_once. + sauto lq:on rew:off ctrs:RRed.R. + + hauto lq:on use:RReds.ProjCong. +Admitted. + +Lemma η_nf' n (a b : PTm n) : ERed'.R a b -> rtc ERed'.R (tstar a) (tstar b). +Proof. + move => h. + elim : n a b /h. + - move => n a /=. + set p := (X in (PAbs X)). + have : (exists a1, ren_PTm shift a = PAbs a1 /\ p = subst_PTm (scons (VarPTm var_zero) VarPTm) (tstar a1)) \/ + p = PApp (tstar (ren_PTm shift a)) (VarPTm var_zero) by hauto lq:on rew:off. + case. + + move => [a2 [+]]. + subst p. + case : a => //=. + move => p [h0] . subst => _. + rewrite TStar.renaming. asimpl. + sfirstorder. + + move => ->. + rewrite TStar.renaming. + hauto lq:on ctrs:ERed'.R, rtc. + - move => n a. + case : (tstar_proj n a). + + move => [_ h]. + rewrite TStar.pair. + rewrite !h. + hauto lq:on ctrs:ERed'.R, rtc. + + move => [a2][b0][?]. subst. + move => h. + rewrite TStar.pair. + rewrite !h. + sfirstorder. + - (* easy *) + eauto using EReds.AbsCong. + (* hard application cases *) + - admit. + - admit. + (* Trivial congruence cases *) + - move => n a0 a1 b ha iha. + hauto lq:on ctrs:rtc use:EReds.PairCong. + - hauto lq:on ctrs:rtc use:EReds.PairCong. + (* hard projection cases *) + - move => n p a0 a1 h0 h1. + case : (tstar_proj n a0). + + move => [ha0 ->]. + case : (tstar_proj n a1). + * move => [ha1 ->]. + (* Trivial by proj cong *) + hauto lq:on use:EReds.ProjCong. + * move => [a2][b0][?]. subst. + move => ->. + elim /ERed'.inv : h0 => //_. + ** move => a1 a3 ? *. subst. + (* Contradiction *) + admit. + ** hauto lqb:on. + ** hauto lqb:on. + ** hauto lqb:on. + + move => [a2][b0][?] ->. subst. + case : (tstar_proj n a1). + * move => [ha1 ->]. + simpl in h1. + inversion h0; subst. + ** hauto lq:on. + ** hauto lqb:on. + ** hauto lqb:on. + * move => [a0][b1][?]. subst => ->. + rewrite !TStar.pair in h1. + inversion h0; subst. + ** admit. + ** best. + +Lemma η_nf n (a b : PTm n) : ERed.R a b -> ERed.R (tstar a) (tstar b). +Proof. + move => h. + elim : n a b /h. + - move => n a0 a1 h h0 /=. + set p := (X in (PAbs X)). + have : (exists a1, ren_PTm shift a0 = PAbs a1 /\ p = subst_PTm (scons (VarPTm var_zero) VarPTm) (tstar a1)) \/ + p = PApp (tstar (ren_PTm shift a0)) (VarPTm var_zero) by hauto lq:on rew:off. + case. + + move => [a2 [+]]. + subst p. + case : a0 h h0 => //=. + move => p h0 h1 [?]. subst => _. + rewrite TStar.renaming. by asimpl. + + move => ->. + rewrite TStar.renaming. + hauto lq:on ctrs:ERed.R. + - move => n a0 a1 ha iha. + case : (tstar_proj n a0). + + move => [_ h]. + change (tstar (PPair (PProj PL a0) (PProj PR a0))) with + (PPair (tstar (PProj PL a0)) (tstar (PProj PR a0))). + rewrite !h. + hauto lq:on ctrs:ERed.R. + + move => [a2][b0][?]. subst. + move => h. + rewrite TStar.pair. + rewrite !h. + sfirstorder. + - hauto lq:on ctrs:ERed.R. + - admit. + - hauto lq:on ctrs:ERed.R. + - move => n p a0 a1 h0 h1. + case : (tstar_proj n a0). + + move => [ha0 ->]. + case : (tstar_proj n a1). + * move => [ha1 ->]. + hauto lq:on ctrs:ERed.R. + * move => [a2][b0][?]. subst. + move => ->. + elim /ERed.inv : h0 => //_. + ** move => a1 a3 ? *. subst. + (* Contradiction *) + admit. + ** hauto lqb:on. + ** hauto lqb:on. + + move => [a2][b0][?] ->. subst. + case : (tstar_proj n a1). + * move => [ha1 ->]. + inversion h0; subst. + ** admit. + ** scongruence. + * move => [a0][b1][?]. subst => ->. + rewrite !TStar.pair in h1. + inversion h1; subst. + ** + ** hauto lq:on. + + + + + move : b. + apply tstar_ind => {}n {}a => //=. + - hauto lq:on ctrs:ERed.R inv:ERed.R. + - move => a0 ? ih. subst. + move => b hb. + elim /ERed.inv : hb => //=_. + + move => a1 a2 ha [*]. subst. + simpl. + case : a1 ih ha => //=. + + + - move => a0 ? ih u. subst. + elim /ERed.inv => //=_. + + move => a1 a2 h [? ?]. subst. + have : ERed.R (PApp (ren_PTm shift a1) (VarPTm var_zero)) (PApp (ren_PTm shift u) (VarPTm var_zero)) + by hauto lq:on ctrs:ERed.R use:ERed.renaming. + move /ih. + + move => h0. simpl. + move => h. elim : n a b /h => n. - move => a0 a1 ha iha. - + simpl. + move => h. + move /iha : (h) {iha}. move : ha. clear. best. clear. - sfirstorder. From 61e743ee74461fa04f616e941f90deaa6c5e8b9c Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Tue, 28 Jan 2025 15:13:41 -0500 Subject: [PATCH 04/18] Add ne ered --- theories/fp_red.v | 52 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/theories/fp_red.v b/theories/fp_red.v index dbe7312..cb3bdb4 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -105,6 +105,58 @@ Module ERed. End ERed. +Module NeERed. + Inductive R_nonelim {n} : PTm n -> PTm n -> Prop := + (****************** Eta ***********************) + | AppEta A a0 a1 : + R_nonelim a0 a1 -> + R_nonelim (PAbs A (PApp (ren_PTm shift a0) (VarPTm var_zero))) a1 + | PairEta a0 a1 : + R_nonelim a0 a1 -> + R_nonelim (PPair (PProj PL a0) (PProj PR a0)) a1 + (*************** Congruence ********************) + | AbsCong A a0 a1 : + R_nonelim a0 a1 -> + R_nonelim (PAbs A a0) (PAbs A a1) + | AppCong a0 a1 b0 b1 : + R_elim a0 a1 -> + R_nonelim b0 b1 -> + R_nonelim (PApp a0 b0) (PApp a1 b1) + | PairCong a0 a1 b0 b1 : + R_nonelim a0 a1 -> + R_nonelim b0 b1 -> + R_nonelim (PPair a0 b0) (PPair a1 b1) + | ProjCong p a0 a1 : + R_elim a0 a1 -> + R_nonelim (PProj p a0) (PProj p a1) + | VarTm i : + R_nonelim (VarPTm i) (VarPTm i) + with R_elim {n} : PTm n -> PTm n -> Prop := + | NAbsCong A a0 a1 : + R_nonelim a0 a1 -> + R_elim (PAbs A a0) (PAbs A a1) + | NAppCong a0 a1 b0 b1 : + R_elim a0 a1 -> + R_nonelim b0 b1 -> + R_elim (PApp a0 b0) (PApp a1 b1) + | NPairCong a0 a1 b0 b1 : + R_nonelim a0 a1 -> + R_nonelim b0 b1 -> + R_elim (PPair a0 b0) (PPair a1 b1) + | NProjCong p a0 a1 : + R_elim a0 a1 -> + R_elim (PProj p a0) (PProj p a1) + | NVarTm i : + R_elim (VarPTm i) (VarPTm i). + + Scheme ered_elim_ind := Induction for R_elim Sort Prop + with ered_nonelim_ind := Induction for R_nonelim Sort Prop. + + Combined Scheme ered_mutual from ered_elim_ind, ered_nonelim_ind. + + +End NeERed. + Inductive SNe {n} : PTm n -> Prop := | N_Var i : SNe (VarPTm i) From 24693b8928989c823c5cd4ee75e1f465148e9f64 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Tue, 28 Jan 2025 16:07:52 -0500 Subject: [PATCH 05/18] Add "beta-free" eta contraction --- theories/fp_red.v | 142 +++++++++++++++++++++++++++++----------------- 1 file changed, 90 insertions(+), 52 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index cb3bdb4..4b6f624 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -105,58 +105,6 @@ Module ERed. End ERed. -Module NeERed. - Inductive R_nonelim {n} : PTm n -> PTm n -> Prop := - (****************** Eta ***********************) - | AppEta A a0 a1 : - R_nonelim a0 a1 -> - R_nonelim (PAbs A (PApp (ren_PTm shift a0) (VarPTm var_zero))) a1 - | PairEta a0 a1 : - R_nonelim a0 a1 -> - R_nonelim (PPair (PProj PL a0) (PProj PR a0)) a1 - (*************** Congruence ********************) - | AbsCong A a0 a1 : - R_nonelim a0 a1 -> - R_nonelim (PAbs A a0) (PAbs A a1) - | AppCong a0 a1 b0 b1 : - R_elim a0 a1 -> - R_nonelim b0 b1 -> - R_nonelim (PApp a0 b0) (PApp a1 b1) - | PairCong a0 a1 b0 b1 : - R_nonelim a0 a1 -> - R_nonelim b0 b1 -> - R_nonelim (PPair a0 b0) (PPair a1 b1) - | ProjCong p a0 a1 : - R_elim a0 a1 -> - R_nonelim (PProj p a0) (PProj p a1) - | VarTm i : - R_nonelim (VarPTm i) (VarPTm i) - with R_elim {n} : PTm n -> PTm n -> Prop := - | NAbsCong A a0 a1 : - R_nonelim a0 a1 -> - R_elim (PAbs A a0) (PAbs A a1) - | NAppCong a0 a1 b0 b1 : - R_elim a0 a1 -> - R_nonelim b0 b1 -> - R_elim (PApp a0 b0) (PApp a1 b1) - | NPairCong a0 a1 b0 b1 : - R_nonelim a0 a1 -> - R_nonelim b0 b1 -> - R_elim (PPair a0 b0) (PPair a1 b1) - | NProjCong p a0 a1 : - R_elim a0 a1 -> - R_elim (PProj p a0) (PProj p a1) - | NVarTm i : - R_elim (VarPTm i) (VarPTm i). - - Scheme ered_elim_ind := Induction for R_elim Sort Prop - with ered_nonelim_ind := Induction for R_nonelim Sort Prop. - - Combined Scheme ered_mutual from ered_elim_ind, ered_nonelim_ind. - - -End NeERed. - Inductive SNe {n} : PTm n -> Prop := | N_Var i : SNe (VarPTm i) @@ -564,6 +512,96 @@ Proof. elim : n a b /h=>//=; hauto qb:on use:ne_nf_ren, ne_nf. Qed. +Definition ishf {n} (a : PTm n) := + match a with + | PPair _ _ => true + | PAbs _ => true + | _ => false + end. + +Module NeERed. + Inductive R_nonelim {n} : PTm n -> PTm n -> Prop := + (****************** Eta ***********************) + | AppEta a0 a1 : + ~~ ishf a0 -> + R_elim a0 a1 -> + R_nonelim (PAbs (PApp (ren_PTm shift a0) (VarPTm var_zero))) a1 + | PairEta a0 a1 : + ~~ ishf a0 -> + R_elim a0 a1 -> + R_nonelim (PPair (PProj PL a0) (PProj PR a0)) a1 + (*************** Congruence ********************) + | AbsCong a0 a1 : + R_nonelim a0 a1 -> + R_nonelim (PAbs a0) (PAbs a1) + | AppCong a0 a1 b0 b1 : + R_elim a0 a1 -> + R_nonelim b0 b1 -> + R_nonelim (PApp a0 b0) (PApp a1 b1) + | PairCong a0 a1 b0 b1 : + R_nonelim a0 a1 -> + R_nonelim b0 b1 -> + R_nonelim (PPair a0 b0) (PPair a1 b1) + | ProjCong p a0 a1 : + R_elim a0 a1 -> + R_nonelim (PProj p a0) (PProj p a1) + | VarTm i : + R_nonelim (VarPTm i) (VarPTm i) + with R_elim {n} : PTm n -> PTm n -> Prop := + | NAbsCong a0 a1 : + R_nonelim a0 a1 -> + R_elim (PAbs a0) (PAbs a1) + | NAppCong a0 a1 b0 b1 : + R_elim a0 a1 -> + R_nonelim b0 b1 -> + R_elim (PApp a0 b0) (PApp a1 b1) + | NPairCong a0 a1 b0 b1 : + R_nonelim a0 a1 -> + R_nonelim b0 b1 -> + R_elim (PPair a0 b0) (PPair a1 b1) + | NProjCong p a0 a1 : + R_elim a0 a1 -> + R_elim (PProj p a0) (PProj p a1) + | NVarTm i : + R_elim (VarPTm i) (VarPTm i). + + Scheme ered_elim_ind := Induction for R_elim Sort Prop + with ered_nonelim_ind := Induction for R_nonelim Sort Prop. + + Combined Scheme ered_mutual from ered_elim_ind, ered_nonelim_ind. + + Lemma R_elim_nf n : + (forall (a b : PTm n), R_elim a b -> nf b -> nf a) /\ + (forall (a b : PTm n), R_nonelim a b -> nf b -> nf a). + Proof. + move : n. apply ered_mutual => n //=. + - move => a0 a1 b0 b1 h ih h' ih' /andP [h0 h1]. + have hb0 : nf b0 by eauto. + suff : ne a0 by qauto b:on. + qauto l:on inv:R_elim. + - hauto lb:on. + - hauto lq:on inv:R_elim. + - move => a0 a1 /negP ha' ha ih ha1. + have {ih} := ih ha1. + move => ha0. + suff : ne a0 by hauto lb:on drew:off use:ne_nf_ren. + inversion ha; subst => //=. + - move => a0 a1 /negP ha' ha ih ha1. + have {}ih := ih ha1. + have : ne a0 by hauto lq:on inv:PTm. + qauto lb:on. + - move => a0 a1 b0 b1 ha iha hb ihb /andP [h0 h1]. + have {}ihb := ihb h1. + have {}iha := iha ltac:(eauto using ne_nf). + suff : ne a0 by hauto lb:on. + move : ha h0. hauto lq:on inv:R_elim. + - hauto lb: on drew: off. + - hauto lq:on rew:off inv:R_elim. + Qed. + + +End NeERed. + Lemma η_nf_to_ne n (a0 a1 : PTm n) : ERed'.R a0 a1 -> nf a0 -> ~~ ne a0 -> ne a1 -> (a0 = PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) \/ From 3f3703990d5b333cc453cfd458aa0df83709bc15 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Tue, 28 Jan 2025 16:37:23 -0500 Subject: [PATCH 06/18] Save progress --- theories/fp_red.v | 49 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/theories/fp_red.v b/theories/fp_red.v index 4b6f624..6f7240c 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -283,6 +283,17 @@ Module RRed. Proof. move => ->. by apply AppAbs. Qed. + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). + Proof. + move => h. move : m ξ. + elim : n a b /h. + + move => n a b m ξ /=. + apply AppAbs'. by asimpl. + all : qauto ctrs:R. + Qed. + Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) : R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b. @@ -497,6 +508,13 @@ Module RReds. rtc RRed.R a0 a1 -> rtc RRed.R (PProj p a0) (PProj p a1). Proof. solve_s. Qed. + + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + rtc RRed.R a b -> rtc RRed.R (ren_PTm ξ a) (ren_PTm ξ b). + Proof. + move => h. move : m ξ. elim : a b /h; hauto lq:on ctrs:rtc use:RRed.renaming. + Qed. + End RReds. @@ -599,9 +617,40 @@ Module NeERed. - hauto lq:on rew:off inv:R_elim. Qed. + Lemma R_nonelim_nothf n (a b : PTm n) : + R_nonelim a b -> + ~~ ishf a -> + R_elim a b. + Proof. + move => h. elim : n a b /h=>//=; hauto lq:on ctrs:R_elim. + Qed. End NeERed. +Lemma bool_dec (a : bool) : a \/ ~~ a. +Proof. hauto lq:on inv:bool. Qed. + +Lemma η_split n (a0 a1 : PTm n) : + ERed.R a0 a1 -> + exists b, rtc RRed.R a0 b /\ NeERed.R_nonelim b a1. +Proof. + move => h. elim : n a0 a1 /h . + - move => n a0 a1 ha [b [ih0 ih1]]. + case : (bool_dec (ishf b)); cycle 1. + exists (PAbs (PApp (ren_PTm shift b) (VarPTm var_zero))). + split. apply RReds.AbsCong. apply RReds.AppCong; auto using rtc_refl. + by eauto using RReds.renaming. + apply NeERed.AppEta=>//. + sfirstorder use:NeERed.R_nonelim_nothf. + + case : b ih0 ih1 => //=. + + move => p ih0 ih1 _. + inversion ih1; subst. + + (* Violates SN *) + + admit. + + Lemma η_nf_to_ne n (a0 a1 : PTm n) : ERed'.R a0 a1 -> nf a0 -> ~~ ne a0 -> ne a1 -> (a0 = PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) \/ From 08b9395acb199f515b296562ad6d86b9a501f807 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Wed, 29 Jan 2025 13:37:54 -0500 Subject: [PATCH 07/18] Push some important cases of the split lemma --- theories/fp_red.v | 42 ++++++++++++++++++++++++++++++++++++++---- 1 file changed, 38 insertions(+), 4 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 6f7240c..08a4183 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -625,6 +625,12 @@ Module NeERed. move => h. elim : n a b /h=>//=; hauto lq:on ctrs:R_elim. Qed. + Lemma R_elim_nonelim n (a b : PTm n) : + R_elim a b -> + R_nonelim a b. + move => h. elim : n a b /h=>//=; hauto lq:on ctrs:R_nonelim. + Qed. + End NeERed. Lemma bool_dec (a : bool) : a \/ ~~ a. @@ -636,7 +642,7 @@ Lemma η_split n (a0 a1 : PTm n) : Proof. move => h. elim : n a0 a1 /h . - move => n a0 a1 ha [b [ih0 ih1]]. - case : (bool_dec (ishf b)); cycle 1. + case /orP : (orNb (ishf b)). exists (PAbs (PApp (ren_PTm shift b) (VarPTm var_zero))). split. apply RReds.AbsCong. apply RReds.AppCong; auto using rtc_refl. by eauto using RReds.renaming. @@ -645,11 +651,39 @@ Proof. case : b ih0 ih1 => //=. + move => p ih0 ih1 _. - inversion ih1; subst. - - (* Violates SN *) + set q := PAbs _. + suff : rtc RRed.R q (PAbs p) by sfirstorder. + subst q. + apply : rtc_r. + apply RReds.AbsCong. apply RReds.AppCong. + by eauto using RReds.renaming. + apply rtc_refl. + apply : RRed.AbsCong => /=. + apply RRed.AppAbs'. by asimpl. + (* violates SN *) + admit. + - move => n a0 a1 h. + move => [b [ih0 ih1]]. + case /orP : (orNb (ishf b)). + exists (PPair (PProj PL b) (PProj PR b)). + split. sfirstorder use:RReds.PairCong,RReds.ProjCong. + hauto lq:on ctrs:NeERed.R_nonelim use:NeERed.R_nonelim_nothf. + case : b ih0 ih1 => //=. + (* violates SN *) + + admit. + + move => t0 t1 ih0 h1 _. + exists (PPair t0 t1). + split => //=. + apply RReds.PairCong. + apply : rtc_r; eauto using RReds.ProjCong. + apply RRed.ProjPair. + apply : rtc_r; eauto using RReds.ProjCong. + apply RRed.ProjPair. + - move => n a0 a1 ha [b [ih0 ih1]]. + best ctrs:rtc use:NeERed.R_nonelim use:RReds.AbsCong. + +Admitted. Lemma η_nf_to_ne n (a0 a1 : PTm n) : ERed'.R a0 a1 -> nf a0 -> ~~ ne a0 -> ne a1 -> From 710b59fd8f89e76adc18d26a4328dc3278659cca Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Wed, 29 Jan 2025 14:01:35 -0500 Subject: [PATCH 08/18] Prove all application cases --- theories/fp_red.v | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 08a4183..3f439e7 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -680,9 +680,27 @@ Proof. apply RRed.ProjPair. apply : rtc_r; eauto using RReds.ProjCong. apply RRed.ProjPair. - - move => n a0 a1 ha [b [ih0 ih1]]. - best ctrs:rtc use:NeERed.R_nonelim use:RReds.AbsCong. + - hauto lq:on ctrs:NeERed.R_nonelim use:RReds.AbsCong. + - move => n a0 a1 b0 b1 ha [a2 [iha0 iha1]] hb [b2 [ihb0 ihb1]]. + case /orP : (orNb (ishf a2)) => [h|]. + + exists (PApp a2 b2). split; first by eauto using RReds.AppCong. + hauto lq:on ctrs:NeERed.R_nonelim use:NeERed.R_nonelim_nothf. + + case : a2 iha0 iha1 => //=. + * move => p h0 h1 _. + inversion h1; subst. + ** exists (PApp a2 b2). + split. + apply : rtc_r. + apply RReds.AppCong; eauto. + apply RRed.AppAbs'. by asimpl. + hauto lq:on ctrs:NeERed.R_nonelim. + ** hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.AppCong. + (* Impossible *) + * admit. + - hauto lq:on ctrs:NeERed.R_nonelim use:RReds.PairCong. + - move => n p a0 a1 ha [a2 [iha0 iha1]]. + - hauto lq:on ctrs:rtc, NeERed.R_nonelim. Admitted. Lemma η_nf_to_ne n (a0 a1 : PTm n) : From 5f619c0980fef1293d25cf4e9142a4c8e47bff0e Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Wed, 29 Jan 2025 15:52:05 -0500 Subject: [PATCH 09/18] Finish the split lemma up to strong normalization --- theories/fp_red.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/theories/fp_red.v b/theories/fp_red.v index 3f439e7..5578bf7 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -699,7 +699,23 @@ Proof. * admit. - hauto lq:on ctrs:NeERed.R_nonelim use:RReds.PairCong. - move => n p a0 a1 ha [a2 [iha0 iha1]]. + case /orP : (orNb (ishf a2)) => [h|]. + exists (PProj p a2). + split. eauto using RReds.ProjCong. + qauto l:on ctrs:NeERed.R_nonelim, NeERed.R_elim use:NeERed.R_nonelim_nothf. + case : a2 iha0 iha1 => //=. + + move => u iha0 iha1 _. + (* Impossible by SN *) + admit. + + move => u0 u1 iha0 iha1 _. + inversion iha1; subst. + * exists (PProj p a2). split. + apply : rtc_r. + apply RReds.ProjCong; eauto. + clear. hauto l:on inv:PTag. + hauto lq:on ctrs:NeERed.R_nonelim. + * hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.ProjCong. - hauto lq:on ctrs:rtc, NeERed.R_nonelim. Admitted. From 369bd55932661788b2c9f886d3629a95fb0a944b Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Wed, 29 Jan 2025 21:27:49 -0500 Subject: [PATCH 10/18] Add red sn preservation --- theories/fp_red.v | 135 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 135 insertions(+) diff --git a/theories/fp_red.v b/theories/fp_red.v index 5578bf7..3e3e387 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -324,7 +324,122 @@ Module RRed. End RRed. +Module RPar. + Inductive R {n} : PTm n -> PTm n -> Prop := + (****************** Beta ***********************) + | AppAbs a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PApp (PAbs a0) b0) (subst_PTm (scons b1 VarPTm) a1) + | ProjPair p a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PProj p (PPair a0 b0)) (if p is PL then a1 else b1) + + (*************** Congruence ********************) + | AbsCong a0 a1 : + R a0 a1 -> + R (PAbs a0) (PAbs a1) + | AppCong a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PApp a0 b0) (PApp a1 b1) + | PairCong a0 a1 b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (PPair a0 b0) (PPair a1 b1) + | ProjCong p a0 a1 : + R a0 a1 -> + R (PProj p a0) (PProj p a1) + | VarTm i : + R (VarPTm i) (VarPTm i). + + Lemma refl n (a : PTm n) : R a a. + Proof. + elim : n / a; hauto lq:on ctrs:R. + Qed. + + Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop. + + Lemma AppAbs' n a0 a1 (b0 b1 : PTm n) u : + u = (subst_PTm (scons b1 VarPTm) a1) -> + R a0 a1 -> + R b0 b1 -> + R (PApp (PAbs a0) b0) u. + Proof. move => ->. apply AppAbs. Qed. + + Lemma ProjPair' n p u (a0 a1 b0 b1 : PTm n) : + u = (if p is PL then a1 else b1) -> + R a0 a1 -> + R b0 b1 -> + R (PProj p (PPair a0 b0)) u. + Proof. move => ->. apply ProjPair. Qed. + + Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). + Proof. + move => h. move : m ξ. + elim : n a b /h. + + move => n a0 a1 b0 b1 ha iha hb ihb m ξ /=. + eapply AppAbs'; eauto. by asimpl. + all : qauto ctrs:R use:ProjPair'. + Qed. + + Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> PTm m) (ξ : fin m -> fin p) : + (forall i, R (ρ0 i) (ρ1 i)) -> + (forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ1) i)). + Proof. eauto using renaming. Qed. + + Lemma morphing_ext n m (ρ0 ρ1 : fin n -> PTm m) a b : + R a b -> + (forall i, R (ρ0 i) (ρ1 i)) -> + (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)). + Proof. hauto q:on inv:option. Qed. + + Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) : + (forall i, R (ρ0 i) (ρ1 i)) -> + (forall i, R (up_PTm_PTm ρ0 i) (up_PTm_PTm ρ1 i)). + Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_PTm_PTm. Qed. + + Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) : + (forall i, R (ρ0 i) (ρ1 i)) -> + R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b). + Proof. + move => + h. move : m ρ0 ρ1. elim : n a b / h => n. + move => a0 a1 b0 b1 ha iha hb ihb m ρ0 ρ1 hρ /=. + eapply AppAbs'; eauto; cycle 1. sfirstorder use:morphing_up. + by asimpl. + all : hauto lq:on ctrs:R use:morphing_up, ProjPair'. + Qed. + + Lemma substing n m (a : PTm n) b (ρ : fin n -> PTm m) : + R a b -> + R (subst_PTm ρ a) (subst_PTm ρ b). + Proof. + hauto l:on use:morphing, refl. + Qed. + +End RPar. + +Lemma red_sn_preservation n : + (forall (a : PTm n) (s : SNe a), forall b, RPar.R a b -> SNe b) /\ + (forall (a : PTm n) (s : SN a), forall b, RPar.R a b -> SN b) /\ + (forall (a b : PTm n) (_ : TRedSN a b), forall c, RPar.R a c -> exists d, TRedSN' c d /\ RPar.R b d). +Proof. + move : n. apply sn_mutual => n. + - hauto l:on inv:RPar.R. + - qauto l:on inv:RPar.R,SNe,SN ctrs:SNe. + - hauto lq:on inv:RPar.R, SNe ctrs:SNe. + - qauto l:on ctrs:SN inv:RPar.R. + - hauto lq:on ctrs:SN inv:RPar.R. + - hauto lq:on ctrs:SN. + - hauto q:on ctrs:SN inv:SN, TRedSN'. + - + - admit. + - sauto q:on. + - Function tstar {n} (a : PTm n) := match a with @@ -633,6 +748,26 @@ Module NeERed. End NeERed. +Module Type NoForbid. + Parameter P : forall n, PTm n -> Prop. + Arguments P {n}. + + Axiom P_ERed : forall n (a b : PTm n), ERed.R a b -> P a -> P b. + Axiom P_RRed : forall n (a b : PTm n), RRed.R a b -> P a -> P b. + Axiom P_AppPair : forall n (a b c : PTm n), ~ P (PApp (PPair a b) c). + Axiom P_ProjAbs : forall n p (a : PTm (S n)), ~ P (PProj p (PAbs a)). + +End NoForbid. + +Module SN_NoForbid : NoForbid. + Definition P := @SN. + Arguments P {n}. + + Lemma P_ERed : forall n (a b : PTm n), ERed.R a b -> P a -> P b. + Proof. sfirstorder use:ered_sn_preservation. Qed. + + Lemma P_RRed : forall n (a b : PTm n), RRed.R a b -> P a -> P b. + Lemma bool_dec (a : bool) : a \/ ~~ a. Proof. hauto lq:on inv:bool. Qed. From 99b5e87ea304a375991de957235ecbb76bb8599d Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Wed, 29 Jan 2025 22:09:08 -0500 Subject: [PATCH 11/18] Finish red sn preservation --- theories/fp_red.v | 43 ++++++++++++++++++++++++++++++++----------- 1 file changed, 32 insertions(+), 11 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 3e3e387..2657781 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -96,13 +96,6 @@ Module ERed. all : hauto lq:on ctrs:R use:morphing_up. Qed. - Lemma substing n m (a : PTm n) b (ρ : fin n -> PTm m) : - R a b -> - R (subst_PTm ρ a) (subst_PTm ρ b). - Proof. - hauto l:on use:morphing, refl. - Qed. - End ERed. Inductive SNe {n} : PTm n -> Prop := @@ -147,6 +140,8 @@ with TRedSN {n} : PTm n -> PTm n -> Prop := TRedSN a b -> TRedSN (PProj p a) (PProj p b). +Derive Dependent Inversion tred_inv with (forall n (a b : PTm n), TRedSN a b) Sort Prop. + Scheme sne_ind := Induction for SNe Sort Prop with sn_ind := Induction for SN Sort Prop with sred_ind := Induction for TRedSN Sort Prop. @@ -421,6 +416,16 @@ Module RPar. hauto l:on use:morphing, refl. Qed. + + Lemma cong n (a0 a1 : PTm (S n)) b0 b1 : + R a0 a1 -> + R b0 b1 -> + R (subst_PTm (scons b0 VarPTm) a0) (subst_PTm (scons b1 VarPTm) a1). + Proof. + move => h0 h1. apply morphing=>//. + hauto q:on inv:option ctrs:R. + Qed. + End RPar. Lemma red_sn_preservation n : @@ -436,10 +441,26 @@ Proof. - hauto lq:on ctrs:SN inv:RPar.R. - hauto lq:on ctrs:SN. - hauto q:on ctrs:SN inv:SN, TRedSN'. - - - - admit. - - sauto q:on. - - + - move => a b ha iha hb ihb. + elim /RPar.inv : ihb => //=_. + + move => a0 a1 b0 b1 ha0 hb0 [*]. subst. + eauto using RPar.cong, T_Refl. + + move => a0 a1 b0 b1 h0 h1 [*]. subst. + elim /RPar.inv : h0 => //=_. + move => a0 a2 h [*]. subst. + eexists. split. apply T_Once. hauto lq:on ctrs:TRedSN. + eauto using RPar.cong. + - move => a0 a1 b ha iha c. + elim /RPar.inv => //=_. + + qauto l:on inv:TRedSN. + + move => a2 a3 b0 b1 h0 h1 [*]. subst. + have {}/iha := h0. + move => [d [iha0 iha1]]. + hauto lq:on rew:off inv:TRedSN' ctrs:TRedSN, RPar.R, TRedSN'. + - hauto lq:on inv:RPar.R ctrs:RPar.R, TRedSN', TRedSN. + - hauto lq:on inv:RPar.R ctrs:RPar.R, TRedSN', TRedSN. + - sauto. +Qed. Function tstar {n} (a : PTm n) := match a with From a47d69f42744884c74dbfb9940af768b595c2e48 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Wed, 29 Jan 2025 22:14:01 -0500 Subject: [PATCH 12/18] More no forbid --- theories/fp_red.v | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/theories/fp_red.v b/theories/fp_red.v index 2657781..9c68907 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -426,6 +426,12 @@ Module RPar. hauto q:on inv:option ctrs:R. Qed. + Lemma FromRRed n (a b : PTm n) : + RRed.R a b -> RPar.R a b. + Proof. + induction 1; qauto l:on use:RPar.refl ctrs:RPar.R. + Qed. + End RPar. Lemma red_sn_preservation n : @@ -788,6 +794,11 @@ Module SN_NoForbid : NoForbid. Proof. sfirstorder use:ered_sn_preservation. Qed. Lemma P_RRed : forall n (a b : PTm n), RRed.R a b -> P a -> P b. + Proof. hauto q:on use:red_sn_preservation, RPar.FromRRed. Qed. + + Lemma P_AppPair : forall n (a b c : PTm n), ~ P (PApp (PPair a b) c). + Proof. + Lemma bool_dec (a : bool) : a \/ ~~ a. Proof. hauto lq:on inv:bool. Qed. From aa2c2ca151dc919e3ef2c6ca3b5b8645576c23af Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Wed, 29 Jan 2025 22:25:14 -0500 Subject: [PATCH 13/18] Add lemmas that bad forms are impossible --- theories/fp_red.v | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 9c68907..30a8823 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -142,13 +142,32 @@ with TRedSN {n} : PTm n -> PTm n -> Prop := Derive Dependent Inversion tred_inv with (forall n (a b : PTm n), TRedSN a b) Sort Prop. +Lemma PProjAbs_imp n p (a : PTm (S n)) : + ~ SN (PProj p (PAbs a)). +Proof. + move E : (PProj p (PAbs a)) => u hu. + move : p a E. + elim : n u / hu=>//=. + hauto lq:on inv:SNe. + hauto lq:on inv:TRedSN. +Qed. + +Lemma PProjPair_imp n (a b0 b1 : PTm n ) : + ~ SN (PApp (PPair b0 b1) a). +Proof. + move E : (PApp (PPair b0 b1) a) => u hu. + move : a b0 b1 E. + elim : n u / hu=>//=. + hauto lq:on inv:SNe. + hauto lq:on inv:TRedSN. +Qed. + Scheme sne_ind := Induction for SNe Sort Prop with sn_ind := Induction for SN Sort Prop with sred_ind := Induction for TRedSN Sort Prop. Combined Scheme sn_mutual from sne_ind, sn_ind, sred_ind. - Fixpoint ne {n} (a : PTm n) := match a with | VarPTm i => true @@ -797,8 +816,12 @@ Module SN_NoForbid : NoForbid. Proof. hauto q:on use:red_sn_preservation, RPar.FromRRed. Qed. Lemma P_AppPair : forall n (a b c : PTm n), ~ P (PApp (PPair a b) c). - Proof. + Proof. sfirstorder use:PProjPair_imp. Qed. + Lemma P_ProjAbs : forall n p (a : PTm (S n)), ~ P (PProj p (PAbs a)). + Proof. sfirstorder use:PProjAbs_imp. Qed. + +End SN_NoForbid. Lemma bool_dec (a : bool) : a \/ ~~ a. Proof. hauto lq:on inv:bool. Qed. @@ -905,6 +928,8 @@ Proof. - scongruence b:on. Qed. + + Lemma η_nf'' n (a b : PTm n) : ERed'.R a b -> nf b -> nf a \/ rtc RRed.R a b. Proof. move => h. From 20eef7801489fee12774d5e881b7bc29a81b07de Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Wed, 29 Jan 2025 22:59:57 -0500 Subject: [PATCH 14/18] Finish one example case of violate sn --- theories/fp_red.v | 221 +++++++++++++++++++++++++++++----------------- 1 file changed, 140 insertions(+), 81 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 30a8823..4978c34 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -1,5 +1,6 @@ From Ltac2 Require Ltac2. Import Ltac2.Notations. + Import Ltac2.Control. Require Import ssreflect ssrbool. Require Import FunInd. @@ -803,8 +804,34 @@ Module Type NoForbid. Axiom P_AppPair : forall n (a b c : PTm n), ~ P (PApp (PPair a b) c). Axiom P_ProjAbs : forall n p (a : PTm (S n)), ~ P (PProj p (PAbs a)). + Axiom P_AppInv : forall n (a b : PTm n), P (PApp a b) -> P a /\ P b. + Axiom P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a. + Axiom P_renaming : forall n m (ξ : fin n -> fin m) a , P (ren_PTm ξ a) <-> P a. + End NoForbid. +Module Type NoForbid_FactSig (M : NoForbid). + + Axiom P_EReds : forall n (a b : PTm n), rtc ERed.R a b -> M.P a -> M.P b. + + Axiom P_RReds : forall n (a b : PTm n), rtc RRed.R a b -> M.P a -> M.P b. + +End NoForbid_FactSig. + +Module NoForbid_Fact (M : NoForbid) : NoForbid_FactSig M. + Import M. + + Lemma P_EReds : forall n (a b : PTm n), rtc ERed.R a b -> P a -> P b. + Proof. + induction 1; eauto using P_ERed, rtc_l, rtc_refl. + Qed. + + Lemma P_RReds : forall n (a b : PTm n), rtc RRed.R a b -> P a -> P b. + Proof. + induction 1; eauto using P_RRed, rtc_l, rtc_refl. + Qed. +End NoForbid_Fact. + Module SN_NoForbid : NoForbid. Definition P := @SN. Arguments P {n}. @@ -821,93 +848,125 @@ Module SN_NoForbid : NoForbid. Lemma P_ProjAbs : forall n p (a : PTm (S n)), ~ P (PProj p (PAbs a)). Proof. sfirstorder use:PProjAbs_imp. Qed. + Lemma P_AppInv : forall n (a b : PTm n), P (PApp a b) -> P a /\ P b. + Admitted. + + Lemma P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a. + Proof. + move => n a. move E : (PAbs a) => u h. + move : E. move : a. + induction h; sauto lq:on rew:off. + Qed. + + Lemma P_renaming : forall n m (ξ : fin n -> fin m) a , P (ren_PTm ξ a) <-> P a. + Admitted. + End SN_NoForbid. -Lemma bool_dec (a : bool) : a \/ ~~ a. -Proof. hauto lq:on inv:bool. Qed. +Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). + Import M MFacts. + #[local]Hint Resolve P_ERed P_RRed P_AppPair P_ProjAbs : forbid. -Lemma η_split n (a0 a1 : PTm n) : - ERed.R a0 a1 -> - exists b, rtc RRed.R a0 b /\ NeERed.R_nonelim b a1. -Proof. - move => h. elim : n a0 a1 /h . - - move => n a0 a1 ha [b [ih0 ih1]]. - case /orP : (orNb (ishf b)). - exists (PAbs (PApp (ren_PTm shift b) (VarPTm var_zero))). - split. apply RReds.AbsCong. apply RReds.AppCong; auto using rtc_refl. - by eauto using RReds.renaming. - apply NeERed.AppEta=>//. - sfirstorder use:NeERed.R_nonelim_nothf. - - case : b ih0 ih1 => //=. - + move => p ih0 ih1 _. - set q := PAbs _. - suff : rtc RRed.R q (PAbs p) by sfirstorder. - subst q. - apply : rtc_r. - apply RReds.AbsCong. apply RReds.AppCong. + Lemma η_split n (a0 a1 : PTm n) : + ERed.R a0 a1 -> + P a0 -> + exists b, rtc RRed.R a0 b /\ NeERed.R_nonelim b a1. + Proof. + move => h. elim : n a0 a1 /h . + - move => n a0 a1 ha ih /[dup] hP. + move /P_AbsInv /P_AppInv => [/P_renaming ha0 _]. + have {ih} := ih ha0. + move => [b [ih0 ih1]]. + case /orP : (orNb (ishf b)). + exists (PAbs (PApp (ren_PTm shift b) (VarPTm var_zero))). + split. apply RReds.AbsCong. apply RReds.AppCong; auto using rtc_refl. by eauto using RReds.renaming. - apply rtc_refl. - apply : RRed.AbsCong => /=. - apply RRed.AppAbs'. by asimpl. - (* violates SN *) - + admit. - - move => n a0 a1 h. - move => [b [ih0 ih1]]. - case /orP : (orNb (ishf b)). - exists (PPair (PProj PL b) (PProj PR b)). - split. sfirstorder use:RReds.PairCong,RReds.ProjCong. - hauto lq:on ctrs:NeERed.R_nonelim use:NeERed.R_nonelim_nothf. + apply NeERed.AppEta=>//. + sfirstorder use:NeERed.R_nonelim_nothf. - case : b ih0 ih1 => //=. - (* violates SN *) - + admit. - + move => t0 t1 ih0 h1 _. - exists (PPair t0 t1). - split => //=. - apply RReds.PairCong. - apply : rtc_r; eauto using RReds.ProjCong. - apply RRed.ProjPair. - apply : rtc_r; eauto using RReds.ProjCong. - apply RRed.ProjPair. - - hauto lq:on ctrs:NeERed.R_nonelim use:RReds.AbsCong. - - move => n a0 a1 b0 b1 ha [a2 [iha0 iha1]] hb [b2 [ihb0 ihb1]]. - case /orP : (orNb (ishf a2)) => [h|]. - + exists (PApp a2 b2). split; first by eauto using RReds.AppCong. - hauto lq:on ctrs:NeERed.R_nonelim use:NeERed.R_nonelim_nothf. - + case : a2 iha0 iha1 => //=. - * move => p h0 h1 _. - inversion h1; subst. - ** exists (PApp a2 b2). - split. - apply : rtc_r. - apply RReds.AppCong; eauto. - apply RRed.AppAbs'. by asimpl. - hauto lq:on ctrs:NeERed.R_nonelim. - ** hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.AppCong. - (* Impossible *) - * admit. - - hauto lq:on ctrs:NeERed.R_nonelim use:RReds.PairCong. - - move => n p a0 a1 ha [a2 [iha0 iha1]]. - case /orP : (orNb (ishf a2)) => [h|]. - exists (PProj p a2). - split. eauto using RReds.ProjCong. - qauto l:on ctrs:NeERed.R_nonelim, NeERed.R_elim use:NeERed.R_nonelim_nothf. - - case : a2 iha0 iha1 => //=. - + move => u iha0 iha1 _. - (* Impossible by SN *) - admit. - + move => u0 u1 iha0 iha1 _. - inversion iha1; subst. - * exists (PProj p a2). split. + case : b ih0 ih1 => //=. + + move => p ih0 ih1 _. + set q := PAbs _. + suff : rtc RRed.R q (PAbs p) by sfirstorder. + subst q. apply : rtc_r. - apply RReds.ProjCong; eauto. - clear. hauto l:on inv:PTag. - hauto lq:on ctrs:NeERed.R_nonelim. - * hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.ProjCong. - - hauto lq:on ctrs:rtc, NeERed.R_nonelim. -Admitted. + apply RReds.AbsCong. apply RReds.AppCong. + by eauto using RReds.renaming. + apply rtc_refl. + apply : RRed.AbsCong => /=. + apply RRed.AppAbs'. by asimpl. + (* violates SN *) + + move => p p0 h. exfalso. + have : P (PApp (ren_PTm shift a0) (VarPTm var_zero)) + by sfirstorder use:P_AbsInv. + + have : rtc RRed.R (PApp (ren_PTm shift a0) (VarPTm var_zero)) + (PApp (ren_PTm shift (PPair p p0)) (VarPTm var_zero)) + by hauto lq:on use:RReds.AppCong, RReds.renaming, rtc_refl. + + move : P_RReds. repeat move/[apply] => /=. + hauto l:on use:P_AppPair. + - move => n a0 a1 h. + move => [b [ih0 ih1]]. + case /orP : (orNb (ishf b)). + exists (PPair (PProj PL b) (PProj PR b)). + split. sfirstorder use:RReds.PairCong,RReds.ProjCong. + hauto lq:on ctrs:NeERed.R_nonelim use:NeERed.R_nonelim_nothf. + + case : b ih0 ih1 => //=. + (* violates SN *) + + admit. + + move => t0 t1 ih0 h1 _. + exists (PPair t0 t1). + split => //=. + apply RReds.PairCong. + apply : rtc_r; eauto using RReds.ProjCong. + apply RRed.ProjPair. + apply : rtc_r; eauto using RReds.ProjCong. + apply RRed.ProjPair. + - hauto lq:on ctrs:NeERed.R_nonelim use:RReds.AbsCong. + - move => n a0 a1 b0 b1 ha [a2 [iha0 iha1]] hb [b2 [ihb0 ihb1]]. + case /orP : (orNb (ishf a2)) => [h|]. + + exists (PApp a2 b2). split; first by eauto using RReds.AppCong. + hauto lq:on ctrs:NeERed.R_nonelim use:NeERed.R_nonelim_nothf. + + case : a2 iha0 iha1 => //=. + * move => p h0 h1 _. + inversion h1; subst. + ** exists (PApp a2 b2). + split. + apply : rtc_r. + apply RReds.AppCong; eauto. + apply RRed.AppAbs'. by asimpl. + hauto lq:on ctrs:NeERed.R_nonelim. + ** hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.AppCong. + (* Impossible *) + * admit. + - hauto lq:on ctrs:NeERed.R_nonelim use:RReds.PairCong. + - move => n p a0 a1 ha [a2 [iha0 iha1]]. + case /orP : (orNb (ishf a2)) => [h|]. + exists (PProj p a2). + split. eauto using RReds.ProjCong. + qauto l:on ctrs:NeERed.R_nonelim, NeERed.R_elim use:NeERed.R_nonelim_nothf. + + case : a2 iha0 iha1 => //=. + + move => u iha0 iha1 _. + (* Impossible by SN *) + admit. + + move => u0 u1 iha0 iha1 _. + inversion iha1; subst. + * exists (PProj p a2). split. + apply : rtc_r. + apply RReds.ProjCong; eauto. + clear. hauto l:on inv:PTag. + hauto lq:on ctrs:NeERed.R_nonelim. + * hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.ProjCong. + - hauto lq:on ctrs:rtc, NeERed.R_nonelim. + Admitted. + + + +End UniqueNF. + Lemma η_nf_to_ne n (a0 a1 : PTm n) : ERed'.R a0 a1 -> nf a0 -> ~~ ne a0 -> ne a1 -> From e4c2bd39db0861fd22f7c65798594ec4e16a81d2 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Wed, 29 Jan 2025 23:41:38 -0500 Subject: [PATCH 15/18] Finish the eta split proof without any admits --- theories/fp_red.v | 385 +++++----------------------------------------- 1 file changed, 37 insertions(+), 348 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 4978c34..58d711d 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -578,34 +578,6 @@ Module ERed'. (forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ1) i)). Proof. eauto using renaming. Qed. - (* Lemma morphing_ext n m (ρ0 ρ1 : fin n -> PTm m) a b : *) - (* R a b -> *) - (* (forall i, R (ρ0 i) (ρ1 i)) -> *) - (* (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)). *) - (* Proof. hauto q:on inv:option. Qed. *) - - (* Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) : *) - (* (forall i, R (ρ0 i) (ρ1 i)) -> *) - (* (forall i, R (up_PTm_PTm ρ0 i) (up_PTm_PTm ρ1 i)). *) - (* Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_PTm_PTm. Qed. *) - - (* Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) : *) - (* (forall i, R (ρ0 i) (ρ1 i)) -> *) - (* R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b). *) - (* Proof. *) - (* move => + h. move : m ρ0 ρ1. elim : n a b / h => n. *) - (* move => a0 a1 ha iha m ρ0 ρ1 hρ /=. *) - (* eapply AppEta'; eauto. by asimpl. *) - (* all : hauto lq:on ctrs:R use:morphing_up. *) - (* Qed. *) - - (* Lemma substing n m (a : PTm n) b (ρ : fin n -> PTm m) : *) - (* R a b -> *) - (* R (subst_PTm ρ a) (subst_PTm ρ b). *) - (* Proof. *) - (* hauto l:on use:morphing, refl. *) - (* Qed. *) - End ERed'. Module EReds. @@ -806,6 +778,8 @@ Module Type NoForbid. Axiom P_AppInv : forall n (a b : PTm n), P (PApp a b) -> P a /\ P b. Axiom P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a. + Axiom P_PairInv : forall n (a b : PTm n), P (PPair a b) -> P a /\ P b. + Axiom P_ProjInv : forall n p (a : PTm n), P (PProj p a) -> P a. Axiom P_renaming : forall n m (ξ : fin n -> fin m) a , P (ren_PTm ξ a) <-> P a. End NoForbid. @@ -851,6 +825,13 @@ Module SN_NoForbid : NoForbid. Lemma P_AppInv : forall n (a b : PTm n), P (PApp a b) -> P a /\ P b. Admitted. + Lemma P_PairInv : forall n (a b : PTm n), P (PPair a b) -> P a /\ P b. + move => n a b. move E : (PPair a b) => u h. + move : a b E. elim : n u / h; sauto lq:on rew:off. Qed. + + Lemma P_ProjInv : forall n p (a : PTm n), P (PProj p a) -> P a. + Admitted. + Lemma P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a. Proof. move => n a. move E : (PAbs a) => u h. @@ -906,7 +887,9 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). move : P_RReds. repeat move/[apply] => /=. hauto l:on use:P_AppPair. - - move => n a0 a1 h. + - move => n a0 a1 h ih /[dup] hP. + move /P_PairInv => [/P_ProjInv + _]. + move : ih => /[apply]. move => [b [ih0 ih1]]. case /orP : (orNb (ishf b)). exists (PPair (PProj PL b) (PProj PR b)). @@ -915,7 +898,12 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). case : b ih0 ih1 => //=. (* violates SN *) - + admit. + + move => p ?. exfalso. + have {}hP : P (PProj PL a0) by sfirstorder use:P_PairInv. + have : rtc RRed.R (PProj PL a0) (PProj PL (PAbs p)) + by eauto using RReds.ProjCong. + move : P_RReds hP. repeat move/[apply] => /=. + sfirstorder use:P_ProjAbs. + move => t0 t1 ih0 h1 _. exists (PPair t0 t1). split => //=. @@ -924,8 +912,11 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). apply RRed.ProjPair. apply : rtc_r; eauto using RReds.ProjCong. apply RRed.ProjPair. - - hauto lq:on ctrs:NeERed.R_nonelim use:RReds.AbsCong. - - move => n a0 a1 b0 b1 ha [a2 [iha0 iha1]] hb [b2 [ihb0 ihb1]]. + - hauto lq:on ctrs:NeERed.R_nonelim use:RReds.AbsCong, P_AbsInv. + - move => n a0 a1 b0 b1 ha iha hb ihb. + move => /[dup] hP /P_AppInv [hP0 hP1]. + have {iha} [a2 [iha0 iha1]] := iha hP0. + have {ihb} [b2 [ihb0 ihb1]] := ihb hP1. case /orP : (orNb (ishf a2)) => [h|]. + exists (PApp a2 b2). split; first by eauto using RReds.AppCong. hauto lq:on ctrs:NeERed.R_nonelim use:NeERed.R_nonelim_nothf. @@ -940,18 +931,25 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). hauto lq:on ctrs:NeERed.R_nonelim. ** hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.AppCong. (* Impossible *) - * admit. - - hauto lq:on ctrs:NeERed.R_nonelim use:RReds.PairCong. - - move => n p a0 a1 ha [a2 [iha0 iha1]]. + * move => u0 u1 h. exfalso. + have : rtc RRed.R (PApp a0 b0) (PApp (PPair u0 u1) b0) + by hauto lq:on ctrs:rtc use:RReds.AppCong. + move : P_RReds hP; repeat move/[apply]. + sfirstorder use:P_AppPair. + - hauto lq:on ctrs:NeERed.R_nonelim use:RReds.PairCong, P_PairInv. + - move => n p a0 a1 ha ih /[dup] hP /P_ProjInv. + move : ih => /[apply]. move => [a2 [iha0 iha1]]. case /orP : (orNb (ishf a2)) => [h|]. exists (PProj p a2). split. eauto using RReds.ProjCong. qauto l:on ctrs:NeERed.R_nonelim, NeERed.R_elim use:NeERed.R_nonelim_nothf. case : a2 iha0 iha1 => //=. - + move => u iha0 iha1 _. - (* Impossible by SN *) - admit. + + move => u iha0. exfalso. + have : rtc RRed.R (PProj p a0) (PProj p (PAbs u)) + by sfirstorder use:RReds.ProjCong ctrs:rtc. + move : P_RReds hP. repeat move/[apply]. + sfirstorder use:P_ProjAbs. + move => u0 u1 iha0 iha1 _. inversion iha1; subst. * exists (PProj p a2). split. @@ -961,13 +959,10 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M). hauto lq:on ctrs:NeERed.R_nonelim. * hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.ProjCong. - hauto lq:on ctrs:rtc, NeERed.R_nonelim. - Admitted. - - + Qed. End UniqueNF. - Lemma η_nf_to_ne n (a0 a1 : PTm n) : ERed'.R a0 a1 -> nf a0 -> ~~ ne a0 -> ne a1 -> (a0 = PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) \/ @@ -986,309 +981,3 @@ Proof. - sfirstorder b:on. - scongruence b:on. Qed. - - - -Lemma η_nf'' n (a b : PTm n) : ERed'.R a b -> nf b -> nf a \/ rtc RRed.R a b. -Proof. - move => h. - elim : n a b / h. - - move => n a. - case : a => //=. - * tauto. - * move => p hp. right. - apply rtc_once. - apply RRed.AbsCong. - apply RRed.AppAbs'. by asimpl. - * hauto lb:on use:ne_nf_ren. - * move => p p0 /andP [h0 h1]. - right. - (* violates SN *) - admit. - * move => p u h. - hauto lb:on use:ne_nf_ren. - - move => n a ha. - case : a ha => //=. - * tauto. - * move => p hp. right. - (* violates SN *) - admit. - * sfirstorder b:on. - * hauto lq:on ctrs:rtc,RRed.R. - * qauto b:on. - - move => n a0 a1 ha h0 /= h1. - specialize h0 with (1 := h1). - case : h0. tauto. - eauto using RReds.AbsCong. - - move => n a0 a1 b ha h /= /andP [h0 h1]. - have h2 : nf a1 by sfirstorder use:ne_nf. - have {}h := h h2. - case : h => h. - + have : ne a0 \/ ~~ ne a0 by sauto lq:on. - case; first by sfirstorder b:on. - move : η_nf_to_ne (ha) h h0; repeat move/[apply]. - case => ?; subst. - * simpl. - right. - apply rtc_once. - apply : RRed.AppAbs'. - by asimpl. - * simpl. - (* violates SN *) - admit. - + right. - hauto lq:on ctrs:rtc use:RReds.AppCong. - - move => n a b0 b1 h h0 /=. - move /andP => [h1 h2]. - have {h0} := h0 h2. - case => h3. - + sfirstorder b:on. - + right. - hauto lq:on ctrs:rtc use:RReds.AppCong. - - hauto lqb:on drew:off use:RReds.PairCong. - - hauto lqb:on drew:off use:RReds.PairCong. - - move => n p a0 a1 h0 h1 h2. - simpl in h2. - have : nf a1 by sfirstorder use:ne_nf. - move : h1 => /[apply]. - case=> h. - + have : ne a0 \/ ~~ ne a0 by sauto lq:on. - case;first by tauto. - move : η_nf_to_ne (h0) h h2; repeat move/[apply]. - case => ?. subst => //=. - * right. - (* violates SN *) - admit. - * right. - subst. - apply rtc_once. - sauto lq:on rew:off ctrs:RRed.R. - + hauto lq:on use:RReds.ProjCong. -Admitted. - -Lemma η_nf' n (a b : PTm n) : ERed'.R a b -> rtc ERed'.R (tstar a) (tstar b). -Proof. - move => h. - elim : n a b /h. - - move => n a /=. - set p := (X in (PAbs X)). - have : (exists a1, ren_PTm shift a = PAbs a1 /\ p = subst_PTm (scons (VarPTm var_zero) VarPTm) (tstar a1)) \/ - p = PApp (tstar (ren_PTm shift a)) (VarPTm var_zero) by hauto lq:on rew:off. - case. - + move => [a2 [+]]. - subst p. - case : a => //=. - move => p [h0] . subst => _. - rewrite TStar.renaming. asimpl. - sfirstorder. - + move => ->. - rewrite TStar.renaming. - hauto lq:on ctrs:ERed'.R, rtc. - - move => n a. - case : (tstar_proj n a). - + move => [_ h]. - rewrite TStar.pair. - rewrite !h. - hauto lq:on ctrs:ERed'.R, rtc. - + move => [a2][b0][?]. subst. - move => h. - rewrite TStar.pair. - rewrite !h. - sfirstorder. - - (* easy *) - eauto using EReds.AbsCong. - (* hard application cases *) - - admit. - - admit. - (* Trivial congruence cases *) - - move => n a0 a1 b ha iha. - hauto lq:on ctrs:rtc use:EReds.PairCong. - - hauto lq:on ctrs:rtc use:EReds.PairCong. - (* hard projection cases *) - - move => n p a0 a1 h0 h1. - case : (tstar_proj n a0). - + move => [ha0 ->]. - case : (tstar_proj n a1). - * move => [ha1 ->]. - (* Trivial by proj cong *) - hauto lq:on use:EReds.ProjCong. - * move => [a2][b0][?]. subst. - move => ->. - elim /ERed'.inv : h0 => //_. - ** move => a1 a3 ? *. subst. - (* Contradiction *) - admit. - ** hauto lqb:on. - ** hauto lqb:on. - ** hauto lqb:on. - + move => [a2][b0][?] ->. subst. - case : (tstar_proj n a1). - * move => [ha1 ->]. - simpl in h1. - inversion h0; subst. - ** hauto lq:on. - ** hauto lqb:on. - ** hauto lqb:on. - * move => [a0][b1][?]. subst => ->. - rewrite !TStar.pair in h1. - inversion h0; subst. - ** admit. - ** best. - -Lemma η_nf n (a b : PTm n) : ERed.R a b -> ERed.R (tstar a) (tstar b). -Proof. - move => h. - elim : n a b /h. - - move => n a0 a1 h h0 /=. - set p := (X in (PAbs X)). - have : (exists a1, ren_PTm shift a0 = PAbs a1 /\ p = subst_PTm (scons (VarPTm var_zero) VarPTm) (tstar a1)) \/ - p = PApp (tstar (ren_PTm shift a0)) (VarPTm var_zero) by hauto lq:on rew:off. - case. - + move => [a2 [+]]. - subst p. - case : a0 h h0 => //=. - move => p h0 h1 [?]. subst => _. - rewrite TStar.renaming. by asimpl. - + move => ->. - rewrite TStar.renaming. - hauto lq:on ctrs:ERed.R. - - move => n a0 a1 ha iha. - case : (tstar_proj n a0). - + move => [_ h]. - change (tstar (PPair (PProj PL a0) (PProj PR a0))) with - (PPair (tstar (PProj PL a0)) (tstar (PProj PR a0))). - rewrite !h. - hauto lq:on ctrs:ERed.R. - + move => [a2][b0][?]. subst. - move => h. - rewrite TStar.pair. - rewrite !h. - sfirstorder. - - hauto lq:on ctrs:ERed.R. - - admit. - - hauto lq:on ctrs:ERed.R. - - move => n p a0 a1 h0 h1. - case : (tstar_proj n a0). - + move => [ha0 ->]. - case : (tstar_proj n a1). - * move => [ha1 ->]. - hauto lq:on ctrs:ERed.R. - * move => [a2][b0][?]. subst. - move => ->. - elim /ERed.inv : h0 => //_. - ** move => a1 a3 ? *. subst. - (* Contradiction *) - admit. - ** hauto lqb:on. - ** hauto lqb:on. - + move => [a2][b0][?] ->. subst. - case : (tstar_proj n a1). - * move => [ha1 ->]. - inversion h0; subst. - ** admit. - ** scongruence. - * move => [a0][b1][?]. subst => ->. - rewrite !TStar.pair in h1. - inversion h1; subst. - ** - ** hauto lq:on. - - - - - move : b. - apply tstar_ind => {}n {}a => //=. - - hauto lq:on ctrs:ERed.R inv:ERed.R. - - move => a0 ? ih. subst. - move => b hb. - elim /ERed.inv : hb => //=_. - + move => a1 a2 ha [*]. subst. - simpl. - case : a1 ih ha => //=. - - - - move => a0 ? ih u. subst. - elim /ERed.inv => //=_. - + move => a1 a2 h [? ?]. subst. - have : ERed.R (PApp (ren_PTm shift a1) (VarPTm var_zero)) (PApp (ren_PTm shift u) (VarPTm var_zero)) - by hauto lq:on ctrs:ERed.R use:ERed.renaming. - move /ih. - - move => h0. simpl. - - move => h. - elim : n a b /h => n. - - move => a0 a1 ha iha. - simpl. - move => h. - move /iha : (h) {iha}. - move : ha. clear. best. - clear. - - sfirstorder. - - - - -Lemma η_nf n (a b c : PTm n) : ERed.R a b -> nf b -> RRed.R a c -> - ERed.R c b. -Proof. - move => h. move : c. - elim : n a b /h=>//=n. - - move => a0 a1 ha iha u hu. - elim /RRed.inv => //= _. - move => a2 a3 h [*]. subst. - elim / RRed.inv : h => //_. - + move => a2 b0 [h0 h1 h2]. subst. - case : a0 h0 ha iha =>//=. - move => u [?] ha iha. subst. - by asimpl. - + move => a2 b4 b0 h [*]. subst. - move /RRed.antirenaming : h. - hauto lq:on ctrs:ERed.R. - + move => a2 b0 b1 h [*]. subst. - inversion h. - - move => a0 b0 a1 ha iha hb ihb u hu. - elim /RRed.inv => //=_. - + move => a2 a3 b1 h0 [*]. subst. - elim /RRed.inv : h0 => //=_. - * move => p a2 b1 [*]. subst. - elim /ERed.inv : ha => //=_. - ** sauto lq:on. - ** move => a0 a2 b2 b3 h h' [*]. subst. - - -Lemma η_nf n (a b c : PTm n) : ERed.R a b -> nf b -> RRed.R a c -> - ERed.R a c. -Proof. - move => h. move : c. - elim : n a b /h=>//=. - - move => n A a0 a1 ha iha c ha1. - elim /RRed.inv => //=_. - move => A0 a2 a3 hr [*]. subst. - set u := a0 in hr *. - set q := a3 in hr *. - elim / RRed.inv : hr => //_. - + move => A0 a2 b0 [h0] h1 h2. subst. - subst u q. - rewrite h0. apply ERed.AppEta. - subst. - case : a0 ha iha h0 => //= B a ha iha [*]. subst. - asimpl. - admit. - + subst u q. - move => a2 a4 b0 hr [*]. subst. - move /RRed.antirenaming : hr => [b0 [h0 h1]]. subst. - hauto lq:on ctrs:ERed.R use:ERed.renaming. - + subst u q. - move => a2 b0 b1 h [*]. subst. - inversion h. - - move => n a0 a1 ha iha v hv. - elim /RRed.inv => //=_. - + move => a2 a3 b0 h [*]. subst. - elim /RRed.inv : h => //=_. - * move => p a2 b0 [*]. subst. - elim /ERed.inv : ha=>//= _. - move => a0 a2 h [*]. subst. - best. - apply ERed.PairEta. - - - From c83be0323003b05619953792366841344f60fa87 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 30 Jan 2025 16:14:03 -0500 Subject: [PATCH 16/18] Finish antirenaming --- theories/fp_red.v | 49 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/theories/fp_red.v b/theories/fp_red.v index 58d711d..d4fbd49 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -204,6 +204,55 @@ Proof. elim : n u / h => n //=; sauto. Qed. +Lemma N_β' n a (b : PTm n) u : + u = (subst_PTm (scons b VarPTm) a) -> + SN b -> + TRedSN (PApp (PAbs a) b) u. +Proof. move => ->. apply N_β. Qed. + +Lemma sn_renaming n : + (forall (a : PTm n) (s : SNe a), forall m (ξ : fin n -> fin m), SNe (ren_PTm ξ a)) /\ + (forall (a : PTm n) (s : SN a), forall m (ξ : fin n -> fin m), SN (ren_PTm ξ a)) /\ + (forall (a b : PTm n) (_ : TRedSN a b), forall m (ξ : fin n -> fin m), TRedSN (ren_PTm ξ a) (ren_PTm ξ b)). +Proof. + move : n. apply sn_mutual => n; try qauto ctrs:SN, SNe, TRedSN depth:1. + move => a b ha iha m ξ /=. + apply N_β'. by asimpl. eauto. +Qed. + +#[export]Hint Constructors SN SNe TRedSN : sn. + +Ltac2 rec solve_anti_ren () := + let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in + intro $x; + lazy_match! Constr.type (Control.hyp x) with + | fin ?x -> fin ?y => (ltac1:(case;qauto depth:2 db:sn)) + | _ => solve_anti_ren () + end. + +Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren). + +Lemma sn_antirenaming n : + (forall (a : PTm n) (s : SNe a), forall m (ξ : fin m -> fin n) b, a = ren_PTm ξ b -> SNe b) /\ + (forall (a : PTm n) (s : SN a), forall m (ξ : fin m -> fin n) b, a = ren_PTm ξ b -> SN b) /\ + (forall (a b : PTm n) (_ : TRedSN a b), forall m (ξ : fin m -> fin n) a0, + a = ren_PTm ξ a0 -> exists b0, TRedSN a0 b0 /\ b = ren_PTm ξ b0). +Proof. + move : n. apply sn_mutual => n; try solve_anti_ren. + + move => a b ha iha m ξ []//= u u0 [+ ?]. subst. + case : u => //= => u [*]. subst. + spec_refl. eexists. split. apply N_β=>//. by asimpl. + + move => a b hb ihb m ξ[]//= p p0 [? +]. subst. + case : p0 => //= p p0 [*]. subst. + spec_refl. by eauto with sn. + + move => a b ha iha m ξ[]//= u u0 [? ]. subst. + case : u0 => //=. move => p p0 [*]. subst. + spec_refl. by eauto with sn. +Qed. + Lemma ered_sn_preservation n : (forall (a : PTm n) (s : SNe a), forall b, ERed.R a b -> SNe b) /\ (forall (a : PTm n) (s : SN a), forall b, ERed.R a b -> SN b) /\ From 64e558f09ee8dc17d06d914d92561f74ef3448cc Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 30 Jan 2025 20:17:00 -0500 Subject: [PATCH 17/18] Finish sn unsubst --- theories/fp_red.v | 73 +++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 68 insertions(+), 5 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index d4fbd49..818286b 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -129,6 +129,7 @@ with TRedSN {n} : PTm n -> PTm n -> Prop := SN b -> TRedSN (PApp (PAbs a) b) (subst_PTm (scons b VarPTm) a) | N_AppL a0 a1 b : + SN b -> TRedSN a0 a1 -> TRedSN (PApp a0 b) (PApp a1 b) | N_ProjPairL a b : @@ -143,6 +144,16 @@ with TRedSN {n} : PTm n -> PTm n -> Prop := Derive Dependent Inversion tred_inv with (forall n (a b : PTm n), TRedSN a b) Sort Prop. +Inductive SNe' {n} : PTm n -> Prop := +| N_Var' i : + SNe' (VarPTm i) +| N_App' a b : + SNe a -> + SNe' (PApp a b) +| N_Proj' p a : + SNe a -> + SNe' (PProj p a). + Lemma PProjAbs_imp n p (a : PTm (S n)) : ~ SN (PProj p (PAbs a)). Proof. @@ -226,7 +237,7 @@ Ltac2 rec solve_anti_ren () := let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in intro $x; lazy_match! Constr.type (Control.hyp x) with - | fin ?x -> fin ?y => (ltac1:(case;qauto depth:2 db:sn)) + | fin ?x -> _ ?y => (ltac1:(case;qauto depth:2 db:sn)) | _ => solve_anti_ren () end. @@ -253,6 +264,57 @@ Proof. spec_refl. by eauto with sn. Qed. +Lemma sn_unmorphing n : + (forall (a : PTm n) (s : SNe a), forall m (ρ : fin m -> PTm n) b, a = subst_PTm ρ b -> SNe b) /\ + (forall (a : PTm n) (s : SN a), forall m (ρ : fin m -> PTm n) b, a = subst_PTm ρ b -> SN b) /\ + (forall (a b : PTm n) (_ : TRedSN a b), forall m (ρ : fin m -> PTm n) a0, + a = subst_PTm ρ a0 -> (exists b0, b = subst_PTm ρ b0 /\ TRedSN a0 b0) \/ SNe a0). +Proof. + move : n. apply sn_mutual => n; try solve_anti_ren. + - move => a b ha iha m ξ b0. + case : b0 => //=. + + hauto lq:on rew:off db:sn. + + move => p p0 [+ ?]. subst. + case : p => //=. + hauto lq:on db:sn. + move => p [?]. subst. + asimpl. left. + spec_refl. + eexists. split; last by eauto using N_β. + by asimpl. + - move => a0 a1 b hb ihb ha iha m ρ []//=. + + hauto lq:on rew:off db:sn. + + move => t0 t1 [*]. subst. + spec_refl. + case : iha. + * move => [u [? hu]]. subst. + left. eexists. split; eauto using N_AppL. + reflexivity. + * move => h. + right. + apply N_App => //. + - move => a b hb ihb m ρ []//=. + + hauto l:on ctrs:TRedSN. + + move => p p0 [?]. subst. + case : p0 => //=. + * hauto lq:on rew:off db:sn. + * move => p p0 [*]. subst. + hauto lq:on db:sn. + - move => a b ha iha m ρ []//=; first by hauto l:on db:sn. + hauto q:on inv:PTm db:sn. + - move => p a b ha iha m ρ []//=; first by hauto l:on db:sn. + move => t0 t1 [*]. subst. + spec_refl. + case : iha. + + move => [b0 [? h]]. subst. + left. eexists. split; last by eauto with sn. + reflexivity. + + hauto lq:on db:sn. +Qed. + +Lemma SN_AppInv : forall n (a b : PTm n), SN (PApp a b) -> SN a /\ SN b. +Admitted. + Lemma ered_sn_preservation n : (forall (a : PTm n) (s : SNe a), forall b, ERed.R a b -> SNe b) /\ (forall (a : PTm n) (s : SN a), forall b, ERed.R a b -> SN b) /\ @@ -273,7 +335,8 @@ Proof. apply ERed.AppCong; eauto using ERed.refl. sfirstorder use:ERed.renaming. move /iha. - admit. + move /SN_AppInv => [+ _]. + hauto l:on use:sn_antirenaming. + sauto lq:on. - sauto lq:on. - sauto lq:on. @@ -308,7 +371,7 @@ Proof. sauto lq:on. + sauto lq:on. - sauto. -Admitted. +Qed. Module RRed. Inductive R {n} : PTm n -> PTm n -> Prop := @@ -525,7 +588,7 @@ Proof. move => a0 a2 h [*]. subst. eexists. split. apply T_Once. hauto lq:on ctrs:TRedSN. eauto using RPar.cong. - - move => a0 a1 b ha iha c. + - move => a0 a1 b hb ihb ha iha c. elim /RPar.inv => //=_. + qauto l:on inv:TRedSN. + move => a2 a3 b0 b1 h0 h1 [*]. subst. @@ -872,7 +935,7 @@ Module SN_NoForbid : NoForbid. Proof. sfirstorder use:PProjAbs_imp. Qed. Lemma P_AppInv : forall n (a b : PTm n), P (PApp a b) -> P a /\ P b. - Admitted. + Proof. sfirstorder use:SN_AppInv. Qed. Lemma P_PairInv : forall n (a b : PTm n), P (PPair a b) -> P a /\ P b. move => n a b. move E : (PPair a b) => u h. From fc666956e220a851d339be29319b8187daa91f5f Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 30 Jan 2025 20:23:25 -0500 Subject: [PATCH 18/18] Finish off the SN proof --- theories/fp_red.v | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 818286b..a53a692 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -313,7 +313,25 @@ Proof. Qed. Lemma SN_AppInv : forall n (a b : PTm n), SN (PApp a b) -> SN a /\ SN b. -Admitted. +Proof. + move => n a b. move E : (PApp a b) => u hu. move : a b E. + elim : n u /hu=>//=. + hauto lq:on rew:off inv:SNe db:sn. + move => n a b ha hb ihb a0 b0 ?. subst. + inversion ha; subst. + move {ihb}. + hecrush use:sn_unmorphing. + hauto lq:on db:sn. +Qed. + +Lemma SN_ProjInv : forall n p (a : PTm n), SN (PProj p a) -> SN a. +Proof. + move => n p a. move E : (PProj p a) => u hu. + move : p a E. + elim : n u / hu => //=. + hauto lq:on rew:off inv:SNe db:sn. + hauto lq:on rew:off inv:TRedSN db:sn. +Qed. Lemma ered_sn_preservation n : (forall (a : PTm n) (s : SNe a), forall b, ERed.R a b -> SNe b) /\ @@ -942,7 +960,7 @@ Module SN_NoForbid : NoForbid. move : a b E. elim : n u / h; sauto lq:on rew:off. Qed. Lemma P_ProjInv : forall n p (a : PTm n), P (PProj p a) -> P a. - Admitted. + Proof. sfirstorder use:SN_ProjInv. Qed. Lemma P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a. Proof. @@ -952,7 +970,7 @@ Module SN_NoForbid : NoForbid. Qed. Lemma P_renaming : forall n m (ξ : fin n -> fin m) a , P (ren_PTm ξ a) <-> P a. - Admitted. + Proof. hauto lq:on use:sn_antirenaming, sn_renaming. Qed. End SN_NoForbid.