From Tealeaves Require Export
  Backends.LN
  Simplification.Simplification.

Export DecoratedTraversableMonad.UsefulInstances.

Import LN.Simplification.
Export LN.Notations.

#[local] Generalizable Variables G A B C.
#[local] Set Implicit Arguments.

(** * Language definition *)
(**********************************************************************)
Inductive term (v: Type) :=
| tvar: v -> term v
| abs: term v -> term v
| letin: list (term v) -> term v -> term v
| app: term v -> term v -> term v.

#[export] Instance Return_Lam: Return term := tvar.

Section term_mut_ind1.

  Variables
    (v: Type)
    (P: term v -> Prop).

  Context
    (tvar_case: forall v, P (tvar v))
    (abs_case: forall t: term v, P t -> P (abs t))
    (letin_nil_case:  forall t, P t -> P (letin nil t))
    (letin_cons_case: forall (u: term v) (l: list (term v)) (t: term v)
    (IHu: P u) (IHl: List.Forall P l)
    (IHt: P t), P (letin (u :: l) t))
    (app_case: forall t: term v, P t -> forall u: term v, P u -> P (app t u)).

  Definition term_mut_ind: forall t, P t :=
    fix F t :=
      match t with
      | tvar v => tvar_case v
      | abs body => @abs_case body (F body)
      | letin defs body =>
          match defs with
          | nil => @letin_nil_case body (F body)
          | cons u rest =>
              @letin_cons_case u rest body
                (F u)
                ((fix G l: List.Forall P l
                  := match l with
                     | nil =>
                         List.Forall_nil P
                     | cons x xs =>
                         List.Forall_cons x (l := xs) (F x) (G xs)
                     end) rest)
                (F body)
          end
      | app t1 t2 =>
          @app_case t1 (F t1) t2 (F t2)
      end.

End term_mut_ind1.

Lemma Forall_compat_list: forall (A: Type) (l: list A) (P: A -> Prop),
    List.Forall P l <-> Forall_List P l.
forall (A : Type) (l : list A) (P : A -> Prop),
List.Forall P l <-> Forall_List P l
Proof.
forall (A : Type) (l : list A) (P : A -> Prop),
List.Forall P l <-> Forall_List P l
  intros.
A: Type
l: list A
P: A -> Prop
List.Forall P l <-> Forall_List P l
  induction l.
A: Type
P: A -> Prop
List.Forall P [] <-> Forall_List P []
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
List.Forall P (a :: l) <-> Forall_List P (a :: l)
  -
A: Type
P: A -> Prop
List.Forall P [] <-> Forall_List P [] split.
A: Type
P: A -> Prop
List.Forall P [] -> Forall_List P []
A: Type
P: A -> Prop
Forall_List P [] -> List.Forall P []
    +
A: Type
P: A -> Prop
List.Forall P [] -> Forall_List P [] intros _.
A: Type
P: A -> Prop
Forall_List P [] exact I.
    +
A: Type
P: A -> Prop
Forall_List P [] -> List.Forall P [] intros.
A: Type
P: A -> Prop
H: Forall_List P []
List.Forall P [] apply List.Forall_nil.
  -
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
List.Forall P (a :: l) <-> Forall_List P (a :: l) split.
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
List.Forall P (a :: l) -> Forall_List P (a :: l)
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
Forall_List P (a :: l) -> List.Forall P (a :: l)
    +
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
List.Forall P (a :: l) -> Forall_List P (a :: l) intro H.
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
H: List.Forall P (a :: l)
Forall_List P (a :: l)
      inversion H; subst.
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
H: List.Forall P (a :: l)
H2: P a
H3: List.Forall P l
Forall_List P (a :: l)
      cbn.
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
H: List.Forall P (a :: l)
H2: P a
H3: List.Forall P l
P a ● crush_list (map P l) split.
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
H: List.Forall P (a :: l)
H2: P a
H3: List.Forall P l
P a
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
H: List.Forall P (a :: l)
H2: P a
H3: List.Forall P l
crush_list (map P l) assumption.
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
H: List.Forall P (a :: l)
H2: P a
H3: List.Forall P l
crush_list (map P l) now apply IHl.
    +
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
Forall_List P (a :: l) -> List.Forall P (a :: l) intro H.
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
H: Forall_List P (a :: l)
List.Forall P (a :: l)
      inversion H.
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
H: Forall_List P (a :: l)
H0: P a
H1: crush_list (Map_list A Prop P l)
List.Forall P (a :: l)
      apply List.Forall_cons.
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
H: Forall_List P (a :: l)
H0: P a
H1: crush_list (Map_list A Prop P l)
P a
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
H: Forall_List P (a :: l)
H0: P a
H1: crush_list (Map_list A Prop P l)
List.Forall P l assumption.
A: Type
a: A
l: list A
P: A -> Prop
IHl: List.Forall P l <-> Forall_List P l
H: Forall_List P (a :: l)
H0: P a
H1: crush_list (Map_list A Prop P l)
List.Forall P l now apply IHl.
Qed.

Section term_mut_ind2.

  Variables
    (v: Type)
    (P: term v -> Prop).

  Hypotheses
    (tvar_case: forall v, P (tvar v))
    (abs_case: forall t: term v, P t -> P (abs t))
    (letin_case: forall (defs: list (term v))
                      (body: term v)
                      (IHdefs: forall (t: term v), t ∈ defs -> P t)
                      (IHbody: P body),
          P (letin defs body))
    (app_case: forall t: term v, P t -> forall u: term v, P u -> P (app t u)).

  Definition term_mut_ind2: forall t, P t.
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
forall t : term v, P t
  Proof.
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
forall t : term v, P t
    intros.
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t: term v
P t
    induction t using term_mut_ind.
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
v0: v
P (tvar v0)
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t: term v
IHt: P t
P (abs t)
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t: term v
IHt: P t
P (letin [] t)
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1: term v
l: list (term v)
t2: term v
IHl: List.Forall (fun t : term v => P t) l
IHt1: P t1
IHt2: P t2
P (letin (t1 :: l) t2)
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1, t2: term v
IHt1: P t1
IHt2: P t2
P (app t1 t2)
    -
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
v0: v
P (tvar v0) auto.
    -
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t: term v
IHt: P t
P (abs t) auto.
    -
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t: term v
IHt: P t
P (letin [] t) apply letin_case.
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t: term v
IHt: P t
forall t : term v, t ∈ [] -> P t
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t: term v
IHt: P t
P t
      +
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t: term v
IHt: P t
forall t : term v, t ∈ [] -> P t inversion 1.
      +
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t: term v
IHt: P t
P t assumption.
    -
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1: term v
l: list (term v)
t2: term v
IHl: List.Forall (fun t : term v => P t) l
IHt1: P t1
IHt2: P t2
P (letin (t1 :: l) t2) apply letin_case.
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1: term v
l: list (term v)
t2: term v
IHl: List.Forall (fun t : term v => P t) l
IHt1: P t1
IHt2: P t2
forall t : term v, t ∈ (t1 :: l) -> P t
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1: term v
l: list (term v)
t2: term v
IHl: List.Forall (fun t : term v => P t) l
IHt1: P t1
IHt2: P t2
P t2
      +
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1: term v
l: list (term v)
t2: term v
IHl: List.Forall (fun t : term v => P t) l
IHt1: P t1
IHt2: P t2
forall t : term v, t ∈ (t1 :: l) -> P t introv Hin.
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1: term v
l: list (term v)
t2: term v
IHl: List.Forall (fun t : term v => P t) l
IHt1: P t1
IHt2: P t2
t: term v
Hin: t ∈ (t1 :: l)
P t
        autorewrite with tea_list in Hin.
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1: term v
l: list (term v)
t2: term v
IHl: List.Forall (fun t : term v => P t) l
IHt1: P t1
IHt2: P t2
t: term v
Hin: t = t1 \/ t ∈ l
P t
        inversion Hin.
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1: term v
l: list (term v)
t2: term v
IHl: List.Forall (fun t : term v => P t) l
IHt1: P t1
IHt2: P t2
t: term v
Hin: t = t1 \/ t ∈ l
H: t = t1
P t
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1: term v
l: list (term v)
t2: term v
IHl: List.Forall (fun t : term v => P t) l
IHt1: P t1
IHt2: P t2
t: term v
Hin: t = t1 \/ t ∈ l
H: t ∈ l
P t
        *
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1: term v
l: list (term v)
t2: term v
IHl: List.Forall (fun t : term v => P t) l
IHt1: P t1
IHt2: P t2
t: term v
Hin: t = t1 \/ t ∈ l
H: t = t1
P t now subst.
        *
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1: term v
l: list (term v)
t2: term v
IHl: List.Forall (fun t : term v => P t) l
IHt1: P t1
IHt2: P t2
t: term v
Hin: t = t1 \/ t ∈ l
H: t ∈ l
P t rewrite Forall_compat_list in IHl.
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1: term v
l: list (term v)
t2: term v
IHl: Forall_List (fun t : term v => P t) l
IHt1: P t1
IHt2: P t2
t: term v
Hin: t = t1 \/ t ∈ l
H: t ∈ l
P t
          rewrite List.forall_iff in IHl.
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1: term v
l: list (term v)
t2: term v
IHl: forall a : term v, a ∈ l -> P a
IHt1: P t1
IHt2: P t2
t: term v
Hin: t = t1 \/ t ∈ l
H: t ∈ l
P t
          now apply IHl.
      +
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1: term v
l: list (term v)
t2: term v
IHl: List.Forall (fun t : term v => P t) l
IHt1: P t1
IHt2: P t2
P t2 assumption.
    -
v: Type
P: term v -> Prop
tvar_case: forall v0 : v, P (tvar v0)
abs_case: forall t : term v, P t -> P (abs t)
letin_case: forall (defs : list (term v))
  (body : term v),
(forall t : term v, t ∈ defs -> P t) ->
P body -> P (letin defs body)
app_case: forall t : term v,
P t ->
forall u : term v, P u -> P (app t u)
t1, t2: term v
IHt1: P t1
IHt2: P t2
P (app t1 t2) auto.
  Qed.

End term_mut_ind2.

#[global] Ltac derive_dtm_custom_IH ::=
  constr:(term_mut_ind2).