Library LambdaES_occ
Require Import Metatheory.
Require Import LambdaES_Defs LambdaES_Tactics.
Require Import LambdaES_Infrastructure.
Counts the number of occurences of the bound variable k in t
Fixpoint bv_occ_k (k : nat) (t : pterm) : nat :=
match t with
| pterm_bvar i => if k === i then 1 else 0
| pterm_fvar x => 0
| pterm_abs t1 => bv_occ_k (S k) t1
| pterm_app t1 t2 => (bv_occ_k k t1) + (bv_occ_k k t2)
| pterm_sub t1 t2 => (bv_occ_k (S k) t1) + (bv_occ_k k t2)
end.
match t with
| pterm_bvar i => if k === i then 1 else 0
| pterm_fvar x => 0
| pterm_abs t1 => bv_occ_k (S k) t1
| pterm_app t1 t2 => (bv_occ_k k t1) + (bv_occ_k k t2)
| pterm_sub t1 t2 => (bv_occ_k (S k) t1) + (bv_occ_k k t2)
end.
Number of bounded variables pointing directly above the term
Counts the number of occurences of the free variable x in t
Fixpoint fv_occ (x: var) (t: pterm) : nat :=
match t with
| pterm_bvar k => 0
| pterm_fvar z => if z == x then 1 else 0
| pterm_abs t' => fv_occ x t'
| pterm_app t1 t2 => fv_occ x t1 + fv_occ x t2
| t1[t2] => fv_occ x t1 + fv_occ x t2
end.
match t with
| pterm_bvar k => 0
| pterm_fvar z => if z == x then 1 else 0
| pterm_abs t' => fv_occ x t'
| pterm_app t1 t2 => fv_occ x t1 + fv_occ x t2
| t1[t2] => fv_occ x t1 + fv_occ x t2
end.
Elim tactics for the various bv_occ ? = 0
Ltac local_elim_bv_occ_k H :=
match type of H with
| bv_occ_k 0 (pterm_bvar ?n) = 0 => case_eq n ; intros ; subst ; simpl in H ; try elim_zero_one ; try auto
| bv_occ_k _ (pterm_bvar _) = 0 => simpl in H ; case_nat ; try elim_zero_one ; try auto
| bv_occ_k _ (pterm_fvar _) = 0 => clear H
| bv_occ_k _ (pterm_abs _) = 0 => simpl in H
| bv_occ_k ?k (pterm_app ?t1 ?t2) = 0 =>
simpl in H ;
let Hfresh1 := fresh H in
let Hfresh2 := fresh H in
assert (bv_occ_k k t1 = 0) as Hfresh1 by omega ;
assert (bv_occ_k k t2 = 0) as Hfresh2 by omega ;
clear H
| bv_occ_k ?k (?t1[?t2]) = 0 =>
simpl in H ;
let Hfresh1 := fresh H in
let Hfresh2 := fresh H in
assert (bv_occ_k (S k) t1 = 0) as Hfresh1 by omega ;
assert (bv_occ_k k t2 = 0) as Hfresh2 by omega ;
clear H
end.
Ltac elim_bv_occ :=
match goal with
| H : bv_occ _ = 0 |- _ => unfold bv_occ in H ; local_elim_bv_occ_k H
| H : bv_occ_k _ _ = 0 |- _ => local_elim_bv_occ_k H
end.
match type of H with
| bv_occ_k 0 (pterm_bvar ?n) = 0 => case_eq n ; intros ; subst ; simpl in H ; try elim_zero_one ; try auto
| bv_occ_k _ (pterm_bvar _) = 0 => simpl in H ; case_nat ; try elim_zero_one ; try auto
| bv_occ_k _ (pterm_fvar _) = 0 => clear H
| bv_occ_k _ (pterm_abs _) = 0 => simpl in H
| bv_occ_k ?k (pterm_app ?t1 ?t2) = 0 =>
simpl in H ;
let Hfresh1 := fresh H in
let Hfresh2 := fresh H in
assert (bv_occ_k k t1 = 0) as Hfresh1 by omega ;
assert (bv_occ_k k t2 = 0) as Hfresh2 by omega ;
clear H
| bv_occ_k ?k (?t1[?t2]) = 0 =>
simpl in H ;
let Hfresh1 := fresh H in
let Hfresh2 := fresh H in
assert (bv_occ_k (S k) t1 = 0) as Hfresh1 by omega ;
assert (bv_occ_k k t2 = 0) as Hfresh2 by omega ;
clear H
end.
Ltac elim_bv_occ :=
match goal with
| H : bv_occ _ = 0 |- _ => unfold bv_occ in H ; local_elim_bv_occ_k H
| H : bv_occ_k _ _ = 0 |- _ => local_elim_bv_occ_k H
end.
If a variable does not appear in a pterm, substituting it leaves the pterm intact
Lemma fv_occ_open_var : forall t x y, ~(x = y) -> fv_occ x t = fv_occ x (t^y).
Proof.
intros t. unfold open. generalize 0.
basic_pterm_induction t using (case_nat ; auto ; simpl ; case_var ; auto).
Qed.
Proof.
intros t. unfold open. generalize 0.
basic_pterm_induction t using (case_nat ; auto ; simpl ; case_var ; auto).
Qed.
Open a pterm with a variable z does not change the number of occurences of
the variable x
Lemma fv_open : forall x z t n, x<> z -> fv_occ x (t^z) = n -> fv_occ x t = n.
Proof.
intros x z t n x_neq_z.
unfolds open. generalize 0 as k.
gen n.
induction t ; intros m k fv_occ_.
compare k n ; intro ; simpls ; case_nat ; simpls ; auto.
case_var. assumption.
simpl in *. assumption.
simpls. apply IHt with (k:=S k). assumption.
simpls.
assert(exists n1, fv_occ x ({k ~> pterm_fvar z}t1) = n1).
exists (fv_occ x ({k ~> pterm_fvar z}t1)). reflexivity.
assert(exists n2, fv_occ x ({k ~> pterm_fvar z}t2) = n2).
exists (fv_occ x ({k ~> pterm_fvar z}t2)). reflexivity.
destruct H as [n1 H].
destruct H0 as [n2 H0].
rewrite IHt1 with (k:=k) (n:=n1) ; auto.
rewrite IHt2 with (k:=k) (n:=n2) ; auto.
rewrite H, H0 in fv_occ_.
assumption.
simpls.
assert(exists n1, fv_occ x ({S k ~> pterm_fvar z}t1) = n1).
exists (fv_occ x ({S k ~> pterm_fvar z}t1)). reflexivity.
assert(exists n2, fv_occ x ({k ~> pterm_fvar z}t2) = n2).
exists (fv_occ x ({k ~> pterm_fvar z}t2)). reflexivity.
destruct H as [n1 H].
destruct H0 as [n2 H0].
rewrite IHt1 with (k:=S k) (n:=n1) ; auto.
rewrite IHt2 with (k:=k) (n:=n2) ; auto.
rewrite H, H0 in fv_occ_.
assumption.
Qed.
Lemma fv_occ_close : forall t x y, ~(x=y) -> fv_occ y t = fv_occ y (close t x).
Proof.
intros ; unfold close. generalize 0.
basic_pterm_induction t using (repeat (case_var ; simpl ; auto)).
Qed.
Lemma fv_occ_subs_decompose : forall t y u, fv_occ y u + fv_occ y t = fv_occ y (t[u]).
Proof.
intros. assert(forall x y, x + y = y + x) as H by (intros ; omega).
basic_pterm_induction t.
Qed.
Lemma fv_occ_notin : forall t y, y \notin fv t -> fv_occ y t = 0.
Proof.
intros. induction t ; simpl ; auto.
case_var.
elim H. simpl. VSD.fsetdec.
reflexivity.
simpl in H. rewrite IHt1 ; [|VSD.fsetdec]. rewrite IHt2 ; [|VSD.fsetdec]. reflexivity.
simpl in H. rewrite IHt1 ; [|VSD.fsetdec]. rewrite IHt2 ; [|VSD.fsetdec]. reflexivity.
Qed.
Lemma fv_occ_open : forall t x u, x \notin fv u -> fv_occ x t = fv_occ x (t^^u).
Proof.
intros t. unfold open. generalize 0.
induction t ; intros n' x u x_notin_u ; simpls ; try eauto.
case_nat.
rewrite fv_occ_notin ; auto.
simpl. reflexivity.
Qed.
Lemma subst_fv_occ : forall a b t u, a \notin fv u -> a <> b -> fv_occ a ([b ~> u]t) = fv_occ a t.
Proof.
intros. induction t ; simpls ; auto.
case_var* ; case_var*. apply fv_occ_notin ; auto.
Qed.
Proof.
intros x z t n x_neq_z.
unfolds open. generalize 0 as k.
gen n.
induction t ; intros m k fv_occ_.
compare k n ; intro ; simpls ; case_nat ; simpls ; auto.
case_var. assumption.
simpl in *. assumption.
simpls. apply IHt with (k:=S k). assumption.
simpls.
assert(exists n1, fv_occ x ({k ~> pterm_fvar z}t1) = n1).
exists (fv_occ x ({k ~> pterm_fvar z}t1)). reflexivity.
assert(exists n2, fv_occ x ({k ~> pterm_fvar z}t2) = n2).
exists (fv_occ x ({k ~> pterm_fvar z}t2)). reflexivity.
destruct H as [n1 H].
destruct H0 as [n2 H0].
rewrite IHt1 with (k:=k) (n:=n1) ; auto.
rewrite IHt2 with (k:=k) (n:=n2) ; auto.
rewrite H, H0 in fv_occ_.
assumption.
simpls.
assert(exists n1, fv_occ x ({S k ~> pterm_fvar z}t1) = n1).
exists (fv_occ x ({S k ~> pterm_fvar z}t1)). reflexivity.
assert(exists n2, fv_occ x ({k ~> pterm_fvar z}t2) = n2).
exists (fv_occ x ({k ~> pterm_fvar z}t2)). reflexivity.
destruct H as [n1 H].
destruct H0 as [n2 H0].
rewrite IHt1 with (k:=S k) (n:=n1) ; auto.
rewrite IHt2 with (k:=k) (n:=n2) ; auto.
rewrite H, H0 in fv_occ_.
assumption.
Qed.
Lemma fv_occ_close : forall t x y, ~(x=y) -> fv_occ y t = fv_occ y (close t x).
Proof.
intros ; unfold close. generalize 0.
basic_pterm_induction t using (repeat (case_var ; simpl ; auto)).
Qed.
Lemma fv_occ_subs_decompose : forall t y u, fv_occ y u + fv_occ y t = fv_occ y (t[u]).
Proof.
intros. assert(forall x y, x + y = y + x) as H by (intros ; omega).
basic_pterm_induction t.
Qed.
Lemma fv_occ_notin : forall t y, y \notin fv t -> fv_occ y t = 0.
Proof.
intros. induction t ; simpl ; auto.
case_var.
elim H. simpl. VSD.fsetdec.
reflexivity.
simpl in H. rewrite IHt1 ; [|VSD.fsetdec]. rewrite IHt2 ; [|VSD.fsetdec]. reflexivity.
simpl in H. rewrite IHt1 ; [|VSD.fsetdec]. rewrite IHt2 ; [|VSD.fsetdec]. reflexivity.
Qed.
Lemma fv_occ_open : forall t x u, x \notin fv u -> fv_occ x t = fv_occ x (t^^u).
Proof.
intros t. unfold open. generalize 0.
induction t ; intros n' x u x_notin_u ; simpls ; try eauto.
case_nat.
rewrite fv_occ_notin ; auto.
simpl. reflexivity.
Qed.
Lemma subst_fv_occ : forall a b t u, a \notin fv u -> a <> b -> fv_occ a ([b ~> u]t) = fv_occ a t.
Proof.
intros. induction t ; simpls ; auto.
case_var* ; case_var*. apply fv_occ_notin ; auto.
Qed.
Lemma bv_occ_subst : forall t u k, (bv_occ_k k t = 0) -> ({k ~> u} t = t).
Proof.
intro t. basic_pterm_induction t prefixed_by (try elim_bv_occ).
Qed.
a body with no arrows pointing outside is a term
Lemma bv_occ_body_term : forall (t : pterm), body t -> bv_occ t = 0 -> term t.
Proof.
intros t H1 H2. destruct H1 as [? H1]. pick_fresh y. specialize (H1 y).
assert (term ({0 ~> pterm_fvar y} t)) as H3 by auto.
rewrite bv_occ_subst in H3; [|auto].
assumption.
Qed.
Hint Resolve bv_occ_body_term : term_building_db.
Lemma bv_occ_open_gen : forall t x k n, (n < k) -> bv_occ_k k ({n ~> (pterm_fvar x)}t) = bv_occ_k k t.
Proof.
intro t.
basic_pterm_induction t using (repeat (case_nat* ; stupid_hyp)).
Qed.
Hint Rewrite bv_occ_open_gen : bv_occ.
Lemma bv_occ_k_term : forall t, term t -> forall k, bv_occ_k k t = 0.
intros t H. induction H as [|? ? ? H1|? ? ? H1 ? H2|? ? ? ? H1].
reflexivity.
intro k ; simpl. pick_fresh y. rewrite <-H1 with (k:=S k) (x:= y) ; auto. unfold open.
rewrite bv_occ_open_gen ; auto ; try omega.
intro ; simpl. rewrite H1 ; rewrite H2 ; auto.
intro k ; simpl. pick_fresh y. rewrite <-H1 with (k:=S k) (x:= y) ; auto.
unfold open ; rewrite bv_occ_open_gen ; auto ; try omega.
rewrite IHterm ; auto.
Qed.
Hint Rewrite bv_occ_k_term : bv_occ.
Lemma bv_occ_term : forall t, term t -> bv_occ t = 0.
Proof.
intros. apply bv_occ_k_term ; auto.
Qed.
Proof.
intros t H1 H2. destruct H1 as [? H1]. pick_fresh y. specialize (H1 y).
assert (term ({0 ~> pterm_fvar y} t)) as H3 by auto.
rewrite bv_occ_subst in H3; [|auto].
assumption.
Qed.
Hint Resolve bv_occ_body_term : term_building_db.
Lemma bv_occ_open_gen : forall t x k n, (n < k) -> bv_occ_k k ({n ~> (pterm_fvar x)}t) = bv_occ_k k t.
Proof.
intro t.
basic_pterm_induction t using (repeat (case_nat* ; stupid_hyp)).
Qed.
Hint Rewrite bv_occ_open_gen : bv_occ.
Lemma bv_occ_k_term : forall t, term t -> forall k, bv_occ_k k t = 0.
intros t H. induction H as [|? ? ? H1|? ? ? H1 ? H2|? ? ? ? H1].
reflexivity.
intro k ; simpl. pick_fresh y. rewrite <-H1 with (k:=S k) (x:= y) ; auto. unfold open.
rewrite bv_occ_open_gen ; auto ; try omega.
intro ; simpl. rewrite H1 ; rewrite H2 ; auto.
intro k ; simpl. pick_fresh y. rewrite <-H1 with (k:=S k) (x:= y) ; auto.
unfold open ; rewrite bv_occ_open_gen ; auto ; try omega.
rewrite IHterm ; auto.
Qed.
Hint Rewrite bv_occ_k_term : bv_occ.
Lemma bv_occ_term : forall t, term t -> bv_occ t = 0.
Proof.
intros. apply bv_occ_k_term ; auto.
Qed.
Lemma bv_occ_close_decompose : forall t y, bv_occ t + fv_occ y t = bv_occ (close t y).
Proof.
assert (forall a b c d, a + b + (c + d) = a + c + (b + d))as Harith by (intros ; omega).
intros t ?. unfold close. unfold bv_occ. generalize 0.
basic_pterm_induction t using (case_var ; simpl ; auto ; case_nat ; auto).
Qed.
Lemma bv_occ_open_decompose : forall t y, bv_occ t + fv_occ y t = fv_occ y (t^y).
Proof.
intros. unfold bv_occ. unfold open. generalize 0.
basic_pterm_induction t.
case_nat ; simpl ; [|reflexivity]. case_var ; simpl ; auto.
Qed.
Lemma bv_occ_open_decompose_simpl : forall t y, y \notin fv t -> bv_occ t = fv_occ y (t^y).
Proof.
intros. rewrite <- bv_occ_open_decompose.
rewrite fv_occ_notin ; auto.
Qed.
Lemma bv_occ_close_decompose_simpl : forall t y, y \notin fv t -> bv_occ t = bv_occ (close t y).
Proof.
intros. rewrite <- bv_occ_close_decompose.
rewrite fv_occ_notin ; auto.
Qed.
Hint Rewrite ->fv_occ_notin using (solve [auto]) : bv_occ_rewrite.
Hint Rewrite <-fv_occ_subs_decompose : bv_occ_rewrite.
Hint Rewrite <-fv_occ_close using (solve [auto]) : bv_occ_rewrite.
Hint Rewrite <-fv_occ_open_var using (solve [auto]) : bv_occ_rewrite.
Hint Rewrite <-fv_occ_open using (solve [auto]) : bv_occ_rewrite.
Hint Rewrite <-bv_occ_close_decompose : bv_occ_rewrite.
Hint Rewrite <-bv_occ_open_decompose : bv_occ_rewrite.
Hint Rewrite bv_occ_term using (solve [auto]) : bv_occ_rewrite.
Hint Rewrite <-fv_occ_subs_decompose : bv_occ_rewrite.
Hint Rewrite <-fv_occ_close using (solve [auto]) : bv_occ_rewrite.
Hint Rewrite <-fv_occ_open_var using (solve [auto]) : bv_occ_rewrite.
Hint Rewrite <-fv_occ_open using (solve [auto]) : bv_occ_rewrite.
Hint Rewrite <-bv_occ_close_decompose : bv_occ_rewrite.
Hint Rewrite <-bv_occ_open_decompose : bv_occ_rewrite.
Hint Rewrite bv_occ_term using (solve [auto]) : bv_occ_rewrite.