Library Stlc.Lemmas
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Program.Equality.
Require Export Metalib.Metatheory.
Require Export Metalib.LibLNgen.
Require Export Stlc.Definitions.
Require Import Coq.Program.Equality.
Require Export Metalib.Metatheory.
Require Export Metalib.LibLNgen.
Require Export Stlc.Definitions.
NOTE: Auxiliary theorems are hidden in generated documentation.
In general, there is a _rec version of every lemma involving
open and close.
Fixpoint close_exp_wrt_exp_rec (n1 : nat) (x1 : var) (e1 : exp) {struct e1} : exp :=
match e1 with
| abs e2 ⇒ abs (close_exp_wrt_exp_rec (S n1) x1 e2)
| var_f x2 ⇒ if (x1 == x2) then (var_b n1) else (var_f x2)
| var_b n2 ⇒ if (lt_ge_dec n2 n1) then (var_b n2) else (var_b (S n2))
| app e2 e3 ⇒ app (close_exp_wrt_exp_rec n1 x1 e2) (close_exp_wrt_exp_rec n1 x1 e3)
end.
Definition close_exp_wrt_exp x1 e1 := close_exp_wrt_exp_rec 0 x1 e1.
Fixpoint size_typ (T1 : typ) {struct T1} : nat :=
match T1 with
| typ_base ⇒ 1
| typ_arrow T2 T3 ⇒ 1 + (size_typ T2) + (size_typ T3)
end.
Fixpoint size_exp (e1 : exp) {struct e1} : nat :=
match e1 with
| abs e2 ⇒ 1 + (size_exp e2)
| var_f x1 ⇒ 1
| var_b n1 ⇒ 1
| app e2 e3 ⇒ 1 + (size_exp e2) + (size_exp e3)
end.
Inductive degree_exp_wrt_exp : nat → exp → Prop :=
| degree_wrt_exp_abs : ∀ n1 e1,
degree_exp_wrt_exp (S n1) e1 →
degree_exp_wrt_exp n1 (abs e1)
| degree_wrt_exp_var_f : ∀ n1 x1,
degree_exp_wrt_exp n1 (var_f x1)
| degree_wrt_exp_var_b : ∀ n1 n2,
lt n2 n1 →
degree_exp_wrt_exp n1 (var_b n2)
| degree_wrt_exp_app : ∀ n1 e1 e2,
degree_exp_wrt_exp n1 e1 →
degree_exp_wrt_exp n1 e2 →
degree_exp_wrt_exp n1 (app e1 e2).
Scheme degree_exp_wrt_exp_ind' := Induction for degree_exp_wrt_exp Sort Prop.
Definition degree_exp_wrt_exp_mutind :=
fun H1 H2 H3 H4 H5 ⇒
degree_exp_wrt_exp_ind' H1 H2 H3 H4 H5.
Hint Constructors degree_exp_wrt_exp : core lngen.
Definition body_exp_wrt_exp e1 := ∀ x1, lc_exp (open_exp_wrt_exp e1 (var_f x1)).
Hint Unfold body_exp_wrt_exp.
Redefine some tactics.
Ltac default_case_split ::=
first
[ progress destruct_notin
| progress destruct_sum
| progress safe_f_equal
].
Theorems about size
Ltac default_auto ::= auto with arith lngen; tauto.
Ltac default_autorewrite ::= fail.
Lemma size_typ_min :
∀ T1, 1 ≤ size_typ T1.
Proof.
pose proof size_typ_min_mutual as H; intuition eauto.
Qed.
Hint Resolve size_typ_min : lngen.
Lemma size_exp_min :
∀ e1, 1 ≤ size_exp e1.
Proof.
pose proof size_exp_min_mutual as H; intuition eauto.
Qed.
Hint Resolve size_exp_min : lngen.
Lemma size_exp_close_exp_wrt_exp :
∀ e1 x1,
size_exp (close_exp_wrt_exp x1 e1) = size_exp e1.
Proof.
unfold close_exp_wrt_exp; default_simp.
Qed.
Hint Resolve size_exp_close_exp_wrt_exp : lngen.
Hint Rewrite size_exp_close_exp_wrt_exp using solve [auto] : lngen.
Lemma size_exp_open_exp_wrt_exp :
∀ e1 e2,
size_exp e1 ≤ size_exp (open_exp_wrt_exp e1 e2).
Proof.
unfold open_exp_wrt_exp; default_simp.
Qed.
Hint Resolve size_exp_open_exp_wrt_exp : lngen.
Lemma size_exp_open_exp_wrt_exp_var :
∀ e1 x1,
size_exp (open_exp_wrt_exp e1 (var_f x1)) = size_exp e1.
Proof.
unfold open_exp_wrt_exp; default_simp.
Qed.
Hint Resolve size_exp_open_exp_wrt_exp_var : lngen.
Hint Rewrite size_exp_open_exp_wrt_exp_var using solve [auto] : lngen.
Ltac default_auto ::= auto with lngen; tauto.
Ltac default_autorewrite ::= fail.
Lemma degree_exp_wrt_exp_S :
∀ n1 e1,
degree_exp_wrt_exp n1 e1 →
degree_exp_wrt_exp (S n1) e1.
Proof.
pose proof degree_exp_wrt_exp_S_mutual as H; intuition eauto.
Qed.
Hint Resolve degree_exp_wrt_exp_S : lngen.
Lemma degree_exp_wrt_exp_O :
∀ n1 e1,
degree_exp_wrt_exp O e1 →
degree_exp_wrt_exp n1 e1.
Proof.
induction n1; default_simp.
Qed.
Hint Resolve degree_exp_wrt_exp_O : lngen.
Lemma degree_exp_wrt_exp_close_exp_wrt_exp :
∀ e1 x1,
degree_exp_wrt_exp 0 e1 →
degree_exp_wrt_exp 1 (close_exp_wrt_exp x1 e1).
Proof.
unfold close_exp_wrt_exp; default_simp.
Qed.
Hint Resolve degree_exp_wrt_exp_close_exp_wrt_exp : lngen.
Lemma degree_exp_wrt_exp_close_exp_wrt_exp_inv :
∀ e1 x1,
degree_exp_wrt_exp 1 (close_exp_wrt_exp x1 e1) →
degree_exp_wrt_exp 0 e1.
Proof.
unfold close_exp_wrt_exp; eauto with lngen.
Qed.
Hint Immediate degree_exp_wrt_exp_close_exp_wrt_exp_inv : lngen.
Lemma degree_exp_wrt_exp_open_exp_wrt_exp :
∀ e1 e2,
degree_exp_wrt_exp 1 e1 →
degree_exp_wrt_exp 0 e2 →
degree_exp_wrt_exp 0 (open_exp_wrt_exp e1 e2).
Proof.
unfold open_exp_wrt_exp; default_simp.
Qed.
Hint Resolve degree_exp_wrt_exp_open_exp_wrt_exp : lngen.
Lemma degree_exp_wrt_exp_open_exp_wrt_exp_inv :
∀ e1 e2,
degree_exp_wrt_exp 0 (open_exp_wrt_exp e1 e2) →
degree_exp_wrt_exp 1 e1.
Proof.
unfold open_exp_wrt_exp; eauto with lngen.
Qed.
Hint Immediate degree_exp_wrt_exp_open_exp_wrt_exp_inv : lngen.
Theorems about open and close
Ltac default_auto ::= auto with lngen brute_force; tauto.
Ltac default_autorewrite ::= fail.
Lemma close_exp_wrt_exp_inj :
∀ e1 e2 x1,
close_exp_wrt_exp x1 e1 = close_exp_wrt_exp x1 e2 →
e1 = e2.
Proof.
unfold close_exp_wrt_exp; eauto with lngen.
Qed.
Hint Immediate close_exp_wrt_exp_inj : lngen.
Lemma close_exp_wrt_exp_open_exp_wrt_exp :
∀ e1 x1,
x1 `notin` fv_exp e1 →
close_exp_wrt_exp x1 (open_exp_wrt_exp e1 (var_f x1)) = e1.
Proof.
unfold close_exp_wrt_exp; unfold open_exp_wrt_exp; default_simp.
Qed.
Hint Resolve close_exp_wrt_exp_open_exp_wrt_exp : lngen.
Hint Rewrite close_exp_wrt_exp_open_exp_wrt_exp using solve [auto] : lngen.
Lemma open_exp_wrt_exp_close_exp_wrt_exp :
∀ e1 x1,
open_exp_wrt_exp (close_exp_wrt_exp x1 e1) (var_f x1) = e1.
Proof.
unfold close_exp_wrt_exp; unfold open_exp_wrt_exp; default_simp.
Qed.
Hint Resolve open_exp_wrt_exp_close_exp_wrt_exp : lngen.
Hint Rewrite open_exp_wrt_exp_close_exp_wrt_exp using solve [auto] : lngen.
Lemma open_exp_wrt_exp_inj :
∀ e2 e1 x1,
x1 `notin` fv_exp e2 →
x1 `notin` fv_exp e1 →
open_exp_wrt_exp e2 (var_f x1) = open_exp_wrt_exp e1 (var_f x1) →
e2 = e1.
Proof.
unfold open_exp_wrt_exp; eauto with lngen.
Qed.
Hint Immediate open_exp_wrt_exp_inj : lngen.
Ltac default_auto ::= auto with lngen brute_force; tauto.
Ltac default_autorewrite ::= autorewrite with lngen.
Lemma degree_exp_wrt_exp_of_lc_exp :
∀ e1,
lc_exp e1 →
degree_exp_wrt_exp 0 e1.
Proof.
pose proof degree_exp_wrt_exp_of_lc_exp_mutual as H; intuition eauto.
Qed.
Hint Resolve degree_exp_wrt_exp_of_lc_exp : lngen.
Lemma lc_exp_of_degree :
∀ e1,
degree_exp_wrt_exp 0 e1 →
lc_exp e1.
Proof.
intros e1; intros;
pose proof (lc_exp_of_degree_size_mutual (size_exp e1));
intuition eauto.
Qed.
Hint Resolve lc_exp_of_degree : lngen.
Ltac typ_lc_exists_tac :=
repeat (match goal with
| H : _ |- _ ⇒
fail 1
end).
Ltac exp_lc_exists_tac :=
repeat (match goal with
| H : _ |- _ ⇒
let J1 := fresh in pose proof H as J1; apply degree_exp_wrt_exp_of_lc_exp in J1; clear H
end).
Lemma lc_abs_exists :
∀ x1 e1,
lc_exp (open_exp_wrt_exp e1 (var_f x1)) →
lc_exp (abs e1).
Proof.
intros; exp_lc_exists_tac; eauto with lngen.
Qed.
Hint Extern 1 (lc_exp (abs _)) ⇒
let x1 := fresh in
pick_fresh x1;
apply (lc_abs_exists x1).
Lemma lc_body_exp_wrt_exp :
∀ e1 e2,
body_exp_wrt_exp e1 →
lc_exp e2 →
lc_exp (open_exp_wrt_exp e1 e2).
Proof.
unfold body_exp_wrt_exp;
default_simp;
let x1 := fresh "x" in
pick_fresh x1;
specialize_all x1;
exp_lc_exists_tac;
eauto with lngen.
Qed.
Hint Resolve lc_body_exp_wrt_exp : lngen.
Lemma lc_body_abs_1 :
∀ e1,
lc_exp (abs e1) →
body_exp_wrt_exp e1.
Proof.
default_simp.
Qed.
Hint Resolve lc_body_abs_1 : lngen.
More theorems about open and close
Ltac default_auto ::= auto with lngen; tauto.
Ltac default_autorewrite ::= fail.
Lemma close_exp_wrt_exp_lc_exp :
∀ e1 x1,
lc_exp e1 →
x1 `notin` fv_exp e1 →
close_exp_wrt_exp x1 e1 = e1.
Proof.
unfold close_exp_wrt_exp; default_simp.
Qed.
Hint Resolve close_exp_wrt_exp_lc_exp : lngen.
Hint Rewrite close_exp_wrt_exp_lc_exp using solve [auto] : lngen.
Lemma open_exp_wrt_exp_lc_exp :
∀ e2 e1,
lc_exp e2 →
open_exp_wrt_exp e2 e1 = e2.
Proof.
unfold open_exp_wrt_exp; default_simp.
Qed.
Hint Resolve open_exp_wrt_exp_lc_exp : lngen.
Hint Rewrite open_exp_wrt_exp_lc_exp using solve [auto] : lngen.
Ltac default_auto ::= auto with set lngen; tauto.
Ltac default_autorewrite ::= autorewrite with lngen.
Lemma fv_exp_close_exp_wrt_exp :
∀ e1 x1,
fv_exp (close_exp_wrt_exp x1 e1) [=] remove x1 (fv_exp e1).
Proof.
unfold close_exp_wrt_exp; default_simp.
Qed.
Hint Resolve fv_exp_close_exp_wrt_exp : lngen.
Hint Rewrite fv_exp_close_exp_wrt_exp using solve [auto] : lngen.
Lemma fv_exp_open_exp_wrt_exp_lower :
∀ e1 e2,
fv_exp e1 [<=] fv_exp (open_exp_wrt_exp e1 e2).
Proof.
unfold open_exp_wrt_exp; default_simp.
Qed.
Hint Resolve fv_exp_open_exp_wrt_exp_lower : lngen.
Lemma fv_exp_open_exp_wrt_exp_upper :
∀ e1 e2,
fv_exp (open_exp_wrt_exp e1 e2) [<=] fv_exp e2 `union` fv_exp e1.
Proof.
unfold open_exp_wrt_exp; default_simp.
Qed.
Hint Resolve fv_exp_open_exp_wrt_exp_upper : lngen.
Lemma fv_exp_subst_exp_fresh :
∀ e1 e2 x1,
x1 `notin` fv_exp e1 →
fv_exp (subst_exp e2 x1 e1) [=] fv_exp e1.
Proof.
pose proof fv_exp_subst_exp_fresh_mutual as H; intuition eauto.
Qed.
Hint Resolve fv_exp_subst_exp_fresh : lngen.
Hint Rewrite fv_exp_subst_exp_fresh using solve [auto] : lngen.
Lemma fv_exp_subst_exp_lower :
∀ e1 e2 x1,
remove x1 (fv_exp e1) [<=] fv_exp (subst_exp e2 x1 e1).
Proof.
pose proof fv_exp_subst_exp_lower_mutual as H; intuition eauto.
Qed.
Hint Resolve fv_exp_subst_exp_lower : lngen.
Lemma fv_exp_subst_exp_notin :
∀ e1 e2 x1 x2,
x2 `notin` fv_exp e1 →
x2 `notin` fv_exp e2 →
x2 `notin` fv_exp (subst_exp e2 x1 e1).
Proof.
pose proof fv_exp_subst_exp_notin_mutual as H; intuition eauto.
Qed.
Hint Resolve fv_exp_subst_exp_notin : lngen.
Lemma fv_exp_subst_exp_upper :
∀ e1 e2 x1,
fv_exp (subst_exp e2 x1 e1) [<=] fv_exp e2 `union` remove x1 (fv_exp e1).
Proof.
pose proof fv_exp_subst_exp_upper_mutual as H; intuition eauto.
Qed.
Hint Resolve fv_exp_subst_exp_upper : lngen.
Ltac default_auto ::= auto with lngen brute_force; tauto.
Ltac default_autorewrite ::= autorewrite with lngen.
Lemma subst_exp_close_exp_wrt_exp_rec :
∀ e2 e1 x1 x2 n1,
degree_exp_wrt_exp n1 e1 →
x1 ≠ x2 →
x2 `notin` fv_exp e1 →
subst_exp e1 x1 (close_exp_wrt_exp_rec n1 x2 e2) = close_exp_wrt_exp_rec n1 x2 (subst_exp e1 x1 e2).
Proof.
pose proof subst_exp_close_exp_wrt_exp_rec_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_exp_close_exp_wrt_exp_rec : lngen.
Lemma subst_exp_close_exp_wrt_exp :
∀ e2 e1 x1 x2,
lc_exp e1 → x1 ≠ x2 →
x2 `notin` fv_exp e1 →
subst_exp e1 x1 (close_exp_wrt_exp x2 e2) = close_exp_wrt_exp x2 (subst_exp e1 x1 e2).
Proof.
unfold close_exp_wrt_exp; default_simp.
Qed.
Hint Resolve subst_exp_close_exp_wrt_exp : lngen.
Lemma subst_exp_degree_exp_wrt_exp :
∀ e1 e2 x1 n1,
degree_exp_wrt_exp n1 e1 →
degree_exp_wrt_exp n1 e2 →
degree_exp_wrt_exp n1 (subst_exp e2 x1 e1).
Proof.
pose proof subst_exp_degree_exp_wrt_exp_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_exp_degree_exp_wrt_exp : lngen.
Lemma subst_exp_fresh_eq :
∀ e2 e1 x1,
x1 `notin` fv_exp e2 →
subst_exp e1 x1 e2 = e2.
Proof.
pose proof subst_exp_fresh_eq_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_exp_fresh_eq : lngen.
Hint Rewrite subst_exp_fresh_eq using solve [auto] : lngen.
Lemma subst_exp_fresh_same :
∀ e2 e1 x1,
x1 `notin` fv_exp e1 →
x1 `notin` fv_exp (subst_exp e1 x1 e2).
Proof.
pose proof subst_exp_fresh_same_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_exp_fresh_same : lngen.
Lemma subst_exp_fresh :
∀ e2 e1 x1 x2,
x1 `notin` fv_exp e2 →
x1 `notin` fv_exp e1 →
x1 `notin` fv_exp (subst_exp e1 x2 e2).
Proof.
pose proof subst_exp_fresh_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_exp_fresh : lngen.
Lemma subst_exp_lc_exp :
∀ e1 e2 x1,
lc_exp e1 →
lc_exp e2 →
lc_exp (subst_exp e2 x1 e1).
Proof.
default_simp.
Qed.
Hint Resolve subst_exp_lc_exp : lngen.
Lemma subst_exp_open_exp_wrt_exp :
∀ e3 e1 e2 x1,
lc_exp e1 →
subst_exp e1 x1 (open_exp_wrt_exp e3 e2) = open_exp_wrt_exp (subst_exp e1 x1 e3) (subst_exp e1 x1 e2).
Proof.
unfold open_exp_wrt_exp; default_simp.
Qed.
Hint Resolve subst_exp_open_exp_wrt_exp : lngen.
Lemma subst_exp_open_exp_wrt_exp_var :
∀ e2 e1 x1 x2,
x1 ≠ x2 →
lc_exp e1 →
open_exp_wrt_exp (subst_exp e1 x1 e2) (var_f x2) = subst_exp e1 x1 (open_exp_wrt_exp e2 (var_f x2)).
Proof.
intros; rewrite subst_exp_open_exp_wrt_exp; default_simp.
Qed.
Hint Resolve subst_exp_open_exp_wrt_exp_var : lngen.
Lemma subst_exp_spec :
∀ e1 e2 x1,
subst_exp e2 x1 e1 = open_exp_wrt_exp (close_exp_wrt_exp x1 e1) e2.
Proof.
unfold close_exp_wrt_exp; unfold open_exp_wrt_exp; default_simp.
Qed.
Hint Resolve subst_exp_spec : lngen.
Lemma subst_exp_subst_exp :
∀ e1 e2 e3 x2 x1,
x2 `notin` fv_exp e2 →
x2 ≠ x1 →
subst_exp e2 x1 (subst_exp e3 x2 e1) = subst_exp (subst_exp e2 x1 e3) x2 (subst_exp e2 x1 e1).
Proof.
pose proof subst_exp_subst_exp_mutual as H; intuition eauto.
Qed.
Hint Resolve subst_exp_subst_exp : lngen.
Lemma subst_exp_close_exp_wrt_exp_open_exp_wrt_exp :
∀ e2 e1 x1 x2,
x2 `notin` fv_exp e2 →
x2 `notin` fv_exp e1 →
x2 ≠ x1 →
lc_exp e1 →
subst_exp e1 x1 e2 = close_exp_wrt_exp x2 (subst_exp e1 x1 (open_exp_wrt_exp e2 (var_f x2))).
Proof.
unfold close_exp_wrt_exp; unfold open_exp_wrt_exp; default_simp.
Qed.
Hint Resolve subst_exp_close_exp_wrt_exp_open_exp_wrt_exp : lngen.
Lemma subst_exp_abs :
∀ x2 e2 e1 x1,
lc_exp e1 →
x2 `notin` fv_exp e1 `union` fv_exp e2 `union` singleton x1 →
subst_exp e1 x1 (abs e2) = abs (close_exp_wrt_exp x2 (subst_exp e1 x1 (open_exp_wrt_exp e2 (var_f x2)))).
Proof.
default_simp.
Qed.
Hint Resolve subst_exp_abs : lngen.
Lemma subst_exp_intro :
∀ x1 e1 e2,
x1 `notin` fv_exp e1 →
open_exp_wrt_exp e1 e2 = subst_exp e2 x1 (open_exp_wrt_exp e1 (var_f x1)).
Proof.
unfold open_exp_wrt_exp; default_simp.
Qed.
Hint Resolve subst_exp_intro : lngen.
Ltac default_auto ::= auto; tauto.
Ltac default_autorewrite ::= fail.