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

Import STLC.Syntax.TermNotations.

(** ** Rewriting lemmas for <<LC>> *)
(******************************************************************************)
Theorem term_lcn11 : forall (n : nat) (m : nat),
    LCn m (tvar (Bd n)) <-> n < m.
forall n m : nat, LCn m (tvar n) <-> n < m
Proof.
forall n m : nat, LCn m (tvar n) <-> n < m
  intros.
n, m: nat
LCn m (tvar n) <-> n < m simplify_LN.
n, m: nat
n < m <-> n < m reflexivity.
Qed.

Theorem term_lcn12 : forall (x : atom) (m : nat),
    LCn m (tvar (Fr x)) <-> True.
forall (x : atom) (m : nat), LCn m (tvar x) <-> True
Proof.
forall (x : atom) (m : nat), LCn m (tvar x) <-> True
  intros.
x: atom
m: nat
LCn m (tvar x) <-> True simplify_LN.
x: atom
m: nat
True <-> True reflexivity.
Qed.

Theorem term_lcn2 : forall (X : typ) (t : term) (m : nat),
    LCn m (lam X t) <-> LCn (S m) t.
forall (X : typ) (t : term) (m : nat),
LCn m ((λ) X t) <-> LCn (S m) t
Proof.
forall (X : typ) (t : term) (m : nat),
LCn m ((λ) X t) <-> LCn (S m) t
  intros.
X: typ
t: term
m: nat
LCn m ((λ) X t) <-> LCn (S m) t simplify_LN.
X: typ
t: term
m: nat
LCn (S m) t <-> LCn (S m) t reflexivity.
Qed.

Theorem term_lcn3 : forall (t1 t2 : term) (m : nat),
    LCn m (⟨t1⟩(t2)) <->
      LCn m t1 /\ LCn m t2.
forall (t1 t2 : term) (m : nat),
LCn m (⟨ t1 ⟩ (t2)) <-> LCn m t1 /\ LCn m t2
Proof.
forall (t1 t2 : term) (m : nat),
LCn m (⟨ t1 ⟩ (t2)) <-> LCn m t1 /\ LCn m t2
  intros.
t1, t2: term
m: nat
LCn m (⟨ t1 ⟩ (t2)) <-> LCn m t1 /\ LCn m t2 simplify_LN.
t1, t2: term
m: nat
LCn m t1 ● LCn m t2 <-> LCn m t1 /\ LCn m t2 reflexivity.
Qed.

Theorem term_lc11 : forall (n : nat),
    LC (tvar (Bd n)) <-> False.
forall n : nat, LC (tvar n) <-> False
Proof.
forall n : nat, LC (tvar n) <-> False
  intros.
n: nat
LC (tvar n) <-> False simplify_LN.
n: nat
False <-> False lia.
Qed.

Theorem term_lc12 : forall (x : atom),
    LC (tvar (Fr x)) <-> True.
forall x : atom, LC (tvar x) <-> True
Proof.
forall x : atom, LC (tvar x) <-> True
  intros.
x: atom
LC (tvar x) <-> True simplify_LN.
x: atom
True <-> True reflexivity.
Qed.

Theorem term_lc2 : forall (X : typ) (t : term),
    LC (lam X t) <-> LCn 1 t.
forall (X : typ) (t : term), LC ((λ) X t) <-> LCn 1 t
Proof.
forall (X : typ) (t : term), LC ((λ) X t) <-> LCn 1 t
  intros.
X: typ
t: term
LC ((λ) X t) <-> LCn 1 t simplify_LN.
X: typ
t: term
LCn 1 t <-> LCn 1 t reflexivity.
Qed.

Theorem term_lc3 : forall (t1 t2 : term),
    LC (⟨t1⟩ (t2)) <-> LC t1 /\ LC t2.
forall t1 t2 : term,
LC (⟨ t1 ⟩ (t2)) <-> LC t1 /\ LC t2
Proof.
forall t1 t2 : term,
LC (⟨ t1 ⟩ (t2)) <-> LC t1 /\ LC t2
  intros.
t1, t2: term
LC (⟨ t1 ⟩ (t2)) <-> LC t1 /\ LC t2 simplify_LN.
t1, t2: term
LC t1 ● LC t2 <-> LC t1 /\ LC t2 reflexivity.
Qed.

(** ** Rewriting lemmas for <<free>>, <<freeset>> *)
(******************************************************************************)
Section term_free_rewrite.

  Definition term_free11 : forall (b : nat),
      free (tvar (Bd b)) = [].
forall b : nat, free (tvar b) = []
  Proof.
forall b : nat, free (tvar b) = []
    intros.
b: nat
free (tvar b) = [] simplify_LN.
b: nat
[] = [] reflexivity.
  Qed.

  Definition term_in_free11 : forall (b : nat) (x : atom),
      x ∈ free (tvar (Bd b)) <-> False.
forall (b : nat) (x : atom),
x ∈ free (tvar b) <-> False
  Proof.
forall (b : nat) (x : atom),
x ∈ free (tvar b) <-> False
    intros.
b: nat
x: atom
x ∈ free (tvar b) <-> False simplify_LN.
b: nat
x: atom
x ∈ [] <-> False reflexivity.
  Qed.

  Definition term_free12 : forall (y : atom),
      free (tvar (Fr y)) = [y].
forall y : atom, free (tvar y) = [y]
  Proof.
forall y : atom, free (tvar y) = [y]
    intros.
y: atom
free (tvar y) = [y] simplify_LN.
y: atom
[y] = [y] reflexivity.
  Qed.

  Definition term_in_free12 : forall (y : atom) (x : atom),
      x ∈ free (tvar (Fr y)) <-> x = y.
forall y x : atom, x ∈ free (tvar y) <-> x = y
  Proof.
forall y x : atom, x ∈ free (tvar y) <-> x = y
    intros.
y, x: atom
x ∈ free (tvar y) <-> x = y simplify_LN.
y, x: atom
x = y <-> x = y reflexivity.
  Qed.

  Definition term_free2 : forall (t : term) (X : typ),
      free (lam X t) = free t.
forall (t : term) (X : typ), free ((λ) X t) = free t
  Proof.
forall (t : term) (X : typ), free ((λ) X t) = free t
    intros.
t: term
X: typ
free ((λ) X t) = free t simplify_LN.
t: term
X: typ
free t = free t reflexivity.
  Qed.

  Definition term_in_free2 : forall (x : atom) (t : term) (X : typ),
      x ∈ free (lam X t) <-> x ∈ free t.
forall (x : atom) (t : term) (X : typ),
x ∈ free ((λ) X t) <-> x ∈ free t
  Proof.
forall (x : atom) (t : term) (X : typ),
x ∈ free ((λ) X t) <-> x ∈ free t
    intros.
x: atom
t: term
X: typ
x ∈ free ((λ) X t) <-> x ∈ free t simplify_LN.
x: atom
t: term
X: typ
x ∈ free t <-> x ∈ free t reflexivity.
  Qed.

  Definition term_free3 : forall (x : atom) (t1 t2 : term),
      free (app t1 t2) = free t1 ++ free t2.
atom ->
forall t1 t2 : term,
free (⟨ t1 ⟩ (t2)) = free t1 ++ free t2
  Proof.
atom ->
forall t1 t2 : term,
free (⟨ t1 ⟩ (t2)) = free t1 ++ free t2
    intros.
x: atom
t1, t2: term
free (⟨ t1 ⟩ (t2)) = free t1 ++ free t2 simplify_LN.
x: atom
t1, t2: term
free t1 ++ free t2 = free t1 ++ free t2 reflexivity.
  Qed.

  Definition term_in_free3 : forall (x : atom) (t1 t2 : term),
      x ∈ free (app t1 t2) <-> x ∈ free t1 \/ x ∈ free t2.
forall (x : atom) (t1 t2 : term),
x ∈ free (⟨ t1 ⟩ (t2)) <-> x ∈ free t1 \/ x ∈ free t2
  Proof.
forall (x : atom) (t1 t2 : term),
x ∈ free (⟨ t1 ⟩ (t2)) <-> x ∈ free t1 \/ x ∈ free t2
    intros.
x: atom
t1, t2: term
x ∈ free (⟨ t1 ⟩ (t2)) <-> x ∈ free t1 \/ x ∈ free t2 simplify_LN.
x: atom
t1, t2: term
x ∈ free t1 \/ x ∈ free t2 <->
x ∈ free t1 \/ x ∈ free t2 reflexivity.
  Qed.

  Definition term_in_FV11 : forall (b : nat) (x : atom),
      x `in` FV (tvar (Bd b)) <-> False.
forall (b : nat) (x : atom),
x `in` FV (tvar b) <-> False
  Proof.
forall (b : nat) (x : atom),
x `in` FV (tvar b) <-> False
    intros.
b: nat
x: atom
x `in` FV (tvar b) <-> False simplify_FV.
b: nat
x: atom
False <-> False reflexivity.
  Qed.

  Definition term_in_FV12 : forall (y : atom) (x : atom),
      AtomSet.In x (FV (tvar (Fr y))) <-> x = y.
forall y x : atom, x `in` FV (tvar y) <-> x = y
  Proof.
forall y x : atom, x `in` FV (tvar y) <-> x = y
    intros.
y, x: atom
x `in` FV (tvar y) <-> x = y simplify_FV.
y, x: atom
x = y <-> x = y reflexivity.
  Qed.

  Lemma term_in_FV2 : forall (x : atom) (t : term) (X : typ),
      AtomSet.In x (FV (lam X t)) <-> AtomSet.In x (FV t).
forall (x : atom) (t : term) (X : typ),
x `in` FV ((λ) X t) <-> x `in` FV t
  Proof.
forall (x : atom) (t : term) (X : typ),
x `in` FV ((λ) X t) <-> x `in` FV t
    intros.
x: atom
t: term
X: typ
x `in` FV ((λ) X t) <-> x `in` FV t simplify_FV.
x: atom
t: term
X: typ
x `in` FV t <-> x `in` FV t reflexivity.
  Qed.

  Lemma term_in_FV3 : forall (x : atom) (t1 t2 : term),
      AtomSet.In x (FV (app t1 t2)) <->
        AtomSet.In x (FV t1) \/ AtomSet.In x (FV t2).
forall (x : atom) (t1 t2 : term),
x `in` FV (⟨ t1 ⟩ (t2)) <->
x `in` FV t1 \/ x `in` FV t2
  Proof.
forall (x : atom) (t1 t2 : term),
x `in` FV (⟨ t1 ⟩ (t2)) <->
x `in` FV t1 \/ x `in` FV t2
    intros.
x: atom
t1, t2: term
x `in` FV (⟨ t1 ⟩ (t2)) <->
x `in` FV t1 \/ x `in` FV t2 simplify_FV.
x: atom
t1, t2: term
x `in` FV t1 \/ x `in` FV t2 <->
x `in` FV t1 \/ x `in` FV t2 reflexivity.
  Qed.

  Open Scope set_scope.

  Lemma term_FV11 : forall (b : nat) (x : atom),
      FV (tvar (Bd b)) [=] ∅.
forall b : nat, atom -> FV (tvar b) [=] ∅
  Proof.
forall b : nat, atom -> FV (tvar b) [=] ∅
    intros.
b: nat
x: atom
FV (tvar b) [=] ∅ simplify_FV.
b: nat
x: atom
∅ [=] ∅ fsetdec.
  Qed.

  Lemma term_FV12 : forall (y : atom),
      FV (tvar (Fr y)) [=] {{ y }}.
forall y : atom, FV (tvar y) [=] {{y}}
  Proof.
forall y : atom, FV (tvar y) [=] {{y}}
    intros.
y: atom
FV (tvar y) [=] {{y}} simplify_FV.
y: atom
{{y}} [=] {{y}} fsetdec.
  Qed.

  Lemma term_FV2 : forall (t : term) (X : typ),
      FV (lam X t) [=] FV t.
forall (t : term) (X : typ), FV ((λ) X t) [=] FV t
  Proof.
forall (t : term) (X : typ), FV ((λ) X t) [=] FV t
    intros.
t: term
X: typ
FV ((λ) X t) [=] FV t simplify_FV.
t: term
X: typ
FV t [=] FV t fsetdec.
  Qed.

  Lemma term_FV3 : forall (t1 t2 : term),
      FV (app t1 t2) [=] FV t1 ∪ FV t2.
forall t1 t2 : term,
FV (⟨ t1 ⟩ (t2)) [=] FV t1 ∪ FV t2
  Proof.
forall t1 t2 : term,
FV (⟨ t1 ⟩ (t2)) [=] FV t1 ∪ FV t2
    intros.
t1, t2: term
FV (⟨ t1 ⟩ (t2)) [=] FV t1 ∪ FV t2 simplify_FV.
t1, t2: term
FV t1 ∪ FV t2 [=] FV t1 ∪ FV t2 fsetdec.
  Qed.

End term_free_rewrite.


(** ** Rewriting lemmas for <<open>> *)
(******************************************************************************)
Lemma open_term_rw1: forall (v: LN) (u: term),
    open u (tvar v) = open_loc u (0, v).
forall (v : LN) (u : term),
open u (tvar v) = open_loc u (0, v)
Proof.
forall (v : LN) (u : term),
open u (tvar v) = open_loc u (0, v)
  intros.
v: LN
u: term
open u (tvar v) = open_loc u (0, v) simplify_open.
v: LN
u: term
open_loc u (Ƶ, v) = open_loc u (0, v) reflexivity.
Qed.

Lemma open_term_rw2: forall (t1 t2: term) u,
    open u (app t1 t2) = app (open u t1) (open u t2).
forall t1 t2 u : term,
open u (⟨ t1 ⟩ (t2)) = (⟨ open u t1 ⟩ (open u t2))
Proof.
forall t1 t2 u : term,
open u (⟨ t1 ⟩ (t2)) = (⟨ open u t1 ⟩ (open u t2))
  intros.
t1, t2, u: term
open u (⟨ t1 ⟩ (t2)) = (⟨ open u t1 ⟩ (open u t2)) simplify_open.
t1, t2, u: term
(⟨ open u t1 ⟩ (open u t2)) =
(⟨ open u t1 ⟩ (open u t2)) reflexivity.
Qed.

Lemma open_term_rw3: forall τ (t: term) u,
    open u (λ τ t) = λ τ (bindd (open_loc u ⦿ 1) t).
forall (τ : typ) (t u : term),
open u ((λ) τ t) = (λ) τ (bindd (open_loc u ⦿ 1) t)
Proof.
forall (τ : typ) (t u : term),
open u ((λ) τ t) = (λ) τ (bindd (open_loc u ⦿ 1) t)
  intros.
τ: typ
t, u: term
open u ((λ) τ t) = (λ) τ (bindd (open_loc u ⦿ 1) t) simplify_open.
τ: typ
t, u: term
(λ) τ (bindd (open_loc u ⦿ 1) t) =
(λ) τ (bindd (open_loc u ⦿ 1) t) reflexivity.
Qed.

(** ** Rewriting lemmas for <<subst>> *)
(******************************************************************************)
Lemma subst_term_rw1: forall (v: LN) x u,
    subst x u (tvar v) = subst_loc x u v.
forall (v : LN) (x : atom) (u : term),
subst x u (tvar v) = subst_loc x u v
Proof.
forall (v : LN) (x : atom) (u : term),
subst x u (tvar v) = subst_loc x u v
  intros.
v: LN
x: atom
u: term
subst x u (tvar v) = subst_loc x u v
  simplify_subst.
v: LN
x: atom
u: term
subst_loc x u v = subst_loc x u v
  conclude.
Qed.

Lemma subst_term_rw2: forall (t1 t2: term) x u,
    subst x u (app t1 t2) =
      app (subst x u t1) (subst x u t2).
forall (t1 t2 : term) (x : atom) (u : term),
subst x u (⟨ t1 ⟩ (t2)) =
(⟨ subst x u t1 ⟩ (subst x u t2))
Proof.
forall (t1 t2 : term) (x : atom) (u : term),
subst x u (⟨ t1 ⟩ (t2)) =
(⟨ subst x u t1 ⟩ (subst x u t2))
  intros.
t1, t2: term
x: atom
u: term
subst x u (⟨ t1 ⟩ (t2)) =
(⟨ subst x u t1 ⟩ (subst x u t2))
  simplify_subst.
t1, t2: term
x: atom
u: term
(⟨ subst x u t1 ⟩ (subst x u t2)) =
(⟨ subst x u t1 ⟩ (subst x u t2))
  conclude.
Qed.

Lemma subst_term_rw3: forall τ (t: term) x u,
    subst x u (λ τ t) =
      λ τ (subst x u t).
forall (τ : typ) (t : term) (x : atom) (u : term),
subst x u ((λ) τ t) = (λ) τ (subst x u t)
Proof.
forall (τ : typ) (t : term) (x : atom) (u : term),
subst x u ((λ) τ t) = (λ) τ (subst x u t)
  intros.
τ: typ
t: term
x: atom
u: term
subst x u ((λ) τ t) = (λ) τ (subst x u t)
  simplify_subst.
τ: typ
t: term
x: atom
u: term
(λ) τ (subst x u t) = (λ) τ (subst x u t)
  conclude.
Qed.

Goal forall (v: LN) x u,
    v = Fr x ->
    subst x u (tvar v) = u.
forall (v : LN) (x : atom) (u : term),
v = x -> subst x u (tvar v) = u
Proof.
forall (v : LN) (x : atom) (u : term),
v = x -> subst x u (tvar v) = u
  intros.
v: LN
x: atom
u: term
H: v = x
subst x u (tvar v) = u
  simplify_subst.
v: LN
x: atom
u: term
H: v = x
u = u
  conclude.
Qed.

Goal forall (v: LN) x u,
    v <> Fr x ->
    subst x u (tvar v) = tvar v.
forall (v : LN) (x : atom) (u : term),
v <> x -> subst x u (tvar v) = tvar v
Proof.
forall (v : LN) (x : atom) (u : term),
v <> x -> subst x u (tvar v) = tvar v
  intros.
v: LN
x: atom
u: term
H: v <> x
subst x u (tvar v) = tvar v
  simplify_subst.
v: LN
x: atom
u: term
H: v <> x
ret v = ret v
  conclude.
Qed.

Goal forall y x u,
    x = y ->
    subst x u (tvar (Fr y)) = u.
forall (y x : atom) (u : term),
x = y -> subst x u (tvar y) = u
Proof.
forall (y x : atom) (u : term),
x = y -> subst x u (tvar y) = u
  intros.
y, x: atom
u: term
H: x = y
subst x u (tvar y) = u
  simplify_subst.
y, x: atom
u: term
H: x = y
u = u
  conclude.
Qed.

Goal forall y x u,
    x <> y ->
    subst x u (tvar (Fr y)) = tvar (Fr y).
forall (y x : atom) (u : term),
x <> y -> subst x u (tvar y) = tvar y
Proof.
forall (y x : atom) (u : term),
x <> y -> subst x u (tvar y) = tvar y
  intros.
y, x: atom
u: term
H: x <> y
subst x u (tvar y) = tvar y
  simplify_subst.
y, x: atom
u: term
H: x <> y
ret y = ret y
  conclude.
Qed.

Goal forall v y x u,
    y <> x ->
    v = x ->
    subst x u (app (ret (Fr v)) (ret (Fr y))) = app u (ret (Fr v)).
forall (v y x : atom) (u : term),
y <> x ->
v = x ->
subst x u (⟨ ret v ⟩ (ret y)) = (⟨ u ⟩ (ret v))
Proof.
forall (v y x : atom) (u : term),
y <> x ->
v = x ->
subst x u (⟨ ret v ⟩ (ret y)) = (⟨ u ⟩ (ret v))
  intros.
v, y, x: atom
u: term
H: y <> x
H0: v = x
subst x u (⟨ ret v ⟩ (ret y)) = (⟨ u ⟩ (ret v))
  rewrite subst_to_bind.
v, y, x: atom
u: term
H: y <> x
H0: v = x
bind (subst_loc x u) (⟨ ret v ⟩ (ret y)) =
(⟨ u ⟩ (ret v))
  rewrite bind_to_bindd.
v, y, x: atom
u: term
H: y <> x
H0: v = x
bindd (subst_loc x u ∘ extract) (⟨ ret v ⟩ (ret y)) =
(⟨ u ⟩ (ret v))
  rewrite bindd_to_binddt.
v, y, x: atom
u: term
H: y <> x
H0: v = x
binddt (subst_loc x u ∘ extract) (⟨ ret v ⟩ (ret y)) =
(⟨ u ⟩ (ret v))
  cbn [binddt Binddt_STLC binddt_Lam].
v, y, x: atom
u: term
H: y <> x
H0: v = x
pure (app (V:=LN)) <⋆>
binddt (subst_loc x u ∘ extract) (ret v) <⋆>
binddt (subst_loc x u ∘ extract) (ret y) =
(⟨ u ⟩ (ret v))
  cbn [binddt Binddt_STLC binddt_Lam].
v, y, x: atom
u: term
H: y <> x
H0: v = x
pure (app (V:=LN)) <⋆>
binddt (subst_loc x u ∘ extract) (ret v) <⋆>
binddt (subst_loc x u ∘ extract) (ret y) =
(⟨ u ⟩ (ret v))
  cbn [binddt Binddt_STLC binddt_Lam ret Return_STLC].
v, y, x: atom
u: term
H: y <> x
H0: v = x
pure (app (V:=LN)) <⋆>
(subst_loc x u ∘ extract) (0, v) <⋆>
(subst_loc x u ∘ extract) (0, y) = (⟨ u ⟩ (ret v))
Abort.

Goal forall v y x u,
    y <> Fr x ->
    v = Fr x ->
    subst x u (app (tvar v) (tvar y)) = u.
forall (v y : LN) (x : atom) (u : term),
y <> x -> v = x -> subst x u (⟨ tvar v ⟩ (tvar y)) = u
Proof.
forall (v y : LN) (x : atom) (u : term),
y <> x -> v = x -> subst x u (⟨ tvar v ⟩ (tvar y)) = u
  intros.
v, y: LN
x: atom
u: term
H: y <> x
H0: v = x
subst x u (⟨ tvar v ⟩ (tvar y)) = u
  rewrite subst_to_bind.
v, y: LN
x: atom
u: term
H: y <> x
H0: v = x
bind (subst_loc x u) (⟨ tvar v ⟩ (tvar y)) = u
  rewrite bind_to_bindd.
v, y: LN
x: atom
u: term
H: y <> x
H0: v = x
bindd (subst_loc x u ∘ extract) (⟨ tvar v ⟩ (tvar y)) =
u
  rewrite bindd_to_binddt.
v, y: LN
x: atom
u: term
H: y <> x
H0: v = x
binddt (subst_loc x u ∘ extract) (⟨ tvar v ⟩ (tvar y)) =
u
  cbn [binddt Binddt_STLC binddt_Lam].
v, y: LN
x: atom
u: term
H: y <> x
H0: v = x
pure (app (V:=LN)) <⋆>
(subst_loc x u ∘ extract) (0, v) <⋆>
(subst_loc x u ∘ extract) (0, y) = u
Abort.