Restructure proof to use hindley rosen

theories/confluence.v

@@ -9,7 +9,7 @@ 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.
+Module ηPar.
   Inductive R : Tm -> Tm -> Prop :=
   | VarCong i :
     R (VarTm i) (VarTm i)
@@ -20,10 +20,6 @@ Module βηPar.
   | 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))).
@@ -32,13 +28,6 @@ Module βη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 ->
@@ -54,7 +43,6 @@ Module βηPar.
   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.
 
@@ -94,33 +82,286 @@ Module βηPar.
   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.
+End ηPar.
+
+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).
+
+  #[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 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.
+  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.
+  Qed.
+
+End βPar.
+
+
+Module ηexp.
+  Inductive R : Tm -> Tm -> Prop :=
+  | AppCong0 b0 b1 a :
+    R b0 b1 ->
+    R (App b0 a) (App b1 a)
+  | AppCong1 b a0 a1 :
+    R a0 a1 ->
+    R (App b a0) (App b a1)
+  | AbsCong a0 a1 :
+    R a0 a1 ->
+    R (Abs a0) (Abs a1)
+  | AbsEta a :
+    R a (Abs (App (ren_Tm shift a) (VarTm var_zero))).
+
+  Derive Inversion inv with (forall a b, R a b).
+
+  Lemma AbsEta' a u :
+    u = (Abs (App (ren_Tm shift a) (VarTm var_zero))) ->
+    R a u.
+  Proof. move => ->. apply AbsEta. Qed.
+
+  Lemma morphing a b ρ :
+    R a b ->
+    R (subst_Tm ρ a) (subst_Tm ρ b).
+  Proof.
+    move => h. move : ρ. elim : a b /h => //=; try qauto ctrs:R.
+    - move => *; apply : AbsEta'; eauto. by asimpl.
+  Qed.
+
+End ηexp.
+
+Module ηexps.
+
+  #[local]Ltac solve_s_rec :=
+  move => *; eapply rtc_l; eauto;
+         hauto lq:on ctrs:ηexp.R.
+
+  #[local]Ltac solve_s :=
+    repeat (induction 1; last by solve_s_rec); apply rtc_refl.
+
+  Lemma AbsCong (a b : Tm) :
+    rtc ηexp.R a b ->
+    rtc ηexp.R (Abs a) (Abs b).
+  Proof. solve_s. Qed.
+
+  Lemma AppCong (a0 a1 b0 b1 : Tm) :
+    rtc ηexp.R a0 a1 ->
+    rtc ηexp.R b0 b1 ->
+    rtc ηexp.R (App a0 b0) (App a1 b1).
+  Proof. solve_s. Qed.
+
+  Lemma morphing a b ρ :
+    rtc ηexp.R a b ->
+    rtc ηexp.R (subst_Tm ρ a) (subst_Tm ρ b).
+  Proof.
+    induction 1; hauto l:on use:ηexp.morphing ctrs:rtc.
+  Qed.
+
+  Lemma renaming a b ξ :
+    rtc ηexp.R a b ->
+    rtc ηexp.R (ren_Tm ξ a) (ren_Tm ξ b).
+  Proof. substify. apply morphing. Qed.
+
+  Definition lifting_ok ρ0 ρ1 := forall (i : nat), rtc ηexp.R (ρ0 i) (ρ1 i).
+
+  Lemma lifting_ren (ξ : nat -> nat) ρ0 ρ1 :
+    lifting_ok ρ0 ρ1 ->
+    lifting_ok (funcomp (ren_Tm ξ) ρ0) (funcomp (ren_Tm ξ) ρ1).
+  Proof. rewrite /lifting_ok; eauto using renaming. Qed.
+
+  Lemma lifting_ext a b ρ0 ρ1 :
+    rtc ηexp.R a b ->
+    lifting_ok ρ0 ρ1 ->
+    lifting_ok (scons a ρ0) (scons b ρ1).
+  Proof.
+    move => * [|i] //=.
+  Qed.
+
+  Lemma lifting_up ρ0 ρ1 :
+    lifting_ok ρ0 ρ1 ->
+    lifting_ok (up_Tm_Tm ρ0) (up_Tm_Tm ρ1).
+  Proof.
+    move => h.
+    apply lifting_ext. apply rtc_refl.
+    by apply lifting_ren.
+  Qed.
+
+  Lemma lifting a ρ0 ρ1 :
+    lifting_ok ρ0 ρ1 ->
+    rtc ηexp.R (subst_Tm ρ0 a) (subst_Tm ρ1 a).
+  Proof.
+    move : ρ0 ρ1.
+    elim : a => //=;
+      qauto use:lifting_up, ηexps.AbsCong,ηexps.AppCong .
+  Qed.
+
+End ηexps.
+
+Lemma subst_id b :  subst_Tm (scons (VarTm var_zero) (funcomp VarTm shift)) b = b.
+  symmetry. have h : b = subst_Tm VarTm b by asimpl.
+  rewrite {1}h.
+  apply ext_Tm.
+  case => //=.
+Qed.
+
+Lemma βη_commute0 a b c :
+  βPar.R a b ->
+  ηexp.R a c ->
+  exists d, rtc ηexp.R b d /\ βPar.R c d.
+Proof.
+  move => h. move : c.
+  elim  :a b /h.
+  - move => i c. elim /ηexp.inv => //=_.
+    move => *. subst.
+    eexists. split; last by apply βPar.refl.
+    apply rtc_once. constructor.
+  - move => b0 b1 a0 a1 hb ihb ha iha u.
+    elim /ηexp.inv => //=_.
+    + move => b2 b3 a2 hb' [*]. subst.
+      move : ihb hb' => /[apply]. move=> [b2 [ihb0 ihb1]].
+      clear iha.
+      exists (App b2 a1).
+      split.
+      sfirstorder use:ηexps.AppCong, rtc_refl.
+      hauto lq:on ctrs:βPar.R  use:βPar.refl.
+    + move => b2 ? a2 + [*]. subst.
+      move => {}/iha {ihb} [a12 [ih0 ih1]].
+      exists (App b1 a12).
+      split.
+      sfirstorder use:ηexps.AppCong, rtc_refl.
+      hauto lq:on ctrs:βPar.R  use:βPar.refl.
+    + move => *. subst. move {ihb iha}.
+      eexists. split.
+      apply rtc_once. apply ηexp.AbsEta. simpl.
+      hauto lq:on ctrs:βPar.R use:βPar.renaming.
+  - move => a0 a1 ha iha u.
+    elim /ηexp.inv => //=_.
+    + qauto l:on ctrs:βPar.R use:ηexps.AbsCong.
+    + move => *. subst. move {iha}.
+      eexists.
+      split.
+      apply rtc_once. apply ηexp.AbsEta.
+      hauto lq:on ctrs:βPar.R use:βPar.renaming.
+  - move => b0 b1 a0 a1 hb ihb ha iha u.
+    elim /ηexp.inv => //=_.
+    + move => b2 b3 a2 + [*]. subst.
+      elim /ηexp.inv => //=_.
+      * move => a2 a3 + [*]. subst.
+        move => /[dup] hba.
+        move => {}/ihb {iha}.
+        move => [bd [ih0 ih1]].
+        exists (subst_Tm (scons a1 VarTm ) bd).
+        split.
+        ** sfirstorder use:ηexps.morphing.
+        ** constructor; eauto.
+      * move => *. subst. move {ihb iha}.
+        exists (subst_Tm (scons a1 VarTm) b1).
+        split. apply rtc_refl.
+        constructor.
+        apply : βPar.AppAbs'; cycle 1. sfirstorder use:βPar.renaming.
+        constructor. by asimpl; rewrite subst_id.
+        eauto.
+    + move => b2 a2 a3 + [*]. subst.
+      move => {}/iha {ihb}.
+      move => [a13 [ih0 ih1]].
+      exists (subst_Tm (scons a13 VarTm) b1).
+      split; last by constructor.
+      apply ηexps.lifting.
+      case => //=. eauto using rtc_refl.
+    + move => *. subst. move {ihb iha}.
+      exists (Abs (App (ren_Tm shift (subst_Tm (scons a1 VarTm) b1)) (VarTm var_zero))). split.
+      * apply rtc_once. constructor.
+      * constructor. constructor; last by apply βPar.refl.
+        apply : βPar.AppAbs'; eauto using βPar.renaming.
+        by asimpl.
+Qed.
 
 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 b0 b1 ->
-    βηPar.R a0 a1 ->
+    ηPar.R a0 a1 ->
     R (App b0 a0) (App b1 a1)
   | AbsCong a0 a1 :
-    βηPar.R a0 a1 ->
+    ηPar.R a0 a1 ->
-    R (Abs a0) (Abs 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.
+  Lemma ToηPar a b : R a b -> ηPar.R a b.
-  Proof. induction 1; hauto lq:on ctrs:βηPar.R. Qed.
+  Proof. induction 1; hauto lq:on ctrs:ηPar.R. Qed.
 End IPar.
 
 Module OExp.
@@ -131,22 +372,22 @@ Module OExp.
   Derive Inversion inv with (forall a b, R a b).
 End OExp.
 
-Lemma βηO_commute a b c :
+Lemma ηO_commute a b c :
-  βηPar.R a b -> OExp.R a c ->
+  ηPar.R a b -> OExp.R a c ->
-  exists d, OExp.R b d /\ βηPar.R c d.
+  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.
+  hauto lq:on inv:OExp.R ctrs:OExp.R,ηPar.R use:ηPar.renaming, ηPar.refl.
 Qed.
 
-Lemma βηO_commute0 a b c :
+Lemma ηO_commute0 a b c :
-  βηPar.R a b -> rtc OExp.R a c ->
+  ηPar.R a b -> rtc OExp.R a c ->
-  exists d, rtc OExp.R b d /\ βηPar.R c d.
+  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.
+  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.
+  η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).
@@ -159,9 +400,6 @@ Proof.
   - 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.
@@ -169,41 +407,15 @@ Proof.
 Qed.
 
 Lemma IO_merge a b c :
-  βηPar.R a b -> OExp.R b c -> βηPar.R a c.
+  ηPar.R a b -> OExp.R b c -> ηPar.R a c.
-Proof. hauto lq:on inv:OExp.R ctrs:βηPar.R. Qed.
+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.
+  η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.
+  η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.
@@ -213,7 +425,7 @@ Proof.
     split => //=.
     apply : IO_merge'; eauto.
     constructor.
-    apply βηPar.refl.
+    apply ηPar.refl.
   - move => b0 b1 a0 a1 hb ihb ha iha b2 /IO_factorization.
     move => [u [h0 h1]].
     elim /IPar.inv : h0=>//_.
@@ -221,15 +433,27 @@ Proof.
       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.
+      have : ηPar.R q (App b14 a13) by constructor.
-      move : βηO_commute0 h1. subst q. repeat move/[apply].
+      move : ηO_commute0 h1. subst q. repeat move/[apply].
       move => [d [h0 h1]].
       exists d.
       split => //.
-      apply : IO_merge'; eauto using βηPar.AppCong.
+      apply : IO_merge'; eauto using ηPar.AppCong.
-    + move => b3 b4 a2 a3 hb' ha' [*]. subst.
+  - move => a0 a1 ha iha u /IO_factorization.
-      move /IO_factorization : hb.
+    move => [v [ih0 ih1]].
-      move => [b []].
+    elim /IPar.inv : ih0 => //= _.
-      elim /IPar.inv => //=_ a2 b5 hb'' [?]? ho. subst.
+    move => a2 a3 + [*]. subst.
-      move /βηPar.AbsCong : hb'. move => {}/ihb. move => [b14 [ihb0 ihb1]].
+    move => {}/iha. move => [a2 [h0 h1]].
-      move : iha ha'  => /[apply]. move => [a13 [iha0 iha1]].
+    move /ηPar.AbsCong in h1.
+    move : ηO_commute0 ih1 h1; repeat move/[apply].
+    move => [d [h1 h2]].
+    exists d.
+    split => //.
+    apply : IO_merge'; eauto.
+    by constructor.
+  - move => b0 b1 hb ihb b2 {}/ihb.
+    move => [c [h0 h1]].
+    eexists. split; cycle 1.
+    apply ηPar.AbsEta; eauto.
+    hauto lq:on ctrs:ηPar.R use:ηPar.renaming.
+Qed.