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..30b96ef 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 @@ -40,7 +43,21 @@ Module Par. R a0 a1 -> R b0 b1 -> R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) - + | 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 -> + R (If (BVal a) b0 c0) (if a then b1 else c1) (****************** Eta ***********************) | AppEta a0 a1 : R a0 a1 -> @@ -73,7 +90,27 @@ 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) + | 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. @@ -93,12 +130,27 @@ 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 -> 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. @@ -107,11 +159,11 @@ 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' + | [ |- 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). @@ -124,6 +176,11 @@ Module Par. - hauto lq:on rew:off ctrs:R. - hauto l:on inv:option use:renaming ctrs:R. - hauto lq:on use:ProjPair'. + - 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. - hauto lq:on ctrs:R. @@ -135,6 +192,11 @@ Module Par. - hauto l:on inv:option ctrs:R use:renaming. - sfirstorder. - sfirstorder. + - 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) : @@ -174,6 +236,26 @@ Module Par. move : ihb => [c0 [? ?]]. subst. eexists. split. by eauto using ProjPair. hauto q:on. + - 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 [? ?]]. + 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. @@ -214,6 +296,16 @@ 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. + - 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. @@ -282,6 +374,127 @@ 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 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) + | 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) + | 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 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 + | 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. + 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 ***********************) Module RPar. Inductive R {n} : Tm n -> Tm n -> Prop := @@ -302,6 +515,21 @@ Module RPar. R a0 a1 -> R b0 b1 -> R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1) + | 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 -> + R (If (BVal a) b0 c0) (if a then b1 else c1) (*************** Congruence ********************) @@ -327,7 +555,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. @@ -350,13 +587,28 @@ 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 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'. + 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) : @@ -387,6 +639,11 @@ 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. + - 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. - hauto lq:on ctrs:R use:morphing_up. @@ -395,6 +652,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) : @@ -415,7 +675,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) : @@ -485,231 +745,36 @@ Module RPar. 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. - -(***************** 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). - - 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 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 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_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 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 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_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. - - 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. + - 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 : ihb (hρ) => /[apply] ihb. + move : ihc hρ => /[apply] ihc. spec_refl. - move : iha => [c1][ih0]?. subst. - move : ihb => [c2][ih1]?. subst. - eexists. split. - apply AppAbs; eauto. + 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 p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; - first by antiimp. - move => p0 []//=; first by antiimp. move => t t0[*]. - subst. + - 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. - move : iha => [b0 [? ?]]. - move : ihb => [c0 [? ?]]. subst. - eexists. split. by eauto using ProjPair. - hauto q:on. + 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. + 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. @@ -759,16 +824,87 @@ 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'. -Module ERed. + 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 + | Bool => Bool + | 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). + 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. + - 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. + + +Module RRed. 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)) + (****************** 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 : @@ -798,71 +934,626 @@ Module ERed. 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. +End RRed. - 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. - - 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. - -Module EReds. +Module RReds. #[local]Ltac solve_s_rec := move => *; eapply rtc_l; eauto; - hauto lq:on ctrs:ERed.R. + 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 ERed.R a b -> - rtc ERed.R (Abs a) (Abs b). + 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 ERed.R a0 a1 -> - rtc ERed.R b0 b1 -> - rtc ERed.R (App a0 b0) (App a1 b1). + 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 ERed.R a0 a1 -> - rtc ERed.R b0 b1 -> - rtc ERed.R (TBind p a0 b0) (TBind p a1 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 ERed.R a0 a1 -> - rtc ERed.R b0 b1 -> - rtc ERed.R (Pair a0 b0) (Pair a1 b1). + 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 ERed.R a0 a1 -> - rtc ERed.R (Proj p a0) (Proj p a1). + rtc RRed.R a0 a1 -> + rtc RRed.R (Proj p a0) (Proj p a1). Proof. solve_s. Qed. -End EReds. +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 /\ 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. 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 b2 [*]. subst. + elim /CRed.inv : ha => //= _ a0 a3 ha [*]. subst. + move {iha ihb}. + exists (subst_Tm (scons b1 VarTm) a3). + split. hauto lq:on ctrs:RRed.R use:@rtc_once. + hauto lq:on use:CRed.cong. + + sauto lq:on. + + move => a2 a3 b2 ha0 [*]. subst. + move /iha : ha0 => [a4 [h0 h1]]. + exists (App a4 b1). + split. hauto lq:on ctrs:rtc use: RReds.AppCong. + sauto lq:on rew:off. + + 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 => 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. + +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. + + 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. + + +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. + + 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. + + +(* (***************** 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). *) + +(* 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 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 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_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 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 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_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. *) + +(* 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)) *) + +(* (*************** 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 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. *) + +(* 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. *) + +(* End ERed. *) + +(* Module EReds. *) + +(* #[local]Ltac solve_s_rec := *) +(* move => *; eapply rtc_l; eauto; *) +(* hauto lq:on ctrs:ERed.R. *) + +(* #[local]Ltac solve_s := *) +(* repeat (induction 1; last by solve_s_rec); apply rtc_refl. *) + +(* Lemma AbsCong n (a b : 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 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 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 := @@ -897,7 +1588,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. @@ -942,6 +1642,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) : @@ -1031,6 +1734,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). @@ -1086,100 +1796,105 @@ 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'. *) + +(* (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 /\ - 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. @@ -1190,45 +1905,227 @@ 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 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 /\ + 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 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 /\ + 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 /\ + 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 iha b ?. subst. + (* move /Abs_EPar : ha. *) + spec_refl. + move : iha => [d [hd h]]. + exists d. + 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 ): h1 => [e [h1 h2]]. + eexists; split; cycle 1. + apply : rtc_r; eauto. + apply OExp.PairEta. + apply : rtc_l. + 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) : 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. @@ -1242,44 +2139,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. @@ -1288,67 +2185,107 @@ 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. - + 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. - + 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 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 /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. + + move => a2 b2 c d [*]. 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. + 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 {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]]]]. + 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. + 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. 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. @@ -1357,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 +. @@ -1472,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 -> @@ -1519,94 +2486,63 @@ 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. + - 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 - | 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. +(* 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 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. +(* 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. *) -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'_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'_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_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 ->