Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Program.Equality.

Require Export Metalib.Metatheory.
Require Export Metalib.LibLNgen.

Require Export Definitions.

(* *********************************************************************** *)

Scheme term_ind' := Induction for term Sort Prop.

Definition term_mutind :=
  fun H1 H2 H3 H4 H5 ⇒
  term_ind' H1 H2 H3 H4 H5.

Scheme term_rec' := Induction for term Sort Type.

Definition term_mutrec :=
  fun H1 H2 H3 H4 H5 ⇒
  term_rec' H1 H2 H3 H4 H5.

(* *********************************************************************** *)

Fixpoint close_rec (n : nat) (x : atom) (t : term) : term :=
  match t with
  | BVar m ⇒ if lt_ge_dec m n then BVar m else BVar (S m)
  | Var y ⇒ if (x == y) then BVar n else Var y
  | Let t1 t2 ⇒ Let (close_rec n x t1) (close_rec (S n) x t2)
  | Lam t ⇒ Lam (close_rec (S n) x t)
  | App t1 t2 ⇒ App (close_rec n x t1) (close_rec n x t2)
  | Unit ⇒ Unit
  | Pair t1 t2 ⇒ Pair (close_rec n x t1) (close_rec n x t2)
  | Fst t ⇒ Fst (close_rec n x t)
  | Snd t ⇒ Snd (close_rec n x t)
  | InjL t ⇒ InjL (close_rec n x t)
  | InjR t ⇒ InjR (close_rec n x t)
  | Match t t1 t2 ⇒ Match (close_rec n x t) (close_rec (S n) x t1) (close_rec (S n) x t2)
  end.

Definition close x t := close_rec 0 x t.

(* *********************************************************************** *)

Fixpoint size (t : term) : nat :=
  match t with
  | BVar _ ⇒ 1
  | Var _ ⇒ 1
  | Let t1 t2 ⇒ 1 + size t1 + size t2
  | Lam t ⇒ 1 + size t
  | Unit ⇒ 1
  | App t1 t2 ⇒ 1 + size t1 + size t2
  | Pair t1 t2 ⇒ 1 + size t1 + size t2
  | Fst t ⇒ 1 + size t
  | Snd t ⇒ 1 + size t
  | InjL t ⇒ 1 + size t
  | InjR t ⇒ 1 + size t
  | Match t t1 t2 ⇒ 1 + size t + size t1 + size t2
  end.

(* *********************************************************************** *)

Inductive degree : nat → term → Prop :=
| degree_Var : ∀ n x,
    degree n (Var x)
| degree_BVar : ∀ n1 n2,
    lt n2 n1 →
    degree n1 (BVar n2)
| degree_Let : ∀ n t1 t2,
    degree n t1 →
    degree (S n) t2 →
    degree n (Let t1 t2)
| degree_Lam : ∀ n t,
    degree (S n) t →
    degree n (Lam t)
| degree_App : ∀ n t1 t2,
    degree n t1 →
    degree n t2 →
    degree n (App t1 t2)
| degree_Unit : ∀ n,
    degree n Unit
| degree_Pair : ∀ n t1 t2,
    degree n t1 →
    degree n t2 →
    degree n (Pair t1 t2)
| degree_Fst : ∀ n t,
    degree n t →
    degree n (Fst t)
| degree_Snd : ∀ n t,
    degree n t →
    degree n (Snd t)
| degree_InjL : ∀ n t,
    degree n t →
    degree n (InjL t)
| degree_InjR : ∀ n t,
    degree n t →
    degree n (InjR t)
| degree_Match : ∀ n t t1 t2,
    degree n t →
    degree (S n) t1 →
    degree (S n) t2 →
    degree n (Match t t1 t2)
.

Scheme degree_ind' := Induction for degree Sort Prop.

Definition degree_mutind :=
  fun H1 H2 H3 H4 H5 ⇒
  degree_ind' H1 H2 H3 H4 H5.

Hint Constructors degree : core lngen.

(* *********************************************************************** *)

Inductive lc_set : term → Type :=
| lc_set_Var : ∀ x,
    lc_set (Var x)
| lc_set_Let : ∀ t1 t2,
    lc_set t1 →
    (∀ x : atom, lc_set (open t2 (Var x))) →
    lc_set (Let t1 t2)
| lc_set_Lam : ∀ t,
    (∀ x : atom, lc_set (open t (Var x))) →
    lc_set (Lam t)
| lc_set_App : ∀ t1 t2,
    lc_set t1 →
    lc_set t2 →
    lc_set (App t1 t2)
| lc_set_Unit :
    lc_set Unit
| lc_set_Pair : ∀ t1 t2,
    lc_set t1 →
    lc_set t2 →
    lc_set (Pair t1 t2)
| lc_set_Fst : ∀ t,
    lc_set t →
    lc_set (Fst t)
| lc_set_Snd : ∀ t,
    lc_set t →
    lc_set (Snd t)
| lc_set_InjL : ∀ t,
    lc_set t →
    lc_set (InjL t)
| lc_set_InjR : ∀ t,
    lc_set t →
    lc_set (InjR t)
| lc_set_Match : ∀ t t1 t2,
    lc_set t →
    (∀ x : atom, lc_set (open t1 (Var x))) →
    (∀ x : atom, lc_set (open t2 (Var x))) →
    lc_set (Match t t1 t2)
.

Scheme lc_ind' := Induction for lc Sort Prop.

Definition lc_mutind :=
  fun H1 H2 H3 H4 ⇒
  lc_ind' H1 H2 H3 H4.

Scheme lc_set_ind' := Induction for lc_set Sort Prop.

Definition lc_set_mutind :=
  fun H1 H2 H3 H4 ⇒
  lc_set_ind' H1 H2 H3 H4.

Scheme lc_set_rec' := Induction for lc_set Sort Type.

Definition lc_set_mutrec :=
  fun H1 H2 H3 H4 ⇒
  lc_set_rec' H1 H2 H3 H4.

Hint Constructors lc : core lngen.

Hint Constructors lc_set : core lngen.

(* *********************************************************************** *)

Definition body t := ∀ x, lc (open t (Var x)).

Hint Unfold body : lngen.

(* *********************************************************************** *)

Hint Resolve @plus_le_compat : lngen.

Ltac default_case_split ::=
  first
    [ progress destruct_notin
    | progress destruct_sum
    | progress safe_f_equal
    ].

(* *********************************************************************** *)

Ltac default_auto ::= auto with arith lngen; tauto.
Ltac default_autorewrite ::= fail.


Lemma size_min :
∀ t, 1 ≤ size t.
Proof.
pose proof size_min_mutual as H; intuition eauto.
Qed.

Hint Resolve size_min : lngen.



Lemma size_close :
∀ t x,
  size (close x t) = size t.
Proof.
unfold close; default_simp.
Qed.

Hint Resolve size_close : lngen.
Hint Rewrite size_close using solve [auto] : lngen.



Lemma size_open :
∀ t1 t2,
  size t1 ≤ size (open t1 t2).
Proof.
unfold open; default_simp.
Qed.

Hint Resolve size_open : lngen.



Lemma size_open_var :
∀ t x,
  size (open t (Var x)) = size t.
Proof.
unfold open; default_simp.
Qed.

Hint Resolve size_open_var : lngen.
Hint Rewrite size_open_var using solve [auto] : lngen.

(* *********************************************************************** *)

Ltac default_auto ::= auto with lngen; tauto.
Ltac default_autorewrite ::= fail.


Lemma degree_S :
∀ n e,
  degree n e →
  degree (S n) e.
Proof.
pose proof degree_S_mutual as H; intuition eauto.
Qed.

Hint Resolve degree_S : lngen.

Lemma degree_O :
∀ n e,
  degree O e →
  degree n e.
Proof.
induction n; default_simp.
Qed.

Hint Resolve degree_O : lngen.



Lemma degree_close :
∀ e x,
  degree 0 e →
  degree 1 (close x e).
Proof.
unfold close; default_simp.
Qed.

Hint Resolve degree_close : lngen.



Lemma degree_close_inv :
∀ t1 x1,
  degree 1 (close x1 t1) →
  degree 0 t1.
Proof.
unfold close; eauto with lngen.
Qed.

Hint Immediate degree_close_inv : lngen.



Lemma degree_open :
∀ t1 t2,
  degree 1 t1 →
  degree 0 t2 →
  degree 0 (open t1 t2).
Proof.
unfold open; default_simp.
Qed.

Hint Resolve degree_open : lngen.



Lemma degree_open_inv :
∀ t1 t2,
  degree 0 (open t1 t2) →
  degree 1 t1.
Proof.
unfold open; eauto with lngen.
Qed.

Hint Immediate degree_open_inv : lngen.

(* *********************************************************************** *)

Ltac default_auto ::= auto with lngen brute_force; tauto.
Ltac default_autorewrite ::= fail.



Lemma close_inj :
∀ t1 t2 x1,
  close x1 t1 = close x1 t2 →
  t1 = t2.
Proof.
unfold close; eauto with lngen.
Qed.

Hint Immediate close_inj : lngen.



Lemma close_open :
∀ t1 x1,
  x1 `notin` fv t1 →
  close x1 (open t1 (Var x1)) = t1.
Proof.
unfold close; unfold open; default_simp.
Qed.

Hint Resolve close_open : lngen.
Hint Rewrite close_open using solve [auto] : lngen.



Lemma open_close :
∀ t1 x1,
  open (close x1 t1) (Var x1) = t1.
Proof.
unfold close; unfold open; default_simp.
Qed.

Hint Resolve open_close : lngen.
Hint Rewrite open_close using solve [auto] : lngen.



Lemma open_inj :
∀ t2 t1 x1,
  x1 `notin` fv t2 →
  x1 `notin` fv t1 →
  open t2 (Var x1) = open t1 (Var x1) →
  t2 = t1.
Proof.
unfold open; eauto with lngen.
Qed.

Hint Immediate open_inj : lngen.

(* *********************************************************************** *)

Ltac default_auto ::= auto with lngen brute_force; tauto.
Ltac default_autorewrite ::= autorewrite with lngen.


Lemma degree_of_lc :
∀ t1,
  lc t1 →
  degree 0 t1.
Proof.
pose proof degree_of_lc_mutual as H; intuition eauto.
Qed.

Hint Resolve degree_of_lc : lngen.


Lemma lc_of_degree :
∀ t1,
  degree 0 t1 →
  lc t1.
Proof.
intros t1; intros;
pose proof (lc_of_degree_size_mutual (size t1));
intuition eauto.
Qed.

Hint Resolve lc_of_degree : lngen.

Ltac typ_lc_exists_tac :=
  repeat (match goal with
            | H : _ |- _ ⇒
              fail 1
          end).

Ltac term_lc_exists_tac :=
  repeat (match goal with
            | H : _ |- _ ⇒
              let J1 := fresh in pose proof H as J1; apply degree_of_lc in J1; clear H
          end).

Lemma lc_Lam_exists :
∀ x1 t1,
  lc (open t1 (Var x1)) →
  lc (Lam t1).
Proof.
intros; term_lc_exists_tac; eauto with lngen.
Qed.

Hint Extern 1 (lc (Lam _)) ⇒
  let x1 := fresh in
  pick_fresh x1;
  apply (lc_Lam_exists x1) : lngen.

Lemma lc_Let_exists :
∀ x t1 t2,
  lc t1 →
  lc (open t2 (Var x)) →
  lc (Let t1 t2).
Proof.
intros; term_lc_exists_tac; eauto with lngen.
Qed.

Hint Extern 1 (lc (Let _ _)) ⇒
  let x1 := fresh in
  pick_fresh x1;
  apply (lc_Let_exists x1) : lngen.

Lemma lc_Match_exists :
∀ x1 x2 t t1 t2,
  lc t →
  lc (open t1 (Var x1)) →
  lc (open t2 (Var x2)) →
  lc (Match t t1 t2).
Proof.
intros; term_lc_exists_tac; eauto with lngen.
Qed.

Hint Extern 1 (lc (Match _ _ _)) ⇒
  let x1 := fresh in
  let x2 := fresh in
  pick_fresh x1;
  pick_fresh x2;
  apply (lc_Match_exists x1 x2) : lngen.

Lemma lc_body :
∀ t1 t2,
  body t1 →
  lc t2 →
  lc (open t1 t2).
Proof.
unfold body;
default_simp;
let x1 := fresh "x" in
pick_fresh x1;
specialize_all x1;
term_lc_exists_tac;
eauto with lngen.
Qed.

Hint Resolve lc_body : lngen.

Lemma lc_body_Lam_1 :
∀ t1,
  lc (Lam t1) →
  body t1.
Proof.
default_simp.
Qed.

Hint Resolve lc_body_Lam_1 : lngen.

Lemma lc_body_Let_2 :
∀ t1 t2,
  lc (Let t1 t2) →
  body t2.
Proof.
default_simp.
Qed.

Hint Resolve lc_body_Let_2 : lngen.

Lemma lc_body_Match_2 :
∀ t t1 t2,
  lc (Match t t1 t2) →
  body t1.
Proof.
default_simp.
Qed.

Hint Resolve lc_body_Match_2 : lngen.

Lemma lc_body_Match_3 :
∀ t1 t2 t3,
  lc (Match t1 t2 t3) →
  body t3.
Proof.
default_simp.
Qed.

Hint Resolve lc_body_Match_3 : lngen.


Lemma lc_unique :
∀ t1 (proof2 proof3 : lc t1), proof2 = proof3.
Proof.
pose proof lc_unique_mutual as H; intuition eauto.
Qed.

Hint Resolve lc_unique : lngen.


Lemma lc_of_lc_set :
∀ t1, lc_set t1 → lc t1.
Proof.
pose proof lc_of_lc_set_mutual as H; intuition eauto.
Qed.

Hint Resolve lc_of_lc_set : lngen.


Lemma lc_set_of_lc :
∀ t1,
  lc t1 →
  lc_set t1.
Proof.
intros t1; intros;
pose proof (lc_set_of_lc_size_mutual (size t1));
intuition eauto.
Qed.

Hint Resolve lc_set_of_lc : lngen.

(* *********************************************************************** *)

Ltac default_auto ::= auto with lngen; tauto.
Ltac default_autorewrite ::= fail.



Lemma close_lc :
∀ t1 x1,
  lc t1 →
  x1 `notin` fv t1 →
  close x1 t1 = t1.
Proof.
unfold close; default_simp.
Qed.

Hint Resolve close_lc : lngen.
Hint Rewrite close_lc using solve [auto] : lngen.



Lemma open_lc :
∀ t2 t1,
  lc t2 →
  open t2 t1 = t2.
Proof.
unfold open; default_simp.
Qed.

Hint Resolve open_lc : lngen.
Hint Rewrite open_lc using solve [auto] : lngen.

(* *********************************************************************** *)

Ltac default_auto ::= auto with set lngen; tauto.
Ltac default_autorewrite ::= autorewrite with lngen.



Lemma fv_close :
∀ t1 x1,
  fv (close x1 t1) [=] remove x1 (fv t1).
Proof.
unfold close; default_simp.
Qed.

Hint Resolve fv_close : lngen.
Hint Rewrite fv_close using solve [auto] : lngen.



Lemma fv_open_lower :
∀ t1 t2,
  fv t1 [<=] fv (open t1 t2).
Proof.
unfold open; default_simp.
Qed.

Hint Resolve fv_open_lower : lngen.



Lemma fv_open_upper :
∀ t1 t2,
  fv (open t1 t2) [<=] fv t2 `union` fv t1.
Proof.
unfold open; default_simp.
Qed.

Hint Resolve fv_open_upper : lngen.


Lemma fv_subst_fresh :
∀ t1 t2 x1,
  x1 `notin` fv t1 →
  fv (subst t2 x1 t1) [=] fv t1.
Proof.
pose proof fv_subst_fresh_mutual as H; intuition eauto.
Qed.

Hint Resolve fv_subst_fresh : lngen.
Hint Rewrite fv_subst_fresh using solve [auto] : lngen.


Lemma fv_subst_lower :
∀ t1 t2 x1,
  remove x1 (fv t1) [<=] fv (subst t2 x1 t1).
Proof.
pose proof fv_subst_lower_mutual as H; intuition eauto.
Qed.

Hint Resolve fv_subst_lower : lngen.


Lemma fv_subst_notin :
∀ t1 t2 x1 x2,
  x2 `notin` fv t1 →
  x2 `notin` fv t2 →
  x2 `notin` fv (subst t2 x1 t1).
Proof.
pose proof fv_subst_notin_mutual as H; intuition eauto.
Qed.

Hint Resolve fv_subst_notin : lngen.


Lemma fv_subst_upper :
∀ t1 t2 x1,
  fv (subst t2 x1 t1) [<=] fv t2 `union` remove x1 (fv t1).
Proof.
pose proof fv_subst_upper_mutual as H; intuition eauto.
Qed.

Hint Resolve fv_subst_upper : lngen.

(* *********************************************************************** *)

Ltac default_auto ::= auto with lngen brute_force; tauto.
Ltac default_autorewrite ::= autorewrite with lngen.


Lemma subst_close_rec :
∀ t2 t1 x1 x2 n1,
  degree n1 t1 →
  x1 ≠ x2 →
  x2 `notin` fv t1 →
  subst t1 x1 (close_rec n1 x2 t2) = close_rec n1 x2 (subst t1 x1 t2).
Proof.
pose proof subst_close_rec_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_close_rec : lngen.

Lemma subst_close :
∀ t2 t1 x1 x2,
  lc t1 → x1 ≠ x2 →
  x2 `notin` fv t1 →
  subst t1 x1 (close x2 t2) = close x2 (subst t1 x1 t2).
Proof.
unfold close; default_simp.
Qed.

Hint Resolve subst_close : lngen.


Lemma subst_degree :
∀ t1 t2 x1 n1,
  degree n1 t1 →
  degree n1 t2 →
  degree n1 (subst t2 x1 t1).
Proof.
pose proof subst_degree_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_degree : lngen.


Lemma subst_fresh_eq :
∀ t2 t1 x1,
  x1 `notin` fv t2 →
  subst t1 x1 t2 = t2.
Proof.
pose proof subst_fresh_eq_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_fresh_eq : lngen.
Hint Rewrite subst_fresh_eq using solve [auto] : lngen.


Lemma subst_fresh_same :
∀ t2 t1 x1,
  x1 `notin` fv t1 →
  x1 `notin` fv (subst t1 x1 t2).
Proof.
pose proof subst_fresh_same_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_fresh_same : lngen.


Lemma subst_fresh :
∀ t2 t1 x1 x2,
  x1 `notin` fv t2 →
  x1 `notin` fv t1 →
  x1 `notin` fv (subst t1 x2 t2).
Proof.
pose proof subst_fresh_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_fresh : lngen.

Lemma subst_lc :
∀ t1 t2 x1,
  lc t1 →
  lc t2 →
  lc (subst t2 x1 t1).
Proof.
default_simp.
Qed.

Hint Resolve subst_lc : lngen.



Lemma subst_open :
∀ e3 t1 t2 x1,
  lc t1 →
  subst t1 x1 (open e3 t2) = open (subst t1 x1 e3) (subst t1 x1 t2).
Proof.
unfold open; default_simp.
Qed.

Hint Resolve subst_open : lngen.

Lemma subst_open_var :
∀ t2 t1 x1 x2,
  x1 ≠ x2 →
  lc t1 →
  open (subst t1 x1 t2) (Var x2) = subst t1 x1 (open t2 (Var x2)).
Proof.
intros; rewrite subst_open; default_simp.
Qed.

Hint Resolve subst_open_var : lngen.



Lemma subst_spec :
∀ t1 t2 x1,
  subst t2 x1 t1 = open (close x1 t1) t2.
Proof.
unfold close; unfold open; default_simp.
Qed.

Hint Resolve subst_spec : lngen.


Lemma subst_subst :
∀ t1 t2 e3 x2 x1,
  x2 `notin` fv t2 →
  x2 ≠ x1 →
  subst t2 x1 (subst e3 x2 t1) = subst (subst t2 x1 e3) x2 (subst t2 x1 t1).
Proof.
pose proof subst_subst_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_subst : lngen.



Lemma subst_close_open :
∀ t2 t1 x1 x2,
  x2 `notin` fv t2 →
  x2 `notin` fv t1 →
  x2 ≠ x1 →
  lc t1 →
  subst t1 x1 t2 = close x2 (subst t1 x1 (open t2 (Var x2))).
Proof.
unfold close; unfold open; default_simp.
Qed.

Hint Resolve subst_close_open : lngen.

Lemma subst_Lam :
∀ x2 t2 t1 x1,
  lc t1 →
  x2 `notin` fv t1 `union` fv t2 `union` singleton x1 →
  subst t1 x1 (Lam t2) = Lam (close x2 (subst t1 x1 (open t2 (Var x2)))).
Proof.
default_simp.
Qed.

Hint Resolve subst_Lam : lngen.

Lemma subst_Let :
∀ t0 x2 t2 t1 x1,
  lc t0 →
  lc t1 →
  x2 `notin` fv t1 `union` fv t2 `union` singleton x1 →
  subst t1 x1 (Let t0 t2) = Let (subst t1 x1 t0) (close x2 (subst t1 x1 (open t2 (Var x2)))).
Proof.
default_simp.
Qed.

Hint Resolve subst_Let : lngen.

Lemma subst_Match :
∀ t0 x2 t2 t3 t1 x1,
  lc t0 →
  lc t1 →
  x2 `notin` fv t1 `union` fv t2 `union` fv t3 `union` singleton x1 →
  subst t1 x1 (Match t0 t2 t3) = Match (subst t1 x1 t0) (close x2 (subst t1 x1 (open t2 (Var x2)))) (close x2 (subst t1 x1 (open t3 (Var x2)))).
Proof.
default_simp.
Qed.

Hint Resolve subst_Match : lngen.


Lemma subst_intro_rec :
∀ t1 x1 t2 n1,
  x1 `notin` fv t1 →
  open_rec n1 t2 t1 = subst t2 x1 (open_rec n1 (Var x1) t1).
Proof.
pose proof subst_intro_rec_mutual as H; intuition eauto.
Qed.

Hint Resolve subst_intro_rec : lngen.
Hint Rewrite subst_intro_rec using solve [auto] : lngen.

Lemma subst_intro :
∀ x1 t1 t2,
  x1 `notin` fv t1 →
  open t1 t2 = subst t2 x1 (open t1 (Var x1)).
Proof.
unfold open; default_simp.
Qed.

Hint Resolve subst_intro : lngen.

(* *********************************************************************** *)

Ltac default_auto ::= auto; tauto.
Ltac default_autorewrite ::= fail.