From Tealeaves Require Import
  Examples.Lambda.Confluence
  Classes.Monoid
  Simplification.Binddt.

Import Monoid.Notations.
Import DecoratedTraversableMonad.UsefulInstances.

Fixpoint mwp {A B: Type} (P: (A -> B) -> (A -> B)) (f: A -> B) (t: lam A): lam B :=
  match t with
  | tvar a    => tvar (f a)
  | abs body  => abs (mwp P (P f) body)
  | app t1 t2 => app (mwp P f t1) (mwp P f t2)
  end.

Fixpoint bwp {A B: Type} (P: (A -> lam B) -> (A -> lam B)) (f: A -> lam B) (t: lam A): lam B :=
  match t with
  | tvar a    => f a
  | abs body  => abs (bwp P (P f) body)
  | app t1 t2 => app (bwp P f t1) (bwp P f t2)
  end.

Lemma mwp_equiv: forall A B (f: nat * A -> B) (t: lam A),
    mapd f t = mwp (fun f => f ⦿ 1) f (mwp id (fun a => (0, a)) t).
forall (A B : Type) (f : nat * A -> B) (t : lam A),
mapd f t =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t)
Proof.
forall (A B : Type) (f : nat * A -> B) (t : lam A),
mapd f t =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t)
  intros.
A, B: Type
f: nat * A -> B
t: lam A
mapd f t =
mwp (fun f : nat * A -> B => f ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t)
  generalize dependent f.
A, B: Type
t: lam A
forall f : nat * A -> B,
mapd f t =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t)
  induction t; intro f.
A, B: Type
v: A
f: nat * A -> B
mapd f (tvar v) =
mwp (fun f : nat * A -> B => f ⦿ 1) f
  (mwp id (fun a : A => (0, a)) (tvar v))
A, B: Type
t: lam A
IHt: forall f : nat * A -> B,
mapd f t =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f (mwp id (fun a : A => (0, a)) t)
f: nat * A -> B
mapd f (abs t) =
mwp (fun f : nat * A -> B => f ⦿ 1) f
  (mwp id (fun a : A => (0, a)) (abs t))
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> B,
mapd f t1 =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t1)
IHt2: forall f : nat * A -> B,
mapd f t2 =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t2)
f: nat * A -> B
mapd f (app t1 t2) =
mwp (fun f : nat * A -> B => f ⦿ 1) f
  (mwp id (fun a : A => (0, a)) (app t1 t2))
  -
A, B: Type
v: A
f: nat * A -> B
mapd f (tvar v) =
mwp (fun f : nat * A -> B => f ⦿ 1) f
  (mwp id (fun a : A => (0, a)) (tvar v)) reflexivity.
  -
A, B: Type
t: lam A
IHt: forall f : nat * A -> B,
mapd f t =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t)
f: nat * A -> B
mapd f (abs t) =
mwp (fun f : nat * A -> B => f ⦿ 1) f
  (mwp id (fun a : A => (0, a)) (abs t)) simplify_mapd.
A, B: Type
t: lam A
IHt: forall f : nat * A -> B,
mapd f t =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t)
f: nat * A -> B
abs (mapd (f ⦿ 1) t) =
mwp (fun f : nat * A -> B => f ⦿ 1) f
  (mwp id (fun a : A => (0, a)) (abs t))
    cbn.
A, B: Type
t: lam A
IHt: forall f : nat * A -> B,
mapd f t =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t)
f: nat * A -> B
abs (mapd (f ⦿ 1) t) =
abs
  (mwp (fun f : nat * A -> B => f ⦿ 1) 
     (f ⦿ 1) (mwp id (id (fun a : A => (0, a))) t)) fequal.
A, B: Type
t: lam A
IHt: forall f : nat * A -> B,
mapd f t =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t)
f: nat * A -> B
mapd (f ⦿ 1) t =
mwp (fun f : nat * A -> B => f ⦿ 1) 
  (f ⦿ 1) (mwp id (id (fun a : A => (0, a))) t)
    rewrite IHt.
A, B: Type
t: lam A
IHt: forall f : nat * A -> B,
mapd f t =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t)
f: nat * A -> B
mwp (fun f : nat * A -> B => f ⦿ 1) 
  (f ⦿ 1) (mwp id (fun a : A => (0, a)) t) =
mwp (fun f : nat * A -> B => f ⦿ 1) 
  (f ⦿ 1) (mwp id (id (fun a : A => (0, a))) t)
    reflexivity.
  -
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> B,
mapd f t1 =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t1)
IHt2: forall f : nat * A -> B,
mapd f t2 =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t2)
f: nat * A -> B
mapd f (app t1 t2) =
mwp (fun f : nat * A -> B => f ⦿ 1) f
  (mwp id (fun a : A => (0, a)) (app t1 t2)) simplify_mapd.
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> B,
mapd f t1 =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t1)
IHt2: forall f : nat * A -> B,
mapd f t2 =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t2)
f: nat * A -> B
app (mapd f t1) (mapd f t2) =
mwp (fun f : nat * A -> B => f ⦿ 1) f
  (mwp id (fun a : A => (0, a)) (app t1 t2))
    cbn.
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> B,
mapd f t1 =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t1)
IHt2: forall f : nat * A -> B,
mapd f t2 =
mwp (fun f0 : nat * A -> B => f0 ⦿ 1) f
  (mwp id (fun a : A => (0, a)) t2)
f: nat * A -> B
app (mapd f t1) (mapd f t2) =
app
  (mwp (fun f : nat * A -> B => f ⦿ 1) f
     (mwp id (fun a : A => (0, a)) t1))
  (mwp (fun f : nat * A -> B => f ⦿ 1) f
     (mwp id (fun a : A => (0, a)) t2)) fequal; auto.
Qed.

Lemma bwp_equiv: forall A B (f: nat * A -> lam B) (t: lam A),
    bindd f t = bwp (fun f => f ⦿ 1) f (bwp id (fun a => ret (0, a)) t).
forall (A B : Type) (f : nat * A -> lam B) (t : lam A),
bindd f t =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t)
Proof.
forall (A B : Type) (f : nat * A -> lam B) (t : lam A),
bindd f t =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t)
  intros.
A, B: Type
f: nat * A -> lam B
t: lam A
bindd f t =
bwp (fun f : nat * A -> lam B => f ⦿ 1) f
  (bwp id (ret ○ pair 0) t)
  generalize dependent f.
A, B: Type
t: lam A
forall f : nat * A -> lam B,
bindd f t =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t)
  induction t; intro f.
A, B: Type
v: A
f: nat * A -> lam B
bindd f (tvar v) =
bwp (fun f : nat * A -> lam B => f ⦿ 1) f
  (bwp id (ret ○ pair 0) (tvar v))
A, B: Type
t: lam A
IHt: forall f : nat * A -> lam B,
bindd f t =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f (bwp id (ret ○ pair 0) t)
f: nat * A -> lam B
bindd f (abs t) =
bwp (fun f : nat * A -> lam B => f ⦿ 1) f
  (bwp id (ret ○ pair 0) (abs t))
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> lam B,
bindd f t1 =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t1)
IHt2: forall f : nat * A -> lam B,
bindd f t2 =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t2)
f: nat * A -> lam B
bindd f (app t1 t2) =
bwp (fun f : nat * A -> lam B => f ⦿ 1) f
  (bwp id (ret ○ pair 0) (app t1 t2))
  -
A, B: Type
v: A
f: nat * A -> lam B
bindd f (tvar v) =
bwp (fun f : nat * A -> lam B => f ⦿ 1) f
  (bwp id (ret ○ pair 0) (tvar v)) reflexivity.
  -
A, B: Type
t: lam A
IHt: forall f : nat * A -> lam B,
bindd f t =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t)
f: nat * A -> lam B
bindd f (abs t) =
bwp (fun f : nat * A -> lam B => f ⦿ 1) f
  (bwp id (ret ○ pair 0) (abs t)) simplify_bindd.
A, B: Type
t: lam A
IHt: forall f : nat * A -> lam B,
bindd f t =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t)
f: nat * A -> lam B
abs (bindd (f ⦿ 1) t) =
bwp (fun f : nat * A -> lam B => f ⦿ 1) f
  (bwp id (ret ○ pair 0) (abs t))
    cbn.
A, B: Type
t: lam A
IHt: forall f : nat * A -> lam B,
bindd f t =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t)
f: nat * A -> lam B
abs (bindd (f ⦿ 1) t) =
abs
  (bwp (fun f : nat * A -> lam B => f ⦿ 1) 
     (f ⦿ 1) (bwp id (id (ret ○ pair 0)) t)) fequal.
A, B: Type
t: lam A
IHt: forall f : nat * A -> lam B,
bindd f t =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t)
f: nat * A -> lam B
bindd (f ⦿ 1) t =
bwp (fun f : nat * A -> lam B => f ⦿ 1) 
  (f ⦿ 1) (bwp id (id (ret ○ pair 0)) t)
    rewrite IHt.
A, B: Type
t: lam A
IHt: forall f : nat * A -> lam B,
bindd f t =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t)
f: nat * A -> lam B
bwp (fun f : nat * A -> lam B => f ⦿ 1) 
  (f ⦿ 1) (bwp id (ret ○ pair 0) t) =
bwp (fun f : nat * A -> lam B => f ⦿ 1) 
  (f ⦿ 1) (bwp id (id (ret ○ pair 0)) t)
    reflexivity.
  -
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> lam B,
bindd f t1 =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t1)
IHt2: forall f : nat * A -> lam B,
bindd f t2 =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t2)
f: nat * A -> lam B
bindd f (app t1 t2) =
bwp (fun f : nat * A -> lam B => f ⦿ 1) f
  (bwp id (ret ○ pair 0) (app t1 t2)) simplify_bindd.
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> lam B,
bindd f t1 =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t1)
IHt2: forall f : nat * A -> lam B,
bindd f t2 =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t2)
f: nat * A -> lam B
app (bindd f t1) (bindd f t2) =
bwp (fun f : nat * A -> lam B => f ⦿ 1) f
  (bwp id (ret ○ pair 0) (app t1 t2))
    cbn.
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> lam B,
bindd f t1 =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t1)
IHt2: forall f : nat * A -> lam B,
bindd f t2 =
bwp (fun f0 : nat * A -> lam B => f0 ⦿ 1) f
  (bwp id (ret ○ pair 0) t2)
f: nat * A -> lam B
app (bindd f t1) (bindd f t2) =
app
  (bwp (fun f : nat * A -> lam B => f ⦿ 1) f
     (bwp id (ret ○ pair 0) t1))
  (bwp (fun f : nat * A -> lam B => f ⦿ 1) f
     (bwp id (ret ○ pair 0) t2)) fequal; auto.
Qed.