From 5dbde6d45f7fe2a8494bd7ed2507cec0b8bd9d3b Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 13 Apr 2025 21:46:22 -0400 Subject: [PATCH] Add alternative direct commutativity proof --- theories/confluence.v | 156 ++++++++++++++++++++---------------------- 1 file changed, 76 insertions(+), 80 deletions(-) diff --git a/theories/confluence.v b/theories/confluence.v index 239bac4..8f1cc55 100644 --- a/theories/confluence.v +++ b/theories/confluence.v @@ -358,88 +358,84 @@ Proof. move => + h. move : b. induction h; hauto lq:on ctrs:rtc use:ηO_commute. Qed. -(* Lemma βη_commute0 a b c : *) -(* βPar.R a b -> *) -(* ηPar.R a c -> *) -(* exists d, ηPar.R b d /\ βPar.R c d. *) -(* Proof. *) -(* move => h. move : c. *) -(* elim :a b /h. *) -(* - move => i c. move /IO_factorization. *) -(* move => [b [ihb0 ihb1]]. *) -(* elim /IPar.inv : ihb0 => //=_. *) -(* move => ? [*]. subst. *) -(* exists c. split. apply : IO_merge'; eauto. constructor. *) -(* apply βPar.refl. *) -(* - move => b0 b1 a0 a1 hb ihb ha iha u /IO_factorization. *) -(* move => [v [+ hv]]. *) -(* elim /IPar.inv => //=_. *) -(* move => b2 b3 a2 a3 hb2 ha2 [*]. subst. *) -(* rename b3 into b2. rename a3 into a2. *) -(* move : hb2 => {}/ihb. move => [b12 [ihb0 ihb1]]. *) -(* move : ha2 => {}/iha. move => [a12 [iha0 iha1]]. *) -(* have h2 : βPar.R (App b2 a2) (App b12 a12) by constructor. *) -(* move : βO_commute0 hv h2. repeat move/[apply]. *) -(* move => [v][h0 h1]. *) -(* exists v. split => //. apply : IO_merge'; eauto; by constructor. *) -(* - move => a0 a1 ha iha u /IO_factorization. *) -(* move => [v][hb0]hb1. *) -(* elim /IPar.inv : hb0 => //=_. *) -(* move => ? a2 + [*]. subst. *) -(* move => {}/iha. move => [a12 [ih0 ih1]]. *) -(* have {ih1} : βPar.R (Abs a2) (Abs a12) by constructor. *) -(* move : βO_commute0 hb1. repeat move/[apply]. *) -(* move => [d [h0 h1]]. exists d. split => //. *) -(* apply : IO_merge'; eauto; by constructor. *) -(* - move => b0 b1 a0 a1 hb ihb ha iha u /IO_factorization. *) -(* move => [v][hv0]hv1. *) -(* elim /IPar.inv : hv0 => //=_. *) -(* move => ? b2 ? a2 hb2 ha2 [*]. subst. *) -(* move /IO_factorization : hb2 => [b [h0 h1]]. *) -(* elim /IPar.inv : h0 => //=_. *) -(* move => ? b' ha' [*]. subst. *) -(* move : ihb ha' => /[apply]. move => [b12 [ihb0 ihb1]]. *) -(* move : iha ha2 => /[apply]. move => [a12 [iha0 iha1]]. *) - - - (* - move => b0 b1 a0 a1 hb ihb ha iha u. *) - (* elim /ηexp.inv => //=_. *) - (* + move => b2 b3 a2 hb' [*]. subst. *) - (* move : ihb hb' => /[apply]. move=> [b2 [ihb0 ihb1]]. *) - (* clear iha. *) - (* exists (App b2 a1). *) - (* split. *) - (* sfirstorder use:ηexps.AppCong, rtc_refl. *) - (* hauto lq:on ctrs:βPar.R use:βPar.refl. *) - (* + move => b2 ? a2 + [*]. subst. *) - (* move => {}/iha {ihb} [a12 [ih0 ih1]]. *) - - -(* Lemma ηβ_commute0 a b c : *) -(* ηPar.R a b -> *) -(* βPar.R a c -> *) -(* exists d, βPar.R b d /\ ηPar.R c d. *) -(* Proof. *) -(* move => h. move : c. elim : a b /h. *) -(* - hauto lq:on ctrs:βPar.R, ηPar.R inv:βPar.R. *) -(* - move => b0 b1 a0 a1 hb ihb ha iha u. *) -(* elim /βPar.inv => //=_. *) -(* + hauto lq:on ctrs:βPar.R, ηPar.R inv:βPar.R. *) -(* + move => b3 b2 a3 a2 hb2 ha2 [*]. subst. *) -(* rename b3 into b0. *) -(* have {}/ihb : βPar.R (Abs b0) (Abs b2) by eauto using βPar.AbsCong. *) -(* move => [b12 [ihb0 ihb1]]. *) - - -(* rename b3 into b4. rename b2 into b3. rename b4 into b2. *) -(* move => b2 b3 a2 a3 hb2 ha2 [*]. subst. *) -(* rename b3 into b2. rename a3 into a2. *) -(* move : ihb hb2 => /[apply]. move => [b12 [ihb0 ihb1]]. *) -(* move : iha ha2 => /[apply]. move => [a12 [iha0 iha1]]. *) - - +Lemma oexp_appabs b b' b0 a0 a1 : + rtc OExp.R (Abs b) b0 -> + βPar.R b b' -> + βPar.R a0 a1 -> + βPar.R (App b0 a0) (subst_Tm (scons a1 VarTm) b'). +Proof. + move E : (Abs b) => u hu. + move : b E b' a0 a1. + elim : u b0 /hu => //=. + - move => ? b ? b' a0 a1 hb ha. subst. + by constructor. + - move => c0 c1 c2 hc0 hc1 ih b ? b' a0 a1 hb ha. subst. + elim /OExp.inv : hc0 => //= _. + move => ? ? ?. subst. + specialize ih with (1 := eq_refl). + apply ih => //. + eapply βPar.AppAbs' with (b1 := ren_Tm (upRen_Tm_Tm shift) b') (a1 := VarTm var_zero). by asimpl; rewrite subst_id. + by apply βPar.renaming. + constructor. +Qed. +(* Direct commutativity proof with parallel η *) Lemma βη_commute0 a b c : + βPar.R a b -> + ηPar.R a c -> + exists d, ηPar.R b d /\ βPar.R c d. +Proof. + move => h. move : c. + elim :a b /h. + - move => i c. move /IO_factorization. + move => [b [ihb0 ihb1]]. + elim /IPar.inv : ihb0 => //=_. + move => ? [*]. subst. + exists c. split. apply : IO_merge'; eauto. constructor. + apply βPar.refl. + - move => b0 b1 a0 a1 hb ihb ha iha u /IO_factorization. + move => [v [+ hv]]. + elim /IPar.inv => //=_. + move => b2 b3 a2 a3 hb2 ha2 [*]. subst. + rename b3 into b2. rename a3 into a2. + move : hb2 => {}/ihb. move => [b12 [ihb0 ihb1]]. + move : ha2 => {}/iha. move => [a12 [iha0 iha1]]. + have h2 : βPar.R (App b2 a2) (App b12 a12) by constructor. + move : βO_commute0 hv h2. repeat move/[apply]. + move => [v][h0 h1]. + exists v. split => //. apply : IO_merge'; eauto; by constructor. + - move => a0 a1 ha iha u /IO_factorization. + move => [v][hb0]hb1. + elim /IPar.inv : hb0 => //=_. + move => ? a2 + [*]. subst. + move => {}/iha. move => [a12 [ih0 ih1]]. + have {ih1} : βPar.R (Abs a2) (Abs a12) by constructor. + move : βO_commute0 hb1. repeat move/[apply]. + move => [d [h0 h1]]. exists d. split => //. + apply : IO_merge'; eauto; by constructor. + - move => b0 b1 a0 a1 hb ihb ha iha u /IO_factorization. + move => [v][hv0]hv1. + elim /IPar.inv : hv0 => //=_. + move => ? b2 ? a2 hb2 ha2 [*]. subst. + move /IO_factorization : hb2 => [b [h0 h1]]. + elim /IPar.inv : h0 => //=_. + move => ? b' ha' [*]. subst. + move : ihb (ha') => /[apply]. move => [b12 [ihb0 ihb1]]. + move : iha (ha2) => /[apply]. move => [a12 [iha0 iha1]]. + have : βPar.R (App b2 a2) (subst_Tm (scons a12 VarTm) b12) + by eauto using oexp_appabs. + move : βO_commute0 hv1. repeat move/[apply]. + move => [v][hv0]hv1. + exists v. split => //. + apply : IO_merge'; eauto. + apply ηPar.morphing2 => //. + apply ηPar.morphing2_ext => //. + move => *. constructor. +Qed. + +(* Indirect but perhaps nicer proof with an extra + definition of full non-paralell η expansion *) +Lemma βη_commute0' a b c : βPar.R a b -> ηexp.R a c -> exists d, rtc ηexp.R b d /\ βPar.R c d.