From b750ea4095c9c2195a056c9987bac03b5d23c01d Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 10 Jan 2025 16:51:49 -0500 Subject: [PATCH 01/17] Initial commit (still tweaking the rules) --- syntax.sig | 4 ++ theories/Autosubst2/syntax.v | 86 +++++++++++++++++++++++++++++++++++- theories/fp_red.v | 21 ++++++++- 3 files changed, 109 insertions(+), 2 deletions(-) diff --git a/syntax.sig b/syntax.sig index 4549f7f..d2354e2 100644 --- a/syntax.sig +++ b/syntax.sig @@ -2,6 +2,7 @@ nat : Type Tm(VarTm) : Type PTag : Type TTag : Type +bool : Type TPi : TTag TSig : TTag @@ -14,3 +15,6 @@ Proj : PTag -> Tm -> Tm TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm Bot : Tm Univ : nat -> Tm +Bool : Tm +BVal : bool -> Tm +If : Tm -> Tm -> Tm -> Tm \ No newline at end of file diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v index b972476..ffb7c7c 100644 --- a/theories/Autosubst2/syntax.v +++ b/theories/Autosubst2/syntax.v @@ -41,7 +41,10 @@ Inductive Tm (n_Tm : nat) : Type := | Proj : PTag -> Tm n_Tm -> Tm n_Tm | TBind : TTag -> Tm n_Tm -> Tm (S n_Tm) -> Tm n_Tm | Bot : Tm n_Tm - | Univ : nat -> Tm n_Tm. + | Univ : nat -> Tm n_Tm + | Bool : Tm n_Tm + | BVal : bool -> Tm n_Tm + | If : Tm n_Tm -> Tm n_Tm -> Tm 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. @@ -94,6 +97,27 @@ Proof. exact (eq_trans eq_refl (ap (fun x => Univ m_Tm x) H0)). Qed. +Lemma congr_Bool {m_Tm : nat} : Bool m_Tm = Bool m_Tm. +Proof. +exact (eq_refl). +Qed. + +Lemma congr_BVal {m_Tm : nat} {s0 : bool} {t0 : bool} (H0 : s0 = t0) : + BVal m_Tm s0 = BVal m_Tm t0. +Proof. +exact (eq_trans eq_refl (ap (fun x => BVal m_Tm x) H0)). +Qed. + +Lemma congr_If {m_Tm : nat} {s0 : Tm m_Tm} {s1 : Tm m_Tm} {s2 : Tm m_Tm} + {t0 : Tm m_Tm} {t1 : Tm m_Tm} {t2 : Tm m_Tm} (H0 : s0 = t0) (H1 : s1 = t1) + (H2 : s2 = t2) : If m_Tm s0 s1 s2 = If m_Tm t0 t1 t2. +Proof. +exact (eq_trans + (eq_trans (eq_trans eq_refl (ap (fun x => If m_Tm x s1 s2) H0)) + (ap (fun x => If m_Tm t0 x s2) H1)) + (ap (fun x => If m_Tm t0 t1 x) H2)). +Qed. + Lemma upRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) : fin (S m) -> fin (S n). Proof. @@ -118,6 +142,10 @@ Fixpoint ren_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm) TBind n_Tm s0 (ren_Tm xi_Tm s1) (ren_Tm (upRen_Tm_Tm xi_Tm) s2) | Bot _ => Bot n_Tm | Univ _ s0 => Univ n_Tm s0 + | Bool _ => Bool n_Tm + | BVal _ s0 => BVal n_Tm s0 + | If _ s0 s1 s2 => + If n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1) (ren_Tm xi_Tm s2) end. Lemma up_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) : @@ -145,6 +173,11 @@ Fixpoint subst_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm) TBind n_Tm s0 (subst_Tm sigma_Tm s1) (subst_Tm (up_Tm_Tm sigma_Tm) s2) | Bot _ => Bot n_Tm | Univ _ s0 => Univ n_Tm s0 + | Bool _ => Bool n_Tm + | BVal _ s0 => BVal n_Tm s0 + | If _ s0 s1 s2 => + If n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1) + (subst_Tm sigma_Tm s2) end. Lemma upId_Tm_Tm {m_Tm : nat} (sigma : fin m_Tm -> Tm m_Tm) @@ -185,6 +218,11 @@ subst_Tm sigma_Tm s = s := (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) + | Bool _ => congr_Bool + | BVal _ s0 => congr_BVal (eq_refl s0) + | If _ s0 s1 s2 => + congr_If (idSubst_Tm sigma_Tm Eq_Tm s0) (idSubst_Tm sigma_Tm Eq_Tm s1) + (idSubst_Tm sigma_Tm Eq_Tm s2) end. Lemma upExtRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) @@ -229,6 +267,11 @@ Fixpoint extRen_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm) (upExtRen_Tm_Tm _ _ Eq_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) + | Bool _ => congr_Bool + | BVal _ s0 => congr_BVal (eq_refl s0) + | If _ s0 s1 s2 => + congr_If (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0) + (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s2) end. Lemma upExt_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) @@ -274,6 +317,11 @@ Fixpoint ext_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) + | Bool _ => congr_Bool + | BVal _ s0 => congr_BVal (eq_refl s0) + | If _ s0 s1 s2 => + congr_If (ext_Tm sigma_Tm tau_Tm Eq_Tm s0) + (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) (ext_Tm sigma_Tm tau_Tm Eq_Tm s2) end. Lemma up_ren_ren_Tm_Tm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l) @@ -319,6 +367,12 @@ Fixpoint compRenRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) + | Bool _ => congr_Bool + | BVal _ s0 => congr_BVal (eq_refl s0) + | If _ s0 s1 s2 => + congr_If (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0) + (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1) + (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s2) end. Lemma up_ren_subst_Tm_Tm {k : nat} {l : nat} {m_Tm : nat} @@ -375,6 +429,12 @@ Fixpoint compRenSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) + | Bool _ => congr_Bool + | BVal _ s0 => congr_BVal (eq_refl s0) + | If _ s0 s1 s2 => + congr_If (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0) + (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1) + (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s2) end. Lemma up_subst_ren_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat} @@ -452,6 +512,12 @@ ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s := (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) + | Bool _ => congr_Bool + | BVal _ s0 => congr_BVal (eq_refl s0) + | If _ s0 s1 s2 => + congr_If (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0) + (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1) + (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s2) end. Lemma up_subst_subst_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat} @@ -530,6 +596,12 @@ subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s := (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) + | Bool _ => congr_Bool + | BVal _ s0 => congr_BVal (eq_refl s0) + | If _ s0 s1 s2 => + congr_If (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0) + (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1) + (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s2) end. Lemma renRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} @@ -646,6 +718,12 @@ Fixpoint rinst_inst_Tm {m_Tm : nat} {n_Tm : nat} (rinstInst_up_Tm_Tm _ _ Eq_Tm) s2) | Bot _ => congr_Bot | Univ _ s0 => congr_Univ (eq_refl s0) + | Bool _ => congr_Bool + | BVal _ s0 => congr_BVal (eq_refl s0) + | If _ s0 s1 s2 => + congr_If (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0) + (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1) + (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s2) end. Lemma rinstInst'_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm) @@ -844,6 +922,12 @@ Core. Arguments VarTm {n_Tm}. +Arguments If {n_Tm}. + +Arguments BVal {n_Tm}. + +Arguments Bool {n_Tm}. + Arguments Univ {n_Tm}. Arguments Bot {n_Tm}. diff --git a/theories/fp_red.v b/theories/fp_red.v index d2fbdf6..9424da6 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -33,6 +33,8 @@ Module Par. R b0 b1 -> R c0 c1 -> R (App (Pair a0 b0) c0) (Pair (App a1 c1) (App b1 c1)) + | AppBool b a : + R (App (BVal b) a) (BVal b) | ProjAbs p a0 a1 : R a0 a1 -> R (Proj p (Abs a0)) (Abs (Proj p a1)) @@ -40,7 +42,24 @@ Module Par. R a0 a1 -> R b0 b1 -> R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) - + | ProjBool p b : + R (Proj p (BVal b)) (BVal b) + | IfAbs a0 a1 b0 b1 c0 c1 d0 d1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R d0 d1 -> + R (If (Abs a0) b0 c0) (Abs (If a0 (ren_Tm shift b0) (ren_Tm shift c0))) + | IfPair a0 a1 b0 b1 c0 c1 d0 d1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R d0 d1 -> + R (If (Pair a0 b0) c0 d0) (Pair (If a0 c0 d0) (If b0 c0 d0)) + | IfBool a b0 b1 c0 c1 : + R b0 b1 -> + R c0 c1 -> + R (If (BVal a) b0 c0) (if a then b1 else c1) (****************** Eta ***********************) | AppEta a0 a1 : R a0 a1 -> From bec803949f4da3522031a185cdfcd522be675b82 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 10 Jan 2025 20:51:59 -0500 Subject: [PATCH 02/17] Finish Par and RPar lemmas --- theories/fp_red.v | 117 +++++++++++++++++++++++++++++++++++++--------- 1 file changed, 96 insertions(+), 21 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 9424da6..c8076e1 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -33,8 +33,8 @@ Module Par. R b0 b1 -> R c0 c1 -> R (App (Pair a0 b0) c0) (Pair (App a1 c1) (App b1 c1)) - | AppBool b a : - R (App (BVal b) a) (BVal b) + (* | AppBool b a : *) + (* R (App (BVal b) a) (BVal b) *) | ProjAbs p a0 a1 : R a0 a1 -> R (Proj p (Abs a0)) (Abs (Proj p a1)) @@ -42,20 +42,20 @@ Module Par. R a0 a1 -> R b0 b1 -> R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) - | ProjBool p b : - R (Proj p (BVal b)) (BVal b) - | IfAbs a0 a1 b0 b1 c0 c1 d0 d1 : - R a0 a1 -> - R b0 b1 -> - R c0 c1 -> - R d0 d1 -> - R (If (Abs a0) b0 c0) (Abs (If a0 (ren_Tm shift b0) (ren_Tm shift c0))) - | IfPair a0 a1 b0 b1 c0 c1 d0 d1 : - R a0 a1 -> - R b0 b1 -> - R c0 c1 -> - R d0 d1 -> - R (If (Pair a0 b0) c0 d0) (Pair (If a0 c0 d0) (If b0 c0 d0)) + (* | ProjBool p b : *) + (* R (Proj p (BVal b)) (BVal b) *) + (* | IfAbs a0 a1 b0 b1 c0 c1 d0 d1 : *) + (* R a0 a1 -> *) + (* R b0 b1 -> *) + (* R c0 c1 -> *) + (* R d0 d1 -> *) + (* R (If (Abs a0) b0 c0) (Abs (If a0 (ren_Tm shift b0) (ren_Tm shift c0))) *) + (* | IfPair a0 a1 b0 b1 c0 c1 d0 d1 : *) + (* R a0 a1 -> *) + (* R b0 b1 -> *) + (* R c0 c1 -> *) + (* R d0 d1 -> *) + (* R (If (Pair a0 b0) c0 d0) (Pair (If a0 c0 d0) (If b0 c0 d0)) *) | IfBool a b0 b1 c0 c1 : R b0 b1 -> R c0 c1 -> @@ -92,7 +92,16 @@ Module Par. | BotCong : R Bot Bot | UnivCong i : - R (Univ i) (Univ i). + R (Univ i) (Univ i) + | BoolCong : + R Bool Bool + | BValCong b : + R (BVal b) (BVal b) + | IfCong a0 a1 b0 b1 c0 c1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R (If a0 b0 c0) (If a1 b1 c1). Lemma refl n (a : Tm n) : R a a. elim : n /a; hauto ctrs:R. @@ -112,6 +121,13 @@ Module Par. R (Proj p (Pair a0 b0)) t. Proof. move => > ->. apply ProjPair. Qed. + Lemma IfBool' n a b0 b1 c0 c1 u : + u = (if a then (b1 : Tm n) else c1) -> + R b0 b1 -> + R c0 c1 -> + R (If (BVal a) b0 c0) u. + Proof. move => ->. apply IfBool. Qed. + Lemma AppEta' n (a0 a1 b : Tm n) : b = (Abs (App (ren_Tm shift a1) (VarTm var_zero))) -> R a0 a1 -> @@ -126,7 +142,7 @@ Module Par. move => *; apply : AppAbs'; eauto; by asimpl. all : match goal with | [ |- context[var_zero]] => move => *; apply : AppEta'; eauto; by asimpl - | _ => qauto ctrs:R use:ProjPair' + | _ => qauto ctrs:R use:ProjPair', IfBool' end. Qed. @@ -143,6 +159,7 @@ Module Par. - hauto lq:on rew:off ctrs:R. - hauto l:on inv:option use:renaming ctrs:R. - hauto lq:on use:ProjPair'. + - hauto q:on use:IfBool'. - move => n a0 a1 ha iha m ρ0 ρ1 hρ /=. apply : AppEta'; eauto. by asimpl. - hauto lq:on ctrs:R. @@ -154,6 +171,9 @@ Module Par. - hauto l:on inv:option ctrs:R use:renaming. - sfirstorder. - sfirstorder. + - sfirstorder. + - sfirstorder. + - hauto lq:on ctrs:R. Qed. Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : @@ -193,6 +213,12 @@ Module Par. move : ihb => [c0 [? ?]]. subst. eexists. split. by eauto using ProjPair. hauto q:on. + - move => n a b0 b1 c0 c1 hb ihb hc ihc m ξ []//= p0 p1 p2 [h *]. subst. + spec_refl. + move : ihb => [b0 [? ?]]. + move : ihc => [c0 [? ?]]. subst. + case : p0 h => //=. + hauto q:on use:IfBool'. - move => n a0 a1 ha iha m ξ a ?. subst. spec_refl. move : iha => [a0 [? ?]]. subst. eexists. split. apply AppEta; eauto. @@ -233,6 +259,11 @@ Module Par. by asimpl. - move => n n0 ξ []//=. hauto l:on. - move => n i n0 ξ []//=. hauto l:on. + - move => n m ξ []//=. hauto l:on. + - move => n b m ξ []//=. hauto l:on. + - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ξ []//= t t0 t1[*]. subst. + spec_refl. + qauto l:on ctrs:R. Qed. End Par. @@ -321,6 +352,10 @@ Module RPar. R a0 a1 -> R b0 b1 -> R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) + | IfBool a b0 b1 c0 c1 : + R b0 b1 -> + R c0 c1 -> + R (If (BVal a) b0 c0) (if a then b1 else c1) (*************** Congruence ********************) @@ -346,7 +381,16 @@ Module RPar. | BotCong : R Bot Bot | UnivCong i : - R (Univ i) (Univ i). + R (Univ i) (Univ i) + | BoolCong : + R Bool Bool + | BValCong b : + R (BVal b) (BVal b) + | IfCong a0 a1 b0 b1 c0 c1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R (If a0 b0 c0) (If a1 b1 c1). Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. @@ -369,13 +413,21 @@ Module RPar. R (Proj p (Pair a0 b0)) t. Proof. move => > ->. apply ProjPair. Qed. + Lemma IfBool' n a b0 b1 c0 c1 u : + u = (if a then (b1 : Tm n) else c1) -> + R b0 b1 -> + R c0 c1 -> + R (If (BVal a) b0 c0) u. + Proof. move => ->. apply IfBool. Qed. + + Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). Proof. move => h. move : m ξ. elim : n a b /h. move => *; apply : AppAbs'; eauto; by asimpl. - all : qauto ctrs:R use:ProjPair'. + all : qauto ctrs:R use:ProjPair', IfBool'. Qed. Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> Tm m) (ξ : fin m -> fin p) : @@ -406,6 +458,7 @@ Module RPar. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R use:ProjPair' use:morphing_up. + - hauto lq:on ctrs:R use:IfBool' use:morphing_up. - hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R use:morphing_up. @@ -414,6 +467,9 @@ 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. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. Qed. Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : @@ -434,7 +490,7 @@ Module RPar. var_or_bot a -> a = b -> ~~ var_or_bot b -> False. Proof. - hauto lq:on inv:Tm. + hauto l:on inv:Tm. Qed. Lemma var_or_bot_up n m (ρ : fin n -> Tm m) : @@ -504,6 +560,14 @@ Module RPar. move : ihb => [c0 [? ?]]. subst. eexists. split. by eauto using ProjPair. hauto q:on. + - move => n a b0 b1 c0 c1 hb ihb hc ihc m ρ hρ []//=; first by antiimp. + move => t t0 t1 [h *]. subst. + case : t h => //=; first by antiimp. + move => b [*]. subst. + have {}/ihb := (hρ) => ihb. + have {}/ihc := (hρ) => ihc. + spec_refl. + hauto q:on use:IfBool. - move => n i m ρ hρ []//=. hauto l:on. - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp. @@ -553,6 +617,17 @@ Module RPar. - hauto q:on ctrs:R inv:Tm. - move => n i n0 ρ hρ []//=; first by antiimp. hauto l:on. + - move => n m ρ hρ []//=; first by antiimp. + hauto lq:on ctrs:R. + - move => n b m ρ hρ []//; first by antiimp. + hauto lq:on ctrs:R. + - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=; first by antiimp. + move => t t0 t1 [*]. subst. + have {}/iha := (hρ) => iha. + have {}/ihb := (hρ) => ihb. + have {}/ihc := (hρ) => ihc. + spec_refl. + hauto lq:on ctrs:R. Qed. End RPar. From 53bef034ad74a93ff6b98e330b48c4139e4f3962 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 10 Jan 2025 22:28:53 -0500 Subject: [PATCH 03/17] Add the "junk" rules for boolean --- theories/fp_red.v | 897 ++++++++++++++++++++++++++-------------------- 1 file changed, 509 insertions(+), 388 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index c8076e1..a8c8a3a 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -33,8 +33,8 @@ Module Par. R b0 b1 -> R c0 c1 -> R (App (Pair a0 b0) c0) (Pair (App a1 c1) (App b1 c1)) - (* | AppBool b a : *) - (* R (App (BVal b) a) (BVal b) *) + | AppBool b a : + R (App (BVal b) a) (BVal b) | ProjAbs p a0 a1 : R a0 a1 -> R (Proj p (Abs a0)) (Abs (Proj p a1)) @@ -42,20 +42,19 @@ Module Par. R a0 a1 -> R b0 b1 -> R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) - (* | ProjBool p b : *) - (* R (Proj p (BVal b)) (BVal b) *) - (* | IfAbs a0 a1 b0 b1 c0 c1 d0 d1 : *) - (* R a0 a1 -> *) - (* R b0 b1 -> *) - (* R c0 c1 -> *) - (* R d0 d1 -> *) - (* R (If (Abs a0) b0 c0) (Abs (If a0 (ren_Tm shift b0) (ren_Tm shift c0))) *) - (* | IfPair a0 a1 b0 b1 c0 c1 d0 d1 : *) - (* R a0 a1 -> *) - (* R b0 b1 -> *) - (* R c0 c1 -> *) - (* R d0 d1 -> *) - (* R (If (Pair a0 b0) c0 d0) (Pair (If a0 c0 d0) (If b0 c0 d0)) *) + | ProjBool p b : + R (Proj p (BVal b)) (BVal b) + | IfAbs (a0 a1 : Tm (S n)) b0 b1 c0 c1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R (If (Abs a0) b0 c0) (Abs (If a1 (ren_Tm shift b1) (ren_Tm shift c1))) + | IfPair a0 a1 b0 b1 c0 c1 d0 d1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R d0 d1 -> + R (If (Pair a0 b0) c0 d0) (Pair (If a1 c1 d1) (If b1 c1 d1)) | IfBool a b0 b1 c0 c1 : R b0 b1 -> R c0 c1 -> @@ -134,6 +133,14 @@ Module Par. R a0 b. Proof. move => ->; apply AppEta. Qed. + Lemma IfAbs' n (a0 a1 : Tm (S n)) (b0 b1 c0 c1 : Tm n) u : + u = (Abs (If a1 (ren_Tm shift b1) (ren_Tm shift c1))) -> + @R (S n) a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R (If (Abs a0) b0 c0) u. + Proof. move => ->. apply IfAbs. Qed. + Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). Proof. @@ -142,11 +149,11 @@ Module Par. move => *; apply : AppAbs'; eauto; by asimpl. all : match goal with | [ |- context[var_zero]] => move => *; apply : AppEta'; eauto; by asimpl + | [ |- context[ren_Tm]] => move => * /=; apply : IfAbs'; eauto; by asimpl | _ => qauto ctrs:R use:ProjPair', IfBool' end. Qed. - Lemma morphing n m (a b : Tm n) (ρ0 ρ1 : fin n -> Tm m) : (forall i, R (ρ0 i) (ρ1 i)) -> R a b -> R (subst_Tm ρ0 a) (subst_Tm ρ1 b). @@ -157,8 +164,14 @@ Module Par. by asimpl. hauto l:on use:renaming inv:option. - hauto lq:on rew:off ctrs:R. + - hauto lq:on rew:off ctrs:R. - hauto l:on inv:option use:renaming ctrs:R. - hauto lq:on use:ProjPair'. + - hauto lq:on rew:off ctrs:R. + - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ0 ρ1 hρ /=. + eapply IfAbs' with (a1 := (subst_Tm (up_Tm_Tm ρ1) a1)); eauto. by asimpl. + hauto l:on use:renaming inv:option. + - qauto l:on ctrs:R. - hauto q:on use:IfBool'. - move => n a0 a1 ha iha m ρ0 ρ1 hρ /=. apply : AppEta'; eauto. by asimpl. @@ -204,6 +217,8 @@ Module Par. eexists. split. apply AppPair; hauto. subst. by asimpl. + - move => n b a m ξ []//=. + hauto q:on ctrs:R inv:Tm. - move => n p a0 a1 ha iha m ξ []//= p0 []//= t [*]. subst. spec_refl. move : iha => [b0 [? ?]]. subst. eexists. split. apply ProjAbs; eauto. by asimpl. @@ -213,6 +228,23 @@ Module Par. move : ihb => [c0 [? ?]]. subst. eexists. split. by eauto using ProjPair. hauto q:on. + - move => n p b m ξ []//=. + move => + []//=. + hauto lq:on ctrs:R. + - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ξ []//= t t0 t1 [h *]. subst. + case : t h => // t [*]. subst. + spec_refl. + move : iha => [a2 [iha ?]]. subst. + move : ihb => [b2 [ihb ?]]. subst. + move : ihc => [c2 [ihc ?]]. subst. + exists (Abs (If a2 (ren_Tm shift b2) (ren_Tm shift c2))). + split; last by asimpl. + hauto lq:on ctrs:R. + - move => n a0 a1 b0 b1 c0 c1 d0 d1 ha iha hb ihb hc ihc hd ihd m ξ []//=. + move => a2 b2 c2 [h *]. subst. + case : a2 h => //= a3 b3 [*]. subst. + spec_refl. + hauto lq:on ctrs:R. - move => n a b0 b1 c0 c1 hb ihb hc ihc m ξ []//= p0 p1 p2 [h *]. subst. spec_refl. move : ihb => [b0 [? ?]]. @@ -345,6 +377,8 @@ Module RPar. R b0 b1 -> R c0 c1 -> R (App (Pair a0 b0) c0) (Pair (App a1 c1) (App b1 c1)) + | AppBool b a : + R (App (BVal b) a) (BVal b) | ProjAbs p a0 a1 : R a0 a1 -> R (Proj p (Abs a0)) (Abs (Proj p a1)) @@ -352,6 +386,19 @@ Module RPar. R a0 a1 -> R b0 b1 -> R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) + | ProjBool p b : + R (Proj p (BVal b)) (BVal b) + | IfAbs (a0 a1 : Tm (S n)) b0 b1 c0 c1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R (If (Abs a0) b0 c0) (Abs (If a1 (ren_Tm shift b1) (ren_Tm shift c1))) + | IfPair a0 a1 b0 b1 c0 c1 d0 d1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R d0 d1 -> + R (If (Pair a0 b0) c0 d0) (Pair (If a1 c1 d1) (If b1 c1 d1)) | IfBool a b0 b1 c0 c1 : R b0 b1 -> R c0 c1 -> @@ -421,13 +468,20 @@ Module RPar. Proof. move => ->. apply IfBool. Qed. + Lemma IfAbs' n (a0 a1 : Tm (S n)) (b0 b1 c0 c1 : Tm n) u : + u = (Abs (If a1 (ren_Tm shift b1) (ren_Tm shift c1))) -> + @R (S n) a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R (If (Abs a0) b0 c0) u. + Proof. move => ->. apply IfAbs. Qed. + Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). Proof. move => h. move : m ξ. - elim : n a b /h. - move => *; apply : AppAbs'; eauto; by asimpl. - all : qauto ctrs:R use:ProjPair', IfBool'. + elim : n a b /h; try solve [(move => *; apply : AppAbs'; eauto; by asimpl) | (move => *; apply : IfAbs'; eauto; by asimpl)]. + all : try qauto ctrs:R use:ProjPair', IfBool'. Qed. Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> Tm m) (ξ : fin m -> fin p) : @@ -456,8 +510,14 @@ Module RPar. apply : AppAbs'; eauto using morphing_up. by asimpl. - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. - hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R use:ProjPair' use:morphing_up. + - sfirstorder. + - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ0 ρ1 hρ /=. + apply : IfAbs'; eauto using morphing_up. + by asimpl. + - hauto lq:on ctrs:R. - hauto lq:on ctrs:R use:IfBool' use:morphing_up. - hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R use:morphing_up. @@ -543,6 +603,9 @@ Module RPar. eexists. split. apply AppPair; hauto. subst. by asimpl. + - move => n b a m ρ hρ []//=; first by antiimp. + case => //=; first by antiimp. + hauto lq:on ctrs:R. - move => n p a0 a1 ha iha m ρ hρ []//=; first by antiimp. move => p0 []//= t [*]; first by antiimp. subst. @@ -560,6 +623,31 @@ Module RPar. move : ihb => [c0 [? ?]]. subst. eexists. split. by eauto using ProjPair. hauto q:on. + - move => n p b m ρ hρ []//=; first by antiimp. + move => p0 + []//=. case => //=; first by antiimp. + hauto lq:on ctrs:R. + - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=; first by antiimp. + move => + b2 c2 [+ *]. subst. case => //=; first by antiimp. + move => a [*]. subst. + have /var_or_bot_up hρ' := hρ. + move : iha hρ' => /[apply] iha. + move : ihb (hρ) => /[apply] ihb. + move : ihc hρ => /[apply] ihc. + spec_refl. + move : iha => [a0 [ha0 ?]]. subst. + move : ihb => [b0 [hb0 ?]]. subst. + move : ihc => [c0 [hc0 ?]]. subst. + exists (Abs (If a0 (ren_Tm shift b0) (ren_Tm shift c0))). split. + hauto lq:on ctrs:R. + by asimpl. + - move => n a0 a1 b0 b1 c0 c1 d0 d1 ha iha hb ihb hc ihc hd ihd m ρ hρ []//=; first by antiimp. + move => a2 b2 c2 [+ *]. subst. case : a2 => //=; first by antiimp. + move => a3 b3 [*]. subst. + have {}/iha := (hρ) => iha. + have {}/ihb := (hρ) => ihb. + have {}/ihc := (hρ) => ihc. + spec_refl. + hauto lq:on ctrs:R. - move => n a b0 b1 c0 c1 hb ihb hc ihc m ρ hρ []//=; first by antiimp. move => t t0 t1 [h *]. subst. case : t h => //=; first by antiimp. @@ -631,332 +719,332 @@ Module RPar. Qed. End RPar. -(***************** Beta rules only ***********************) -Module RPar'. - Inductive R {n} : Tm n -> Tm n -> Prop := - (***************** Beta ***********************) - | AppAbs a0 a1 b0 b1 : - R a0 a1 -> - R b0 b1 -> - R (App (Abs a0) b0) (subst_Tm (scons b1 VarTm) a1) - | ProjPair p a0 a1 b0 b1 : - R a0 a1 -> - R b0 b1 -> - R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) +(* (***************** Beta rules only ***********************) *) +(* Module RPar'. *) +(* Inductive R {n} : Tm n -> Tm n -> Prop := *) +(* (***************** Beta ***********************) *) +(* | AppAbs a0 a1 b0 b1 : *) +(* R a0 a1 -> *) +(* R b0 b1 -> *) +(* R (App (Abs a0) b0) (subst_Tm (scons b1 VarTm) a1) *) +(* | ProjPair p a0 a1 b0 b1 : *) +(* R a0 a1 -> *) +(* R b0 b1 -> *) +(* R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) *) - (*************** Congruence ********************) - | Var i : R (VarTm i) (VarTm i) - | AbsCong a0 a1 : - R a0 a1 -> - R (Abs a0) (Abs a1) - | AppCong a0 a1 b0 b1 : - R a0 a1 -> - R b0 b1 -> - R (App a0 b0) (App a1 b1) - | PairCong a0 a1 b0 b1 : - R a0 a1 -> - R b0 b1 -> - R (Pair a0 b0) (Pair a1 b1) - | ProjCong p a0 a1 : - R a0 a1 -> - R (Proj p a0) (Proj p a1) - | BindCong p A0 A1 B0 B1: - R A0 A1 -> - R B0 B1 -> - R (TBind p A0 B0) (TBind p A1 B1) - | BotCong : - R Bot Bot - | UnivCong i : - R (Univ i) (Univ i). +(* (*************** Congruence ********************) *) +(* | Var i : R (VarTm i) (VarTm i) *) +(* | AbsCong a0 a1 : *) +(* R a0 a1 -> *) +(* R (Abs a0) (Abs a1) *) +(* | AppCong a0 a1 b0 b1 : *) +(* R a0 a1 -> *) +(* R b0 b1 -> *) +(* R (App a0 b0) (App a1 b1) *) +(* | PairCong a0 a1 b0 b1 : *) +(* R a0 a1 -> *) +(* R b0 b1 -> *) +(* R (Pair a0 b0) (Pair a1 b1) *) +(* | ProjCong p a0 a1 : *) +(* R a0 a1 -> *) +(* R (Proj p a0) (Proj p a1) *) +(* | BindCong p A0 A1 B0 B1: *) +(* R A0 A1 -> *) +(* R B0 B1 -> *) +(* R (TBind p A0 B0) (TBind p A1 B1) *) +(* | BotCong : *) +(* R Bot Bot *) +(* | UnivCong i : *) +(* R (Univ i) (Univ i). *) - Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. +(* Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. *) - Lemma refl n (a : Tm n) : R a a. - Proof. - induction a; hauto lq:on ctrs:R. - Qed. +(* Lemma refl n (a : Tm n) : R a a. *) +(* Proof. *) +(* induction a; hauto lq:on ctrs:R. *) +(* Qed. *) - Lemma AppAbs' n a0 a1 (b0 b1 t : Tm n) : - t = subst_Tm (scons b1 VarTm) a1 -> - R a0 a1 -> - R b0 b1 -> - R (App (Abs a0) b0) t. - Proof. move => ->. apply AppAbs. Qed. +(* Lemma AppAbs' n a0 a1 (b0 b1 t : Tm n) : *) +(* t = subst_Tm (scons b1 VarTm) a1 -> *) +(* R a0 a1 -> *) +(* R b0 b1 -> *) +(* R (App (Abs a0) b0) t. *) +(* Proof. move => ->. apply AppAbs. Qed. *) - Lemma ProjPair' n p (a0 a1 b0 b1 : Tm n) t : - t = (if p is PL then a1 else b1) -> - R a0 a1 -> - R b0 b1 -> - R (Proj p (Pair a0 b0)) t. - Proof. move => > ->. apply ProjPair. Qed. +(* Lemma ProjPair' n p (a0 a1 b0 b1 : Tm n) t : *) +(* t = (if p is PL then a1 else b1) -> *) +(* R a0 a1 -> *) +(* R b0 b1 -> *) +(* R (Proj p (Pair a0 b0)) t. *) +(* Proof. move => > ->. apply ProjPair. Qed. *) - Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : - R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). - Proof. - move => h. move : m ξ. - elim : n a b /h. - move => *; apply : AppAbs'; eauto; by asimpl. - all : qauto ctrs:R use:ProjPair'. - Qed. +(* Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : *) +(* R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). *) +(* Proof. *) +(* move => h. move : m ξ. *) +(* elim : n a b /h. *) +(* move => *; apply : AppAbs'; eauto; by asimpl. *) +(* all : qauto ctrs:R use:ProjPair'. *) +(* Qed. *) - Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> Tm m) (ξ : fin m -> fin p) : - (forall i, R (ρ0 i) (ρ1 i)) -> - (forall i, R ((funcomp (ren_Tm ξ) ρ0) i) ((funcomp (ren_Tm ξ) ρ1) i)). - Proof. eauto using renaming. Qed. +(* Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> Tm m) (ξ : fin m -> fin p) : *) +(* (forall i, R (ρ0 i) (ρ1 i)) -> *) +(* (forall i, R ((funcomp (ren_Tm ξ) ρ0) i) ((funcomp (ren_Tm ξ) ρ1) i)). *) +(* Proof. eauto using renaming. Qed. *) - Lemma morphing_ext n m (ρ0 ρ1 : fin n -> Tm 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_ext n m (ρ0 ρ1 : fin n -> Tm 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 -> Tm m) : - (forall i, R (ρ0 i) (ρ1 i)) -> - (forall i, R (up_Tm_Tm ρ0 i) (up_Tm_Tm ρ1 i)). - Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_Tm_Tm. Qed. +(* Lemma morphing_up n m (ρ0 ρ1 : fin n -> Tm m) : *) +(* (forall i, R (ρ0 i) (ρ1 i)) -> *) +(* (forall i, R (up_Tm_Tm ρ0 i) (up_Tm_Tm ρ1 i)). *) +(* Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_Tm_Tm. Qed. *) - Lemma morphing n m (a b : Tm n) (ρ0 ρ1 : fin n -> Tm m) : - (forall i, R (ρ0 i) (ρ1 i)) -> - R a b -> R (subst_Tm ρ0 a) (subst_Tm ρ1 b). - Proof. - move => + h. move : m ρ0 ρ1. - elim : n a b /h. - - move => *. - apply : AppAbs'; eauto using morphing_up. - by asimpl. - - hauto lq:on ctrs:R use:ProjPair' use:morphing_up. - - hauto lq:on ctrs:R use:morphing_up. - - hauto lq:on ctrs:R use:morphing_up. - - 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. - - hauto lq:on ctrs:R. - - hauto lq:on ctrs:R. - Qed. +(* Lemma morphing n m (a b : Tm n) (ρ0 ρ1 : fin n -> Tm m) : *) +(* (forall i, R (ρ0 i) (ρ1 i)) -> *) +(* R a b -> R (subst_Tm ρ0 a) (subst_Tm ρ1 b). *) +(* Proof. *) +(* move => + h. move : m ρ0 ρ1. *) +(* elim : n a b /h. *) +(* - move => *. *) +(* apply : AppAbs'; eauto using morphing_up. *) +(* by asimpl. *) +(* - hauto lq:on ctrs:R use:ProjPair' use:morphing_up. *) +(* - hauto lq:on ctrs:R use:morphing_up. *) +(* - hauto lq:on ctrs:R use:morphing_up. *) +(* - 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. *) +(* - hauto lq:on ctrs:R. *) +(* - hauto lq:on ctrs:R. *) +(* Qed. *) - Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : - R a b -> - R (subst_Tm ρ a) (subst_Tm ρ b). - Proof. hauto l:on use:morphing, refl. Qed. +(* Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : *) +(* R a b -> *) +(* R (subst_Tm ρ a) (subst_Tm ρ b). *) +(* Proof. hauto l:on use:morphing, refl. Qed. *) - Lemma cong n (a b : Tm (S n)) c d : - R a b -> - R c d -> - R (subst_Tm (scons c VarTm) a) (subst_Tm (scons d VarTm) b). - Proof. - move => h0 h1. apply morphing => //=. - qauto l:on ctrs:R inv:option. - Qed. +(* Lemma cong n (a b : Tm (S n)) c d : *) +(* R a b -> *) +(* R c d -> *) +(* R (subst_Tm (scons c VarTm) a) (subst_Tm (scons d VarTm) b). *) +(* Proof. *) +(* move => h0 h1. apply morphing => //=. *) +(* qauto l:on ctrs:R inv:option. *) +(* Qed. *) - Lemma var_or_bot_imp {n} (a b : Tm n) : - var_or_bot a -> - a = b -> ~~ var_or_bot b -> False. - Proof. - hauto lq:on inv:Tm. - Qed. +(* Lemma var_or_bot_imp {n} (a b : Tm n) : *) +(* var_or_bot a -> *) +(* a = b -> ~~ var_or_bot b -> False. *) +(* Proof. *) +(* hauto lq:on inv:Tm. *) +(* Qed. *) - Lemma var_or_bot_up n m (ρ : fin n -> Tm m) : - (forall i, var_or_bot (ρ i)) -> - (forall i, var_or_bot (up_Tm_Tm ρ i)). - Proof. - move => h /= [i|]. - - asimpl. - move /(_ i) in h. - rewrite /funcomp. - move : (ρ i) h. - case => //=. - - sfirstorder. - Qed. +(* Lemma var_or_bot_up n m (ρ : fin n -> Tm m) : *) +(* (forall i, var_or_bot (ρ i)) -> *) +(* (forall i, var_or_bot (up_Tm_Tm ρ i)). *) +(* Proof. *) +(* move => h /= [i|]. *) +(* - asimpl. *) +(* move /(_ i) in h. *) +(* rewrite /funcomp. *) +(* move : (ρ i) h. *) +(* case => //=. *) +(* - sfirstorder. *) +(* Qed. *) - Local Ltac antiimp := qauto l:on use:var_or_bot_imp. +(* Local Ltac antiimp := qauto l:on use:var_or_bot_imp. *) - Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) : - (forall i, var_or_bot (ρ i)) -> - R (subst_Tm ρ a) b -> exists b0, R a b0 /\ subst_Tm ρ b0 = b. - Proof. - move E : (subst_Tm ρ a) => u hρ h. - move : n ρ hρ a E. elim : m u b/h. - - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; - first by antiimp. - move => c c0 [+ ?]. subst. - case : c => //=; first by antiimp. - move => c [?]. subst. - spec_refl. - have /var_or_bot_up hρ' := hρ. - move : iha hρ' => /[apply] iha. - move : ihb hρ => /[apply] ihb. - spec_refl. - move : iha => [c1][ih0]?. subst. - move : ihb => [c2][ih1]?. subst. - eexists. split. - apply AppAbs; eauto. - by asimpl. - - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; - first by antiimp. - move => p0 []//=; first by antiimp. move => t t0[*]. - subst. - have {}/iha := (hρ) => iha. - have {}/ihb := (hρ) => ihb. - spec_refl. - move : iha => [b0 [? ?]]. - move : ihb => [c0 [? ?]]. subst. - eexists. split. by eauto using ProjPair. - hauto q:on. - - move => n i m ρ hρ []//=. - hauto l:on. - - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp. - move => t [*]. subst. - have /var_or_bot_up {}/iha := hρ => iha. - spec_refl. - move :iha => [b0 [? ?]]. subst. - eexists. split. by apply AbsCong; eauto. - by asimpl. - - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; - first by antiimp. - move => t t0 [*]. subst. - have {}/iha := (hρ) => iha. - have {}/ihb := (hρ) => ihb. - spec_refl. - move : iha => [b0 [? ?]]. subst. - move : ihb => [c0 [? ?]]. subst. - eexists. split. by apply AppCong; eauto. - done. - - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; - first by antiimp. - move => t t0[*]. subst. - have {}/iha := (hρ) => iha. - have {}/ihb := (hρ) => ihb. - spec_refl. - move : iha => [b0 [? ?]]. subst. - move : ihb => [c0 [? ?]]. subst. - eexists. split. by apply PairCong; eauto. - by asimpl. - - move => n p a0 a1 ha iha m ρ hρ []//=; - first by antiimp. - move => p0 t [*]. subst. - have {}/iha := (hρ) => iha. - spec_refl. - move : iha => [b0 [? ?]]. subst. - eexists. split. apply ProjCong; eauto. reflexivity. - - move => n p A0 A1 B0 B1 ha iha hB ihB m ρ hρ []//=; - first by antiimp. - move => ? t t0 [*]. subst. - have {}/iha := (hρ) => iha. - have /var_or_bot_up {}/ihB := (hρ) => ihB. - spec_refl. - move : iha => [b0 [? ?]]. - move : ihB => [c0 [? ?]]. subst. - eexists. split. by apply BindCong; eauto. - by asimpl. - - hauto q:on ctrs:R inv:Tm. - - move => n i n0 ρ hρ []//=; first by antiimp. - hauto l:on. - Qed. -End RPar'. +(* Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) : *) +(* (forall i, var_or_bot (ρ i)) -> *) +(* R (subst_Tm ρ a) b -> exists b0, R a b0 /\ subst_Tm ρ b0 = b. *) +(* Proof. *) +(* move E : (subst_Tm ρ a) => u hρ h. *) +(* move : n ρ hρ a E. elim : m u b/h. *) +(* - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; *) +(* first by antiimp. *) +(* move => c c0 [+ ?]. subst. *) +(* case : c => //=; first by antiimp. *) +(* move => c [?]. subst. *) +(* spec_refl. *) +(* have /var_or_bot_up hρ' := hρ. *) +(* move : iha hρ' => /[apply] iha. *) +(* move : ihb hρ => /[apply] ihb. *) +(* spec_refl. *) +(* move : iha => [c1][ih0]?. subst. *) +(* move : ihb => [c2][ih1]?. subst. *) +(* eexists. split. *) +(* apply AppAbs; eauto. *) +(* by asimpl. *) +(* - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; *) +(* first by antiimp. *) +(* move => p0 []//=; first by antiimp. move => t t0[*]. *) +(* subst. *) +(* have {}/iha := (hρ) => iha. *) +(* have {}/ihb := (hρ) => ihb. *) +(* spec_refl. *) +(* move : iha => [b0 [? ?]]. *) +(* move : ihb => [c0 [? ?]]. subst. *) +(* eexists. split. by eauto using ProjPair. *) +(* hauto q:on. *) +(* - move => n i m ρ hρ []//=. *) +(* hauto l:on. *) +(* - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp. *) +(* move => t [*]. subst. *) +(* have /var_or_bot_up {}/iha := hρ => iha. *) +(* spec_refl. *) +(* move :iha => [b0 [? ?]]. subst. *) +(* eexists. split. by apply AbsCong; eauto. *) +(* by asimpl. *) +(* - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; *) +(* first by antiimp. *) +(* move => t t0 [*]. subst. *) +(* have {}/iha := (hρ) => iha. *) +(* have {}/ihb := (hρ) => ihb. *) +(* spec_refl. *) +(* move : iha => [b0 [? ?]]. subst. *) +(* move : ihb => [c0 [? ?]]. subst. *) +(* eexists. split. by apply AppCong; eauto. *) +(* done. *) +(* - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; *) +(* first by antiimp. *) +(* move => t t0[*]. subst. *) +(* have {}/iha := (hρ) => iha. *) +(* have {}/ihb := (hρ) => ihb. *) +(* spec_refl. *) +(* move : iha => [b0 [? ?]]. subst. *) +(* move : ihb => [c0 [? ?]]. subst. *) +(* eexists. split. by apply PairCong; eauto. *) +(* by asimpl. *) +(* - move => n p a0 a1 ha iha m ρ hρ []//=; *) +(* first by antiimp. *) +(* move => p0 t [*]. subst. *) +(* have {}/iha := (hρ) => iha. *) +(* spec_refl. *) +(* move : iha => [b0 [? ?]]. subst. *) +(* eexists. split. apply ProjCong; eauto. reflexivity. *) +(* - move => n p A0 A1 B0 B1 ha iha hB ihB m ρ hρ []//=; *) +(* first by antiimp. *) +(* move => ? t t0 [*]. subst. *) +(* have {}/iha := (hρ) => iha. *) +(* have /var_or_bot_up {}/ihB := (hρ) => ihB. *) +(* spec_refl. *) +(* move : iha => [b0 [? ?]]. *) +(* move : ihB => [c0 [? ?]]. subst. *) +(* eexists. split. by apply BindCong; eauto. *) +(* by asimpl. *) +(* - hauto q:on ctrs:R inv:Tm. *) +(* - move => n i n0 ρ hρ []//=; first by antiimp. *) +(* hauto l:on. *) +(* Qed. *) +(* End RPar'. *) -Module ERed. - Inductive R {n} : Tm n -> Tm n -> Prop := - (****************** Eta ***********************) - | AppEta a : - R a (Abs (App (ren_Tm shift a) (VarTm var_zero))) - | PairEta a : - R a (Pair (Proj PL a) (Proj PR a)) +(* Module ERed. *) +(* Inductive R {n} : Tm n -> Tm n -> Prop := *) +(* (****************** Eta ***********************) *) +(* | AppEta a : *) +(* R a (Abs (App (ren_Tm shift a) (VarTm var_zero))) *) +(* | PairEta a : *) +(* R a (Pair (Proj PL a) (Proj PR a)) *) - (*************** Congruence ********************) - | AbsCong a0 a1 : - R a0 a1 -> - R (Abs a0) (Abs a1) - | AppCong0 a0 a1 b : - R a0 a1 -> - R (App a0 b) (App a1 b) - | AppCong1 a b0 b1 : - R b0 b1 -> - R (App a b0) (App a b1) - | PairCong0 a0 a1 b : - R a0 a1 -> - R (Pair a0 b) (Pair a1 b) - | PairCong1 a b0 b1 : - R b0 b1 -> - R (Pair a b0) (Pair a b1) - | ProjCong p a0 a1 : - R a0 a1 -> - R (Proj p a0) (Proj p a1) - | BindCong0 p A0 A1 B: - R A0 A1 -> - R (TBind p A0 B) (TBind p A1 B) - | BindCong1 p A B0 B1: - R B0 B1 -> - R (TBind p A B0) (TBind p A B1). +(* (*************** Congruence ********************) *) +(* | AbsCong a0 a1 : *) +(* R a0 a1 -> *) +(* R (Abs a0) (Abs a1) *) +(* | AppCong0 a0 a1 b : *) +(* R a0 a1 -> *) +(* R (App a0 b) (App a1 b) *) +(* | AppCong1 a b0 b1 : *) +(* R b0 b1 -> *) +(* R (App a b0) (App a b1) *) +(* | PairCong0 a0 a1 b : *) +(* R a0 a1 -> *) +(* R (Pair a0 b) (Pair a1 b) *) +(* | PairCong1 a b0 b1 : *) +(* R b0 b1 -> *) +(* R (Pair a b0) (Pair a b1) *) +(* | ProjCong p a0 a1 : *) +(* R a0 a1 -> *) +(* R (Proj p a0) (Proj p a1) *) +(* | BindCong0 p A0 A1 B: *) +(* R A0 A1 -> *) +(* R (TBind p A0 B) (TBind p A1 B) *) +(* | BindCong1 p A B0 B1: *) +(* R B0 B1 -> *) +(* R (TBind p A B0) (TBind p A B1). *) - Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. +(* Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. *) - Lemma AppEta' n a (u : Tm n) : - u = (Abs (App (ren_Tm shift a) (VarTm var_zero))) -> - R a u. - Proof. move => ->. apply AppEta. Qed. +(* Lemma AppEta' n a (u : Tm n) : *) +(* u = (Abs (App (ren_Tm shift a) (VarTm var_zero))) -> *) +(* R a u. *) +(* Proof. move => ->. apply AppEta. Qed. *) - Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : - R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). - Proof. - move => h. move : m ξ. - elim : n a b /h. +(* Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : *) +(* R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). *) +(* Proof. *) +(* move => h. move : m ξ. *) +(* elim : n a b /h. *) - move => n a m ξ. - apply AppEta'. by asimpl. - all : qauto ctrs:R. - Qed. +(* move => n a m ξ. *) +(* apply AppEta'. by asimpl. *) +(* all : qauto ctrs:R. *) +(* Qed. *) - Lemma substing n m (a : Tm n) b (ρ : fin n -> Tm m) : - R a b -> - R (subst_Tm ρ a) (subst_Tm ρ b). - Proof. - move => h. move : m ρ. elim : n a b / h => n. - move => a m ρ /=. - apply : AppEta'; eauto. by asimpl. - all : hauto ctrs:R inv:option use:renaming. - Qed. +(* Lemma substing n m (a : Tm n) b (ρ : fin n -> Tm m) : *) +(* R a b -> *) +(* R (subst_Tm ρ a) (subst_Tm ρ b). *) +(* Proof. *) +(* move => h. move : m ρ. elim : n a b / h => n. *) +(* move => a m ρ /=. *) +(* apply : AppEta'; eauto. by asimpl. *) +(* all : hauto ctrs:R inv:option use:renaming. *) +(* Qed. *) -End ERed. +(* End ERed. *) -Module EReds. +(* Module EReds. *) - #[local]Ltac solve_s_rec := - move => *; eapply rtc_l; eauto; - hauto lq:on ctrs:ERed.R. +(* #[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. +(* #[local]Ltac solve_s := *) +(* repeat (induction 1; last by solve_s_rec); apply rtc_refl. *) - Lemma AbsCong n (a b : Tm (S n)) : - rtc ERed.R a b -> - rtc ERed.R (Abs a) (Abs b). - Proof. solve_s. Qed. +(* Lemma AbsCong n (a b : Tm (S n)) : *) +(* rtc ERed.R a b -> *) +(* rtc ERed.R (Abs a) (Abs b). *) +(* Proof. solve_s. Qed. *) - Lemma AppCong n (a0 a1 b0 b1 : Tm n) : - rtc ERed.R a0 a1 -> - rtc ERed.R b0 b1 -> - rtc ERed.R (App a0 b0) (App a1 b1). - Proof. solve_s. Qed. +(* Lemma AppCong n (a0 a1 b0 b1 : Tm n) : *) +(* rtc ERed.R a0 a1 -> *) +(* rtc ERed.R b0 b1 -> *) +(* rtc ERed.R (App a0 b0) (App a1 b1). *) +(* Proof. solve_s. Qed. *) - Lemma BindCong n p (a0 a1 : Tm n) b0 b1 : - rtc ERed.R a0 a1 -> - rtc ERed.R b0 b1 -> - rtc ERed.R (TBind p a0 b0) (TBind p a1 b1). - Proof. solve_s. Qed. +(* Lemma BindCong n p (a0 a1 : Tm n) b0 b1 : *) +(* rtc ERed.R a0 a1 -> *) +(* rtc ERed.R b0 b1 -> *) +(* rtc ERed.R (TBind p a0 b0) (TBind p a1 b1). *) +(* Proof. solve_s. Qed. *) - Lemma PairCong n (a0 a1 b0 b1 : Tm n) : - rtc ERed.R a0 a1 -> - rtc ERed.R b0 b1 -> - rtc ERed.R (Pair a0 b0) (Pair a1 b1). - Proof. solve_s. Qed. +(* Lemma PairCong n (a0 a1 b0 b1 : Tm n) : *) +(* rtc ERed.R a0 a1 -> *) +(* rtc ERed.R b0 b1 -> *) +(* rtc ERed.R (Pair a0 b0) (Pair a1 b1). *) +(* Proof. solve_s. Qed. *) - Lemma ProjCong n p (a0 a1 : Tm n) : - rtc ERed.R a0 a1 -> - rtc ERed.R (Proj p a0) (Proj p a1). - Proof. solve_s. Qed. -End EReds. +(* Lemma ProjCong n p (a0 a1 : Tm n) : *) +(* rtc ERed.R a0 a1 -> *) +(* rtc ERed.R (Proj p a0) (Proj p a1). *) +(* Proof. solve_s. Qed. *) +(* End EReds. *) Module EPar. Inductive R {n} : Tm n -> Tm n -> Prop := @@ -991,7 +1079,16 @@ Module EPar. | BotCong : R Bot Bot | UnivCong i : - R (Univ i) (Univ i). + R (Univ i) (Univ i) + | BoolCong : + R Bool Bool + | BValCong b : + R (BVal b) (BVal b) + | IfCong a0 a1 b0 b1 c0 c1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R (If a0 b0 c0) (If a1 b1 c1). Lemma refl n (a : Tm n) : EPar.R a a. Proof. @@ -1036,6 +1133,9 @@ Module EPar. - hauto l:on ctrs:R use:renaming inv:option. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. Qed. Lemma substing n a0 a1 (b0 b1 : Tm n) : @@ -1125,6 +1225,13 @@ Module RPars. rtc RPar.R (Pair a0 b0) (Pair a1 b1). Proof. solve_s. Qed. + Lemma IfCong n (a0 a1 b0 b1 c0 c1 : Tm n) : + rtc RPar.R a0 a1 -> + rtc RPar.R b0 b1 -> + rtc RPar.R c0 c1 -> + rtc RPar.R (If a0 b0 c0) (If a1 b1 c1). + Proof. solve_s. Qed. + Lemma ProjCong n p (a0 a1 : Tm n) : rtc RPar.R a0 a1 -> rtc RPar.R (Proj p a0) (Proj p a1). @@ -1180,92 +1287,92 @@ Module RPars. End RPars. -Module RPars'. +(* Module RPars'. *) - #[local]Ltac solve_s_rec := - move => *; eapply rtc_l; eauto; - hauto lq:on ctrs:RPar'.R use:RPar'.refl. +(* #[local]Ltac solve_s_rec := *) +(* move => *; eapply rtc_l; eauto; *) +(* hauto lq:on ctrs:RPar'.R use:RPar'.refl. *) - #[local]Ltac solve_s := - repeat (induction 1; last by solve_s_rec); apply rtc_refl. +(* #[local]Ltac solve_s := *) +(* repeat (induction 1; last by solve_s_rec); apply rtc_refl. *) - Lemma AbsCong n (a b : Tm (S n)) : - rtc RPar'.R a b -> - rtc RPar'.R (Abs a) (Abs b). - Proof. solve_s. Qed. +(* Lemma AbsCong n (a b : Tm (S n)) : *) +(* rtc RPar'.R a b -> *) +(* rtc RPar'.R (Abs a) (Abs b). *) +(* Proof. solve_s. Qed. *) - Lemma AppCong n (a0 a1 b0 b1 : Tm n) : - rtc RPar'.R a0 a1 -> - rtc RPar'.R b0 b1 -> - rtc RPar'.R (App a0 b0) (App a1 b1). - Proof. solve_s. Qed. +(* Lemma AppCong n (a0 a1 b0 b1 : Tm n) : *) +(* rtc RPar'.R a0 a1 -> *) +(* rtc RPar'.R b0 b1 -> *) +(* rtc RPar'.R (App a0 b0) (App a1 b1). *) +(* Proof. solve_s. Qed. *) - Lemma BindCong n p (a0 a1 : Tm n) b0 b1 : - rtc RPar'.R a0 a1 -> - rtc RPar'.R b0 b1 -> - rtc RPar'.R (TBind p a0 b0) (TBind p a1 b1). - Proof. solve_s. Qed. +(* Lemma BindCong n p (a0 a1 : Tm n) b0 b1 : *) +(* rtc RPar'.R a0 a1 -> *) +(* rtc RPar'.R b0 b1 -> *) +(* rtc RPar'.R (TBind p a0 b0) (TBind p 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 -> - rtc RPar'.R (Pair a0 b0) (Pair 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 -> *) +(* rtc RPar'.R (Pair a0 b0) (Pair a1 b1). *) +(* Proof. solve_s. Qed. *) - Lemma ProjCong n p (a0 a1 : Tm n) : - rtc RPar'.R a0 a1 -> - rtc RPar'.R (Proj p a0) (Proj p a1). - Proof. solve_s. Qed. +(* Lemma ProjCong n p (a0 a1 : Tm n) : *) +(* rtc RPar'.R a0 a1 -> *) +(* rtc RPar'.R (Proj p a0) (Proj p a1). *) +(* Proof. solve_s. Qed. *) - Lemma renaming n (a0 a1 : Tm n) m (ξ : fin n -> fin m) : - rtc RPar'.R a0 a1 -> - rtc RPar'.R (ren_Tm ξ a0) (ren_Tm ξ a1). - Proof. - induction 1. - - apply rtc_refl. - - eauto using RPar'.renaming, rtc_l. - Qed. +(* Lemma renaming n (a0 a1 : Tm n) m (ξ : fin n -> fin m) : *) +(* rtc RPar'.R a0 a1 -> *) +(* rtc RPar'.R (ren_Tm ξ a0) (ren_Tm ξ a1). *) +(* Proof. *) +(* induction 1. *) +(* - apply rtc_refl. *) +(* - eauto using RPar'.renaming, rtc_l. *) +(* Qed. *) - Lemma weakening n (a0 a1 : Tm n) : - rtc RPar'.R a0 a1 -> - rtc RPar'.R (ren_Tm shift a0) (ren_Tm shift a1). - Proof. apply renaming. Qed. +(* Lemma weakening n (a0 a1 : Tm n) : *) +(* rtc RPar'.R a0 a1 -> *) +(* rtc RPar'.R (ren_Tm shift a0) (ren_Tm shift a1). *) +(* Proof. apply renaming. Qed. *) - Lemma Abs_inv n (a : Tm (S n)) b : - rtc RPar'.R (Abs a) b -> exists a', b = Abs a' /\ rtc RPar'.R a a'. - Proof. - move E : (Abs a) => b0 h. move : a E. - elim : b0 b / h. - - hauto lq:on ctrs:rtc. - - hauto lq:on ctrs:rtc inv:RPar'.R, rtc. - Qed. +(* Lemma Abs_inv n (a : Tm (S n)) b : *) +(* rtc RPar'.R (Abs a) b -> exists a', b = Abs a' /\ rtc RPar'.R a a'. *) +(* Proof. *) +(* move E : (Abs a) => b0 h. move : a E. *) +(* elim : b0 b / h. *) +(* - hauto lq:on ctrs:rtc. *) +(* - hauto lq:on ctrs:rtc inv:RPar'.R, rtc. *) +(* Qed. *) - Lemma morphing n m (a b : Tm n) (ρ : fin n -> Tm m) : - rtc RPar'.R a b -> - rtc RPar'.R (subst_Tm ρ a) (subst_Tm ρ b). - Proof. induction 1; qauto l:on ctrs:rtc use:RPar'.substing. Qed. +(* Lemma morphing n m (a b : Tm n) (ρ : fin n -> Tm m) : *) +(* rtc RPar'.R a b -> *) +(* rtc RPar'.R (subst_Tm ρ a) (subst_Tm ρ b). *) +(* Proof. induction 1; qauto l:on ctrs:rtc use:RPar'.substing. Qed. *) - Lemma substing n (a b : Tm (S n)) c : - rtc RPar'.R a b -> - rtc RPar'.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b). - Proof. hauto lq:on use:morphing inv:option. Qed. +(* Lemma substing n (a b : Tm (S n)) c : *) +(* rtc RPar'.R a b -> *) +(* rtc RPar'.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b). *) +(* Proof. hauto lq:on use:morphing inv:option. Qed. *) - Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) : - (forall i, var_or_bot (ρ i)) -> - rtc RPar'.R (subst_Tm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ subst_Tm ρ b0 = b. - Proof. - move E :(subst_Tm ρ a) => u hρ h. - move : a E. - elim : u b /h. - - sfirstorder. - - move => a b c h0 h1 ih1 a0 ?. subst. - move /RPar'.antirenaming : h0. - move /(_ hρ). - move => [b0 [h2 ?]]. subst. - hauto lq:on rew:off ctrs:rtc. - Qed. +(* Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) : *) +(* (forall i, var_or_bot (ρ i)) -> *) +(* rtc RPar'.R (subst_Tm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ subst_Tm ρ b0 = b. *) +(* Proof. *) +(* move E :(subst_Tm ρ a) => u hρ h. *) +(* move : a E. *) +(* elim : u b /h. *) +(* - sfirstorder. *) +(* - move => a b c h0 h1 ih1 a0 ?. subst. *) +(* move /RPar'.antirenaming : h0. *) +(* move /(_ hρ). *) +(* move => [b0 [h2 ?]]. subst. *) +(* hauto lq:on rew:off ctrs:rtc. *) +(* Qed. *) -End RPars'. +(* End RPars'. *) Lemma Abs_EPar n a (b : Tm n) : EPar.R (Abs a) b -> @@ -1421,6 +1528,7 @@ Proof. split. hauto lq:on use:relations.rtc_transitive, RPars.AppCong. apply EPar.PairCong; by apply EPar.AppCong. + + admit. + hauto lq:on ctrs:EPar.R use:RPars.AppCong. - hauto lq:on ctrs:EPar.R inv:RPar.R use:RPars.PairCong. - move => n p a b0 h0 ih0 b1. @@ -1435,11 +1543,21 @@ Proof. move /Pair_EPar : ih1 => [/(_ p)[d [ihd ihd']] _]. exists d. split => //. hauto lq:on use:RPars.ProjCong, relations.rtc_transitive. + + admit. + hauto lq:on ctrs:EPar.R use:RPars.ProjCong. - hauto lq:on inv:RPar.R ctrs:EPar.R, rtc use:RPars.BindCong. - hauto l:on ctrs:EPar.R inv:RPar.R. - hauto l:on ctrs:EPar.R inv:RPar.R. -Qed. + - hauto l:on ctrs:EPar.R inv:RPar.R. + - hauto l:on ctrs:EPar.R inv:RPar.R. + - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc u. + elim /RPar.inv => //= _. + + admit. + + admit. + + admit. + + (* Need the rule that if commutes with abs *) + admit. +Admitted. Lemma commutativity1 n (a b0 b1 : Tm n) : EPar.R a b0 -> rtc RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c. @@ -1615,7 +1733,10 @@ Proof. exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge. - qauto use:Bot_EPar', EPar.refl. - qauto use:Univ_EPar', EPar.refl. -Qed. + - admit. + - admit. + - admit. +Admitted. Function tstar {n} (a : Tm n) := match a with From d0760cd9dbb99910918cebd24a29b9abe6ddb985 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sat, 11 Jan 2025 00:07:30 -0500 Subject: [PATCH 04/17] Stuck at commutativity (trouble with if pair) --- theories/fp_red.v | 48 ++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 45 insertions(+), 3 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index a8c8a3a..5094c57 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -1374,6 +1374,11 @@ End RPars. (* End RPars'. *) +(* (forall p, exists d, rtc RPar.R (Proj p c) d /\ EPar.R (if p is PL then a else b) d) *) +(* (exists d0 d1, rtc RPar.R (App (ren_Tm shift c) (VarTm var_zero)) *) +(* (Pair (App (ren_Tm shift d0) (VarTm var_zero))(App (ren_Tm shift d1) (VarTm var_zero))) /\ *) +(* EPar.R a d0 /\ EPar.R b d1) *) + Lemma Abs_EPar n a (b : Tm n) : EPar.R (Abs a) b -> (exists d, EPar.R a d /\ @@ -1426,6 +1431,32 @@ Proof. apply rtc_once. apply : RPar.ProjAbs; eauto using RPar.refl. Qed. +Lemma Abs_EPar_If n (a : Tm (S n)) q : + EPar.R (Abs a) q -> + exists d, EPar.R a d /\ + forall b c, rtc RPar.R (If q b c) (Abs (If d (ren_Tm shift b) (ren_Tm shift c))). +Proof. + move E : (Abs a) => u h. + move : a E. + elim : n u q /h => //= n. + - move => a0 a1 ha _ b ?. subst. + move /Abs_EPar : ha. + move => [[d [h0 h1]] _]. + exists d. + split => // b0 c. + apply : rtc_l. + apply RPar.IfAbs; auto using RPar.refl. + apply RPars.AbsCong. + apply RPars.IfCong; auto using rtc_refl. + - move => a0 a1 ha _ a ?. subst. + move /Abs_EPar : ha => [_ [d [h0 h1]]]. + exists d. split => //. + move => b c. + apply : rtc_l. + apply RPar.IfPair; auto using RPar.refl. +Admitted. + + Lemma Pair_EPar n (a b c : Tm n) : EPar.R (Pair a b) c -> (forall p, exists d, rtc RPar.R (Proj p c) d /\ EPar.R (if p is PL then a else b) d) /\ @@ -1528,7 +1559,9 @@ Proof. split. hauto lq:on use:relations.rtc_transitive, RPars.AppCong. apply EPar.PairCong; by apply EPar.AppCong. - + admit. + + case : a0 ha iha => //=. + move => b ha hc b3 a0 [*]. subst. + admit. + hauto lq:on ctrs:EPar.R use:RPars.AppCong. - hauto lq:on ctrs:EPar.R inv:RPar.R use:RPars.PairCong. - move => n p a b0 h0 ih0 b1. @@ -1543,7 +1576,8 @@ Proof. move /Pair_EPar : ih1 => [/(_ p)[d [ihd ihd']] _]. exists d. split => //. hauto lq:on use:RPars.ProjCong, relations.rtc_transitive. - + admit. + + move => p0 b2 [*]. subst. + admit. + hauto lq:on ctrs:EPar.R use:RPars.ProjCong. - hauto lq:on inv:RPar.R ctrs:EPar.R, rtc use:RPars.BindCong. - hauto l:on ctrs:EPar.R inv:RPar.R. @@ -1552,7 +1586,15 @@ Proof. - hauto l:on ctrs:EPar.R inv:RPar.R. - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc u. elim /RPar.inv => //= _. - + admit. + + move => a2 a3 b2 b3 c2 c3 ha2 hb2 hc2 [*]. subst. + move /(_ _ ltac:(by eauto using RPar.AbsCong)) : iha => [c [ih0 ih1]]. + move /Abs_EPar : ih1 => [[d [ih2 ih3]] _]. + have {}/ihb := hb2. move => [b4 [ihb0 ihb1]]. + have {}/ihc := hc2. move => [c4 [ihc0 ihc1]]. + + exists (Abs (If d (ren_Tm shift b4) (ren_Tm shift c4))). + split. admit. + hauto lq:on ctrs:EPar.R use:EPar.renaming. + admit. + admit. + (* Need the rule that if commutes with abs *) From c9fcafb47fec609658fca8c1b1747cb8ee38ec9d Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 12 Jan 2025 16:08:56 -0500 Subject: [PATCH 05/17] Add commutativity rules for eliminators --- theories/fp_red.v | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 5094c57..83ee0ff 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -100,7 +100,18 @@ Module Par. R a0 a1 -> R b0 b1 -> R c0 c1 -> - R (If a0 b0 c0) (If a1 b1 c1). + R (If a0 b0 c0) (If a1 b1 c1) + | IfApp a0 a1 b0 b1 c0 c1 d0 d1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R d0 d1 -> + R (If (App a0 b0) c0 d0) (App (If a1 c1 d1) b1) + | IfProj p a0 a1 b0 b1 c0 c1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R (If (Proj p a0) b0 c0) (Proj p (If a1 b1 c1)). Lemma refl n (a : Tm n) : R a a. elim : n /a; hauto ctrs:R. @@ -187,6 +198,8 @@ Module Par. - sfirstorder. - sfirstorder. - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. + - qauto l:on ctrs:R. Qed. Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : @@ -296,6 +309,11 @@ Module Par. - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ξ []//= t t0 t1[*]. subst. spec_refl. qauto l:on ctrs:R. + - move => n a0 a1 b0 b1 c0 c1 d0 d1 ha iha hb ihb hc ihc hd ihd m ξ []//= t0 t1 t2 [h *]. subst. + case : t0 h => //= t t0 [*]. subst. + qauto l:on ctrs:R. + - move => n p a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ξ []//= t0 t1 t [h *]. subst. + case : t0 h => //=. qauto l:on ctrs:R. Qed. End Par. From bc848e91ea7e9c038d18aa5855973920b387bc31 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 12 Jan 2025 16:42:09 -0500 Subject: [PATCH 06/17] Modify the definition of tstar to evaluate more aggressively --- theories/fp_red.v | 123 ++++++++++++++++++++++++---------------------- 1 file changed, 64 insertions(+), 59 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 83ee0ff..38125c8 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -33,8 +33,6 @@ Module Par. R b0 b1 -> R c0 c1 -> R (App (Pair a0 b0) c0) (Pair (App a1 c1) (App b1 c1)) - | AppBool b a : - R (App (BVal b) a) (BVal b) | ProjAbs p a0 a1 : R a0 a1 -> R (Proj p (Abs a0)) (Abs (Proj p a1)) @@ -42,8 +40,6 @@ Module Par. R a0 a1 -> R b0 b1 -> R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) - | ProjBool p b : - R (Proj p (BVal b)) (BVal b) | IfAbs (a0 a1 : Tm (S n)) b0 b1 c0 c1 : R a0 a1 -> R b0 b1 -> @@ -175,10 +171,8 @@ Module Par. by asimpl. hauto l:on use:renaming inv:option. - hauto lq:on rew:off ctrs:R. - - hauto lq:on rew:off ctrs:R. - hauto l:on inv:option use:renaming ctrs:R. - hauto lq:on use:ProjPair'. - - hauto lq:on rew:off ctrs:R. - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ0 ρ1 hρ /=. eapply IfAbs' with (a1 := (subst_Tm (up_Tm_Tm ρ1) a1)); eauto. by asimpl. hauto l:on use:renaming inv:option. @@ -230,8 +224,6 @@ Module Par. eexists. split. apply AppPair; hauto. subst. by asimpl. - - move => n b a m ξ []//=. - hauto q:on ctrs:R inv:Tm. - move => n p a0 a1 ha iha m ξ []//= p0 []//= t [*]. subst. spec_refl. move : iha => [b0 [? ?]]. subst. eexists. split. apply ProjAbs; eauto. by asimpl. @@ -241,9 +233,6 @@ Module Par. move : ihb => [c0 [? ?]]. subst. eexists. split. by eauto using ProjPair. hauto q:on. - - move => n p b m ξ []//=. - move => + []//=. - hauto lq:on ctrs:R. - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ξ []//= t t0 t1 [h *]. subst. case : t h => // t [*]. subst. spec_refl. @@ -395,8 +384,6 @@ Module RPar. R b0 b1 -> R c0 c1 -> R (App (Pair a0 b0) c0) (Pair (App a1 c1) (App b1 c1)) - | AppBool b a : - R (App (BVal b) a) (BVal b) | ProjAbs p a0 a1 : R a0 a1 -> R (Proj p (Abs a0)) (Abs (Proj p a1)) @@ -404,8 +391,6 @@ Module RPar. R a0 a1 -> R b0 b1 -> R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) - | ProjBool p b : - R (Proj p (BVal b)) (BVal b) | IfAbs (a0 a1 : Tm (S n)) b0 b1 c0 c1 : R a0 a1 -> R b0 b1 -> @@ -455,7 +440,18 @@ Module RPar. R a0 a1 -> R b0 b1 -> R c0 c1 -> - R (If a0 b0 c0) (If a1 b1 c1). + R (If a0 b0 c0) (If a1 b1 c1) + | IfApp a0 a1 b0 b1 c0 c1 d0 d1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R d0 d1 -> + R (If (App a0 b0) c0 d0) (App (If a1 c1 d1) b1) + | IfProj p a0 a1 b0 b1 c0 c1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R (If (Proj p a0) b0 c0) (Proj p (If a1 b1 c1)). Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. @@ -528,10 +524,8 @@ Module RPar. apply : AppAbs'; eauto using morphing_up. by asimpl. - hauto lq:on ctrs:R. - - hauto lq:on ctrs:R. - hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R use:ProjPair' use:morphing_up. - - sfirstorder. - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ0 ρ1 hρ /=. apply : IfAbs'; eauto using morphing_up. by asimpl. @@ -548,6 +542,8 @@ Module RPar. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. + - hauto lq:on ctrs:R. Qed. Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : @@ -621,9 +617,6 @@ Module RPar. eexists. split. apply AppPair; hauto. subst. by asimpl. - - move => n b a m ρ hρ []//=; first by antiimp. - case => //=; first by antiimp. - hauto lq:on ctrs:R. - move => n p a0 a1 ha iha m ρ hρ []//=; first by antiimp. move => p0 []//= t [*]; first by antiimp. subst. @@ -641,9 +634,6 @@ Module RPar. move : ihb => [c0 [? ?]]. subst. eexists. split. by eauto using ProjPair. hauto q:on. - - move => n p b m ρ hρ []//=; first by antiimp. - move => p0 + []//=. case => //=; first by antiimp. - hauto lq:on ctrs:R. - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=; first by antiimp. move => + b2 c2 [+ *]. subst. case => //=; first by antiimp. move => a [*]. subst. @@ -734,7 +724,57 @@ Module RPar. have {}/ihc := (hρ) => ihc. spec_refl. hauto lq:on ctrs:R. + Admitted. + + Function tstar {n} (a : Tm n) := + match a with + | VarTm i => a + | Abs a => Abs (tstar a) + | App a b => match tstar a with + | Abs a => subst_Tm (scons (tstar b) VarTm) a + | Pair a c => Pair (App a (tstar b)) (App c (tstar b)) + | _ => App (tstar a) (tstar b) + end + | Pair a b => Pair (tstar a) (tstar b) + | Proj p a => match tstar a with + | Pair a b => if p is PL then a else b + | Abs a => Abs (Proj p a) + | _ => Proj p (tstar a) + end + | TBind p a b => TBind p (tstar a) (tstar b) + | Bot => Bot + | Univ i => Univ i + | Bool => Bool + | BVal b => BVal b + | If a b c => match tstar a with + | BVal v => if v then (tstar b) else (tstar c) + | Abs a => Abs (If a (ren_Tm shift (tstar b)) (ren_Tm shift (tstar c))) + | Pair a0 a1 => Pair (If a0 (tstar b) (tstar c)) (If a1 (tstar b) (tstar c)) + | Proj p a => Proj p (If a (tstar b) (tstar c)) + | App a0 a1 => App (If a0 (tstar b) (tstar c)) a1 + | _ => If (tstar a) (tstar b) (tstar c) + end + end. + + Lemma RPar_triangle n (a : Tm n) : forall b, RPar.R a b -> RPar.R b (tstar a). + Proof. + apply tstar_ind => {n a}. + - hauto lq:on inv:RPar.R ctrs:RPar.R. + - hauto lq:on inv:RPar.R ctrs:RPar.R. + - hauto lq:on use:RPar.cong, RPar.refl ctrs:RPar.R inv:RPar.R. + - hauto lq:on rew:off ctrs:RPar.R inv:RPar.R. + - hauto lq:on rew:off inv:RPar.R ctrs:RPar.R. + - hauto lq:on rew:off inv:RPar.R ctrs:RPar.R. + - hauto drew:off inv:RPar.R use:RPar.refl, RPar.ProjPair'. + - 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. + - hauto lq:on inv:RPar.R ctrs:RPar.R. + - hauto lq:on inv:RPar.R ctrs:RPar.R. Qed. + + End RPar. (* (***************** Beta rules only ***********************) *) @@ -1798,41 +1838,6 @@ Proof. - admit. Admitted. -Function tstar {n} (a : Tm n) := - match a with - | VarTm i => a - | Abs a => Abs (tstar a) - | App (Abs a) b => subst_Tm (scons (tstar b) VarTm) (tstar a) - | App (Pair a b) c => - Pair (App (tstar a) (tstar c)) (App (tstar b) (tstar c)) - | App a b => App (tstar a) (tstar b) - | Pair a b => Pair (tstar a) (tstar b) - | 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) - | TBind p a b => TBind p (tstar a) (tstar b) - | Bot => Bot - | Univ i => Univ i - end. - -Lemma RPar_triangle n (a : Tm n) : forall b, RPar.R a b -> RPar.R b (tstar a). -Proof. - apply tstar_ind => {n a}. - - hauto lq:on inv:RPar.R ctrs:RPar.R. - - hauto lq:on inv:RPar.R ctrs:RPar.R. - - hauto lq:on use:RPar.cong, RPar.refl ctrs:RPar.R inv:RPar.R. - - hauto lq:on rew:off ctrs:RPar.R inv:RPar.R. - - hauto lq:on rew:off inv:RPar.R ctrs:RPar.R. - - hauto lq:on rew:off inv:RPar.R ctrs:RPar.R. - - hauto drew:off inv:RPar.R use:RPar.refl, RPar.ProjPair'. - - 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. - - hauto lq:on inv:RPar.R ctrs:RPar.R. - - hauto lq:on inv:RPar.R ctrs:RPar.R. -Qed. - Function tstar' {n} (a : Tm n) := match a with | VarTm i => a From dd8b316a87ae542f443818cdeeb8b42b6d6f5451 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 12 Jan 2025 18:41:17 -0500 Subject: [PATCH 07/17] Prove the confluence of cred --- theories/fp_red.v | 69 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 69 insertions(+) diff --git a/theories/fp_red.v b/theories/fp_red.v index 38125c8..b5fd905 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -8,6 +8,9 @@ Require Import Psatz. From stdpp Require Import relations (rtc (..), rtc_once, rtc_r). From Hammer Require Import Tactics. Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax. +Import Relation_Operators (clos_refl(..)). +Arguments clos_refl {A}. + Ltac2 spec_refl () := List.iter @@ -371,6 +374,72 @@ Definition var_or_bot {n} (a : Tm n) := | _ => false end. +(* *********** Commutativity rules only ********************** *) +Module CRed. + Inductive R {n} : Tm n -> Tm n -> Prop := + (****************** Eta ***********************) + | IfApp a b c d : + R (If (App a b) c d) (App (If a c d) b) + | IfProj p a b c : + R (If (Proj p a) b c) (Proj p (If a b c)) + + (*************** Congruence ********************) + | AbsCong a0 a1 : + R a0 a1 -> + R (Abs a0) (Abs a1) + | AppCong0 a0 a1 b : + R a0 a1 -> + R (App a0 b) (App a1 b) + | AppCong1 a b0 b1 : + R b0 b1 -> + R (App a b0) (App a b1) + | PairCong0 a0 a1 b : + R a0 a1 -> + R (Pair a0 b) (Pair a1 b) + | PairCong1 a b0 b1 : + R b0 b1 -> + R (Pair a b0) (Pair a b1) + | ProjCong p a0 a1 : + R a0 a1 -> + R (Proj p a0) (Proj p a1) + | BindCong0 p A0 A1 B: + R A0 A1 -> + R (TBind p A0 B) (TBind p A1 B) + | BindCong1 p A B0 B1: + R B0 B1 -> + R (TBind p A B0) (TBind p A B1). + + Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. + + Lemma diamond n (a b c : Tm n) : R a b -> R a c -> exists d, clos_refl R b d /\ clos_refl R c d. + Proof. + move => h. move : c. elim : n a b /h. + - hauto l:on ctrs:R inv:R. + - hauto l:on ctrs:R inv:R. + - move => n a0 a1 ha iha c. + elim /inv => //= _. + move => a2 a3 ha' [*]. subst. + apply iha in ha'. + move : ha' => [d [h0 h1]]. + exists (Abs d). + hauto q:on ctrs:clos_refl,R inv:clos_refl. + - hauto q:on ctrs:clos_refl,R inv:clos_refl, R. + - hauto q:on ctrs:clos_refl,R inv:clos_refl, R. + - hauto q:on ctrs:clos_refl,R inv:clos_refl, R. + - hauto q:on ctrs:clos_refl,R inv:clos_refl, R. + - hauto q:on ctrs:clos_refl,R inv:clos_refl, R. + - hauto q:on ctrs:clos_refl,R inv:clos_refl, R. + - move => n p A B0 B1 hB ihB C. + elim /inv => //= _. + move => p0 A0 A1 B hA [*]. subst. + + hauto lq:on ctrs:clos_refl,R inv:clos_refl. + + move => p0 A0 B2 B3 h [*]. subst. + move /ihB : h{ihB}. + move => [B4 [h0 h1]]. + exists (TBind p A B4). qauto l:on ctrs:clos_refl, R inv:clos_refl. + Qed. +End CRed. + (***************** Beta rules only ***********************) Module RPar. Inductive R {n} : Tm n -> Tm n -> Prop := From b48734ab12f1c75b60ae8f566530a91547d6fcf7 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 12 Jan 2025 18:51:08 -0500 Subject: [PATCH 08/17] Recover confluence for rpar and cred --- theories/fp_red.v | 56 ++++++++++++++++++----------------------------- 1 file changed, 21 insertions(+), 35 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index b5fd905..d171995 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -509,18 +509,7 @@ Module RPar. R a0 a1 -> R b0 b1 -> R c0 c1 -> - R (If a0 b0 c0) (If a1 b1 c1) - | IfApp a0 a1 b0 b1 c0 c1 d0 d1 : - R a0 a1 -> - R b0 b1 -> - R c0 c1 -> - R d0 d1 -> - R (If (App a0 b0) c0 d0) (App (If a1 c1 d1) b1) - | IfProj p a0 a1 b0 b1 c0 c1 : - R a0 a1 -> - R b0 b1 -> - R c0 c1 -> - R (If (Proj p a0) b0 c0) (Proj p (If a1 b1 c1)). + R (If a0 b0 c0) (If a1 b1 c1). Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. @@ -611,8 +600,6 @@ Module RPar. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R. - - hauto lq:on ctrs:R. - - hauto lq:on ctrs:R. Qed. Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : @@ -793,36 +780,29 @@ Module RPar. have {}/ihc := (hρ) => ihc. spec_refl. hauto lq:on ctrs:R. - Admitted. + Qed. Function tstar {n} (a : Tm n) := match a with | VarTm i => a | Abs a => Abs (tstar a) - | App a b => match tstar a with - | Abs a => subst_Tm (scons (tstar b) VarTm) a - | Pair a c => Pair (App a (tstar b)) (App c (tstar b)) - | _ => App (tstar a) (tstar b) - end + | App (Abs a) b => subst_Tm (scons (tstar b) VarTm) (tstar a) + | App (Pair a b) c => + Pair (App (tstar a) (tstar c)) (App (tstar b) (tstar c)) + | App a b => App (tstar a) (tstar b) | Pair a b => Pair (tstar a) (tstar b) - | Proj p a => match tstar a with - | Pair a b => if p is PL then a else b - | Abs a => Abs (Proj p a) - | _ => Proj p (tstar a) - end + | 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) | TBind p a b => TBind p (tstar a) (tstar b) | Bot => Bot | Univ i => Univ i | Bool => Bool - | BVal b => BVal b - | If a b c => match tstar a with - | BVal v => if v then (tstar b) else (tstar c) - | Abs a => Abs (If a (ren_Tm shift (tstar b)) (ren_Tm shift (tstar c))) - | Pair a0 a1 => Pair (If a0 (tstar b) (tstar c)) (If a1 (tstar b) (tstar c)) - | Proj p a => Proj p (If a (tstar b) (tstar c)) - | App a0 a1 => App (If a0 (tstar b) (tstar c)) a1 - | _ => If (tstar a) (tstar b) (tstar c) - end + | If (BVal v) b c => if v then (tstar b) else (tstar c) + | If (Abs a) b c => Abs (If (tstar a) (ren_Tm shift (tstar b)) (ren_Tm shift (tstar c))) + | If (Pair a0 a1) b c => Pair (If (tstar a0) (tstar b) (tstar c)) (If (tstar a1) (tstar b) (tstar c)) + | If a b c => If (tstar a) (tstar b) (tstar c) + | BVal v => BVal v end. Lemma RPar_triangle n (a : Tm n) : forall b, RPar.R a b -> RPar.R b (tstar a). @@ -841,9 +821,15 @@ Module RPar. - 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. + - hauto lq:on ctrs:R inv:R. + - qauto l:on use:refl, IfBool' inv:R. + - hauto drew:off use:refl, IfBool' inv:R. + - hauto lq:on ctrs:RPar.R inv:RPar.R use:renaming. + - hauto lq:on drew:off ctrs:R inv:R. + - hauto lq:on drew:off ctrs:R inv:R. + - hauto lq:on drew:off ctrs:R inv:R. Qed. - End RPar. (* (***************** Beta rules only ***********************) *) From 95a48a380dbcf17f4cb37423229e9f3d0c8e4ab2 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 12 Jan 2025 18:55:08 -0500 Subject: [PATCH 09/17] Add RRed --- theories/fp_red.v | 49 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/theories/fp_red.v b/theories/fp_red.v index d171995..3181f9e 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -832,6 +832,55 @@ Module RPar. End RPar. + +Module RRed. + Inductive R {n} : Tm n -> Tm n -> Prop := + (****************** Beta ***********************) + | AppAbs a b : + R (App (Abs a) b) (subst_Tm (scons b VarTm) a) + | AppPair a b c: + R (App (Pair a b) c) (Pair (App a c) (App b c)) + | ProjAbs p a : + R (Proj p (Abs a)) (Abs (Proj p a)) + | ProjPair p a b : + R (Proj p (Pair a b)) (if p is PL then a else b) + | IfAbs (a : Tm (S n)) b c : + R (If (Abs a) b c) (Abs (If a (ren_Tm shift b) (ren_Tm shift c))) + | IfPair a b c d : + R (If (Pair a b) c d) (Pair (If a c d) (If b c d)) + | IfBool a b c : + R (If (BVal a) b c) (if a then b else c) + + (*************** Congruence ********************) + | AbsCong a0 a1 : + R a0 a1 -> + R (Abs a0) (Abs a1) + | AppCong0 a0 a1 b : + R a0 a1 -> + R (App a0 b) (App a1 b) + | AppCong1 a b0 b1 : + R b0 b1 -> + R (App a b0) (App a b1) + | PairCong0 a0 a1 b : + R a0 a1 -> + R (Pair a0 b) (Pair a1 b) + | PairCong1 a b0 b1 : + R b0 b1 -> + R (Pair a b0) (Pair a b1) + | ProjCong p a0 a1 : + R a0 a1 -> + R (Proj p a0) (Proj p a1) + | BindCong0 p A0 A1 B: + R A0 A1 -> + R (TBind p A0 B) (TBind p A1 B) + | BindCong1 p A B0 B1: + R B0 B1 -> + R (TBind p A B0) (TBind p A B1). + + Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. + +End RRed. + (* (***************** Beta rules only ***********************) *) (* Module RPar'. *) (* Inductive R {n} : Tm n -> Tm n -> Prop := *) From b12872abf9a4c5dbcb0c798d5ce97f4c1df0e0bc Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 12 Jan 2025 19:13:52 -0500 Subject: [PATCH 10/17] Stuck because cred is not parallel enough --- theories/fp_red.v | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/theories/fp_red.v b/theories/fp_red.v index 3181f9e..5840512 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -881,6 +881,41 @@ Module RRed. End RRed. +Module CRedRRed. + Lemma commutativity0 n (a b0 b1 : Tm n) : + CRed.R a b0 -> RRed.R a b1 -> exists c, rtc RRed.R b0 c /\ clos_refl CRed.R b1 c. + Proof. + move => h. move : b1. elim : n a b0/h => n. + - hauto lq:on inv:RRed.R. + - hauto q:on inv:RRed.R. + - move => a0 a1 ha iha b. + elim /RRed.inv => //=_ a2 a3 h [*]. subst. + move /iha : h => [a [h0 h1]]. + exists (Abs a). split. admit. hauto lq:on ctrs:clos_refl, CRed.R inv:clos_refl. + - move => a0 a1 b ha iha b1. + elim /RRed.inv => //=_. + + move => a2 b0 [*]. subst. + elim /CRed.inv : ha => //= _ a0 a3 ha [*]. subst. + exists (subst_Tm (scons b VarTm) a3). + split. hauto lq:on ctrs:RRed.R use:@rtc_once. + apply r_step. + admit. + + sauto lq:on. + + move => a2 a3 b0 ha0 [*]. subst. + move /iha : ha0 => [a4 [h0 h1]]. + exists (App a4 b). + split. admit. + sauto lq:on rew:off. + + sauto lq:on. + - move => a b0 b1 ha iha b2. + elim /RRed.inv => //= _. + + move => a0 b3 [*]. subst. + exists (subst_Tm (scons b1 VarTm) a0). + split. sauto lq:on. + + + + (* (***************** Beta rules only ***********************) *) (* Module RPar'. *) (* Inductive R {n} : Tm n -> Tm n -> Prop := *) From 3732757abec3352a01838296c74b4e72e7d5e65b Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 12 Jan 2025 19:22:06 -0500 Subject: [PATCH 11/17] Parallelize cred --- theories/fp_red.v | 111 ++++++++++++++++++++++++++++------------------ 1 file changed, 69 insertions(+), 42 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 5840512..db3e761 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -378,66 +378,93 @@ Definition var_or_bot {n} (a : Tm n) := Module CRed. Inductive R {n} : Tm n -> Tm n -> Prop := (****************** Eta ***********************) - | IfApp a b c d : - R (If (App a b) c d) (App (If a c d) b) - | IfProj p a b c : - R (If (Proj p a) b c) (Proj p (If a b c)) - + | IfApp a0 a1 b0 b1 c0 c1 d0 d1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R d0 d1 -> + R (If (App a0 b0) c0 d0) (App (If a1 c1 d1) b1) + | IfProj p a0 a1 b0 b1 c0 c1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R (If (Proj p a0) b0 c0) (Proj p (If a1 b1 c1)) (*************** Congruence ********************) + | Var i : R (VarTm i) (VarTm i) | AbsCong a0 a1 : R a0 a1 -> R (Abs a0) (Abs a1) - | AppCong0 a0 a1 b : + | AppCong a0 a1 b0 b1 : R a0 a1 -> - R (App a0 b) (App a1 b) - | AppCong1 a b0 b1 : R b0 b1 -> - R (App a b0) (App a b1) - | PairCong0 a0 a1 b : + R (App a0 b0) (App a1 b1) + | PairCong a0 a1 b0 b1 : R a0 a1 -> - R (Pair a0 b) (Pair a1 b) - | PairCong1 a b0 b1 : R b0 b1 -> - R (Pair a b0) (Pair a b1) + R (Pair a0 b0) (Pair a1 b1) | ProjCong p a0 a1 : R a0 a1 -> R (Proj p a0) (Proj p a1) - | BindCong0 p A0 A1 B: + | BindCong p A0 A1 B0 B1: R A0 A1 -> - R (TBind p A0 B) (TBind p A1 B) - | BindCong1 p A B0 B1: R B0 B1 -> - R (TBind p A B0) (TBind p A B1). + R (TBind p A0 B0) (TBind p A1 B1) + | BotCong : + R Bot Bot + | UnivCong i : + R (Univ i) (Univ i) + | BoolCong : + R Bool Bool + | BValCong b : + R (BVal b) (BVal b) + | IfCong a0 a1 b0 b1 c0 c1 : + R a0 a1 -> + R b0 b1 -> + R c0 c1 -> + R (If a0 b0 c0) (If a1 b1 c1). Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. - Lemma diamond n (a b c : Tm n) : R a b -> R a c -> exists d, clos_refl R b d /\ clos_refl R c d. + Lemma refl n (a : Tm n) : R a a. + Proof. elim : n / a; hauto lq:on ctrs:R. Qed. + + Function tstar {n} (a : Tm n) := + match a with + | VarTm i => a + | Abs a => Abs (tstar a) + | App a b => App (tstar a) (tstar b) + | Pair a b => Pair (tstar a) (tstar b) + | Proj p a => Proj p (tstar a) + | TBind p a b => TBind p (tstar a) (tstar b) + | Bot => Bot + | Univ i => Univ i + | Bool => Bool + | If (Proj p a) b c => Proj p (If (tstar a) (tstar b) (tstar c)) + | If (App a d) b c => App (If (tstar a) (tstar b) (tstar c)) (tstar d) + | If a b c => If (tstar a) (tstar b) (tstar c) + | BVal v => BVal v + end. + + Lemma triangle n (a : Tm n) : forall b, R a b -> R b (tstar a). Proof. - move => h. move : c. elim : n a b /h. - - hauto l:on ctrs:R inv:R. - - hauto l:on ctrs:R inv:R. - - move => n a0 a1 ha iha c. - elim /inv => //= _. - move => a2 a3 ha' [*]. subst. - apply iha in ha'. - move : ha' => [d [h0 h1]]. - exists (Abs d). - hauto q:on ctrs:clos_refl,R inv:clos_refl. - - hauto q:on ctrs:clos_refl,R inv:clos_refl, R. - - hauto q:on ctrs:clos_refl,R inv:clos_refl, R. - - hauto q:on ctrs:clos_refl,R inv:clos_refl, R. - - hauto q:on ctrs:clos_refl,R inv:clos_refl, R. - - hauto q:on ctrs:clos_refl,R inv:clos_refl, R. - - hauto q:on ctrs:clos_refl,R inv:clos_refl, R. - - move => n p A B0 B1 hB ihB C. - elim /inv => //= _. - move => p0 A0 A1 B hA [*]. subst. - + hauto lq:on ctrs:clos_refl,R inv:clos_refl. - + move => p0 A0 B2 B3 h [*]. subst. - move /ihB : h{ihB}. - move => [B4 [h0 h1]]. - exists (TBind p A B4). qauto l:on ctrs:clos_refl, R inv:clos_refl. + apply tstar_ind => {n a}. + - hauto lq:on inv:R ctrs:R. + - hauto lq:on inv:R ctrs:R. + - hauto lq:on rew:off ctrs:R inv:R. + - hauto lq:on rew:off inv:R ctrs:R. + - hauto lq:on rew:off inv:R ctrs:R. + - hauto lq:on inv:R ctrs:R. + - hauto lq:on inv:R ctrs:R. + - hauto lq:on inv:R ctrs:R. + - hauto lq:on inv:R ctrs:R. + - hauto lq:on inv:R ctrs:R. + - hauto lq:on ctrs:R inv:R. + - hauto lq:on drew:off ctrs:R inv:R. + - hauto lq:on drew:off ctrs:R inv:R. Qed. + + Lemma diamond n (a b c : Tm n) : R a b -> R a c -> exists d, R b d /\ R c d. + Proof. sfirstorder use:triangle. Qed. End CRed. (***************** Beta rules only ***********************) From 764606cf2da22872227f07297b8b9721de6ca8ff Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 12 Jan 2025 19:46:32 -0500 Subject: [PATCH 12/17] Prove the commutativity of cred and rred --- theories/fp_red.v | 161 +++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 144 insertions(+), 17 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index db3e761..b619fa7 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -428,6 +428,34 @@ Module CRed. Lemma refl n (a : Tm n) : R a a. Proof. elim : n / a; hauto lq:on ctrs:R. Qed. + Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : + R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). + Proof. + move => h. move : m ξ. + elim : n a b /h; hauto lq:on ctrs:R. + Qed. + + Lemma morphing n m (a b : Tm n) (ρ0 ρ1 : fin n -> Tm m) : + (forall i, R (ρ0 i) (ρ1 i)) -> + R a b -> R (subst_Tm ρ0 a) (subst_Tm ρ1 b). + Proof. + move => + h. move : m ρ0 ρ1. elim : a b /h; hauto l:on ctrs:R inv:option use:renaming. + Qed. + + Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : + R a b -> + R (subst_Tm ρ a) (subst_Tm ρ b). + Proof. hauto l:on use:morphing, refl. Qed. + + Lemma cong n (a b : Tm (S n)) c d : + R a b -> + R c d -> + R (subst_Tm (scons c VarTm) a) (subst_Tm (scons d VarTm) b). + Proof. + move => h0 h1. apply morphing => //=. + qauto l:on ctrs:R inv:option. + Qed. + Function tstar {n} (a : Tm n) := match a with | VarTm i => a @@ -908,40 +936,139 @@ Module RRed. End RRed. +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 : Tm (S n)) : + rtc RRed.R a b -> + rtc RRed.R (Abs a) (Abs b). + Proof. solve_s. Qed. + + Lemma AppCong n (a0 a1 b0 b1 : Tm n) : + rtc RRed.R a0 a1 -> + rtc RRed.R b0 b1 -> + rtc RRed.R (App a0 b0) (App a1 b1). + Proof. solve_s. Qed. + + Lemma BindCong n p (a0 a1 : Tm n) b0 b1 : + rtc RRed.R a0 a1 -> + rtc RRed.R b0 b1 -> + rtc RRed.R (TBind p a0 b0) (TBind p a1 b1). + Proof. solve_s. Qed. + + Lemma PairCong n (a0 a1 b0 b1 : Tm n) : + rtc RRed.R a0 a1 -> + rtc RRed.R b0 b1 -> + rtc RRed.R (Pair a0 b0) (Pair a1 b1). + Proof. solve_s. Qed. + + Lemma ProjCong n p (a0 a1 : Tm n) : + rtc RRed.R a0 a1 -> + rtc RRed.R (Proj p a0) (Proj p a1). + Proof. solve_s. Qed. +End RReds. + + Module CRedRRed. Lemma commutativity0 n (a b0 b1 : Tm n) : - CRed.R a b0 -> RRed.R a b1 -> exists c, rtc RRed.R b0 c /\ clos_refl CRed.R b1 c. + CRed.R a b0 -> RRed.R a b1 -> exists c, rtc RRed.R b0 c /\ CRed.R b1 c. Proof. move => h. move : b1. elim : n a b0/h => n. - hauto lq:on inv:RRed.R. - hauto q:on inv:RRed.R. + - hauto q:on inv:RRed.R. - move => a0 a1 ha iha b. elim /RRed.inv => //=_ a2 a3 h [*]. subst. move /iha : h => [a [h0 h1]]. - exists (Abs a). split. admit. hauto lq:on ctrs:clos_refl, CRed.R inv:clos_refl. - - move => a0 a1 b ha iha b1. + exists (Abs a). split. auto using RReds.AbsCong. hauto lq:on ctrs:CRed.R. + - move => a0 a1 b0 b1 ha iha hb ihb u. elim /RRed.inv => //=_. - + move => a2 b0 [*]. subst. + + move => a2 b2 [*]. subst. elim /CRed.inv : ha => //= _ a0 a3 ha [*]. subst. - exists (subst_Tm (scons b VarTm) a3). + move {iha ihb}. + exists (subst_Tm (scons b1 VarTm) a3). split. hauto lq:on ctrs:RRed.R use:@rtc_once. - apply r_step. - admit. + hauto lq:on use:CRed.cong. + sauto lq:on. - + move => a2 a3 b0 ha0 [*]. subst. + + move => a2 a3 b2 ha0 [*]. subst. move /iha : ha0 => [a4 [h0 h1]]. - exists (App a4 b). - split. admit. + exists (App a4 b1). + split. hauto lq:on ctrs:rtc use: RReds.AppCong. sauto lq:on rew:off. - + sauto lq:on. - - move => a b0 b1 ha iha b2. + + move => a2 b2 b3 hb2 [*]. subst. + move /ihb : hb2 => [b4 [ih0 ih1]]. + exists (App a1 b4). + split. + hauto lq:on ctrs:rtc use:RReds.AppCong. + hauto lq:on ctrs:CRed.R. + - move => a0 a1 b0 b1 ha iha hb ihb u. elim /RRed.inv => //= _. - + move => a0 b3 [*]. subst. - exists (subst_Tm (scons b1 VarTm) a0). + + move => a2 a3 b2 + [*]. subst. + move /iha => [a4 [ih0 ih1]]. + exists (Pair a4 b1). + split. hauto lq:on ctrs:rtc use:RReds.PairCong. + sauto lq:on. + + move => a2 b2 b3 + [*]. subst. + move /ihb {ihb}. + move => [b4 [ih0 ih1]]. + exists (Pair a1 b4). split. hauto lq:on ctrs:rtc use:RReds.PairCong. + sauto lq:on. + - move => p a0 a1 ha iha u. + elim /RRed.inv => //= _. + + sauto lq:on rew:off. + + sauto q:on. + + move => p0 a2 a3 ha2 [*]. subst. + move /iha : ha2 {iha} => [a4 [ih0 ih1]]. + exists (Proj p a4). + split. sfirstorder ctrs:rtc use:RReds.ProjCong. + sauto lq:on. + - move => p A0 A1 B0 B1 hA ihA hB ihB u. + elim /RRed.inv => //=_. + + move => p0 A2 A3 B h [*]. subst. + apply ihA in h. + move : h => [A [h0 h1]]. + exists (TBind p A B1). + split. hauto lq:on use:RReds.BindCong. + sauto lq:on. + + move => p0 A B2 B3 hB0 [*]. subst. + apply ihB in hB0. + move : hB0 => [B [ih0 ih1]]. + exists (TBind p A1 B). + split. hauto ctrs:rtc lq:on use:RReds.BindCong. + sauto lq:on. + - sauto lq:on. + - sauto lq:on. + - sauto lq:on. + - sauto lq:on. + - move => a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc u. + elim /RRed.inv => //= _. + + move => a2 b2 c [*]. subst. + elim /CRed.inv : ha => //=_. + move => a0 a3 ha [*]. subst. + exists (Abs (If a3 (ren_Tm shift b1) (ren_Tm shift c1))). split. sauto lq:on. - - - + apply CRed.AbsCong. + apply CRed.IfCong; eauto using CRed.renaming. + + move => a2 b2 c d [*]. subst. + move {iha ihb ihc}. + elim /CRed.inv : ha => //=_. + move => a0 a3 b3 b4 h0 h1 [*]. subst. + exists (Pair (If a3 b1 c1) (If b4 b1 c1)). + split. sauto lq:on. + sauto lq:on. + + move {iha ihb ihc}. + move => a2 b2 c [*]. subst. + elim /CRed.inv : ha => //= _. + move => b2 [*]. subst. + sauto lq:on. + Qed. +End CRedRRed. (* (***************** Beta rules only ***********************) *) (* Module RPar'. *) From f68efaf938b6fe7c17c7338727d9d038357339f1 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 12 Jan 2025 22:02:19 -0500 Subject: [PATCH 13/17] Add Abs EPar If --- theories/fp_red.v | 220 +++++++++++++++++++++++++++++++++++++++------- 1 file changed, 188 insertions(+), 32 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index b619fa7..af4c202 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -1070,6 +1070,144 @@ Module CRedRRed. Qed. End CRedRRed. +Module CRRed. + Inductive R {n} : Tm n -> Tm n -> Prop := + (****************** Beta ***********************) + | AppAbs a b : + R (App (Abs a) b) (subst_Tm (scons b VarTm) a) + | AppPair a b c: + R (App (Pair a b) c) (Pair (App a c) (App b c)) + | ProjAbs p a : + R (Proj p (Abs a)) (Abs (Proj p a)) + | ProjPair p a b : + R (Proj p (Pair a b)) (if p is PL then a else b) + | IfAbs (a : Tm (S n)) b c : + R (If (Abs a) b c) (Abs (If a (ren_Tm shift b) (ren_Tm shift c))) + | IfPair a b c d : + R (If (Pair a b) c d) (Pair (If a c d) (If b c d)) + | IfBool a b c : + R (If (BVal a) b c) (if a then b else c) + | IfApp a b c d : + R (If (App a b) c d) (App (If a c d) b) + | IfProj p a b c : + R (If (Proj p a) b c) (Proj p (If a b c)) + + (*************** Congruence ********************) + | AbsCong a0 a1 : + R a0 a1 -> + R (Abs a0) (Abs a1) + | AppCong0 a0 a1 b : + R a0 a1 -> + R (App a0 b) (App a1 b) + | AppCong1 a b0 b1 : + R b0 b1 -> + R (App a b0) (App a b1) + | PairCong0 a0 a1 b : + R a0 a1 -> + R (Pair a0 b) (Pair a1 b) + | PairCong1 a b0 b1 : + R b0 b1 -> + R (Pair a b0) (Pair a b1) + | ProjCong p a0 a1 : + R a0 a1 -> + R (Proj p a0) (Proj p a1) + | BindCong0 p A0 A1 B: + R A0 A1 -> + R (TBind p A0 B) (TBind p A1 B) + | BindCong1 p A B0 B1: + R B0 B1 -> + R (TBind p A B0) (TBind p A B1) + | IfCong0 a0 a1 b c : + R a0 a1 -> + R (If a0 b c) (If a1 b c) + | IfCong1 a b0 b1 c : + R b0 b1 -> + R (If a b0 c) (If a b1 c) + | IfCong2 a b c0 c1 : + R c0 c1 -> + R (If a b c0) (If a b c1). + + Lemma AppAbs' n a (b t : Tm n) : + t = subst_Tm (scons b VarTm) a -> + R (App (Abs a) b) t. + Proof. move => ->. apply AppAbs. Qed. + + Lemma IfAbs' n (a : Tm (S n)) (b c : Tm n) u : + u = (Abs (If a (ren_Tm shift b) (ren_Tm shift c))) -> + R (If (Abs a) b c) u. + Proof. move => ->. apply IfAbs. Qed. + + Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : + R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). + Proof. + move => h. move : m ξ. + elim : n a b /h => n; + lazymatch goal with + | [|- context[App (Abs _) _]] => move => * /=; apply AppAbs'; by asimpl + | [|- context[If (BVal _) _]] => hauto l:on use:IfBool + | [|- context[Proj _ (Pair _ _)]] => hauto l:on use:ProjPair + | [|- context[If (Abs _) _]] => move => * /=; apply IfAbs'; by asimpl + | _ => qauto ctrs:R + end. + Qed. + +End CRRed. + + +Module CRReds. + + #[local]Ltac solve_s_rec := + move => *; eapply rtc_l; eauto; + hauto lq:on ctrs:CRRed.R. + + #[local]Ltac solve_s := + repeat (induction 1; last by solve_s_rec); apply rtc_refl. + + Lemma AbsCong n (a b : Tm (S n)) : + rtc CRRed.R a b -> + rtc CRRed.R (Abs a) (Abs b). + Proof. solve_s. Qed. + + Lemma AppCong n (a0 a1 b0 b1 : Tm n) : + rtc CRRed.R a0 a1 -> + rtc CRRed.R b0 b1 -> + rtc CRRed.R (App a0 b0) (App a1 b1). + Proof. solve_s. Qed. + + Lemma BindCong n p (a0 a1 : Tm n) b0 b1 : + rtc CRRed.R a0 a1 -> + rtc CRRed.R b0 b1 -> + rtc CRRed.R (TBind p a0 b0) (TBind p a1 b1). + Proof. solve_s. Qed. + + Lemma PairCong n (a0 a1 b0 b1 : Tm n) : + rtc CRRed.R a0 a1 -> + rtc CRRed.R b0 b1 -> + rtc CRRed.R (Pair a0 b0) (Pair a1 b1). + Proof. solve_s. Qed. + + Lemma ProjCong n p (a0 a1 : Tm n) : + rtc CRRed.R a0 a1 -> + rtc CRRed.R (Proj p a0) (Proj p a1). + Proof. solve_s. Qed. + + Lemma IfCong n (a0 a1 b0 b1 c0 c1 : Tm n) : + rtc CRRed.R a0 a1 -> + rtc CRRed.R b0 b1 -> + rtc CRRed.R c0 c1 -> + rtc CRRed.R (If a0 b0 c0) (If a1 b1 c1). + Proof. solve_s. Qed. + + Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) : + rtc CRRed.R a b -> rtc CRRed.R (ren_Tm ξ a) (ren_Tm ξ b). + Proof. + move => h. move : m ξ. + induction h; hauto lq:on ctrs:rtc use:CRRed.renaming. + Qed. + +End CRReds. + + (* (***************** Beta rules only ***********************) *) (* Module RPar'. *) (* Inductive R {n} : Tm n -> Tm n -> Prop := *) @@ -1733,10 +1871,10 @@ End RPars. Lemma Abs_EPar n a (b : Tm n) : EPar.R (Abs a) b -> (exists d, EPar.R a d /\ - rtc RPar.R (App (ren_Tm shift b) (VarTm var_zero)) d) /\ + rtc CRRed.R (App (ren_Tm shift b) (VarTm var_zero)) d) /\ (exists d, EPar.R a d /\ forall p, - rtc RPar.R (Proj p b) (Abs (Proj p d))). + rtc CRRed.R (Proj p b) (Abs (Proj p d))). Proof. move E : (Abs a) => u h. move : a E. @@ -1747,65 +1885,83 @@ Proof. split; exists d. + split => //. apply : rtc_l. - apply RPar.AppAbs; eauto => //=. - apply RPar.refl. - by apply RPar.refl. + apply CRRed.AppAbs; eauto => //=. move :ih1; substify; by asimpl. + split => // p. apply : rtc_l. - apply : RPar.ProjAbs. - by apply RPar.refl. - eauto using RPars.ProjCong, RPars.AbsCong. + apply : CRRed.ProjAbs. + eauto using CRReds.ProjCong, CRReds.AbsCong. - move => n ? a1 ha iha a0 ?. subst. specialize iha with (1 := eq_refl). move : iha => [_ [d [ih0 ih1]]]. split. + exists (Pair (Proj PL d) (Proj PR d)). split; first by apply EPar.PairEta. apply : rtc_l. - apply RPar.AppPair; eauto using RPar.refl. - suff h : forall p, rtc RPar.R (App (Proj p (ren_Tm shift a1)) (VarTm var_zero)) (Proj p d) by - sfirstorder use:RPars.PairCong. - move => p. move /(_ p) /RPars.weakening in ih1. + apply CRRed.AppPair. + suff h : forall p, rtc CRRed.R (App (Proj p (ren_Tm shift a1)) (VarTm var_zero)) (Proj p d) by + sfirstorder use:CRReds.PairCong. + move => p. move /(_ p) /CRReds.renaming in ih1. apply relations.rtc_transitive with (y := App (ren_Tm shift (Abs (Proj p d))) (VarTm var_zero)). - by eauto using RPars.AppCong, rtc_refl. + by eauto using CRReds.AppCong, rtc_refl. apply relations.rtc_once => /=. - apply : RPar.AppAbs'; eauto using RPar.refl. - by asimpl. + apply : CRRed.AppAbs'. by asimpl. + exists d. repeat split => //. move => p. apply : rtc_l; eauto. - hauto q:on use:RPar.ProjPair', RPar.refl. + case : p; sfirstorder use:CRRed.ProjPair. - move => n a0 a1 ha _ ? [*]. subst. split. + exists a1. split => //. - apply rtc_once. apply : RPar.AppAbs'; eauto using RPar.refl. by asimpl. + apply rtc_once. apply : CRRed.AppAbs'. by asimpl. + exists a1. split => // p. - apply rtc_once. apply : RPar.ProjAbs; eauto using RPar.refl. + apply rtc_once. apply : CRRed.ProjAbs. Qed. Lemma Abs_EPar_If n (a : Tm (S n)) q : EPar.R (Abs a) q -> exists d, EPar.R a d /\ - forall b c, rtc RPar.R (If q b c) (Abs (If d (ren_Tm shift b) (ren_Tm shift c))). + forall b c, exists e, rtc CRRed.R (If q b c) e /\ rtc OExp.R (Abs (If d (ren_Tm shift b) (ren_Tm shift c))) e. Proof. move E : (Abs a) => u h. move : a E. elim : n u q /h => //= n. - - move => a0 a1 ha _ b ?. subst. - move /Abs_EPar : ha. - move => [[d [h0 h1]] _]. + - move => a0 a1 ha iha b ?. subst. + (* move /Abs_EPar : ha. *) + spec_refl. + move : iha => [d [hd h]]. exists d. - split => // b0 c. - apply : rtc_l. - apply RPar.IfAbs; auto using RPar.refl. - apply RPars.AbsCong. - apply RPars.IfCong; auto using rtc_refl. - - move => a0 a1 ha _ a ?. subst. - move /Abs_EPar : ha => [_ [d [h0 h1]]]. + split => //. + move => b0 c0. + move /(_ b0 c0) : h. + move => [e [h0 h1]]. + exists (Abs (App (ren_Tm shift e) (VarTm var_zero))). + split. + apply : rtc_l. apply CRRed.IfAbs. + apply : rtc_l. apply CRRed.AbsCong. + apply CRRed.IfApp. + apply CRReds.AbsCong. apply CRReds.AppCong; eauto using rtc_refl. + change (If (ren_Tm shift a1) (ren_Tm shift b0) (ren_Tm shift c0)) with (ren_Tm shift (If a1 b0 c0)). + hauto lq:on use:CRReds.renaming. + apply : rtc_r; eauto. + apply OExp.AppEta. + - move => a0 a1 ha iha a ?. subst. + spec_refl. + move : iha => [d [h0 h1]]. exists d. split => //. - move => b c. + move => b c. move/(_ b c ): h1 => [e [h1 h2]]. + eexists; split; cycle 1. + apply : rtc_r; eauto. + apply OExp.PairEta. apply : rtc_l. - apply RPar.IfPair; auto using RPar.refl. -Admitted. + apply CRRed.IfPair. + apply : rtc_l. + apply CRRed.PairCong0. + apply CRRed.IfProj. + apply : rtc_l. + apply CRRed.PairCong1. + apply CRRed.IfProj. + by apply CRReds.PairCong; apply CRReds.ProjCong. + - sauto lq: on. +Qed. Lemma Pair_EPar n (a b c : Tm n) : From 5bd998872aa6bbd1774e86ea1936be8fda99b500 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 12 Jan 2025 22:45:06 -0500 Subject: [PATCH 14/17] Four cases left for bool --- theories/fp_red.v | 167 ++++++++++++++++++++++++++-------------------- 1 file changed, 96 insertions(+), 71 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index af4c202..059d98f 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -1151,6 +1151,22 @@ Module CRRed. end. Qed. + Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : + R a b -> R (subst_Tm ρ a) (subst_Tm ρ b). + Proof. + move => h. move : m ρ. + elim : n a b /h => n /=; + lazymatch goal with + | [|- context[App (Abs _) _]] => move => * /=; apply AppAbs'; by asimpl + | [|- context[If (BVal _) _]] => hauto l:on use:IfBool + | [|- context[Proj _ (Pair _ _)]] => hauto l:on use:ProjPair + | [|- context[If (Abs _) _]] => move => * /=; apply IfAbs'; by asimpl + | _ => qauto ctrs:R + end. + Qed. + + Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. + End CRRed. @@ -1205,6 +1221,10 @@ Module CRReds. induction h; hauto lq:on ctrs:rtc use:CRRed.renaming. Qed. + Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : + rtc CRRed.R a b -> rtc CRRed.R (subst_Tm ρ a) (subst_Tm ρ b). + Proof. induction 1; hauto lq:on ctrs:rtc use:CRRed.substing. Qed. + End CRReds. @@ -1963,11 +1983,10 @@ Proof. - sauto lq: on. Qed. - Lemma Pair_EPar n (a b c : Tm n) : EPar.R (Pair a b) c -> - (forall p, exists d, rtc RPar.R (Proj p c) d /\ EPar.R (if p is PL then a else b) d) /\ - (exists d0 d1, rtc RPar.R (App (ren_Tm shift c) (VarTm var_zero)) + (forall p, exists d, rtc CRRed.R (Proj p c) d /\ EPar.R (if p is PL then a else b) d) /\ + (exists d0 d1, rtc CRRed.R (App (ren_Tm shift c) (VarTm var_zero)) (Pair (App (ren_Tm shift d0) (VarTm var_zero))(App (ren_Tm shift d1) (VarTm var_zero))) /\ EPar.R a d0 /\ EPar.R b d1). Proof. @@ -1981,44 +2000,44 @@ Proof. exists (Abs (App (ren_Tm shift (if p is PL then d0 else d1)) (VarTm var_zero))). split. * apply : relations.rtc_transitive. - ** apply RPars.ProjCong. apply RPars.AbsCong. eassumption. - ** apply : rtc_l. apply RPar.ProjAbs; eauto using RPar.refl. apply RPars.AbsCong. - apply : rtc_l. apply RPar.ProjPair; eauto using RPar.refl. + ** apply CRReds.ProjCong. apply CRReds.AbsCong. eassumption. + ** apply : rtc_l. apply CRRed.ProjAbs. apply CRReds.AbsCong. + apply : rtc_l. apply CRRed.ProjPair. hauto l:on. * hauto lq:on use:EPar.AppEta'. + exists d0, d1. repeat split => //. - apply : rtc_l. apply : RPar.AppAbs'; eauto using RPar.refl => //=. + apply : rtc_l. apply : CRRed.AppAbs' => //=. by asimpl; renamify. - move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl). split => [p|]. + move : iha => [/(_ p) [d [ih0 ih1]] _]. exists d. split=>//. - apply : rtc_l. apply RPar.ProjPair; eauto using RPar.refl. - set q := (X in rtc RPar.R X d). + apply : rtc_l. apply CRRed.ProjPair. + set q := (X in rtc CRRed.R X d). by have -> : q = Proj p a1 by hauto lq:on. + move :iha => [iha _]. move : (iha PL) => [d0 [ih0 ih0']]. move : (iha PR) => [d1 [ih1 ih1']] {iha}. exists d0, d1. - apply RPars.weakening in ih0, ih1. + apply CRReds.renaming with (ξ := shift) in ih0, ih1. repeat split => //=. - apply : rtc_l. apply RPar.AppPair; eauto using RPar.refl. - apply RPars.PairCong; apply RPars.AppCong; eauto using rtc_refl. + apply : rtc_l. apply CRRed.AppPair. + apply CRReds.PairCong; apply CRReds.AppCong; eauto using rtc_refl. - move => n a0 a1 b0 b1 ha _ hb _ a b [*]. subst. split. + move => p. exists (if p is PL then a1 else b1). split. - * apply rtc_once. apply : RPar.ProjPair'; eauto using RPar.refl. + * apply rtc_once. apply : CRRed.ProjPair. * hauto lq:on rew:off. + exists a1, b1. - split. apply rtc_once. apply RPar.AppPair; eauto using RPar.refl. + split. apply rtc_once. apply CRRed.AppPair. split => //. Qed. Lemma commutativity0 n (a b0 b1 : Tm n) : - EPar.R a b0 -> RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c. + EPar.R a b0 -> CRRed.R a b1 -> exists c, rtc CRRed.R b0 c /\ EPar.R b1 c. Proof. move => h. move : b1. elim : n a b0 / h. @@ -2027,85 +2046,91 @@ Proof. move => [c [ih0 ih1]]. exists (Abs (App (ren_Tm shift c) (VarTm var_zero))). split. - + hauto lq:on ctrs:rtc use:RPars.AbsCong, RPars.AppCong, RPars.renaming. + + hauto lq:on ctrs:rtc use:CRReds.AbsCong, CRReds.AppCong, CRReds.renaming. + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming. - move => n a b0 hb0 ihb0 b1 /[dup] hb1 {}/ihb0. move => [c [ih0 ih1]]. exists (Pair (Proj PL c) (Proj PR c)). split. - + apply RPars.PairCong; - by apply RPars.ProjCong. + + apply CRReds.PairCong; + by apply CRReds.ProjCong. + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming. - - hauto l:on ctrs:rtc inv:RPar.R. + - hauto l:on ctrs:rtc inv:CRRed.R. - move => n a0 a1 h ih b1. - elim /RPar.inv => //= _. + elim /CRRed.inv => //= _. move => a2 a3 ? [*]. subst. - hauto lq:on ctrs:rtc, RPar.R, EPar.R use:RPars.AbsCong. + hauto lq:on ctrs:rtc, CRRed.R, EPar.R use:CRReds.AbsCong. - move => n a0 a1 b0 b1 ha iha hb ihb b2. - elim /RPar.inv => //= _. - + move => a2 a3 b3 b4 h0 h1 [*]. subst. - move /(_ _ ltac:(by eauto)) : ihb => [b [ihb0 ihb1]]. - have {}/iha : RPar.R (Abs a2) (Abs a3) by hauto lq:on ctrs:RPar.R. - move => [c [ih0 /Abs_EPar [[d [ih1 ih2]] _]]]. - exists (subst_Tm (scons b VarTm) d). + elim /CRRed.inv => //= _. + + move => a2 b3 [*]. subst. move {iha ihb}. + move /Abs_EPar : ha => [[d [ih1 ih2]] _]. + exists (subst_Tm (scons b1 VarTm) d). split. (* By substitution *) - * move /RPars.substing : ih2. - move /(_ b). + * move /CRReds.substing : ih2. + move /(_ _ (scons b1 VarTm)). asimpl. - eauto using relations.rtc_transitive, RPars.AppCong. + eauto using relations.rtc_transitive, CRReds.AppCong. (* By EPar morphing *) * by apply EPar.substing. - + move => a2 a3 b3 b4 c0 c1 h0 h1 h2 [*]. subst. - move /(_ _ ltac:(by eauto using RPar.PairCong)) : iha - => [c [ihc0 ihc1]]. - move /(_ _ ltac:(by eauto)) : ihb => [d [ihd0 ihd1]]. - move /Pair_EPar : ihc1 => [_ [d0 [d1 [ih0 [ih1 ih2]]]]]. - move /RPars.substing : ih0. move /(_ d). + + move => a2 b3 c [*]. subst. move {iha ihb}. + move /Pair_EPar : ha => [_ [d0 [d1 [ih0 [ih1 ih2]]]]]. + move /CRReds.substing : ih0. move /(_ _ (scons b1 VarTm)). asimpl => h. - exists (Pair (App d0 d) (App d1 d)). + exists (Pair (App d0 b1) (App d1 b1)). split. - hauto lq:on use:relations.rtc_transitive, RPars.AppCong. + hauto lq:on use:@relations.rtc_transitive, CRReds.AppCong. apply EPar.PairCong; by apply EPar.AppCong. - + case : a0 ha iha => //=. - move => b ha hc b3 a0 [*]. subst. - admit. - + hauto lq:on ctrs:EPar.R use:RPars.AppCong. - - hauto lq:on ctrs:EPar.R inv:RPar.R use:RPars.PairCong. + + hauto lq:on ctrs:EPar.R, rtc use:CRReds.AppCong. + + move => a2 b3 b4 + [*]. subst. + move /ihb => [b [h0 h1]]. + exists (App a1 b). + hauto q:on ctrs:EPar.R, rtc use:CRReds.AppCong. + - hauto lq:on ctrs:EPar.R, rtc inv:CRRed.R use:CRReds.PairCong. - move => n p a b0 h0 ih0 b1. - elim /RPar.inv => //= _. - + move => ? a0 a1 h [*]. subst. - move /(_ _ ltac:(by eauto using RPar.AbsCong)) : ih0 => [c [ih0 ih1]]. - move /Abs_EPar : ih1 => [_ [d [ih1 ih2]]]. + elim /CRRed.inv => //= _. + + move => ? a0 [*]. subst. move {ih0}. + move /Abs_EPar : h0 => [_ [d [ih1 ih2]]]. exists (Abs (Proj p d)). - qauto l:on ctrs:EPar.R use:RPars.ProjCong, @relations.rtc_transitive. - + move => p0 a0 a1 b2 b3 h1 h2 [*]. subst. - move /(_ _ ltac:(by eauto using RPar.PairCong)) : ih0 => [c [ih0 ih1]]. - move /Pair_EPar : ih1 => [/(_ p)[d [ihd ihd']] _]. + qauto l:on ctrs:EPar.R use:CRReds.ProjCong, @relations.rtc_transitive. + + move => p0 a0 b2 [*]. subst. + move /Pair_EPar : h0 => [/(_ p)[d [ihd ihd']] _]. exists d. split => //. - hauto lq:on use:RPars.ProjCong, relations.rtc_transitive. - + move => p0 b2 [*]. subst. - admit. - + hauto lq:on ctrs:EPar.R use:RPars.ProjCong. - - hauto lq:on inv:RPar.R ctrs:EPar.R, rtc use:RPars.BindCong. - - hauto l:on ctrs:EPar.R inv:RPar.R. - - hauto l:on ctrs:EPar.R inv:RPar.R. - - hauto l:on ctrs:EPar.R inv:RPar.R. - - hauto l:on ctrs:EPar.R inv:RPar.R. + + hauto lq:on ctrs:EPar.R, rtc use:CRReds.ProjCong. + - hauto lq:on inv:CRRed.R ctrs:EPar.R, rtc use:CRReds.BindCong. + - hauto l:on ctrs:EPar.R inv:CRRed.R. + - hauto l:on ctrs:EPar.R inv:CRRed.R. + - hauto l:on ctrs:EPar.R inv:CRRed.R. + - hauto l:on ctrs:EPar.R inv:CRRed.R. - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc u. - elim /RPar.inv => //= _. - + move => a2 a3 b2 b3 c2 c3 ha2 hb2 hc2 [*]. subst. - move /(_ _ ltac:(by eauto using RPar.AbsCong)) : iha => [c [ih0 ih1]]. - move /Abs_EPar : ih1 => [[d [ih2 ih3]] _]. - have {}/ihb := hb2. move => [b4 [ihb0 ihb1]]. - have {}/ihc := hc2. move => [c4 [ihc0 ihc1]]. - - exists (Abs (If d (ren_Tm shift b4) (ren_Tm shift c4))). - split. admit. + elim /CRRed.inv => //= _. + + move => a2 b2 c [*]{iha ihb ihc}. subst. + move /Abs_EPar_If : ha => [d [h0 h1]]. + move /(_ b1 c1) : h1 => [e [h1 h2]]. + exists e. split => //. + apply : OExp.merge; eauto. hauto lq:on ctrs:EPar.R use:EPar.renaming. - + admit. - + admit. + + move => a2 b2 c d [*]. subst. + admit. + + move => a2 b2 c [*]. subst. + admit. + (* Need the rule that if commutes with abs *) admit. + + move => p a2 b2 c [*]. subst. + move {iha ihb ihc}. + admit. + + move => a2 a3 b2 c h [*]. subst. + move /iha : h {iha} => [a [ha0 ha1]]. + exists (If a b1 c1). split. + hauto lq:on ctrs:rtc use:CRReds.IfCong. + hauto lq:on ctrs:EPar.R. + + move => a2 b2 b3 c + [*]. subst. + move /ihb => [b [? ?]]. + exists (If a1 b c1). + hauto lq:on ctrs:rtc,EPar.R use:CRReds.IfCong. + + move => a2 b2 c2 c3 + [*]. subst. + move /ihc => {ihc} [c [? ?]]. + exists (If a1 b1 c). + hauto lq:on ctrs:rtc,EPar.R use:CRReds.IfCong. Admitted. Lemma commutativity1 n (a b0 b1 : Tm n) : From 433eef83ae5e94bc235b42afd2a79008300d328f Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 12 Jan 2025 23:20:52 -0500 Subject: [PATCH 15/17] Two cases left! --- theories/fp_red.v | 86 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 83 insertions(+), 3 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 059d98f..d87a9b3 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -1936,6 +1936,80 @@ Proof. apply rtc_once. apply : CRRed.ProjAbs. Qed. +Lemma Proj_EPar_If n p (a : Tm n) q : + EPar.R (Proj p a) q -> + exists d, EPar.R a d /\ + forall b c, exists e, rtc CRRed.R (If q b c) e /\ rtc OExp.R (Proj p (If d b c)) e. +Proof. + move E :(Proj p a) => u h. move : p a E. + elim : n u q /h => //=. + - move => n a0 a1 ha iha p a ?. subst. + spec_refl. + move : iha => [d [ih0 ih1]]. + exists d. split => // b c. + move /(_ b c) : ih1 => [e [ih1 ih2]]. + eexists; split; cycle 1. + apply : rtc_r; eauto. + apply OExp.AppEta. + apply : rtc_l. + apply CRRed.IfAbs. + apply : rtc_l. + apply CRRed.AbsCong. + apply CRRed.IfApp. + apply CRReds.AbsCong. + apply CRReds.AppCong; eauto using rtc_refl. + set (x := If _ _ _). + change x with (ren_Tm shift (If a1 b c)). + eauto using CRReds.renaming. + - move => n a0 a1 ha ih p a ?. subst. + spec_refl. move : ih => [d [ih0 ih1]]. + exists d. split => // b c. + move /(_ b c) : ih1 => [e [h0 h1]]. + eexists; split; cycle 1. + apply : rtc_r; eauto. + apply OExp.PairEta. + apply : rtc_l. + apply CRRed.IfPair. + apply CRReds.PairCong; hauto lq:on ctrs:rtc use:CRRed.IfProj, CRReds.ProjCong. + - sauto lq:on rew:off. +Qed. + +Lemma Pair_EPar_If n (r0 r1 : Tm n) q : + EPar.R (Pair r0 r1) q -> + exists d0 d1, EPar.R r0 d0 /\ EPar.R r1 d1 /\ + forall b c, exists e, rtc CRRed.R (If q b c) e /\ rtc OExp.R (Pair (If d0 b c) (If d1 b c)) e. +Proof. + move E : (Pair r0 r1) => u h. + move : r0 r1 E. + elim : n u q /h => //= n. + - move => a0 a1 ha iha r0 r1 ?. subst. + spec_refl. + move : iha => [d0 [d1 [ih0 [ih1 ih2]]]]. + exists d0, d1. repeat split => //. + move => b c. + move /(_ b c) : ih2 => [e [h0 h1]]. + eexists; split; cycle 1. + apply : rtc_r; eauto. + apply OExp.AppEta. + apply : rtc_l. apply CRRed.IfAbs. + apply CRReds.AbsCong. + apply : rtc_l. apply CRRed.IfApp. + apply CRReds.AppCong; auto using rtc_refl. + set (x := If _ _ _). + change x with (ren_Tm shift (If a1 b c)). + auto using CRReds.renaming. + - move => a0 a1 ha iha r0 r1 ?. subst. + spec_refl. move : iha => [d0 [d1 [ih0 [ih1 ih2]]]]. + exists d0, d1. (repeat split) => // b c. + move /(_ b c) : ih2 => [d [h0 h1]]. + eexists; split; cycle 1. + apply : rtc_r; eauto. + apply OExp.PairEta. + apply : rtc_l. apply CRRed.IfPair. + hauto lq:on ctrs:rtc use:CRRed.IfProj, CRReds.ProjCong, CRReds.PairCong. + - sauto lq:on. +Qed. + Lemma Abs_EPar_If n (a : Tm (S n)) q : EPar.R (Abs a) q -> exists d, EPar.R a d /\ @@ -2110,14 +2184,20 @@ Proof. apply : OExp.merge; eauto. hauto lq:on ctrs:EPar.R use:EPar.renaming. + move => a2 b2 c d [*]. subst. - admit. - + move => a2 b2 c [*]. subst. + move {iha ihb ihc}. + move /Pair_EPar_If : ha => [r0 [r1 [h0 [h1 h2]]]]. + move /(_ b1 c1) : h2 => [e [h3 h4]]. + exists e. split => //. + hauto lq:on ctrs:EPar.R use:EPar.renaming, OExp.merge. + + move => a2 b2 c [*] {iha ihb ihc}. subst. admit. + (* Need the rule that if commutes with abs *) + move => a2 b2 c d [*]. subst. admit. + move => p a2 b2 c [*]. subst. move {iha ihb ihc}. - admit. + move /Proj_EPar_If : ha => [d [h0 /(_ b1 c1) [e [h1 h2]]]]. + hauto lq:on ctrs:EPar.R use:EPar.renaming, OExp.merge. + move => a2 a3 b2 c h [*]. subst. move /iha : h {iha} => [a [ha0 ha1]]. exists (If a b1 c1). split. From 4d40dcf8d4521de171b5e5a01c31b2c70786143e Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 12 Jan 2025 23:38:15 -0500 Subject: [PATCH 16/17] Finish proving commutativity --- theories/fp_red.v | 169 ++++++++++++++++++++++++++++++++-------------- 1 file changed, 117 insertions(+), 52 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index d87a9b3..6981c43 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -1936,6 +1936,34 @@ Proof. apply rtc_once. apply : CRRed.ProjAbs. Qed. +Lemma BVal_EPar_If n (v : bool) q : + EPar.R (BVal v : Tm n) q -> + forall b c, exists e, rtc CRRed.R (If q b c) e /\ rtc OExp.R (if v then b else c) e. +Proof. + move E :(BVal v) => u h. move : v E. + elim : n u q /h => //=. + - move => n a0 a1 ha iha v ? b c. subst. + spec_refl. + move /(_ b c) : iha => [e [h0 h1]]. + eexists. split; cycle 1. + apply : rtc_r; eauto. apply OExp.AppEta. + apply : rtc_l. apply CRRed.IfAbs. + apply CRReds.AbsCong. + apply : rtc_l. apply CRRed.IfApp. + apply CRReds.AppCong; auto using rtc_refl. + set (x := If _ _ _). + change x with (ren_Tm shift (If a1 b c)). + eauto using CRReds.renaming. + - move => n a0 a1 ha iha v ? b c. subst. + spec_refl. + move /(_ b c) : iha => [e [h0 h1]]. + eexists; split; cycle 1. + apply : rtc_r; eauto. apply OExp.PairEta. + apply : rtc_l. apply CRRed.IfPair. + apply CRReds.PairCong; hauto lq:on ctrs:rtc use:CRRed.IfProj, CRReds.ProjCong. + - sauto lq:on. +Qed. + Lemma Proj_EPar_If n p (a : Tm n) q : EPar.R (Proj p a) q -> exists d, EPar.R a d /\ @@ -1974,6 +2002,43 @@ Proof. - sauto lq:on rew:off. Qed. +Lemma App_EPar_If n (r0 r1 : Tm n) q : + EPar.R (App r0 r1) q -> + exists d0 d1, EPar.R r0 d0 /\ EPar.R r1 d1 /\ + forall b c, exists e, rtc CRRed.R (If q b c) e /\ rtc OExp.R (App (If d0 b c) d1) e. +Proof. + move E : (App r0 r1) => u h. + move : r0 r1 E. + elim : n u q /h => //= n. + - move => a0 a1 ha iha r0 r1 ?. subst. + spec_refl. + move : iha => [d0 [d1 [ih0 [ih1 ih2]]]]. + exists d0, d1. repeat split => //. + move => b c. + move /(_ b c) : ih2 => [e [h0 h1]]. + eexists; split; cycle 1. + apply : rtc_r; eauto. + apply OExp.AppEta. + apply : rtc_l. apply CRRed.IfAbs. + apply CRReds.AbsCong. + apply : rtc_l. apply CRRed.IfApp. + apply CRReds.AppCong; auto using rtc_refl. + set (x := If _ _ _). + change x with (ren_Tm shift (If a1 b c)). + auto using CRReds.renaming. + - move => a0 a1 ha iha r0 r1 ?. subst. + spec_refl. move : iha => [d0 [d1 [ih0 [ih1 ih2]]]]. + exists d0, d1. (repeat split) => // b c. + move /(_ b c) : ih2 => [d [h0 h1]]. + eexists; split; cycle 1. + apply : rtc_r; eauto. + apply OExp.PairEta. + apply : rtc_l. apply CRRed.IfPair. + apply CRReds.PairCong; + hauto lq:on ctrs:rtc use:CRRed.IfProj, CRReds.ProjCong, CRReds.AppCong. + - sauto lq:on. +Qed. + Lemma Pair_EPar_If n (r0 r1 : Tm n) q : EPar.R (Pair r0 r1) q -> exists d0 d1, EPar.R r0 d0 /\ EPar.R r1 d1 /\ @@ -2190,10 +2255,16 @@ Proof. exists e. split => //. hauto lq:on ctrs:EPar.R use:EPar.renaming, OExp.merge. + move => a2 b2 c [*] {iha ihb ihc}. subst. - admit. + move /BVal_EPar_If : ha. + move /(_ b1 c1) => [e [h0 h1]]. + exists e. split => //. + hauto lq:on ctrs:EPar.R use:EPar.renaming, OExp.merge. + (* Need the rule that if commutes with abs *) - move => a2 b2 c d [*]. subst. - admit. + move => a2 b2 c d {iha ihb ihc} [*]. subst. + move /App_EPar_If : ha => [r0 [r1 [h0 [h1 h2]]]]. + move /(_ b1 c1) : h2 => [e [h3 h4]]. + exists e. split => //. + hauto lq:on ctrs:EPar.R use:EPar.renaming, OExp.merge. + move => p a2 b2 c [*]. subst. move {iha ihb ihc}. move /Proj_EPar_If : ha => [d [h0 /(_ b1 c1) [e [h1 h2]]]]. @@ -2211,10 +2282,10 @@ Proof. move /ihc => {ihc} [c [? ?]]. exists (If a1 b1 c). hauto lq:on ctrs:rtc,EPar.R use:CRReds.IfCong. -Admitted. +Qed. Lemma commutativity1 n (a b0 b1 : Tm n) : - EPar.R a b0 -> rtc RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c. + EPar.R a b0 -> rtc CRRed.R a b1 -> exists c, rtc CRRed.R b0 c /\ EPar.R b1 c. Proof. move => + h. move : b0. elim : a b1 / h. @@ -2223,7 +2294,7 @@ Proof. Qed. Lemma commutativity n (a b0 b1 : Tm n) : - rtc EPar.R a b0 -> rtc RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ rtc EPar.R b1 c. + rtc EPar.R a b0 -> rtc CRRed.R a b1 -> exists c, rtc CRRed.R b0 c /\ rtc EPar.R b1 c. move => h. move : b1. elim : a b0 /h. - sfirstorder. - move => a0 a1 a2 + ha1 ih b1 +. @@ -2392,55 +2463,49 @@ Proof. - admit. Admitted. -Function tstar' {n} (a : Tm n) := - match a with - | VarTm i => a - | Abs a => Abs (tstar' a) - | App (Abs a) b => subst_Tm (scons (tstar' b) VarTm) (tstar' a) - | App a b => App (tstar' a) (tstar' b) - | Pair a b => Pair (tstar' a) (tstar' b) - | Proj p (Pair a b) => if p is PL then (tstar' a) else (tstar' b) - | Proj p a => Proj p (tstar' a) - | TBind p a b => TBind p (tstar' a) (tstar' b) - | Bot => Bot - | Univ i => Univ i - end. +(* Function tstar' {n} (a : Tm n) := *) +(* match a with *) +(* | VarTm i => a *) +(* | Abs a => Abs (tstar' a) *) +(* | App (Abs a) b => subst_Tm (scons (tstar' b) VarTm) (tstar' a) *) +(* | App a b => App (tstar' a) (tstar' b) *) +(* | Pair a b => Pair (tstar' a) (tstar' b) *) +(* | Proj p (Pair a b) => if p is PL then (tstar' a) else (tstar' b) *) +(* | Proj p a => Proj p (tstar' a) *) +(* | TBind p a b => TBind p (tstar' a) (tstar' b) *) +(* | Bot => Bot *) +(* | Univ i => Univ i *) +(* end. *) -Lemma RPar'_triangle n (a : Tm n) : forall b, RPar'.R a b -> RPar'.R b (tstar' a). -Proof. - apply tstar'_ind => {n a}. - - hauto lq:on inv:RPar'.R ctrs:RPar'.R. - - hauto lq:on inv:RPar'.R ctrs:RPar'.R. - - hauto lq:on use:RPar'.cong, RPar'.refl ctrs:RPar'.R inv:RPar'.R. - - hauto lq:on rew:off ctrs:RPar'.R inv:RPar'.R. - - hauto lq:on rew:off inv:RPar'.R ctrs:RPar'.R. - - hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'. - - 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. - - hauto lq:on inv:RPar'.R ctrs:RPar'.R. -Qed. +(* Lemma RPar'_triangle n (a : Tm n) : forall b, RPar'.R a b -> RPar'.R b (tstar' a). *) +(* Proof. *) +(* apply tstar'_ind => {n a}. *) +(* - hauto lq:on inv:RPar'.R ctrs:RPar'.R. *) +(* - hauto lq:on inv:RPar'.R ctrs:RPar'.R. *) +(* - hauto lq:on use:RPar'.cong, RPar'.refl ctrs:RPar'.R inv:RPar'.R. *) +(* - hauto lq:on rew:off ctrs:RPar'.R inv:RPar'.R. *) +(* - hauto lq:on rew:off inv:RPar'.R ctrs:RPar'.R. *) +(* - hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'. *) +(* - 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. *) +(* - hauto lq:on inv:RPar'.R ctrs:RPar'.R. *) +(* Qed. *) -Lemma RPar_diamond n (c a1 b1 : Tm n) : - RPar.R c a1 -> - RPar.R c b1 -> - exists d2, RPar.R a1 d2 /\ RPar.R b1 d2. -Proof. hauto l:on use:RPar_triangle. Qed. +(* Lemma RPar'_diamond n (c a1 b1 : Tm n) : *) +(* RPar'.R c a1 -> *) +(* RPar'.R c b1 -> *) +(* exists d2, RPar'.R a1 d2 /\ RPar'.R b1 d2. *) +(* Proof. hauto l:on use:RPar'_triangle. Qed. *) -Lemma RPar'_diamond n (c a1 b1 : Tm n) : - RPar'.R c a1 -> - RPar'.R c b1 -> - exists d2, RPar'.R a1 d2 /\ RPar'.R b1 d2. -Proof. hauto l:on use:RPar'_triangle. Qed. - -Lemma RPar_confluent n (c a1 b1 : Tm n) : - rtc RPar.R c a1 -> - rtc RPar.R c b1 -> - exists d2, rtc RPar.R a1 d2 /\ rtc RPar.R b1 d2. -Proof. - sfirstorder use:relations.diamond_confluent, RPar_diamond. -Qed. +(* Lemma RPar_confluent n (c a1 b1 : Tm n) : *) +(* rtc RPar.R c a1 -> *) +(* rtc RPar.R c b1 -> *) +(* exists d2, rtc RPar.R a1 d2 /\ rtc RPar.R b1 d2. *) +(* Proof. *) +(* sfirstorder use:relations.diamond_confluent, RPar_diamond. *) +(* Qed. *) Lemma EPar_confluent n (c a1 b1 : Tm n) : rtc EPar.R c a1 -> From 2de1e5fa74955b5fbad3afc0210796013cabc450 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Sun, 12 Jan 2025 23:49:31 -0500 Subject: [PATCH 17/17] Recover diamond property --- theories/fp_red.v | 49 +++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 43 insertions(+), 6 deletions(-) diff --git a/theories/fp_red.v b/theories/fp_red.v index 6981c43..30b96ef 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -2409,6 +2409,36 @@ Lemma Univ_EPar' n i (u : Tm n) : - hauto l:on ctrs:OExp.R. Qed. +Lemma BVal_EPar' n i (u : Tm n) : + EPar.R (BVal i) u -> + rtc OExp.R (BVal i) u. + move E : (BVal i) => t h. + move : E. elim : n t u /h => //=. + - move => n a0 a1 h ih ?. subst. + specialize ih with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - move => n a0 a1 h ih ?. subst. + specialize ih with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - hauto l:on ctrs:OExp.R. +Qed. + +Lemma If_EPar' n (a b c u : Tm n) : + EPar.R (If a b c) u -> + (exists a0 b0 c0, EPar.R a a0 /\ EPar.R b b0 /\ EPar.R c c0 /\ rtc OExp.R (If a0 b0 c0) u). +Proof. + move E : (If a b c) => t h. + move : a b c E. elim : n t u /h => //= n. + - move => a0 a1 ha iha a b c ?. subst. + specialize iha with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - move => a0 a1 ha iha a b c ?. subst. + specialize iha with (1 := eq_refl). + hauto lq:on ctrs:OExp.R use:rtc_r. + - hauto l:on ctrs:OExp.R. +Qed. + + Lemma EPar_diamond n (c a1 b1 : Tm n) : EPar.R c a1 -> EPar.R c b1 -> @@ -2456,12 +2486,19 @@ Proof. move : OExp.commutativity0 h2; repeat move/[apply]. move => [d h]. exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge. - - qauto use:Bot_EPar', EPar.refl. - - qauto use:Univ_EPar', EPar.refl. - - admit. - - admit. - - admit. -Admitted. + - qauto use:EPar.refl. + - qauto use:EPar.refl. + - hauto lq:on use:EPar.refl. + - hauto lq:on use:EPar.refl. + - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc u. + move /If_EPar' => [a2 [b2 [c2 [h0 [h1 [h2 h3]]]]]]. + have {}/iha := h0. have {}/ihb := h1. have {}/ihc := h2. + move => [c hc0]. move => [b hb0]. move => [a ha0]. + have : EPar.R (If a2 b2 c2) (If a b c) by hauto lq:on ctrs:EPar.R. + move : OExp.commutativity0 h3. repeat move/[apply]. + move => [d ?]. + exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge. +Qed. (* Function tstar' {n} (a : Tm n) := *) (* match a with *)