pair-eta/theories/fp_red.v

Require Import ssreflect.
From stdpp Require Import relations (rtc (..)).
From Hammer Require Import Tactics.
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.


(* Trying my best to not write C style module_funcname *)
Module Par.
  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 b0 b1 ->
    R c0 c1 ->
    R (App (Pair a0 b0) c0) (Pair (App a1 c1) (App b1 c1))
  | Proj1Abs a0 a1 :
    R a0 a1 ->
    R (Proj1 (Abs a0)) (Abs (Proj1 a0))
  | Proj1Pair a0 a1 b :
    R a0 a1 ->
    R (Proj1 (Pair a0 b)) a1
  | Proj2Abs a0 a1 :
    R a0 a1 ->
    R (Proj2 (Abs a0)) (Abs (Proj2 a0))
  | Proj2Pair a0 a1 b :
    R a0 a1 ->
    R (Proj2 (Pair a0 b)) a1

  (****************** Eta ***********************)
  | AppEta a0 a1 :
    R a0 a1 ->
    R a0 (Abs (App (ren_Tm shift a1) (VarTm var_zero)))
  | PairEta a0 a1 :
    R a0 a1 ->
    R a0 (Pair (Proj1 a1) (Proj2 a1))

  (*************** 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)
  | Proj1Cong a0 a1 :
    R a0 a1 ->
    R (Proj1 a0) (Proj1 a1)
  | Proj2Cong a0 a1 :
    R a0 a1 ->
    R (Proj2 a0) (Proj2 a1).
End Par.

(***************** 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)
  | AppPair a0 a1 b0 b1 c0 c1:
    R a0 a1 ->
    R b0 b1 ->
    R c0 c1 ->
    R (App (Pair a0 b0) c0) (Pair (App a1 c1) (App b1 c1))
  | Proj1Abs a0 a1 :
    R a0 a1 ->
    R (Proj1 (Abs a0)) (Abs (Proj1 a0))
  | Proj1Pair a0 a1 b :
    R a0 a1 ->
    R (Proj1 (Pair a0 b)) a1
  | Proj2Abs a0 a1 :
    R a0 a1 ->
    R (Proj2 (Abs a0)) (Abs (Proj2 a0))
  | Proj2Pair a0 a1 b :
    R a0 a1 ->
    R (Proj2 (Pair a0 b)) a1

  (*************** 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)
  | Proj1Cong a0 a1 :
    R a0 a1 ->
    R (Proj1 a0) (Proj1 a1)
  | Proj2Cong a0 a1 :
    R a0 a1 ->
    R (Proj2 a0) (Proj2 a1).

  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 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.
  Qed.

End RPar.

Module EPar.
  Inductive R {n} : Tm n -> Tm n ->  Prop :=
  (****************** Eta ***********************)
  | AppEta a0 a1 :
    R a0 a1 ->
    R a0 (Abs (App (ren_Tm shift a1) (VarTm var_zero)))
  | PairEta a0 a1 :
    R a0 a1 ->
    R a0 (Pair (Proj1 a1) (Proj2 a1))

  (*************** 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)
  | Proj1Cong a0 a1 :
    R a0 a1 ->
    R (Proj1 a0) (Proj1 a1)
  | Proj2Cong a0 a1 :
    R a0 a1 ->
    R (Proj2 a0) (Proj2 a1).

  Lemma refl n (a : Tm n) : EPar.R a a.
  Proof.
    induction a; hauto lq:on ctrs:EPar.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.

    move => n a0 a1 ha iha m ξ /=.
    move /(_ _ ξ) /AppEta : iha.
    by asimpl.

    all : qauto ctrs:R.
  Qed.

  Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
End EPar.


Local Ltac com_helper :=
  split; [hauto lq:on ctrs:RPar.R use: RPar.refl, RPar.renaming
         |hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming].

Lemma RPars_AbsCong n (a b : Tm (S n)) :
  rtc RPar.R a b ->
  rtc RPar.R (Abs a) (Abs b).
Proof. induction 1; hauto l:on ctrs:RPar.R, rtc. Qed.

Lemma RPars_AppCong n (a0 a1 b : Tm n) :
  rtc RPar.R a0 a1 ->
  rtc RPar.R (App a0 b) (App a1 b).
Proof.
  move => h. move : b.
  elim : a0 a1 /h.
  - qauto ctrs:RPar.R, rtc.
  - move => x y z h0 h1 ih b.
    apply rtc_l with (y := App y b) => //.
    hauto lq:on ctrs:RPar.R use:RPar.refl.
Qed.

Lemma RPars_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.
  move => h. move : b0 b1.
  elim : a0 a1 /h.
  - move => x b0 b1 h.
    elim : b0 b1 /h.
    by auto using rtc_refl.
    move => x0 y z h0 h1 h2.
    apply : rtc_l; eauto.
    by eauto using RPar.refl, RPar.PairCong.
  - move => x y z h0 h1 ih b0 b1 h.
    apply : rtc_l; eauto.
    by eauto using RPar.refl, RPar.PairCong.
Qed.


Lemma RPars_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 RPars_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_EPar n a (b : Tm n) :
  EPar.R (Abs a) b ->
  forall c, exists d,
    EPar.R (subst_Tm (scons c VarTm) a) d /\
      rtc RPar.R (App b c) d.
Proof.
  move E : (Abs a) => u h.
  move : a E.
  elim : n u b /h => //=.
  - move => n a0 a1 ha iha b ? c. subst.
    specialize iha with (1 := eq_refl) (c := c).
    move : iha => [d [ih0 ih1]].
    exists d.
    split => //.
    apply : rtc_l.
    apply RPar.AppAbs; eauto => //=.
    apply RPar.refl.
    by apply RPar.refl.
    by asimpl.
  - move => n a0 a1 ha iha a ? c. subst.
    specialize iha with (1 := eq_refl) (c := c).
    move : iha => [d [ih0 ih1]].
    exists (Pair (Proj1 d) (Proj2 d)). split => //.
    + move { ih1}.
      hauto lq:on ctrs:EPar.R.
    + apply : rtc_l.
      apply RPar.AppPair.
      admit.
      admit.
      apply RPar.refl.
      admit.
  - admit.
Admitted.


Lemma commutativity 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.
Proof.
  move => h. move : b1.
  elim : n a b0 / h.
  - move => n a b0 ha iha b1 hb.
    move : iha (hb) => /[apply].
    move => [c [ih0 ih1]].
    exists (Abs (App (ren_Tm shift c) (VarTm var_zero))).
    split.
    + sfirstorder use:RPars_AbsCong, RPars_AppCong, RPars_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 c c). split.
    + by apply RPars_PairCong.
    + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming.
  - hauto l:on ctrs:rtc inv:RPar.R.
  - move => n a0 a1 h ih b1.
    elim /RPar.inv => //= _.
    move => a2 a3 ? [*]. subst.
    hauto lq:on ctrs:rtc, RPar.R, EPar.R use:RPars_AbsCong.
  - move => n a0 a1 b0 b1 ha iha hb ihb b2.
    elim /RPar.inv => //= _.
    + move =>  a2 a3 b3 b4 h0 h1 [*]. subst.
      elim /EPar.inv : ha => //= _.
      * move => a0 a4 h *. subst.
        move /ihb : h1 {ihb}.
        move => [c [hb1 hb4]].
        have {}/iha : RPar.R (Abs a2) (Abs a3) by hauto lq:on ctrs:RPar.R.
        move => [c0 [hc0 hc1]].
        eexists.
        split.
        ** apply RPar.AppAbs; eauto.
           eauto using RPar.refl.
        ** simpl.


      admit.
    + move => a2 a3 b3 b4 c0 c1 h0 h1 h2 [*]. subst.
      admit.
    + hauto lq:on ctrs:RPar.R, EPar.R.
  - hauto lq:on ctrs:RPar.R, EPar.R inv:RPar.R.
  - move => n a b0 h0 ih0 b1.
    elim /RPar.inv => //= _.
    + move => a0 a1 h [*]. subst.
      admit.
    + move => a0 ? a1 h1 [*]. subst.
      admit.
    + hauto lq:on ctrs:RPar.R, EPar.R.
  - move => n a b0 h0 ih0 b1.
    elim /RPar.inv => //= _.
    + move => a0 a1 ha [*]. subst.
      admit.
    + move => a0 a1 b2 h [*]. subst.
      admit.
    + hauto lq:on ctrs:RPar.R, EPar.R.
Admitted.

Lemma EPar_Par n (a b : Tm n) : EPar.R a b -> Par.R a b.
Proof. induction 1; hauto lq:on ctrs:Par.R. Qed.

Lemma RPar_Par n (a b : Tm n) : RPar.R a b -> Par.R a b.
Proof. induction 1; hauto lq:on ctrs:Par.R. Qed.

Lemma merge n (t a u : Tm n) :
  EPar.R t a ->
  RPar.R a u ->
  Par.R t u.
Proof.
  move => h. move : u.
  elim:t a/h.
  - move => n0 a0 a1 ha iha u hu.
    apply iha.
    inversion hu; subst.


  - hauto lq:on inv:RPar.R.
  - move => a0 a1 b0 b1 ha iha hb ihb u.
    inversion 1; subst.
    + inversion ha.

best use:EPar_Par, RPar_Par.

  best ctrs:Par.R inv:EPar.R,RPar.R use:EPar_Par, RPar_Par.