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)
  | 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 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 : 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 : AbsEta'; eauto using morphing_up. by asimpl.
  Qed.

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.

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).
  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 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 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 η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_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 η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 oexp_appabs b b' b0 a0 a1 :
  rtc OExp.R (Abs b) b0 ->
  βPar.R b b' ->
  βPar.R a0 a1 ->
  βPar.R (App b0 a0) (subst_Tm (scons a1 VarTm) b').
Proof.
  move E : (Abs b) => u hu.
  move : b E b' a0 a1.
  elim : u b0 /hu => //=.
  - move => ? b ? b' a0 a1 hb ha. subst.
    by constructor.
  - move => c0 c1 c2 hc0 hc1 ih b ? b' a0 a1 hb ha. subst.
    elim /OExp.inv : hc0 => //= _.
    move => ? ? ?. subst.
    specialize ih with (1 := eq_refl).
    apply ih => //.
    eapply βPar.AppAbs' with (b1 := ren_Tm (upRen_Tm_Tm shift) b') (a1 := VarTm var_zero). by asimpl; rewrite subst_id.
    by apply βPar.renaming.
    constructor.
Qed.

(* Direct commutativity proof with parallel η *)
Lemma βη_commute0 a b c :
  βPar.R a b ->
  ηPar.R a c ->
  exists d, ηPar.R b d /\ βPar.R c d.
Proof.
  move => h. move : c.
  elim  :a b /h.
  - move => i c. move /IO_factorization.
    move => [b [ihb0 ihb1]].
    elim /IPar.inv : ihb0 => //=_.
    move => ? [*]. subst.
    exists c. split. apply : IO_merge'; eauto. constructor.
    apply βPar.refl.
  - move => b0 b1 a0 a1 hb ihb ha iha u /IO_factorization.
    move => [v [+ hv]].
    elim /IPar.inv => //=_.
    move => b2 b3 a2 a3 hb2 ha2 [*]. subst.
    rename b3 into b2. rename a3 into a2.
    move : hb2 => {}/ihb. move => [b12 [ihb0 ihb1]].
    move : ha2 => {}/iha. move => [a12 [iha0 iha1]].
    have h2 : βPar.R (App b2 a2) (App b12 a12) by constructor.
    move : βO_commute0 hv h2. repeat move/[apply].
    move => [v][h0 h1].
    exists v. split => //. apply : IO_merge'; eauto; by constructor.
  - move => a0 a1 ha iha u /IO_factorization.
    move => [v][hb0]hb1.
    elim /IPar.inv : hb0 => //=_.
    move => ? a2 + [*]. subst.
    move => {}/iha. move => [a12 [ih0 ih1]].
    have {ih1} : βPar.R (Abs a2) (Abs a12) by constructor.
    move : βO_commute0 hb1. repeat move/[apply].
    move => [d [h0 h1]]. exists d. split => //.
    apply : IO_merge'; eauto; by constructor.
  - move => b0 b1 a0 a1 hb ihb ha iha u /IO_factorization.
    move => [v][hv0]hv1.
    elim /IPar.inv : hv0 => //=_.
    move => ? b2 ? a2 hb2 ha2 [*]. subst.
    move /IO_factorization : hb2 => [b [h0 h1]].
    elim /IPar.inv : h0 => //=_.
    move => ? b' ha' [*]. subst.
    move : ihb (ha') => /[apply]. move => [b12 [ihb0 ihb1]].
    move : iha (ha2) => /[apply]. move => [a12 [iha0 iha1]].
    have : βPar.R (App b2 a2) (subst_Tm (scons a12 VarTm) b12)
      by eauto using oexp_appabs.
    move : βO_commute0 hv1. repeat move/[apply].
    move => [v][hv0]hv1.
    exists v. split => //.
    apply : IO_merge'; eauto.
    apply ηPar.morphing2 => //.
    apply ηPar.morphing2_ext => //.
    move => *. constructor.
Qed.

(* Indirect but perhaps nicer proof with an extra
    definition of full non-paralell η expansion *)
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.


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 => a0 a1 ha iha u /IO_factorization.
    move => [v [ih0 ih1]].
    elim /IPar.inv : ih0 => //= _.
    move => a2 a3 + [*]. subst.
    move => {}/iha. move => [a2 [h0 h1]].
    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.