From Ltac2 Require Ltac2. Import Ltac2.Notations. Import Ltac2.Control. Require Import ssreflect ssrbool. Require Import FunInd. Require Import Psatz. From stdpp Require Import relations (rtc (..), rtc_once, rtc_r, sn). From Hammer Require Import Tactics. Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax. Module βηPar. Inductive R : Tm -> Tm -> Prop := | VarCong i : R (VarTm i) (VarTm i) | AppCong b0 b1 a0 a1 : R b0 b1 -> R a0 a1 -> R (App b0 a0) (App b1 a1) | AbsCong a0 a1 : R a0 a1 -> R (Abs a0) (Abs a1) | AppAbs b0 b1 a0 a1 : R b0 b1 -> R a0 a1 -> R (App (Abs b0) a0) (subst_Tm (scons a1 VarTm) b1) | AbsEta b0 b1 : R b0 b1 -> R b0 (Abs (App (ren_Tm shift b1) (VarTm var_zero))). #[export]Hint Constructors R : βηPar. Derive Inversion inv with (forall a b, R a b). Lemma AppAbs' b0 b1 a0 a1 u : u = (subst_Tm (scons a1 VarTm) b1) -> R b0 b1 -> R a0 a1 -> R (App (Abs b0) a0) u. Proof. move => ->. apply AppAbs. Qed. Lemma AbsEta' b0 b1 u : u = (Abs (App (ren_Tm shift b1) (VarTm var_zero))) -> R b0 b1 -> R b0 u. Proof. move => ->. apply AbsEta. Qed. Lemma refl a : R a a. Proof. elim : a => //=; eauto with βηPar. Qed. Lemma morphing a b ρ : R a b -> R (subst_Tm ρ a) (subst_Tm ρ b). Proof. move => h. move : ρ. elim : a b /h => /=; eauto with βηPar. - eauto using refl. - move => *; apply : AppAbs'; eauto. by asimpl. - move => *; apply : AbsEta'; eauto. by asimpl. Qed. Lemma renaming a b ξ : R a b -> R (ren_Tm ξ a) (ren_Tm ξ b). Proof. substify. apply morphing. Qed. Definition morphing2_ok ρ0 ρ1 := forall (i : nat), R (ρ0 i) (ρ1 i). Lemma morphing2_ren (ξ : nat -> nat) ρ0 ρ1 : morphing2_ok ρ0 ρ1 -> morphing2_ok (funcomp (ren_Tm ξ) ρ0) (funcomp (ren_Tm ξ) ρ1). Proof. rewrite /morphing2_ok; eauto using renaming. Qed. Lemma morphing2_ext a b ρ0 ρ1 : R a b -> morphing2_ok ρ0 ρ1 -> morphing2_ok (scons a ρ0) (scons b ρ1). Proof. move => * [|i] //=. Qed. Lemma morphing_up ρ0 ρ1 : morphing2_ok ρ0 ρ1 -> morphing2_ok (up_Tm_Tm ρ0) (up_Tm_Tm ρ1). Proof. move => h. apply morphing2_ext. apply VarCong. by apply morphing2_ren. Qed. Lemma morphing2 a b ρ0 ρ1 : R a b -> morphing2_ok ρ0 ρ1 -> R (subst_Tm ρ0 a) (subst_Tm ρ1 b). Proof. move => h. move : ρ0 ρ1. elim : a b /h => //=; eauto using morphing_up with βηPar. - move => * /=. apply : AppAbs'; eauto using morphing_up. by asimpl. - move => * /=. apply : AbsEta'; eauto using morphing_up. by asimpl. Qed. End βηPar. Module IPar. Inductive R : Tm -> Tm -> Prop := | VarCong i : R (VarTm i) (VarTm i) | AppCong b0 b1 a0 a1 : βηPar.R b0 b1 -> βηPar.R a0 a1 -> R (App b0 a0) (App b1 a1) | AbsCong a0 a1 : βηPar.R a0 a1 -> R (Abs a0) (Abs a1) | AppAbs b0 b1 a0 a1 : βηPar.R b0 b1 -> βηPar.R a0 a1 -> R (App (Abs b0) a0) (subst_Tm (scons a1 VarTm) b1). Derive Inversion inv with (forall a b, R a b). Lemma ToβηPar a b : R a b -> βηPar.R a b. Proof. induction 1; hauto lq:on ctrs:βηPar.R. Qed. End IPar. Module OExp. Inductive R : Tm -> Tm -> Prop := | AbsEta b : R b (Abs (App (ren_Tm shift b) (VarTm var_zero))). Derive Inversion inv with (forall a b, R a b). End OExp. Lemma βηO_commute a b c : βηPar.R a b -> OExp.R a c -> exists d, OExp.R b d /\ βηPar.R c d. Proof. hauto lq:on inv:OExp.R ctrs:OExp.R,βηPar.R use:βηPar.renaming, βηPar.refl. Qed. Lemma βηO_commute0 a b c : βηPar.R a b -> rtc OExp.R a c -> exists d, rtc OExp.R b d /\ βηPar.R c d. Proof. move => + h. move : b. induction h; hauto lq:on ctrs:rtc use:βηO_commute. Qed. Lemma IO_factorization a c : βηPar.R a c -> exists b, IPar.R a b /\ rtc OExp.R b c. Proof. move => h. elim : a c /h. - move => i. exists (VarTm i). split. constructor. apply rtc_refl. - move => b0 b1 a0 a1 hb [b' [ihb0 ihb1]] ha [a' [iha0 iha1]]. exists (App b1 a1). split. apply IPar.AppCong; eauto. apply rtc_refl. - move => a0 a1 ha [a' [iha0 iha1]]. exists (Abs a1). split. by apply IPar.AbsCong. apply rtc_refl. - move => b0 b1 a0 a1 hb [b' [ihb0 ihb1]] ha [a' [iha0 iha1]]. eexists. split. apply IPar.AppAbs; eauto. apply rtc_refl. - move => b0 b1 hb [b' [ihb0 ihb1]]. exists b'. split => //. apply : rtc_r; eauto. constructor. Qed. Lemma IO_merge a b c : βηPar.R a b -> OExp.R b c -> βηPar.R a c. Proof. hauto lq:on inv:OExp.R ctrs:βηPar.R. Qed. Lemma IO_merge' a b c : βηPar.R a b -> rtc OExp.R b c -> βηPar.R a c. Proof. induction 2; hauto l:on use:IO_merge. Qed. (* Lemma AppAbsEta b0 a0 b1 a1 : *) (* βηPar.R b0 (Abs b1) -> *) (* βηPar.R a0 a1 -> *) (* βηPar.R *) Lemma diamond a b c : IPar.R a b -> IPar.R a c -> exists d, IPar.R b d /\ IPar.R c d. Proof. elim : a b c. - hauto lq:on inv:IPar.R ctrs:IPar.R. - move => a iha b c. elim /IPar.inv => //=_. move => a0 a1 + [?]?. subst. move => /[swap]. elim /IPar.inv => //=_. move => a0 a2 + [?]?. subst. move /IO_factorization. move => [a3 [h0 h1]]. move /IO_factorization. move => [a4 [h2 h3]]. move : iha h0 h2. repeat move/[apply]. move => [d [h2 h4]]. move : Lemma diamond a b0 b1 : βηPar.R a b0 -> βηPar.R a b1 -> exists c, βηPar.R b0 c /\ βηPar.R b1 c. Proof. move => h. move : b1. elim : a b0 / h. - move => i b1 /IO_factorization. move => [b [h0 h1]]. inversion h0; subst. exists b1. split => //=. apply : IO_merge'; eauto. constructor. apply βηPar.refl. - move => b0 b1 a0 a1 hb ihb ha iha b2 /IO_factorization. move => [u [h0 h1]]. elim /IPar.inv : h0=>//_. + move => b3 b4 a2 a3 hb' ha' [*]. subst. have {}/ihb [b14 [ihb0 ihb1]] := hb'. have {}/iha [a13 [iha0 iha1]] := ha'. set q := (App _ _) in h1. have : βηPar.R q (App b14 a13) by constructor. move : βηO_commute0 h1. subst q. repeat move/[apply]. move => [d [h0 h1]]. exists d. split => //. apply : IO_merge'; eauto using βηPar.AppCong. + move => b3 b4 a2 a3 hb' ha' [*]. subst. move /IO_factorization : hb. move => [b []]. elim /IPar.inv => //=_ a2 b5 hb'' [?]? ho. subst. move /βηPar.AbsCong : hb'. move => {}/ihb. move => [b14 [ihb0 ihb1]]. move : iha ha' => /[apply]. move => [a13 [iha0 iha1]].