From Tealeaves Require Export
  Examples.STLC.Syntax
  Simplification.Tests.Support.

Import STLC.Syntax.TermNotations.

(** * Simplification tests for derived operations *)
(******************************************************************************)

(** ** Rewriting lemmas for <<mapdReduce>> *)
(******************************************************************************)
Section term_mapdReduce_rewrite.

  Context {A M : Type} (f : nat * A -> M) `{Monoid M}.

  Lemma term_mapdReduce1 : forall (a : A),
      mapdReduce f (tvar a) = f (Ƶ, a).
A, M: Type
f: nat * A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall a : A, mapdReduce f (tvar a) = f (Ƶ, a)
  Proof.
A, M: Type
f: nat * A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall a : A, mapdReduce f (tvar a) = f (Ƶ, a)
    intros.
A, M: Type
f: nat * A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
a: A
mapdReduce f (tvar a) = f (Ƶ, a) simplify_mapdReduce.
A, M: Type
f: nat * A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
a: A
f (Ƶ, a) = f (Ƶ, a) reflexivity.
  Qed.

  Lemma term_mapdReduce2 : forall X (t : Lam A),
      mapdReduce f (λ X t) = mapdReduce (f ⦿ 1) t.
A, M: Type
f: nat * A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (X : typ) (t : Lam A),
mapdReduce f ((λ) X t) = mapdReduce (f ⦿ 1) t
  Proof.
A, M: Type
f: nat * A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (X : typ) (t : Lam A),
mapdReduce f ((λ) X t) = mapdReduce (f ⦿ 1) t
    intros.
A, M: Type
f: nat * A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
X: typ
t: Lam A
mapdReduce f ((λ) X t) = mapdReduce (f ⦿ 1) t simplify_mapdReduce.
A, M: Type
f: nat * A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
X: typ
t: Lam A
mapdReduce (f ⦿ 1) t = mapdReduce (f ⦿ 1) t reflexivity.
  Qed.

  Lemma term_mapdReduce3 : forall (t1 t2 : Lam A),
      mapdReduce f (⟨t1⟩ (t2)) = mapdReduce f t1 ● mapdReduce f t2.
A, M: Type
f: nat * A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall t1 t2 : Lam A,
mapdReduce f (⟨ t1 ⟩ (t2)) =
mapdReduce f t1 ● mapdReduce f t2
  Proof.
A, M: Type
f: nat * A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall t1 t2 : Lam A,
mapdReduce f (⟨ t1 ⟩ (t2)) =
mapdReduce f t1 ● mapdReduce f t2
    intros.
A, M: Type
f: nat * A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
t1, t2: Lam A
mapdReduce f (⟨ t1 ⟩ (t2)) =
mapdReduce f t1 ● mapdReduce f t2 simplify_mapdReduce.
A, M: Type
f: nat * A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
t1, t2: Lam A
mapdReduce f t1 ● mapdReduce f t2 =
mapdReduce f t1 ● mapdReduce f t2 reflexivity.
  Qed.

End term_mapdReduce_rewrite.

(** ** Rewriting lemmas for <<∈d>> *)
(******************************************************************************)
Section term_ind_rewrite.

  Lemma term_ind1 : forall (l1 l2 : LN) (n : nat),
      (n, l1) ∈d (tvar l2) <-> (n = Ƶ /\ l1 = l2).
forall (l1 l2 : LN) (n : nat),
(n, l1) ∈d tvar l2 <-> n = Ƶ /\ l1 = l2
  Proof.
forall (l1 l2 : LN) (n : nat),
(n, l1) ∈d tvar l2 <-> n = Ƶ /\ l1 = l2
    intros.
l1, l2: LN
n: nat
(n, l1) ∈d tvar l2 <-> n = Ƶ /\ l1 = l2
    simplify_LN.
l1, l2: LN
n: nat
n = Ƶ /\ l1 = l2 <-> n = Ƶ /\ l1 = l2
    conclude.
  Qed.

  Lemma term_ind2 : forall (t : term) (l : LN) (n : nat) (X : typ),
      (n, l) ∈d t = (S n, l) ∈d (λ X t).
forall (t : term) (l : LN) (n : nat) (X : typ),
(n, l) ∈d t = (S n, l) ∈d (λ) X t
  Proof.
forall (t : term) (l : LN) (n : nat) (X : typ),
(n, l) ∈d t = (S n, l) ∈d (λ) X t
    intros.
t: term
l: LN
n: nat
X: typ
(n, l) ∈d t = (S n, l) ∈d (λ) X t
    simplify_LN.
t: term
l: LN
n: nat
X: typ
(n, l) ∈d t = (n, l) ∈d t
    conclude.
  Qed.

  Lemma term_ind2_nZ : forall (t : term) (l : LN) (n : nat) (X : typ),
      (n, l) ∈d (λ X t) -> n <> 0.
forall (t : term) (l : LN) (n : nat) (X : typ),
(n, l) ∈d (λ) X t -> n <> 0
  Proof.
forall (t : term) (l : LN) (n : nat) (X : typ),
(n, l) ∈d (λ) X t -> n <> 0
    introv.
t: term
l: LN
n: nat
X: typ
(n, l) ∈d (λ) X t -> n <> 0
    destruct n.
t: term
l: LN
X: typ
(0, l) ∈d (λ) X t -> 0 <> 0
t: term
l: LN
n: nat
X: typ
(S n, l) ∈d (λ) X t -> S n <> 0
    -
t: term
l: LN
X: typ
(0, l) ∈d (λ) X t -> 0 <> 0 simplify_LN.
t: term
l: LN
X: typ
mapdReduce (const False) t -> 0 <> 0
      rewrite exists_false_false.
t: term
l: LN
X: typ
False -> 0 <> 0
      easy.
    -
t: term
l: LN
n: nat
X: typ
(S n, l) ∈d (λ) X t -> S n <> 0 simplify_LN.
t: term
l: LN
n: nat
X: typ
(n, l) ∈d t -> S n <> 0
      easy.
  Qed.

  (* TODO: This is a good example for improving simplify execution times. *)
  Lemma term_ind3 : forall (t1 t2 : term) (n : nat) (l : LN),
      (n, l) ∈d (⟨t1⟩ (t2)) <-> (n, l) ∈d t1 \/ (n, l) ∈d t2.
forall (t1 t2 : term) (n : nat) (l : LN),
(n, l) ∈d (⟨ t1 ⟩ (t2)) <->
(n, l) ∈d t1 \/ (n, l) ∈d t2
  Proof.
forall (t1 t2 : term) (n : nat) (l : LN),
(n, l) ∈d (⟨ t1 ⟩ (t2)) <->
(n, l) ∈d t1 \/ (n, l) ∈d t2
    intros.
t1, t2: term
n: nat
l: LN
(n, l) ∈d (⟨ t1 ⟩ (t2)) <->
(n, l) ∈d t1 \/ (n, l) ∈d t2
    simplify_LN.
t1, t2: term
n: nat
l: LN
(n, l) ∈d t1 ● (n, l) ∈d t2 <->
(n, l) ∈d t1 \/ (n, l) ∈d t2
    (* TODO Investigate why const wasn't unfolded. *)
    unfold const.
t1, t2: term
n: nat
l: LN
(n, l) ∈d t1 ● (n, l) ∈d t2 <->
(n, l) ∈d t1 \/ (n, l) ∈d t2
    simplify_monoid_disjunction.
t1, t2: term
n: nat
l: LN
(n, l) ∈d t1 \/ (n, l) ∈d t2 <->
(n, l) ∈d t1 \/ (n, l) ∈d t2
    conclude.
  Qed.

End term_ind_rewrite.

(** ** Rewriting lemmas for <<mapReduce>> *)
(******************************************************************************)
Section term_mapReduce_rewrite.

  Context {A M : Type} (f : A -> M) `{Monoid M}.

  Lemma term_mapReduce1 : forall (a : A),
      mapReduce f (tvar a) = f a.
A, M: Type
f: A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall a : A, mapReduce f (tvar a) = f a
  Proof.
A, M: Type
f: A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall a : A, mapReduce f (tvar a) = f a
    intros.
A, M: Type
f: A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
a: A
mapReduce f (tvar a) = f a
    simplify_LN.
A, M: Type
f: A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
a: A
f a = f a
    conclude.
  Qed.

  Lemma term_mapReduce2 : forall X (t : Lam A),
      mapReduce f (λ X t) = mapReduce f t.
A, M: Type
f: A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (X : typ) (t : Lam A),
mapReduce f ((λ) X t) = mapReduce f t
  Proof.
A, M: Type
f: A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (X : typ) (t : Lam A),
mapReduce f ((λ) X t) = mapReduce f t
    intros.
A, M: Type
f: A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
X: typ
t: Lam A
mapReduce f ((λ) X t) = mapReduce f t
    simplify_LN.
A, M: Type
f: A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
X: typ
t: Lam A
mapReduce f t = mapReduce f t
    conclude.
  Qed.

  Lemma term_mapReduce3 : forall (t1 t2 : Lam A),
      mapReduce f (⟨t1⟩ (t2)) = mapReduce f t1 ● mapReduce f t2.
A, M: Type
f: A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall t1 t2 : Lam A,
mapReduce f (⟨ t1 ⟩ (t2)) =
mapReduce f t1 ● mapReduce f t2
  Proof.
A, M: Type
f: A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall t1 t2 : Lam A,
mapReduce f (⟨ t1 ⟩ (t2)) =
mapReduce f t1 ● mapReduce f t2
    intros.
A, M: Type
f: A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
t1, t2: Lam A
mapReduce f (⟨ t1 ⟩ (t2)) =
mapReduce f t1 ● mapReduce f t2
    simplify_LN.
A, M: Type
f: A -> M
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
t1, t2: Lam A
mapReduce f t1 ● mapReduce f t2 =
mapReduce f t1 ● mapReduce f t2
    conclude.
  Qed.

End term_mapReduce_rewrite.

(** ** Rewriting lemmas for <<tolist>>, <<toset>>, <<∈>> *)
(******************************************************************************)
Section term_container_rewrite.

  Variable
    (A : Type).

  Lemma tolist_tvar_rw1: forall (x: A),
      tolist (tvar x) = [x].
A: Type
forall x : A, tolist (tvar x) = [x]
  Proof.
A: Type
forall x : A, tolist (tvar x) = [x]
    intros.
A: Type
x: A
tolist (tvar x) = [x]
    unfold tolist.
A: Type
x: A
Tolist_Traverse A (tvar x) = [x]
    unfold Tolist_Traverse.
A: Type
x: A
mapReduce one (tvar x) = [x]
    simplify_LN.
A: Type
x: A
one x = [x]
    reflexivity.
  Qed.

  Lemma tolist_term_rw2: forall (X: typ) (t: term),
      tolist (lam X t) = tolist t.
A: Type
forall (X : typ) (t : term),
tolist ((λ) X t) = tolist t
  Proof.
A: Type
forall (X : typ) (t : term),
tolist ((λ) X t) = tolist t
    intros.
A: Type
X: typ
t: term
tolist ((λ) X t) = tolist t
    simplify_LN.
A: Type
X: typ
t: term
tolist t = tolist t
    conclude.
  Qed.

  Lemma tolist_term_rw3: forall (t1 t2: term),
      tolist (app t1 t2) = tolist t1 ++ tolist t2.
A: Type
forall t1 t2 : term,
tolist (⟨ t1 ⟩ (t2)) = tolist t1 ++ tolist t2
  Proof.
A: Type
forall t1 t2 : term,
tolist (⟨ t1 ⟩ (t2)) = tolist t1 ++ tolist t2
    intros.
A: Type
t1, t2: term
tolist (⟨ t1 ⟩ (t2)) = tolist t1 ++ tolist t2
    simplify_LN.
A: Type
t1, t2: term
tolist t1 ++ tolist t2 = tolist t1 ++ tolist t2
    conclude.
  Qed.

  Lemma toset_tvar_rw1: forall (x: A),
      tosubset (tvar x) = {{x}}.
A: Type
forall x : A, tosubset (tvar x) = {{x}}
  Proof.
A: Type
forall x : A, tosubset (tvar x) = {{x}}
    intros.
A: Type
x: A
tosubset (tvar x) = {{x}}
    simplify_LN.
A: Type
x: A
(fun b : A => x = b) = {{x}}
    fixme.
  Qed.

  Lemma toset_term_rw2: forall (X: typ) (t: term),
      tosubset (lam X t) = tosubset t.
A: Type
forall (X : typ) (t : term),
tosubset ((λ) X t) = tosubset t
  Proof.
A: Type
forall (X : typ) (t : term),
tosubset ((λ) X t) = tosubset t
    intros.
A: Type
X: typ
t: term
tosubset ((λ) X t) = tosubset t
    simplify_LN.
A: Type
X: typ
t: term
tosubset t = tosubset t
    conclude.
  Qed.

  Lemma toset_term_rw3: forall (t1 t2: term),
      tosubset (app t1 t2) = tosubset t1 ∪ tosubset t2.
A: Type
forall t1 t2 : term,
tosubset (⟨ t1 ⟩ (t2)) = tosubset t1 ∪ tosubset t2
  Proof.
A: Type
forall t1 t2 : term,
tosubset (⟨ t1 ⟩ (t2)) = tosubset t1 ∪ tosubset t2
    intros.
A: Type
t1, t2: term
tosubset (⟨ t1 ⟩ (t2)) = tosubset t1 ∪ tosubset t2
    simplify_LN.
A: Type
t1, t2: term
tosubset t1 ∪ tosubset t2 = tosubset t1 ∪ tosubset t2
    conclude.
  Qed.

  Lemma in_term_rw1: forall (x y: A),
      x ∈ tvar y = (x = y).
A: Type
forall x y : A, x ∈ tvar y = (x = y)
  Proof.
A: Type
forall x y : A, x ∈ tvar y = (x = y)
    intros.
A: Type
x, y: A
x ∈ tvar y = (x = y)
    simplify_LN.
A: Type
x, y: A
{{x}} y = (x = y)
    simpl_subset.
A: Type
x, y: A
(x = y) = (x = y)
    conclude.
  Qed.

  Lemma in_term_rw2: forall (y: A) (X: typ) (t: Lam A),
      y ∈ (lam X t) = y ∈ t.
A: Type
forall (y : A) (X : typ) (t : Lam A),
y ∈ (λ) X t = y ∈ t
  Proof.
A: Type
forall (y : A) (X : typ) (t : Lam A),
y ∈ (λ) X t = y ∈ t
    intros.
A: Type
y: A
X: typ
t: Lam A
y ∈ (λ) X t = y ∈ t
    simplify_LN.
A: Type
y: A
X: typ
t: Lam A
y ∈ t = y ∈ t
    conclude.
  Qed.

  Lemma in_term_3: forall (t1 t2: Lam A) (y: A),
      y ∈ (app t1 t2) = (y ∈ t1 \/ y ∈ t2).
A: Type
forall (t1 t2 : Lam A) (y : A),
y ∈ (⟨ t1 ⟩ (t2)) = (y ∈ t1 \/ y ∈ t2)
  Proof.
A: Type
forall (t1 t2 : Lam A) (y : A),
y ∈ (⟨ t1 ⟩ (t2)) = (y ∈ t1 \/ y ∈ t2)
    intros.
A: Type
t1, t2: Lam A
y: A
y ∈ (⟨ t1 ⟩ (t2)) = (y ∈ t1 \/ y ∈ t2)
    simplify_LN.
A: Type
t1, t2: Lam A
y: A
(y ∈ t1 \/ y ∈ t2) = (y ∈ t1 \/ y ∈ t2)
    conclude.
  Qed.

End term_container_rewrite.