diff --git a/theories/fp_red.v b/theories/fp_red.v index 38125c8..5218c4a 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -376,36 +376,34 @@ 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) - | AppPair a0 a1 b0 b1 c0 c1: - R a0 a1 -> + R a0 (Abs a1) -> R b0 b1 -> + R (App a0 b0) (subst_Tm (scons b1 VarTm) a1) + | AppPair a a0 b0 c0 c1: + R a (Pair a0 b0) -> R c0 c1 -> - R (App (Pair a0 b0) c0) (Pair (App a1 c1) (App b1 c1)) + R (App a c0) (Pair (App a0 c1) (App b0 c1)) | ProjAbs p a0 a1 : - R a0 a1 -> - R (Proj p (Abs a0)) (Abs (Proj p 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) - | IfAbs (a0 a1 : Tm (S n)) b0 b1 c0 c1 : - R a0 a1 -> + R a0 (Abs a1) -> + R (Proj p a0) (Abs (Proj p a1)) + | ProjPair p a b c : + R a (Pair b c) -> + R (Proj p a) (if p is PL then b else c) + | IfAbs a0 a1 b0 b1 c0 c1 : + R a0 (Abs 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 (If a0 b0 c0) (Abs (If a1 (ren_Tm shift b1) (ren_Tm shift c1))) + | IfPair a a0 a1 c0 c1 d0 d1 : + R a (Pair a0 a1) -> 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 (If a c0 d0) (Pair (If a0 c1 d1) (If a1 c1 d1)) + | IfBool a v b0 b1 c0 c1 : + R a (BVal v) -> R b0 b1 -> R c0 c1 -> - R (If (BVal a) b0 c0) (if a then b1 else c1) + R (If a b0 c0) (if v then b1 else c1) (*************** Congruence ********************) @@ -460,41 +458,42 @@ Module RPar. 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 -> + Lemma AppAbs' n (a0 : Tm n) a1 b0 b1 u : + u = (subst_Tm (scons b1 VarTm) a1) -> + R a0 (Abs a1) -> R b0 b1 -> - R (App (Abs a0) b0) t. + R (App a0 b0) u. 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 a b c u : + u = (if p is PL then b else c) -> + R a (Pair b c : Tm n) -> + R (Proj p a) u. + Proof. move => > ->. apply ProjPair. Qed. - Lemma IfBool' n a b0 b1 c0 c1 u : - u = (if a then (b1 : Tm n) else c1) -> + Lemma IfBool' n a v b0 b1 c0 c1 u : + u = (if v then b1 else c1) -> + R a (BVal v : Tm n) -> R b0 b1 -> R c0 c1 -> - R (If (BVal a) b0 c0) u. + R (If a b0 c0) u. Proof. move => ->. apply IfBool. Qed. - - Lemma IfAbs' n (a0 a1 : Tm (S n)) (b0 b1 c0 c1 : Tm n) u : + 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 n a0 (Abs a1) -> R b0 b1 -> R c0 c1 -> - R (If (Abs a0) b0 c0) u. + R (If 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; try solve [(move => *; apply : AppAbs'; eauto; by asimpl) | (move => *; apply : IfAbs'; eauto; by asimpl)]. + elim : n a b /h => //=; try solve [(move => *; apply : AppAbs'; eauto; rewrite -/ren_Tm;by asimpl) | + (move => *; apply : IfBool'; eauto; rewrite -/ren_Tm; hauto lq:on) | + (move => *; apply : IfAbs'; eauto; rewrite -/ren_Tm; by asimpl)]. all : try qauto ctrs:R use:ProjPair', IfBool'. Qed. @@ -520,17 +519,18 @@ Module RPar. Proof. move => + h. move : m ρ0 ρ1. elim : n a b /h. - - move => *. + - move => /= *. apply : AppAbs'; eauto using morphing_up. by asimpl. - 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ρ /=. + - move => /= *. apply : IfAbs'; eauto using morphing_up. by asimpl. - hauto lq:on ctrs:R. - - hauto lq:on ctrs:R use:IfBool' use:morphing_up. + - move => n a v b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ0 ρ1 hρ /=. + eapply IfBool' with (v := v); qauto l:on. - hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R use:morphing_up. - hauto lq:on ctrs:R use:morphing_up. @@ -585,145 +585,145 @@ Module 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 a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=; - first by antiimp. - move => []//=; first by antiimp. - move => t t0 t1 [*]. subst. - have {}/iha := hρ => iha. - have {}/ihb := hρ => ihb. - have {}/ihc := hρ => ihc. - spec_refl. - move : iha => [? [*]]. - move : ihb => [? [*]]. - move : ihc => [? [*]]. - eexists. split. - apply AppPair; hauto. subst. - by asimpl. - - move => n p a0 a1 ha iha m ρ hρ []//=; - first by antiimp. - move => p0 []//= t [*]; first by antiimp. subst. - have /var_or_bot_up {}/iha := hρ => iha. - spec_refl. move : iha => [b0 [? ?]]. subst. - eexists. split. apply ProjAbs; 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 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. - 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. - 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. - - 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. + (* 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 a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=; *) + (* first by antiimp. *) + (* move => []//=; first by antiimp. *) + (* move => t t0 t1 [*]. subst. *) + (* have {}/iha := hρ => iha. *) + (* have {}/ihb := hρ => ihb. *) + (* have {}/ihc := hρ => ihc. *) + (* spec_refl. *) + (* move : iha => [? [*]]. *) + (* move : ihb => [? [*]]. *) + (* move : ihc => [? [*]]. *) + (* eexists. split. *) + (* apply AppPair; hauto. subst. *) + (* by asimpl. *) + (* - move => n p a0 a1 ha iha m ρ hρ []//=; *) + (* first by antiimp. *) + (* move => p0 []//= t [*]; first by antiimp. subst. *) + (* have /var_or_bot_up {}/iha := hρ => iha. *) + (* spec_refl. move : iha => [b0 [? ?]]. subst. *) + (* eexists. split. apply ProjAbs; 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 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. *) + (* 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. *) + (* 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. *) + (* - 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. *) Admitted. Function tstar {n} (a : Tm n) := @@ -761,7 +761,78 @@ Module RPar. 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. + - move => n a a0 b ? ih a1 eq ih2 b0. subst. + elim /inv => //= _. + + move => a2 a3 b1 b2 h0 h1 [*]. subst. + apply cong; eauto. + apply ih in h0. + elim /inv : h0 => //=. + scongruence. + + move => a2 a3 b1 c0 c1 h0 h1 [*]. subst. + move /ih : h0. + elim /inv => //=. scongruence. + + hauto l:on use:AppAbs. + - move => n a a0 b ? ih a1 c e ih' h2 b0. + elim /inv => //= _. + + move => a2 a3 b1 b2 ha hb [*]. subst. + have {}/ih := ha. + elim /inv => //=. scongruence. + + move => a2 b3 b1 c0 c1 + + [*]. subst. + move /ih. elim/inv=>//=. move => ? a2 a3 b0 b2 ha hb [*]. subst. + apply PairCong; eauto; + apply AppCong; eauto; scongruence. + + hauto l:on use:AppPair. + - move => n a a0 b ? ih c ? hc iha ihb. subst. + move => b0. elim /inv => //=. + + qblast. + + qblast. + + hauto lq:on ctrs:R. + - hauto lq:on ctrs:R inv:R. + - move => n a p a0 ? ih a1 b h ?. subst. + move => b0. elim /inv => //= _. + + sauto. + + sauto. + + move => p a2 a3 h0 [*]. subst. + have {}/ih := h0. + rewrite h. sfirstorder use:ProjPair'. + - move => n a p a0 ? ih a1 b ih2 p0 ?. subst. + case : p0 => //= _ b0. + elim /inv=>//=. + + sauto. + + sauto. + + move => h p a2 a3 h0 [*]. subst. + have {}/ih := h0. + rewrite ih2. sfirstorder use:ProjPair'. + - sauto use:ProjAbs. + - move => n a p a0 ? ih ? ? h. subst. + move => h0 b. + elim /inv => //=. + + sauto use:ProjAbs. + + scrush use:ProjAbs. + + sauto lq:on use:ProjAbs. + - hauto lq:on ctrs:R inv:R. + - hauto lq:on ctrs:R inv:R. + - hauto lq:on ctrs:R inv:R. + - hauto lq:on ctrs:R inv:R. + - hauto lq:on ctrs:R inv:R. + - move => n a a0 b c ? ih v eq ? hh. subst. + move => b0. elim /inv => //= _. + + sauto q:on. + + sauto q:on. + + sauto. + + move => a1 a2 b1 b2 c0 c1 ha hb hc [*]. subst. + apply ih in ha. apply hh in hb. + apply : IfBool'; eauto; cycle 1. + hauto q:on. + sfirstorder use:refl. + sfirstorder. + + move => a1 a2 b1 b2 c0 c1 d0 d1 ha hb hc hd [*]. subst. + have {}/ih : R (App a1 b1) (App a2 b2) by eauto using AppCong. + rewrite eq. + elim /inv => //= _. + move => a0 a3 b0 b3 ha0 hb0 [*]. subst. + + - 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.