Infrastructure
Require Import Coq.Arith.Wf_nat.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Program.Equality.
Require Export Metalib.Metatheory.
Require Export Metalib.LibLNgen.
Require Export Definitions.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Program.Equality.
Require Export Metalib.Metatheory.
Require Export Metalib.LibLNgen.
Require Export Definitions.
NOTE: Auxiliary theorems are hidden in generated documentation.
In general, there is a _rec version of every lemma involving
open and close.
Scheme typ_ind' := Induction for typ Sort Prop
with dtyp_ind' := Induction for dtyp Sort Prop.
Definition typ_dtyp_mutind :=
fun H1 H2 H3 H4 H5 H6 ⇒
(conj (typ_ind' H1 H2 H3 H4 H5 H6)
(dtyp_ind' H1 H2 H3 H4 H5 H6)).
Scheme typ_rec' := Induction for typ Sort Set
with dtyp_rec' := Induction for dtyp Sort Set.
Definition typ_dtyp_mutrec :=
fun H1 H2 H3 H4 H5 H6 ⇒
(pair (typ_rec' H1 H2 H3 H4 H5 H6)
(dtyp_rec' H1 H2 H3 H4 H5 H6)).
Scheme label_ind' := Induction for label Sort Prop.
Definition label_mutind :=
fun H1 H2 H3 ⇒
label_ind' H1 H2 H3.
Scheme label_rec' := Induction for label Sort Set.
Definition label_mutrec :=
fun H1 H2 H3 ⇒
label_rec' H1 H2 H3.
Scheme trm_ind' := Induction for trm Sort Prop.
Definition trm_mutind :=
fun H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 ⇒
trm_ind' H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12.
Scheme trm_rec' := Induction for trm Sort Set.
Definition trm_mutrec :=
fun H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 ⇒
trm_rec' H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12.
Scheme ityp_ind' := Induction for ityp Sort Prop.
Definition ityp_mutind :=
fun H1 H2 H3 ⇒
ityp_ind' H1 H2 H3.
Scheme ityp_rec' := Induction for ityp Sort Set.
Definition ityp_mutrec :=
fun H1 H2 H3 ⇒
ityp_rec' H1 H2 H3.
Scheme itrm_ind' := Induction for itrm Sort Prop.
Definition itrm_mutind :=
fun H1 H2 H3 H4 H5 H6 H7 H8 ⇒
itrm_ind' H1 H2 H3 H4 H5 H6 H7 H8.
Scheme itrm_rec' := Induction for itrm Sort Set.
Definition itrm_mutrec :=
fun H1 H2 H3 H4 H5 H6 H7 H8 ⇒
itrm_rec' H1 H2 H3 H4 H5 H6 H7 H8.
Fixpoint close_trm_wrt_trm_rec (n1 : nat) (x1 : var) (L1 : trm) {struct L1} : trm :=
match L1 with
| t_var_f x2 ⇒ if (x1 == x2) then (t_var_b n1) else (t_var_f x2)
| t_var_b n2 ⇒ if (lt_ge_dec n2 n1) then (t_var_b n2) else (t_var_b (S n2))
| t_const c1 ⇒ t_const c1
| t_binop M1 N1 ⇒ t_binop (close_trm_wrt_trm_rec n1 x1 M1) (close_trm_wrt_trm_rec n1 x1 N1)
| t_abs A1 N1 ⇒ t_abs A1 (close_trm_wrt_trm_rec (S n1) x1 N1)
| t_app L2 M1 ⇒ t_app (close_trm_wrt_trm_rec n1 x1 L2) (close_trm_wrt_trm_rec n1 x1 M1)
| t_null ⇒ t_null
| t_lift M1 ⇒ t_lift (close_trm_wrt_trm_rec n1 x1 M1)
| t_case L2 M1 N1 ⇒ t_case (close_trm_wrt_trm_rec n1 x1 L2) (close_trm_wrt_trm_rec n1 x1 M1) (close_trm_wrt_trm_rec (S n1) x1 N1)
| t_cast M1 A1 p1 B1 ⇒ t_cast (close_trm_wrt_trm_rec n1 x1 M1) A1 p1 B1
| t_blame p1 ⇒ t_blame p1
end.
Definition close_trm_wrt_trm x1 L1 := close_trm_wrt_trm_rec 0 x1 L1.
Fixpoint close_itrm_wrt_itrm_rec (n1 : nat) (ix1 : ivar) (iL1 : itrm) {struct iL1} : itrm :=
match iL1 with
| itrm_var_f ix2 ⇒ if (ix1 == ix2) then (itrm_var_b n1) else (itrm_var_f ix2)
| itrm_var_b n2 ⇒ if (lt_ge_dec n2 n1) then (itrm_var_b n2) else (itrm_var_b (S n2))
| itrm_const c1 ⇒ itrm_const c1
| itrm_binop iM1 iN1 ⇒ itrm_binop (close_itrm_wrt_itrm_rec n1 ix1 iM1) (close_itrm_wrt_itrm_rec n1 ix1 iN1)
| itrm_abs iA1 iN1 ⇒ itrm_abs iA1 (close_itrm_wrt_itrm_rec (S n1) ix1 iN1)
| itrm_app iL2 iM1 ⇒ itrm_app (close_itrm_wrt_itrm_rec n1 ix1 iL2) (close_itrm_wrt_itrm_rec n1 ix1 iM1)
| itrm_null ⇒ itrm_null
end.
Definition close_itrm_wrt_itrm ix1 iL1 := close_itrm_wrt_itrm_rec 0 ix1 iL1.
Fixpoint size_typ (A1 : typ) {struct A1} : nat :=
match A1 with
| typ_def D1 ⇒ 1 + (size_dtyp D1)
| typ_null D1 ⇒ 1 + (size_dtyp D1)
end
with size_dtyp (D1 : dtyp) {struct D1} : nat :=
match D1 with
| dtyp_base ⇒ 1
| dtyp_arrow A1 B1 ⇒ 1 + (size_typ A1) + (size_typ B1)
end.
Fixpoint size_label (p1 : label) {struct p1} : nat :=
match p1 with
| label_name bl1 ⇒ 1
| label_not_label bl1 ⇒ 1
end.
Fixpoint size_trm (L1 : trm) {struct L1} : nat :=
match L1 with
| t_var_f x1 ⇒ 1
| t_var_b n1 ⇒ 1
| t_const c1 ⇒ 1
| t_binop M1 N1 ⇒ 1 + (size_trm M1) + (size_trm N1)
| t_abs A1 N1 ⇒ 1 + (size_typ A1) + (size_trm N1)
| t_app L2 M1 ⇒ 1 + (size_trm L2) + (size_trm M1)
| t_null ⇒ 1
| t_lift M1 ⇒ 1 + (size_trm M1)
| t_case L2 M1 N1 ⇒ 1 + (size_trm L2) + (size_trm M1) + (size_trm N1)
| t_cast M1 A1 p1 B1 ⇒ 1 + (size_trm M1) + (size_typ A1) + (size_label p1) + (size_typ B1)
| t_blame p1 ⇒ 1 + (size_label p1)
end.
Fixpoint size_ityp (iA1 : ityp) {struct iA1} : nat :=
match iA1 with
| ityp_base ⇒ 1
| ityp_arrow iA2 iB1 ⇒ 1 + (size_ityp iA2) + (size_ityp iB1)
end.
Fixpoint size_itrm (iL1 : itrm) {struct iL1} : nat :=
match iL1 with
| itrm_var_f ix1 ⇒ 1
| itrm_var_b n1 ⇒ 1
| itrm_const c1 ⇒ 1
| itrm_binop iM1 iN1 ⇒ 1 + (size_itrm iM1) + (size_itrm iN1)
| itrm_abs iA1 iN1 ⇒ 1 + (size_ityp iA1) + (size_itrm iN1)
| itrm_app iL2 iM1 ⇒ 1 + (size_itrm iL2) + (size_itrm iM1)
| itrm_null ⇒ 1
end.
Inductive degree_trm_wrt_trm : nat → trm → Prop :=
| degree_wrt_trm_t_var_f : ∀ n1 x1,
degree_trm_wrt_trm n1 (t_var_f x1)
| degree_wrt_trm_t_var_b : ∀ n1 n2,
lt n2 n1 →
degree_trm_wrt_trm n1 (t_var_b n2)
| degree_wrt_trm_t_const : ∀ n1 c1,
degree_trm_wrt_trm n1 (t_const c1)
| degree_wrt_trm_t_binop : ∀ n1 M1 N1,
degree_trm_wrt_trm n1 M1 →
degree_trm_wrt_trm n1 N1 →
degree_trm_wrt_trm n1 (t_binop M1 N1)
| degree_wrt_trm_t_abs : ∀ n1 A1 N1,
degree_trm_wrt_trm (S n1) N1 →
degree_trm_wrt_trm n1 (t_abs A1 N1)
| degree_wrt_trm_t_app : ∀ n1 L1 M1,
degree_trm_wrt_trm n1 L1 →
degree_trm_wrt_trm n1 M1 →
degree_trm_wrt_trm n1 (t_app L1 M1)
| degree_wrt_trm_t_null : ∀ n1,
degree_trm_wrt_trm n1 (t_null)
| degree_wrt_trm_t_lift : ∀ n1 M1,
degree_trm_wrt_trm n1 M1 →
degree_trm_wrt_trm n1 (t_lift M1)
| degree_wrt_trm_t_case : ∀ n1 L1 M1 N1,
degree_trm_wrt_trm n1 L1 →
degree_trm_wrt_trm n1 M1 →
degree_trm_wrt_trm (S n1) N1 →
degree_trm_wrt_trm n1 (t_case L1 M1 N1)
| degree_wrt_trm_t_cast : ∀ n1 M1 A1 p1 B1,
degree_trm_wrt_trm n1 M1 →
degree_trm_wrt_trm n1 (t_cast M1 A1 p1 B1)
| degree_wrt_trm_t_blame : ∀ n1 p1,
degree_trm_wrt_trm n1 (t_blame p1).
Scheme degree_trm_wrt_trm_ind' := Induction for degree_trm_wrt_trm Sort Prop.
Definition degree_trm_wrt_trm_mutind :=
fun H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 ⇒
degree_trm_wrt_trm_ind' H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12.
Hint Constructors degree_trm_wrt_trm : core lngen.
Inductive degree_itrm_wrt_itrm : nat → itrm → Prop :=
| degree_wrt_itrm_itrm_var_f : ∀ n1 ix1,
degree_itrm_wrt_itrm n1 (itrm_var_f ix1)
| degree_wrt_itrm_itrm_var_b : ∀ n1 n2,
lt n2 n1 →
degree_itrm_wrt_itrm n1 (itrm_var_b n2)
| degree_wrt_itrm_itrm_const : ∀ n1 c1,
degree_itrm_wrt_itrm n1 (itrm_const c1)
| degree_wrt_itrm_itrm_binop : ∀ n1 iM1 iN1,
degree_itrm_wrt_itrm n1 iM1 →
degree_itrm_wrt_itrm n1 iN1 →
degree_itrm_wrt_itrm n1 (itrm_binop iM1 iN1)
| degree_wrt_itrm_itrm_abs : ∀ n1 iA1 iN1,
degree_itrm_wrt_itrm (S n1) iN1 →
degree_itrm_wrt_itrm n1 (itrm_abs iA1 iN1)
| degree_wrt_itrm_itrm_app : ∀ n1 iL1 iM1,
degree_itrm_wrt_itrm n1 iL1 →
degree_itrm_wrt_itrm n1 iM1 →
degree_itrm_wrt_itrm n1 (itrm_app iL1 iM1)
| degree_wrt_itrm_itrm_null : ∀ n1,
degree_itrm_wrt_itrm n1 (itrm_null).
Scheme degree_itrm_wrt_itrm_ind' := Induction for degree_itrm_wrt_itrm Sort Prop.
Definition degree_itrm_wrt_itrm_mutind :=
fun H1 H2 H3 H4 H5 H6 H7 H8 ⇒
degree_itrm_wrt_itrm_ind' H1 H2 H3 H4 H5 H6 H7 H8.
Hint Constructors degree_itrm_wrt_itrm : core lngen.
Inductive lc_set_trm : trm → Set :=
| lc_set_t_var_f : ∀ x1,
lc_set_trm (t_var_f x1)
| lc_set_t_const : ∀ c1,
lc_set_trm (t_const c1)
| lc_set_t_binop : ∀ M1 N1,
lc_set_trm M1 →
lc_set_trm N1 →
lc_set_trm (t_binop M1 N1)
| lc_set_t_abs : ∀ A1 N1,
(∀ x1 : var, lc_set_trm (open_trm_wrt_trm N1 (t_var_f x1))) →
lc_set_trm (t_abs A1 N1)
| lc_set_t_app : ∀ L1 M1,
lc_set_trm L1 →
lc_set_trm M1 →
lc_set_trm (t_app L1 M1)
| lc_set_t_null :
lc_set_trm (t_null)
| lc_set_t_lift : ∀ M1,
lc_set_trm M1 →
lc_set_trm (t_lift M1)
| lc_set_t_case : ∀ L1 M1 N1,
lc_set_trm L1 →
lc_set_trm M1 →
(∀ x1 : var, lc_set_trm (open_trm_wrt_trm N1 (t_var_f x1))) →
lc_set_trm (t_case L1 M1 N1)
| lc_set_t_cast : ∀ M1 A1 p1 B1,
lc_set_trm M1 →
lc_set_trm (t_cast M1 A1 p1 B1)
| lc_set_t_blame : ∀ p1,
lc_set_trm (t_blame p1).
Scheme lc_trm_ind' := Induction for lc_trm Sort Prop.
Definition lc_trm_mutind :=
fun H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 ⇒
lc_trm_ind' H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11.
Scheme lc_set_trm_ind' := Induction for lc_set_trm Sort Prop.
Definition lc_set_trm_mutind :=
fun H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 ⇒
lc_set_trm_ind' H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11.
Scheme lc_set_trm_rec' := Induction for lc_set_trm Sort Set.
Definition lc_set_trm_mutrec :=
fun H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 ⇒
lc_set_trm_rec' H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11.
Hint Constructors lc_trm : core lngen.
Hint Constructors lc_set_trm : core lngen.
Inductive lc_set_itrm : itrm → Set :=
| lc_set_itrm_var_f : ∀ ix1,
lc_set_itrm (itrm_var_f ix1)
| lc_set_itrm_const : ∀ c1,
lc_set_itrm (itrm_const c1)
| lc_set_itrm_binop : ∀ iM1 iN1,
lc_set_itrm iM1 →
lc_set_itrm iN1 →
lc_set_itrm (itrm_binop iM1 iN1)
| lc_set_itrm_abs : ∀ iA1 iN1,
(∀ ix1 : ivar, lc_set_itrm (open_itrm_wrt_itrm iN1 (itrm_var_f ix1))) →
lc_set_itrm (itrm_abs iA1 iN1)
| lc_set_itrm_app : ∀ iL1 iM1,
lc_set_itrm iL1 →
lc_set_itrm iM1 →
lc_set_itrm (itrm_app iL1 iM1)
| lc_set_itrm_null :
lc_set_itrm (itrm_null).
Scheme lc_itrm_ind' := Induction for lc_itrm Sort Prop.
Definition lc_itrm_mutind :=
fun H1 H2 H3 H4 H5 H6 H7 ⇒
lc_itrm_ind' H1 H2 H3 H4 H5 H6 H7.
Scheme lc_set_itrm_ind' := Induction for lc_set_itrm Sort Prop.
Definition lc_set_itrm_mutind :=
fun H1 H2 H3 H4 H5 H6 H7 ⇒
lc_set_itrm_ind' H1 H2 H3 H4 H5 H6 H7.
Scheme lc_set_itrm_rec' := Induction for lc_set_itrm Sort Set.
Definition lc_set_itrm_mutrec :=
fun H1 H2 H3 H4 H5 H6 H7 ⇒
lc_set_itrm_rec' H1 H2 H3 H4 H5 H6 H7.
Hint Constructors lc_itrm : core lngen.
Hint Constructors lc_set_itrm : core lngen.
Definition body_trm_wrt_trm L1 := ∀ x1, lc_trm (open_trm_wrt_trm L1 (t_var_f x1)).
Hint Unfold body_trm_wrt_trm : core.
Definition body_itrm_wrt_itrm iL1 := ∀ ix1, lc_itrm (open_itrm_wrt_itrm iL1 (itrm_var_f ix1)).
Hint Unfold body_itrm_wrt_itrm : core.
Redefine some tactics.
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_typ_min :
∀ A1, 1 ≤ size_typ A1.
Proof.
pose proof size_typ_min_size_dtyp_min_mutual as H; intuition eauto.
Qed.
Hint Resolve size_typ_min : lngen.
Lemma size_dtyp_min :
∀ D1, 1 ≤ size_dtyp D1.
Proof.
pose proof size_typ_min_size_dtyp_min_mutual as H; intuition eauto.
Qed.
Hint Resolve size_dtyp_min : lngen.
Lemma size_label_min :
∀ p1, 1 ≤ size_label p1.
Proof.
pose proof size_label_min_mutual as H; intuition eauto.
Qed.
Hint Resolve size_label_min : lngen.
Lemma size_trm_min :
∀ L1, 1 ≤ size_trm L1.
Proof.
pose proof size_trm_min_mutual as H; intuition eauto.
Qed.
Hint Resolve size_trm_min : lngen.
Lemma size_ityp_min :
∀ iA1, 1 ≤ size_ityp iA1.
Proof.
pose proof size_ityp_min_mutual as H; intuition eauto.
Qed.
Hint Resolve size_ityp_min : lngen.
Lemma size_itrm_min :
∀ iL1, 1 ≤ size_itrm iL1.
Proof.
pose proof size_itrm_min_mutual as H; intuition eauto.
Qed.
Hint Resolve size_itrm_min : lngen.
Lemma size_trm_close_trm_wrt_trm :
∀ L1 x1,
size_trm (close_trm_wrt_trm x1 L1) = size_trm L1.
Proof.
unfold close_trm_wrt_trm; default_simp.
Qed.
Hint Resolve size_trm_close_trm_wrt_trm : lngen.
Hint Rewrite size_trm_close_trm_wrt_trm using solve [auto] : lngen.
Lemma size_itrm_close_itrm_wrt_itrm :
∀ iL1 ix1,
size_itrm (close_itrm_wrt_itrm ix1 iL1) = size_itrm iL1.
Proof.
unfold close_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve size_itrm_close_itrm_wrt_itrm : lngen.
Hint Rewrite size_itrm_close_itrm_wrt_itrm using solve [auto] : lngen.
Lemma size_trm_open_trm_wrt_trm :
∀ L1 L2,
size_trm L1 ≤ size_trm (open_trm_wrt_trm L1 L2).
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.
Hint Resolve size_trm_open_trm_wrt_trm : lngen.
Lemma size_itrm_open_itrm_wrt_itrm :
∀ iL1 iL2,
size_itrm iL1 ≤ size_itrm (open_itrm_wrt_itrm iL1 iL2).
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve size_itrm_open_itrm_wrt_itrm : lngen.
Lemma size_trm_open_trm_wrt_trm_var :
∀ L1 x1,
size_trm (open_trm_wrt_trm L1 (t_var_f x1)) = size_trm L1.
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.
Hint Resolve size_trm_open_trm_wrt_trm_var : lngen.
Hint Rewrite size_trm_open_trm_wrt_trm_var using solve [auto] : lngen.
Lemma size_itrm_open_itrm_wrt_itrm_var :
∀ iL1 ix1,
size_itrm (open_itrm_wrt_itrm iL1 (itrm_var_f ix1)) = size_itrm iL1.
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve size_itrm_open_itrm_wrt_itrm_var : lngen.
Hint Rewrite size_itrm_open_itrm_wrt_itrm_var using solve [auto] : lngen.
Ltac default_auto ::= auto with lngen; tauto.
Ltac default_autorewrite ::= fail.
Lemma degree_trm_wrt_trm_S :
∀ n1 L1,
degree_trm_wrt_trm n1 L1 →
degree_trm_wrt_trm (S n1) L1.
Proof.
pose proof degree_trm_wrt_trm_S_mutual as H; intuition eauto.
Qed.
Hint Resolve degree_trm_wrt_trm_S : lngen.
Lemma degree_itrm_wrt_itrm_S :
∀ n1 iL1,
degree_itrm_wrt_itrm n1 iL1 →
degree_itrm_wrt_itrm (S n1) iL1.
Proof.
pose proof degree_itrm_wrt_itrm_S_mutual as H; intuition eauto.
Qed.
Hint Resolve degree_itrm_wrt_itrm_S : lngen.
Lemma degree_trm_wrt_trm_O :
∀ n1 L1,
degree_trm_wrt_trm O L1 →
degree_trm_wrt_trm n1 L1.
Proof.
induction n1; default_simp.
Qed.
Hint Resolve degree_trm_wrt_trm_O : lngen.
Lemma degree_itrm_wrt_itrm_O :
∀ n1 iL1,
degree_itrm_wrt_itrm O iL1 →
degree_itrm_wrt_itrm n1 iL1.
Proof.
induction n1; default_simp.
Qed.
Hint Resolve degree_itrm_wrt_itrm_O : lngen.
Lemma degree_trm_wrt_trm_close_trm_wrt_trm :
∀ L1 x1,
degree_trm_wrt_trm 0 L1 →
degree_trm_wrt_trm 1 (close_trm_wrt_trm x1 L1).
Proof.
unfold close_trm_wrt_trm; default_simp.
Qed.
Hint Resolve degree_trm_wrt_trm_close_trm_wrt_trm : lngen.
Lemma degree_itrm_wrt_itrm_close_itrm_wrt_itrm :
∀ iL1 ix1,
degree_itrm_wrt_itrm 0 iL1 →
degree_itrm_wrt_itrm 1 (close_itrm_wrt_itrm ix1 iL1).
Proof.
unfold close_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve degree_itrm_wrt_itrm_close_itrm_wrt_itrm : lngen.
Lemma degree_trm_wrt_trm_close_trm_wrt_trm_inv :
∀ L1 x1,
degree_trm_wrt_trm 1 (close_trm_wrt_trm x1 L1) →
degree_trm_wrt_trm 0 L1.
Proof.
unfold close_trm_wrt_trm; eauto with lngen.
Qed.
Hint Immediate degree_trm_wrt_trm_close_trm_wrt_trm_inv : lngen.
Lemma degree_itrm_wrt_itrm_close_itrm_wrt_itrm_inv :
∀ iL1 ix1,
degree_itrm_wrt_itrm 1 (close_itrm_wrt_itrm ix1 iL1) →
degree_itrm_wrt_itrm 0 iL1.
Proof.
unfold close_itrm_wrt_itrm; eauto with lngen.
Qed.
Hint Immediate degree_itrm_wrt_itrm_close_itrm_wrt_itrm_inv : lngen.
Lemma degree_trm_wrt_trm_open_trm_wrt_trm :
∀ L1 L2,
degree_trm_wrt_trm 1 L1 →
degree_trm_wrt_trm 0 L2 →
degree_trm_wrt_trm 0 (open_trm_wrt_trm L1 L2).
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.
Hint Resolve degree_trm_wrt_trm_open_trm_wrt_trm : lngen.
Lemma degree_itrm_wrt_itrm_open_itrm_wrt_itrm :
∀ iL1 iL2,
degree_itrm_wrt_itrm 1 iL1 →
degree_itrm_wrt_itrm 0 iL2 →
degree_itrm_wrt_itrm 0 (open_itrm_wrt_itrm iL1 iL2).
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve degree_itrm_wrt_itrm_open_itrm_wrt_itrm : lngen.
Lemma degree_trm_wrt_trm_open_trm_wrt_trm_inv :
∀ L1 L2,
degree_trm_wrt_trm 0 (open_trm_wrt_trm L1 L2) →
degree_trm_wrt_trm 1 L1.
Proof.
unfold open_trm_wrt_trm; eauto with lngen.
Qed.
Hint Immediate degree_trm_wrt_trm_open_trm_wrt_trm_inv : lngen.
Lemma degree_itrm_wrt_itrm_open_itrm_wrt_itrm_inv :
∀ iL1 iL2,
degree_itrm_wrt_itrm 0 (open_itrm_wrt_itrm iL1 iL2) →
degree_itrm_wrt_itrm 1 iL1.
Proof.
unfold open_itrm_wrt_itrm; eauto with lngen.
Qed.
Hint Immediate degree_itrm_wrt_itrm_open_itrm_wrt_itrm_inv : lngen.
Ltac default_auto ::= auto with lngen brute_force; tauto.
Ltac default_autorewrite ::= fail.
Lemma close_trm_wrt_trm_inj :
∀ L1 L2 x1,
close_trm_wrt_trm x1 L1 = close_trm_wrt_trm x1 L2 →
L1 = L2.
Proof.
unfold close_trm_wrt_trm; eauto with lngen.
Qed.
Hint Immediate close_trm_wrt_trm_inj : lngen.
Lemma close_itrm_wrt_itrm_inj :
∀ iL1 iL2 ix1,
close_itrm_wrt_itrm ix1 iL1 = close_itrm_wrt_itrm ix1 iL2 →
iL1 = iL2.
Proof.
unfold close_itrm_wrt_itrm; eauto with lngen.
Qed.
Hint Immediate close_itrm_wrt_itrm_inj : lngen.
Lemma close_trm_wrt_trm_open_trm_wrt_trm :
∀ L1 x1,
x1 `notin` fv_trm L1 →
close_trm_wrt_trm x1 (open_trm_wrt_trm L1 (t_var_f x1)) = L1.
Proof.
unfold close_trm_wrt_trm; unfold open_trm_wrt_trm; default_simp.
Qed.
Hint Resolve close_trm_wrt_trm_open_trm_wrt_trm : lngen.
Hint Rewrite close_trm_wrt_trm_open_trm_wrt_trm using solve [auto] : lngen.
Lemma close_itrm_wrt_itrm_open_itrm_wrt_itrm :
∀ iL1 ix1,
ix1 `notin` fv_itrm iL1 →
close_itrm_wrt_itrm ix1 (open_itrm_wrt_itrm iL1 (itrm_var_f ix1)) = iL1.
Proof.
unfold close_itrm_wrt_itrm; unfold open_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve close_itrm_wrt_itrm_open_itrm_wrt_itrm : lngen.
Hint Rewrite close_itrm_wrt_itrm_open_itrm_wrt_itrm using solve [auto] : lngen.
Lemma open_trm_wrt_trm_close_trm_wrt_trm :
∀ L1 x1,
open_trm_wrt_trm (close_trm_wrt_trm x1 L1) (t_var_f x1) = L1.
Proof.
unfold close_trm_wrt_trm; unfold open_trm_wrt_trm; default_simp.
Qed.
Hint Resolve open_trm_wrt_trm_close_trm_wrt_trm : lngen.
Hint Rewrite open_trm_wrt_trm_close_trm_wrt_trm using solve [auto] : lngen.
Lemma open_itrm_wrt_itrm_close_itrm_wrt_itrm :
∀ iL1 ix1,
open_itrm_wrt_itrm (close_itrm_wrt_itrm ix1 iL1) (itrm_var_f ix1) = iL1.
Proof.
unfold close_itrm_wrt_itrm; unfold open_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve open_itrm_wrt_itrm_close_itrm_wrt_itrm : lngen.
Hint Rewrite open_itrm_wrt_itrm_close_itrm_wrt_itrm using solve [auto] : lngen.
Lemma open_trm_wrt_trm_inj :
∀ L2 L1 x1,
x1 `notin` fv_trm L2 →
x1 `notin` fv_trm L1 →
open_trm_wrt_trm L2 (t_var_f x1) = open_trm_wrt_trm L1 (t_var_f x1) →
L2 = L1.
Proof.
unfold open_trm_wrt_trm; eauto with lngen.
Qed.
Hint Immediate open_trm_wrt_trm_inj : lngen.
Lemma open_itrm_wrt_itrm_inj :
∀ iL2 iL1 ix1,
ix1 `notin` fv_itrm iL2 →
ix1 `notin` fv_itrm iL1 →
open_itrm_wrt_itrm iL2 (itrm_var_f ix1) = open_itrm_wrt_itrm iL1 (itrm_var_f ix1) →
iL2 = iL1.
Proof.
unfold open_itrm_wrt_itrm; eauto with lngen.
Qed.
Hint Immediate open_itrm_wrt_itrm_inj : lngen.
Ltac default_auto ::= auto with lngen brute_force; tauto.
Ltac default_autorewrite ::= autorewrite with lngen.
Lemma degree_trm_wrt_trm_of_lc_trm :
∀ L1,
lc_trm L1 →
degree_trm_wrt_trm 0 L1.
Proof.
pose proof degree_trm_wrt_trm_of_lc_trm_mutual as H; intuition eauto.
Qed.
Hint Resolve degree_trm_wrt_trm_of_lc_trm : lngen.
Lemma degree_itrm_wrt_itrm_of_lc_itrm :
∀ iL1,
lc_itrm iL1 →
degree_itrm_wrt_itrm 0 iL1.
Proof.
pose proof degree_itrm_wrt_itrm_of_lc_itrm_mutual as H; intuition eauto.
Qed.
Hint Resolve degree_itrm_wrt_itrm_of_lc_itrm : lngen.
Lemma lc_trm_of_degree :
∀ L1,
degree_trm_wrt_trm 0 L1 →
lc_trm L1.
Proof.
intros L1; intros;
pose proof (lc_trm_of_degree_size_mutual (size_trm L1));
intuition eauto.
Qed.
Hint Resolve lc_trm_of_degree : lngen.
Lemma lc_itrm_of_degree :
∀ iL1,
degree_itrm_wrt_itrm 0 iL1 →
lc_itrm iL1.
Proof.
intros iL1; intros;
pose proof (lc_itrm_of_degree_size_mutual (size_itrm iL1));
intuition eauto.
Qed.
Hint Resolve lc_itrm_of_degree : lngen.
Ltac typ_dtyp_lc_exists_tac :=
repeat (match goal with
| H : _ |- _ ⇒
fail 1
| H : _ |- _ ⇒
fail 1
end).
Ltac label_lc_exists_tac :=
repeat (match goal with
| H : _ |- _ ⇒
fail 1
end).
Ltac trm_lc_exists_tac :=
repeat (match goal with
| H : _ |- _ ⇒
let J1 := fresh in pose proof H as J1; apply degree_trm_wrt_trm_of_lc_trm in J1; clear H
end).
Ltac ityp_lc_exists_tac :=
repeat (match goal with
| H : _ |- _ ⇒
fail 1
end).
Ltac itrm_lc_exists_tac :=
repeat (match goal with
| H : _ |- _ ⇒
let J1 := fresh in pose proof H as J1; apply degree_itrm_wrt_itrm_of_lc_itrm in J1; clear H
end).
Lemma lc_t_abs_exists :
∀ x1 A1 N1,
lc_trm (open_trm_wrt_trm N1 (t_var_f x1)) →
lc_trm (t_abs A1 N1).
Proof.
intros; trm_lc_exists_tac; eauto with lngen.
Qed.
Lemma lc_t_case_exists :
∀ x1 L1 M1 N1,
lc_trm L1 →
lc_trm M1 →
lc_trm (open_trm_wrt_trm N1 (t_var_f x1)) →
lc_trm (t_case L1 M1 N1).
Proof.
intros; trm_lc_exists_tac; eauto with lngen.
Qed.
Lemma lc_itrm_abs_exists :
∀ ix1 iA1 iN1,
lc_itrm (open_itrm_wrt_itrm iN1 (itrm_var_f ix1)) →
lc_itrm (itrm_abs iA1 iN1).
Proof.
intros; itrm_lc_exists_tac; eauto with lngen.
Qed.
Hint Extern 1 (lc_trm (t_abs _ _)) ⇒
let x1 := fresh in
pick_fresh x1;
apply (lc_t_abs_exists x1) : core.
Hint Extern 1 (lc_trm (t_case _ _ _)) ⇒
let x1 := fresh in
pick_fresh x1;
apply (lc_t_case_exists x1) : core.
Hint Extern 1 (lc_itrm (itrm_abs _ _)) ⇒
let ix1 := fresh in
pick_fresh ix1;
apply (lc_itrm_abs_exists ix1) : core.
Lemma lc_body_trm_wrt_trm :
∀ L1 L2,
body_trm_wrt_trm L1 →
lc_trm L2 →
lc_trm (open_trm_wrt_trm L1 L2).
Proof.
unfold body_trm_wrt_trm;
default_simp;
let x1 := fresh "x" in
pick_fresh x1;
specialize_all x1;
trm_lc_exists_tac;
eauto with lngen.
Qed.
Hint Resolve lc_body_trm_wrt_trm : lngen.
Lemma lc_body_itrm_wrt_itrm :
∀ iL1 iL2,
body_itrm_wrt_itrm iL1 →
lc_itrm iL2 →
lc_itrm (open_itrm_wrt_itrm iL1 iL2).
Proof.
unfold body_itrm_wrt_itrm;
default_simp;
let ix1 := fresh "x" in
pick_fresh ix1;
specialize_all ix1;
itrm_lc_exists_tac;
eauto with lngen.
Qed.
Hint Resolve lc_body_itrm_wrt_itrm : lngen.
Lemma lc_body_t_abs_2 :
∀ A1 N1,
lc_trm (t_abs A1 N1) →
body_trm_wrt_trm N1.
Proof.
default_simp.
Qed.
Hint Resolve lc_body_t_abs_2 : lngen.
Lemma lc_body_t_case_3 :
∀ L1 M1 N1,
lc_trm (t_case L1 M1 N1) →
body_trm_wrt_trm N1.
Proof.
default_simp.
Qed.
Hint Resolve lc_body_t_case_3 : lngen.
Lemma lc_body_itrm_abs_2 :
∀ iA1 iN1,
lc_itrm (itrm_abs iA1 iN1) →
body_itrm_wrt_itrm iN1.
Proof.
default_simp.
Qed.
Hint Resolve lc_body_itrm_abs_2 : lngen.
Lemma lc_trm_unique :
∀ L1 (proof2 proof3 : lc_trm L1), proof2 = proof3.
Proof.
pose proof lc_trm_unique_mutual as H; intuition eauto.
Qed.
Hint Resolve lc_trm_unique : lngen.
Lemma lc_itrm_unique :
∀ iL1 (proof2 proof3 : lc_itrm iL1), proof2 = proof3.
Proof.
pose proof lc_itrm_unique_mutual as H; intuition eauto.
Qed.
Hint Resolve lc_itrm_unique : lngen.
Lemma lc_trm_of_lc_set_trm :
∀ L1, lc_set_trm L1 → lc_trm L1.
Proof.
pose proof lc_trm_of_lc_set_trm_mutual as H; intuition eauto.
Qed.
Hint Resolve lc_trm_of_lc_set_trm : lngen.
Lemma lc_itrm_of_lc_set_itrm :
∀ iL1, lc_set_itrm iL1 → lc_itrm iL1.
Proof.
pose proof lc_itrm_of_lc_set_itrm_mutual as H; intuition eauto.
Qed.
Hint Resolve lc_itrm_of_lc_set_itrm : lngen.
Lemma lc_set_trm_of_lc_trm :
∀ L1,
lc_trm L1 →
lc_set_trm L1.
Proof.
intros L1; intros;
pose proof (lc_set_trm_of_lc_trm_size_mutual (size_trm L1));
intuition eauto.
Qed.
Hint Resolve lc_set_trm_of_lc_trm : lngen.
Lemma lc_set_itrm_of_lc_itrm :
∀ iL1,
lc_itrm iL1 →
lc_set_itrm iL1.
Proof.
intros iL1; intros;
pose proof (lc_set_itrm_of_lc_itrm_size_mutual (size_itrm iL1));
intuition eauto.
Qed.
Hint Resolve lc_set_itrm_of_lc_itrm : lngen.
Ltac default_auto ::= auto with lngen; tauto.
Ltac default_autorewrite ::= fail.
Lemma close_trm_wrt_trm_lc_trm :
∀ L1 x1,
lc_trm L1 →
x1 `notin` fv_trm L1 →
close_trm_wrt_trm x1 L1 = L1.
Proof.
unfold close_trm_wrt_trm; default_simp.
Qed.
Hint Resolve close_trm_wrt_trm_lc_trm : lngen.
Hint Rewrite close_trm_wrt_trm_lc_trm using solve [auto] : lngen.
Lemma close_itrm_wrt_itrm_lc_itrm :
∀ iL1 ix1,
lc_itrm iL1 →
ix1 `notin` fv_itrm iL1 →
close_itrm_wrt_itrm ix1 iL1 = iL1.
Proof.
unfold close_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve close_itrm_wrt_itrm_lc_itrm : lngen.
Hint Rewrite close_itrm_wrt_itrm_lc_itrm using solve [auto] : lngen.
Lemma open_trm_wrt_trm_lc_trm :
∀ L2 L1,
lc_trm L2 →
open_trm_wrt_trm L2 L1 = L2.
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.
Hint Resolve open_trm_wrt_trm_lc_trm : lngen.
Hint Rewrite open_trm_wrt_trm_lc_trm using solve [auto] : lngen.
Lemma open_itrm_wrt_itrm_lc_itrm :
∀ iL2 iL1,
lc_itrm iL2 →
open_itrm_wrt_itrm iL2 iL1 = iL2.
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve open_itrm_wrt_itrm_lc_itrm : lngen.
Hint Rewrite open_itrm_wrt_itrm_lc_itrm using solve [auto] : lngen.
Ltac default_auto ::= auto with set lngen; tauto.
Ltac default_autorewrite ::= autorewrite with lngen.
Lemma fv_trm_close_trm_wrt_trm :
∀ L1 x1,
fv_trm (close_trm_wrt_trm x1 L1) [=] remove x1 (fv_trm L1).
Proof.
unfold close_trm_wrt_trm; default_simp.
Qed.
Hint Resolve fv_trm_close_trm_wrt_trm : lngen.
Hint Rewrite fv_trm_close_trm_wrt_trm using solve [auto] : lngen.
Lemma fv_itrm_close_itrm_wrt_itrm :
∀ iL1 ix1,
fv_itrm (close_itrm_wrt_itrm ix1 iL1) [=] remove ix1 (fv_itrm iL1).
Proof.
unfold close_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve fv_itrm_close_itrm_wrt_itrm : lngen.
Hint Rewrite fv_itrm_close_itrm_wrt_itrm using solve [auto] : lngen.
Lemma fv_trm_open_trm_wrt_trm_lower :
∀ L1 L2,
fv_trm L1 [<=] fv_trm (open_trm_wrt_trm L1 L2).
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.
Hint Resolve fv_trm_open_trm_wrt_trm_lower : lngen.
Lemma fv_itrm_open_itrm_wrt_itrm_lower :
∀ iL1 iL2,
fv_itrm iL1 [<=] fv_itrm (open_itrm_wrt_itrm iL1 iL2).
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve fv_itrm_open_itrm_wrt_itrm_lower : lngen.
Lemma fv_trm_open_trm_wrt_trm_upper :
∀ L1 L2,
fv_trm (open_trm_wrt_trm L1 L2) [<=] fv_trm L2 `union` fv_trm L1.
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.
Hint Resolve fv_trm_open_trm_wrt_trm_upper : lngen.
Lemma fv_itrm_open_itrm_wrt_itrm_upper :
∀ iL1 iL2,
fv_itrm (open_itrm_wrt_itrm iL1 iL2) [<=] fv_itrm iL2 `union` fv_itrm iL1.
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve fv_itrm_open_itrm_wrt_itrm_upper : lngen.
Lemma fv_trm_subst_trm_fresh :
∀ L1 L2 x1,
x1 `notin` fv_trm L1 →
fv_trm (subst_trm L2 x1 L1) [=] fv_trm L1.
Proof.
pose proof fv_trm_subst_trm_fresh_mutual as H; intuition eauto.
Qed.
Hint Resolve fv_trm_subst_trm_fresh : lngen.
Hint Rewrite fv_trm_subst_trm_fresh using solve [auto] : lngen.
Lemma fv_itrm_subst_itrm_fresh :
∀ iL1 iL2 ix1,
ix1 `notin` fv_itrm iL1 →
fv_itrm (subst_itrm iL2 ix1 iL1) [=] fv_itrm iL1.
Proof.
pose proof fv_itrm_subst_itrm_fresh_mutual as H; intuition eauto.
Qed.
Hint Resolve fv_itrm_subst_itrm_fresh : lngen.
Hint Rewrite fv_itrm_subst_itrm_fresh using solve [auto] : lngen.
Lemma fv_trm_subst_trm_lower :
∀ L1 L2 x1,
remove x1 (fv_trm L1) [<=] fv_trm (subst_trm L2 x1 L1).
Proof.
pose proof fv_trm_subst_trm_lower_mutual as H; intuition eauto.
Qed.
Hint Resolve fv_trm_subst_trm_lower : lngen.
Lemma fv_itrm_subst_itrm_lower :
∀ iL1 iL2 ix1,
remove ix1 (fv_itrm iL1) [<=] fv_itrm (subst_itrm iL2 ix1 iL1).
Proof.
pose proof fv_itrm_subst_itrm_lower_mutual as H; intuition eauto.
Qed.
Hint Resolve fv_itrm_subst_itrm_lower : lngen.
Lemma fv_trm_subst_trm_notin :
∀ L1 L2 x1 x2,
x2 `notin` fv_trm L1 →
x2 `notin` fv_trm L2 →
x2 `notin` fv_trm (subst_trm L2 x1 L1).
Proof.
pose proof fv_trm_subst_trm_notin_mutual as H; intuition eauto.
Qed.
Hint Resolve fv_trm_subst_trm_notin : lngen.
Lemma fv_itrm_subst_itrm_notin :
∀ iL1 iL2 ix1 ix2,
ix2 `notin` fv_itrm iL1 →
ix2 `notin` fv_itrm iL2 →
ix2 `notin` fv_itrm (subst_itrm iL2 ix1 iL1).
Proof.
pose proof fv_itrm_subst_itrm_notin_mutual as H; intuition eauto.
Qed.
Hint Resolve fv_itrm_subst_itrm_notin : lngen.
Lemma fv_trm_subst_trm_upper :
∀ L1 L2 x1,
fv_trm (subst_trm L2 x1 L1) [<=] fv_trm L2 `union` remove x1 (fv_trm L1).
Proof.
pose proof fv_trm_subst_trm_upper_mutual as H; intuition eauto.
Qed.
Hint Resolve fv_trm_subst_trm_upper : lngen.
Lemma fv_itrm_subst_itrm_upper :
∀ iL1 iL2 ix1,
fv_itrm (subst_itrm iL2 ix1 iL1) [<=] fv_itrm iL2 `union` remove ix1 (fv_itrm iL1).
Proof.
pose proof fv_itrm_subst_itrm_upper_mutual as H; intuition eauto.
Qed.
Hint Resolve fv_itrm_subst_itrm_upper : lngen.
Ltac default_auto ::= auto with lngen brute_force; tauto.
Ltac default_autorewrite ::= autorewrite with lngen.
Lemma subst_trm_close_trm_wrt_trm_rec :
∀ L2 L1 x1 x2 n1,
degree_trm_wrt_trm n1 L1 →
x1 ≠ x2 →
x2 `notin` fv_trm L1 →
subst_trm L1 x1 (close_trm_wrt_trm_rec n1 x2 L2) = close_trm_wrt_trm_rec n1 x2 (subst_trm L1 x1 L2).
Proof.
pose proof subst_trm_close_trm_wrt_trm_rec_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_trm_close_trm_wrt_trm_rec : lngen.
Lemma subst_itrm_close_itrm_wrt_itrm_rec :
∀ iL2 iL1 ix1 ix2 n1,
degree_itrm_wrt_itrm n1 iL1 →
ix1 ≠ ix2 →
ix2 `notin` fv_itrm iL1 →
subst_itrm iL1 ix1 (close_itrm_wrt_itrm_rec n1 ix2 iL2) = close_itrm_wrt_itrm_rec n1 ix2 (subst_itrm iL1 ix1 iL2).
Proof.
pose proof subst_itrm_close_itrm_wrt_itrm_rec_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_itrm_close_itrm_wrt_itrm_rec : lngen.
Lemma subst_trm_close_trm_wrt_trm :
∀ L2 L1 x1 x2,
lc_trm L1 → x1 ≠ x2 →
x2 `notin` fv_trm L1 →
subst_trm L1 x1 (close_trm_wrt_trm x2 L2) = close_trm_wrt_trm x2 (subst_trm L1 x1 L2).
Proof.
unfold close_trm_wrt_trm; default_simp.
Qed.
Hint Resolve subst_trm_close_trm_wrt_trm : lngen.
Lemma subst_itrm_close_itrm_wrt_itrm :
∀ iL2 iL1 ix1 ix2,
lc_itrm iL1 → ix1 ≠ ix2 →
ix2 `notin` fv_itrm iL1 →
subst_itrm iL1 ix1 (close_itrm_wrt_itrm ix2 iL2) = close_itrm_wrt_itrm ix2 (subst_itrm iL1 ix1 iL2).
Proof.
unfold close_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve subst_itrm_close_itrm_wrt_itrm : lngen.
Lemma subst_trm_degree_trm_wrt_trm :
∀ L1 L2 x1 n1,
degree_trm_wrt_trm n1 L1 →
degree_trm_wrt_trm n1 L2 →
degree_trm_wrt_trm n1 (subst_trm L2 x1 L1).
Proof.
pose proof subst_trm_degree_trm_wrt_trm_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_trm_degree_trm_wrt_trm : lngen.
Lemma subst_itrm_degree_itrm_wrt_itrm :
∀ iL1 iL2 ix1 n1,
degree_itrm_wrt_itrm n1 iL1 →
degree_itrm_wrt_itrm n1 iL2 →
degree_itrm_wrt_itrm n1 (subst_itrm iL2 ix1 iL1).
Proof.
pose proof subst_itrm_degree_itrm_wrt_itrm_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_itrm_degree_itrm_wrt_itrm : lngen.
Lemma subst_trm_fresh_eq :
∀ L2 L1 x1,
x1 `notin` fv_trm L2 →
subst_trm L1 x1 L2 = L2.
Proof.
pose proof subst_trm_fresh_eq_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_trm_fresh_eq : lngen.
Hint Rewrite subst_trm_fresh_eq using solve [auto] : lngen.
Lemma subst_itrm_fresh_eq :
∀ iL2 iL1 ix1,
ix1 `notin` fv_itrm iL2 →
subst_itrm iL1 ix1 iL2 = iL2.
Proof.
pose proof subst_itrm_fresh_eq_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_itrm_fresh_eq : lngen.
Hint Rewrite subst_itrm_fresh_eq using solve [auto] : lngen.
Lemma subst_trm_fresh_same :
∀ L2 L1 x1,
x1 `notin` fv_trm L1 →
x1 `notin` fv_trm (subst_trm L1 x1 L2).
Proof.
pose proof subst_trm_fresh_same_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_trm_fresh_same : lngen.
Lemma subst_itrm_fresh_same :
∀ iL2 iL1 ix1,
ix1 `notin` fv_itrm iL1 →
ix1 `notin` fv_itrm (subst_itrm iL1 ix1 iL2).
Proof.
pose proof subst_itrm_fresh_same_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_itrm_fresh_same : lngen.
Lemma subst_trm_fresh :
∀ L2 L1 x1 x2,
x1 `notin` fv_trm L2 →
x1 `notin` fv_trm L1 →
x1 `notin` fv_trm (subst_trm L1 x2 L2).
Proof.
pose proof subst_trm_fresh_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_trm_fresh : lngen.
Lemma subst_itrm_fresh :
∀ iL2 iL1 ix1 ix2,
ix1 `notin` fv_itrm iL2 →
ix1 `notin` fv_itrm iL1 →
ix1 `notin` fv_itrm (subst_itrm iL1 ix2 iL2).
Proof.
pose proof subst_itrm_fresh_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_itrm_fresh : lngen.
Lemma subst_trm_lc_trm :
∀ L1 L2 x1,
lc_trm L1 →
lc_trm L2 →
lc_trm (subst_trm L2 x1 L1).
Proof.
default_simp.
Qed.
Hint Resolve subst_trm_lc_trm : lngen.
Lemma subst_itrm_lc_itrm :
∀ iL1 iL2 ix1,
lc_itrm iL1 →
lc_itrm iL2 →
lc_itrm (subst_itrm iL2 ix1 iL1).
Proof.
default_simp.
Qed.
Hint Resolve subst_itrm_lc_itrm : lngen.
Lemma subst_trm_open_trm_wrt_trm :
∀ L3 L1 L2 x1,
lc_trm L1 →
subst_trm L1 x1 (open_trm_wrt_trm L3 L2) = open_trm_wrt_trm (subst_trm L1 x1 L3) (subst_trm L1 x1 L2).
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.
Hint Resolve subst_trm_open_trm_wrt_trm : lngen.
Lemma subst_itrm_open_itrm_wrt_itrm :
∀ iL3 iL1 iL2 ix1,
lc_itrm iL1 →
subst_itrm iL1 ix1 (open_itrm_wrt_itrm iL3 iL2) = open_itrm_wrt_itrm (subst_itrm iL1 ix1 iL3) (subst_itrm iL1 ix1 iL2).
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve subst_itrm_open_itrm_wrt_itrm : lngen.
Lemma subst_trm_open_trm_wrt_trm_var :
∀ L2 L1 x1 x2,
x1 ≠ x2 →
lc_trm L1 →
open_trm_wrt_trm (subst_trm L1 x1 L2) (t_var_f x2) = subst_trm L1 x1 (open_trm_wrt_trm L2 (t_var_f x2)).
Proof.
intros; rewrite subst_trm_open_trm_wrt_trm; default_simp.
Qed.
Hint Resolve subst_trm_open_trm_wrt_trm_var : lngen.
Lemma subst_itrm_open_itrm_wrt_itrm_var :
∀ iL2 iL1 ix1 ix2,
ix1 ≠ ix2 →
lc_itrm iL1 →
open_itrm_wrt_itrm (subst_itrm iL1 ix1 iL2) (itrm_var_f ix2) = subst_itrm iL1 ix1 (open_itrm_wrt_itrm iL2 (itrm_var_f ix2)).
Proof.
intros; rewrite subst_itrm_open_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve subst_itrm_open_itrm_wrt_itrm_var : lngen.
Lemma subst_trm_spec :
∀ L1 L2 x1,
subst_trm L2 x1 L1 = open_trm_wrt_trm (close_trm_wrt_trm x1 L1) L2.
Proof.
unfold close_trm_wrt_trm; unfold open_trm_wrt_trm; default_simp.
Qed.
Hint Resolve subst_trm_spec : lngen.
Lemma subst_itrm_spec :
∀ iL1 iL2 ix1,
subst_itrm iL2 ix1 iL1 = open_itrm_wrt_itrm (close_itrm_wrt_itrm ix1 iL1) iL2.
Proof.
unfold close_itrm_wrt_itrm; unfold open_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve subst_itrm_spec : lngen.
Lemma subst_trm_subst_trm :
∀ L1 L2 L3 x2 x1,
x2 `notin` fv_trm L2 →
x2 ≠ x1 →
subst_trm L2 x1 (subst_trm L3 x2 L1) = subst_trm (subst_trm L2 x1 L3) x2 (subst_trm L2 x1 L1).
Proof.
pose proof subst_trm_subst_trm_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_trm_subst_trm : lngen.
Lemma subst_itrm_subst_itrm :
∀ iL1 iL2 iL3 ix2 ix1,
ix2 `notin` fv_itrm iL2 →
ix2 ≠ ix1 →
subst_itrm iL2 ix1 (subst_itrm iL3 ix2 iL1) = subst_itrm (subst_itrm iL2 ix1 iL3) ix2 (subst_itrm iL2 ix1 iL1).
Proof.
pose proof subst_itrm_subst_itrm_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_itrm_subst_itrm : lngen.
Lemma subst_trm_close_trm_wrt_trm_open_trm_wrt_trm :
∀ L2 L1 x1 x2,
x2 `notin` fv_trm L2 →
x2 `notin` fv_trm L1 →
x2 ≠ x1 →
lc_trm L1 →
subst_trm L1 x1 L2 = close_trm_wrt_trm x2 (subst_trm L1 x1 (open_trm_wrt_trm L2 (t_var_f x2))).
Proof.
unfold close_trm_wrt_trm; unfold open_trm_wrt_trm; default_simp.
Qed.
Hint Resolve subst_trm_close_trm_wrt_trm_open_trm_wrt_trm : lngen.
Lemma subst_itrm_close_itrm_wrt_itrm_open_itrm_wrt_itrm :
∀ iL2 iL1 ix1 ix2,
ix2 `notin` fv_itrm iL2 →
ix2 `notin` fv_itrm iL1 →
ix2 ≠ ix1 →
lc_itrm iL1 →
subst_itrm iL1 ix1 iL2 = close_itrm_wrt_itrm ix2 (subst_itrm iL1 ix1 (open_itrm_wrt_itrm iL2 (itrm_var_f ix2))).
Proof.
unfold close_itrm_wrt_itrm; unfold open_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve subst_itrm_close_itrm_wrt_itrm_open_itrm_wrt_itrm : lngen.
Lemma subst_trm_t_abs :
∀ x2 A1 N1 L1 x1,
lc_trm L1 →
x2 `notin` fv_trm L1 `union` fv_trm N1 `union` singleton x1 →
subst_trm L1 x1 (t_abs A1 N1) = t_abs (A1) (close_trm_wrt_trm x2 (subst_trm L1 x1 (open_trm_wrt_trm N1 (t_var_f x2)))).
Proof.
default_simp.
Qed.
Hint Resolve subst_trm_t_abs : lngen.
Lemma subst_trm_t_case :
∀ x2 L2 M1 N1 L1 x1,
lc_trm L1 →
x2 `notin` fv_trm L1 `union` fv_trm N1 `union` singleton x1 →
subst_trm L1 x1 (t_case L2 M1 N1) = t_case (subst_trm L1 x1 L2) (subst_trm L1 x1 M1) (close_trm_wrt_trm x2 (subst_trm L1 x1 (open_trm_wrt_trm N1 (t_var_f x2)))).
Proof.
default_simp.
Qed.
Hint Resolve subst_trm_t_case : lngen.
Lemma subst_itrm_itrm_abs :
∀ ix2 iA1 iN1 iL1 ix1,
lc_itrm iL1 →
ix2 `notin` fv_itrm iL1 `union` fv_itrm iN1 `union` singleton ix1 →
subst_itrm iL1 ix1 (itrm_abs iA1 iN1) = itrm_abs (iA1) (close_itrm_wrt_itrm ix2 (subst_itrm iL1 ix1 (open_itrm_wrt_itrm iN1 (itrm_var_f ix2)))).
Proof.
default_simp.
Qed.
Hint Resolve subst_itrm_itrm_abs : lngen.
Lemma subst_trm_intro_rec :
∀ L1 x1 L2 n1,
x1 `notin` fv_trm L1 →
open_trm_wrt_trm_rec n1 L2 L1 = subst_trm L2 x1 (open_trm_wrt_trm_rec n1 (t_var_f x1) L1).
Proof.
pose proof subst_trm_intro_rec_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_trm_intro_rec : lngen.
Hint Rewrite subst_trm_intro_rec using solve [auto] : lngen.
Lemma subst_itrm_intro_rec :
∀ iL1 ix1 iL2 n1,
ix1 `notin` fv_itrm iL1 →
open_itrm_wrt_itrm_rec n1 iL2 iL1 = subst_itrm iL2 ix1 (open_itrm_wrt_itrm_rec n1 (itrm_var_f ix1) iL1).
Proof.
pose proof subst_itrm_intro_rec_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_itrm_intro_rec : lngen.
Hint Rewrite subst_itrm_intro_rec using solve [auto] : lngen.
Lemma subst_trm_intro :
∀ x1 L1 L2,
x1 `notin` fv_trm L1 →
open_trm_wrt_trm L1 L2 = subst_trm L2 x1 (open_trm_wrt_trm L1 (t_var_f x1)).
Proof.
unfold open_trm_wrt_trm; default_simp.
Qed.
Hint Resolve subst_trm_intro : lngen.
Lemma subst_itrm_intro :
∀ ix1 iL1 iL2,
ix1 `notin` fv_itrm iL1 →
open_itrm_wrt_itrm iL1 iL2 = subst_itrm iL2 ix1 (open_itrm_wrt_itrm iL1 (itrm_var_f ix1)).
Proof.
unfold open_itrm_wrt_itrm; default_simp.
Qed.
Hint Resolve subst_itrm_intro : lngen.
Ltac default_auto ::= auto; tauto.
Ltac default_autorewrite ::= fail.