Rocoma.Lib.Autosubst_FreeVars
Class IdsLemmas (term : Type) {Ids_term : Ids term} := {
(* The identity substitution is injective. *)
ids_inj:
forall x y,
ids x = ids y ->
x = y
}.
Section FreeVars.
Context
{A : Type}
{Ids_A : Ids A}
{Rename_A : Rename A}
{Subst_A : Subst A}
{IdsLemmas_A : IdsLemmas A}
{SubstLemmas_A : SubstLemmas A}.
Context
{B : Type}
{Ids_B : Ids B}
{Rename_B : Rename B}
{Subst_B : Subst B}
{IdsLemmas_B : IdsLemmas B}
{SubstLemmas_B : SubstLemmas B}.
Context
(* {HSubst_BA : HSubst B A} *)
{HSubst_AB : HSubst A B}
{HSubstLemmas_AB : HSubstLemmas A B}
{SubstHSubstComp_AB : SubstHSubstComp A B}.
(* {HSubstLemmas_BA : HSubstLemmas B A}. *)
A reformulation of ids_inj.
Lemma ids_inj_False:
forall x y,
ids x = ids y ->
x <> y ->
False.
Proof.
intros.
assert (x = y). { eauto using ids_inj. }
unfold var in *.
lia.
Qed.
The predicate fv k t means that the free variables of the term t are
contained in the semi-open interval 0..k-1.
Definition fv {C} {_ : Ids C} {_ : Rename C} {_ : Subst C} k (t: C) :=
t.[upn k (ren (+1))] = t.
Definition fvh k (t: B) :=
t.|[upn k (ren (+1))] = t.
Definition closed {C} {_ : Ids C} {_ : Rename C} {_ : Subst C} :=
@fv C _ _ _ 0.
Definition closedh :=
fvh 0.
This technical lemma states that the renaming +1 is injective.
Lemma lift_inj_ids:
forall (t: B) x,
t.[ren (+1)] = ids (S x) <-> t = ids x.
Proof.
split; intros.
- apply lift_inj. autosubst.
- subst. autosubst.
Qed.
This lemma characterizes the meaning of fv k when applied to a variable.
Lemma fv_ids_eq:
forall k x,
fv k (ids x) <-> x < k.
Proof.
unfold fv.
induction k; intros.
(* Base case. *)
{ asimpl. split; intros; exfalso.
{ eauto using ids_inj_False. }
{ lia. }
}
(* Step. *)
{ destruct x; asimpl.
{ split; intros. { lia. } { reflexivity. } }
{ rewrite lift_inj_ids.
rewrite <- id_subst.
rewrite IHk. lia. }
}
Qed.
Lemma fvh_ids:
forall k x,
fvh k (ids x).
Proof.
rewrite /fvh.
by elim=> *; asimpl.
Qed.
Lemma closed_eq:
forall (t: B),
closed t <-> t.[ren (+1)] = t.
Proof.
unfold closed, fv. asimpl. tauto.
Qed.
Lemma closedh_eq:
forall (t: B),
closedh t <-> t.|[ren (+1)] = t.
Proof.
unfold closedh, fvh. asimpl. tauto.
Qed.
A variable is not closed.
Lemma closed_ids:
forall x,
~ closed (ids x).
Proof.
unfold closed, fv. intros. asimpl. intro.
eauto using ids_inj_False.
Qed.
Lemma closedh_ids:
forall x,
closedh (ids x).
Proof.
rewrite /closedh /fvh=> x.
by asimpl.
Qed.
Lemma fv1 s t :
fv 1 s ->
closed t ->
closed s.[t/].
Proof.
rewrite /closed/fv; asimpl=> hs ht.
rewrite -{1}hs ht -{2}hs -{2}hs.
autosubst.
Qed.
Lemma fv1h (s: B) (t: A) :
fvh 1 s ->
closed t ->
closedh s.|[t/].
Proof.
rewrite /closedh/fvh; asimpl=> hs ht.
rewrite -{1}hs ht -{2}hs -{2}hs.
autosubst.
Qed.
Lemma fv1hh (s: B) (t: B) :
closedh s ->
closedh t ->
closedh s.[t/].
Proof.
rewrite /closedh/fvh; asimpl=> hs ht.
by rewrite -{2}hs -{2}ht.
Qed.
End FreeVars.
(* The tactic fv is intended to use a number of lemmas as rewriting rules.
The hint database fv can be extended with language-specific lemmas. *)
Hint Rewrite @fv_ids_eq : fv.
Ltac fv :=
autorewrite with fv in *;
eauto with typeclass_instances.
Ltac fvh :=
autorewrite with fvh in *;
eauto with typeclass_instances.
(* A hint database to prove goals of the form ~ (closed _) or closed _. *)
Hint Resolve closed_ids : closed.
Hint Resolve closedh_ids : closedh.
Section Subst_var.
Context
{A : Type}
{Ids_A : Ids A}
{Rename_A : Rename A}
{Subst_A : Subst A}
{IdsLemmas_A : IdsLemmas A}
{SubstLemmas_A : SubstLemmas A}.
(* subst_var u x is the substitution of u for x. *)
We give a direct definition of it as a function of type var -> term,
defined by cases. I don't know if it could also be nicely defined in
terms of the basic combinators of de Bruijn algebra. Note that the
candidate definition upn x (t .: ids) is WRONG when x > 0.
Definition subst_var (u : A) (x y : var) : A :=
match lt_eq_lt_dec y x with
| inleft (left _) => ids y
| inleft (right _) => u
| inright _ => ids (y - 1)
end.
A nice notation: t.[u // x] is the substitution of u for x in t.
Notation "t .[ u // x ]" := (subst (subst_var u x) t)
(at level 2, u at level 200, left associativity,
format "t .[ u // x ]") : subst_scope.
The following laws serve as sanity checks: we got the definition right.
Lemma subst_var_miss_1:
forall x y u,
y < x ->
(ids y).[u // x] = ids y.
Proof.
intros. asimpl. unfold subst_var. dblib_by_cases. reflexivity.
Qed.
Lemma subst_var_match:
forall x u,
(ids x).[ u // x ] = u.
Proof.
intros. asimpl. unfold subst_var. dblib_by_cases. reflexivity.
Qed.
Lemma subst_var_miss_2:
forall x y u,
x < y ->
(ids y).[u // x] = ids (y - 1).
Proof.
intros. asimpl. unfold subst_var. dblib_by_cases. reflexivity.
Qed.
In the special case where x is 0, the substitution t // 0 can also
be written t/, which is an AutoSubst notation for t .: ids.
Lemma subst_var_0:
forall t u,
t.[u // 0] = t.[u/].
Proof.
intros. f_equal. clear t.
f_ext. intros [|x].
{ reflexivity. }
{ unfold subst_var. simpl. f_equal. lia. }
Qed.
Lemma upnP n σ h :
upn n σ h =
if h < n then ids h else (σ (h - n)).[ren (+n)].
Proof.
case: ifPn.
- elim: h n =>[|h ih][|n]//=/ih e.
rewrite iterate_S. asimpl. rewrite e. autosubst.
- rewrite -leqNgt.
elim: h n => [|h ih][|n]; try autosubst.
+ by case: n.
+ move=>/ih e. rewrite iterate_S. asimpl. rewrite e. autosubst.
Qed.
Lemma upn1 :
up = upn 1.
Proof.
autosubst.
Qed.
Lemma upnP_cond n σ h :
h >= n ->
upn n σ h = (σ (h - n)).[ren (+n)].
Proof.
move=>H.
by rewrite upnP ifF; [reflexivity|lia].
Qed.
Lemma upn2P n σ h :
upn n σ h =
if h < n then ids h else upn n σ h.
Proof.
case: ifPn; rewrite upnP; case: ifPn => //=.
Qed.
Lemma scompA f g h :
f >> (g >> h) = f >> g >> h.
Proof.
by rewrite /scomp -subst_compX compA.
Qed.
Lemma upn_k_sigma_x k σ x:
x < k ->
upn k σ x = ids x.
Proof.
move=> ?.
by rewrite upnP ifT.
Qed.
Lemma fv_unaffected_lift:
forall j t k,
fv k t ->
t.[upn k (ren (+j))] = t.
Proof.
elim=> [|j ih] t k ht.
- asimpl.
rewrite up_id_n.
autosubst.
- have->: ren (+j.+1) = ren (+1) >> ren (+j) by autosubst.
rewrite -up_comp_n.
have->: t.[upn k (ren (+1)) >> upn k (ren (+j))]
= t.[upn k (ren (+1))].[ upn k (ren (+j))] by autosubst.
by rewrite ht ih.
Qed.
Lemma upn_ren_app k n (y : var) :
(upn k (ren (+n)) y) = ids (if y < k then y else n + y).
Proof.
rewrite upnP.
case (boolP (y < k))=>//= h.
by asimpl; f_equal; lia.
Qed.
Lemma upn_ren_miss k n (y : var) j t :
(y < k -> y <> j) ->
(k <= y -> n + y <> j) ->
(upn k (ren (+n)) y).[fun m => if eqn m j then t else ids m]
= upn k (ren (+n)) y.
Proof.
move=> h1 h2.
rewrite upn_ren_app.
case (boolP (y < k))=> hy /=; asimpl;
[ case (boolP (eqn y j))=> he | case (boolP (eqn (n + y) j))=> he ]=>//.
- exfalso. apply h1; by lia.
- exfalso. apply h2; by lia.
Qed.
End Subst_var.
Notation "t .[ u // x ]" := (subst (subst_var u x) t)
(at level 2, u at level 200, left associativity,
format "t .[ u // x ]") : subst_scope.
Section Both.
Context
{A : Type}
{Ids_A : Ids A}
{Rename_A : Rename A}
{Subst_A : Subst A}
{IdsLemmas_A : IdsLemmas A}
{SubstLemmas_A : SubstLemmas A}.
Context
{B : Type}
{Ids_B : Ids B}
{Rename_B : Rename B}
{Subst_B : Subst B}
{IdsLemmas_B : IdsLemmas B}
{SubstLemmas_B : SubstLemmas B}.
Context
{HSubst_AB : HSubst A B}
{HSubstLemmas_AB : HSubstLemmas A B}
{SubstHSubstComp_AB : SubstHSubstComp A B}.
Lemma upn_ren_hsubst n k (θ: var -> A) :
upn n (ren (+k)) >>| θ =
upn n (ren (+k)).
Proof.
f_ext=>x /=.
rewrite upnP.
by case (x < n); asimpl.
Qed.
Corollary ren_hsubst k θ :
ren (+k) >>| θ = ren (+k).
Proof.
have:= upn_ren_hsubst 0 k θ.
by rewrite upn0.
Qed.
Lemma up_comp σ1 σ2 :
up (σ1 >> σ2) = up σ1 >> up σ2.
Proof.
autosubst.
Qed.
Lemma up_compt (σ1 : var -> B) σ2 :
up (σ1 >> σ2) = up σ1 >> up σ2.
Proof.
autosubst.
Qed.
Lemma pushup (σ: var -> B) (θ: var -> A) :
up (σ >>| θ) = up σ >>| θ.
Proof.
autosubst.
Qed.
Lemma subst_var_id x n : subst_var (ids x) n n = ids x.
Proof.
rewrite /subst_var.
by case (lt_eq_lt_dec n n)=> [[]|]; try lia.
Qed.
Lemma subst_var_tsubst_upn k x n m θ :
(upn k (subst_var (ids m) n) x).|[θ] = (upn k (subst_var (ids m) n) x).
Proof.
rewrite upnP.
case (boolP (x < k))=>// *.
by asimpl.
rewrite /subst_var.
by case (lt_eq_lt_dec (x - k) n)=> [[]|] *; asimpl; f_equal.
Qed.
Corollary subst_var_tsubst x n m θ :
((subst_var (ids m) n) x).|[θ] = subst_var (ids m) n x.
Proof.
exact: (subst_var_tsubst_upn 0).
Qed.
Corollary subst_var_tsubst2 θ n m :
subst_var (ids m) n >>| θ = subst_var (ids m) n.
Proof.
unfold ">>|", ">>>".
by f_ext=>x; rewrite subst_var_tsubst.
Qed.
Lemma subst_var_lemma n m t :
upn m (subst_var t n) = subst_var t.[ren (+m)] (n + m).
Proof.
f_ext=> x.
rewrite upnP /subst_var.
case (boolP (x < m))=> *.
- by case (lt_eq_lt_dec x (n + m))=> [[]|] * //; lia.
- case (lt_eq_lt_dec (x - m) n)=> [[]|] *;
case (lt_eq_lt_dec x (n + m))=> [[]|] * //; try lia.
+ by asimpl; f_equal; lia.
+ by asimpl; f_equal; lia.
Qed.
Lemma subst_var_hsubst u n θ :
subst_var u n >>| θ = subst_var u.|[θ] n.
Proof.
f_ext=> x.
rewrite /subst_var/=.
case (lt_eq_lt_dec x n)=>[[]|]//.
by autosubst.
by autosubst.
Qed.
Lemma fv_hsubst s n θ :
fv n s -> fv n s.|[θ].
Proof.
rewrite /fv/= => {2}<-.
asimpl.
f_equal.
f_ext=>/= x.
rewrite upnP.
by case (boolP (x < n)); autosubst.
Qed.
The predicate fvu lo hi t means that the free variables of the term t are
contained in the semi-open interval lo..hi-1.
Definition fvu lo hi t :=
t.[fun i =>
if i < lo then ids i.+1 else
if i < hi then ids i
else ids i.+1] = t.
Lemma fvu0 n t :
fvu 0 n t = fv n t.
Proof.
rewrite /fv /fvu.
do 2 f_equal.
f_ext=> x.
rewrite upnP.
case (boolP (x < 0))=>// h0.
case (boolP (x < n))=>// h.
asimpl.
by f_equal; lia.
Qed.
Lemma fvu_equal_close k s :
fvu k k s = closed s.
Proof.
rewrite /fvu /closed /fv.
do 2 f_equal.
f_ext=> x.
rewrite upnP.
have ->: x - 0 = x by lia.
case (boolP (x < k))=>h;
case (boolP (x < 0))=>h2.
- by lia.
- by autosubst.
- by lia.
- by autosubst.
Qed.
Lemma fvu_equal_close2 lo hi s :
lo > hi ->
fvu lo hi s = closed s.
Proof.
move=> h.
rewrite /fvu /closed /fv.
do 2 f_equal.
f_ext=> x.
rewrite upn0.
case (boolP (x < lo))=>h1;
case (boolP (x < hi))=>h2; try lia; by autosubst.
Qed.
The predicate fvu2 sub lo hi t means that the free variables
of the term t are contained in 0..sub-1 and lo..hi-1.
Definition fvu2 sub lo hi t :=
t.[fun i =>
if i < sub then ids i else
if i < lo then ids i.+1 else
if i < hi then ids i
else ids i.+1
] = t.
This definition generalize fvu
Lemma fvu_fvu2 lo hi t :
fvu2 0 lo hi t = fvu lo hi t.
Proof.
rewrite /fvu2 /fvu.
by do 2 f_equal.
Qed.
End Both.
The tactic subst_var_tac attempts to simplify applications of subst_var.
Ltac subst_var_tac :=
first [
rewrite subst_var_miss_1; lia
| rewrite subst_var_match; lia
| rewrite subst_var_miss_2; lia
].
first [
rewrite subst_var_miss_1; lia
| rewrite subst_var_match; lia
| rewrite subst_var_miss_2; lia
].
Tactic prove_fvu is useful to prove goals of the form:
``` fvu n k (And s t) -> fvu n k s ```
Tactic prove_fvu2 is similar.
Ltac prove_fvu2 :=
unfold fvu2; intros; asimpl; injections; eauto.
Section subst_var2.
Context
{A : Type}
{Ids_A : Ids A}
{Rename_A : Rename A}
{Subst_A : Subst A}
{IdsLemmas_A : IdsLemmas A}
{SubstLemmas_A : SubstLemmas A}.
unfold fvu2; intros; asimpl; injections; eauto.
Section subst_var2.
Context
{A : Type}
{Ids_A : Ids A}
{Rename_A : Rename A}
{Subst_A : Subst A}
{IdsLemmas_A : IdsLemmas A}
{SubstLemmas_A : SubstLemmas A}.
Definition subst_var2 i t :=
fun j : nat => if j == i then t else ids j.
Definition var_not_free (i: var) r :=
r.[subst_var2 i (ids i.+1)] = r.
Ltac trytry := try (by lia); try (by autosubst).
Lemma fvu_succ n k u :
fvu n k u ->
var_not_free n u ->
fvu n.+1 k u.
Proof.
rewrite /fvu /var_not_free=> h1 h2.
rewrite -{2}h1 -h2.
asimpl.
f_equal; f_ext=> x.
rewrite /subst_var2.
asimpl.
case (boolP (eqn x n))=> ?; asimpl;
case (boolP (eqn (n.+2 - n.+1) 0))=> ? /=; trytry.
by case (boolP (eqn (n.+2 - k) 0))=> ? /=; trytry;
case (boolP (eqn (n.+2 - n) 0))=> ? /=; trytry.
by case (boolP (eqn (x.+1 - n.+1) 0))=> ? /=; trytry;
case (boolP (eqn (x.+1 - n) 0))=> ? /=; trytry.
Qed.
Lemma var_not_free_upn_lt j k n f :
j < k ->
var_not_free j f ->
var_not_free j f.[upn k (ren (+n))].
Proof.
rewrite /var_not_free=> hjk h.
rewrite -h.
asimpl.
f_equal; f_ext=> x.
rewrite /subst_var2.
asimpl.
case (boolP (eqn x j))=> hx; asimpl; apply upn_ren_miss; move=> *; by lia.
Qed.
Lemma var_not_free_add j n f :
var_not_free j f ->
var_not_free (n + j) f.[ren (+n)].
Proof.
rewrite /var_not_free=> h.
rewrite -{2}h.
asimpl.
f_equal; f_ext=> x.
rewrite /subst_var2.
asimpl.
rewrite plusE.
case (boolP (eqn (n + x) (n + j)))=> hx;
case (boolP (eqn x j))=> hx'; try by lia.
- asimpl. by rewrite plusE.
- asimpl. by rewrite plusE.
Qed.
Lemma var_not_free_upn_mid j k n f :
k <= j ->
j < k + n ->
var_not_free j f.[upn k (ren (+n))].
Proof.
rewrite /var_not_free=> h1 h2.
asimpl.
f_equal; f_ext=> x.
rewrite /subst_var2.
asimpl.
apply upn_ren_miss; move=> *; by lia.
Qed.
Lemma var_not_free_upn_ge i k n f :
k <= i ->
var_not_free i f ->
var_not_free (i + n) f.[upn k (ren (+n))].
Proof.
rewrite /var_not_free=> hki h.
rewrite -h.
asimpl.
f_equal; f_ext=> x.
rewrite /subst_var2.
asimpl.
case (boolP (eqn x i))=> hx; asimpl; apply upn_ren_miss; move=> *; by lia.
Qed.
Lemma subst_var_lemma_upn_alt (n: nat) k t :
upn k (subst_var2 n t) =
fun j => if j < k then ids j else
if j-k == n then t.[ren (+k)] else ids j.
Proof.
f_ext=> x; rewrite upnP /subst_var2.
case (boolP (x < k))=>//= ?.
asimpl.
case (boolP (eqn (x-k) n))=>//= ?.
asimpl.
f_equal.
by lia.
Qed.
Corollary subst_var_lemma_upn_alt2 (n: nat) k :
upn k (subst_var2 n (ids n.+1)) =
fun j => if j < k then ids j else
if j-k == n then ids (n.+1 +k) else ids j.
Proof.
rewrite subst_var_lemma_upn_alt.
f_ext=> x.
asimpl.
by have->: (k + n)%coq_nat.+1 = n.+1 + k by lia.
Qed.
Corollary subst_var_lemma_up1_alt (n: nat) :
up (subst_var2 n (ids n.+1)) =
fun i => if i < 1 then ids i else
if i-1 == n then ids n.+2 else ids i.
Proof.
rewrite upn1 subst_var_lemma_upn_alt2.
f_ext=> x.
by have->: n.+1 + 1 = n.+2 by lia.
Qed.
Corollary subst_var_lemma_up1_alt_2 (n k: nat) :
upn k (subst_var2 n (ids n.+1)) =
(subst_var2 (n + k) (ids (n + k).+1)).
Proof.
f_ext=> x.
rewrite upnP /subst_var2.
case (boolP (x < k))=> xk.
+ by rewrite ifF; [|lia].
+ have->: (x - k == n) = (x == n + k) by lia.
case (boolP (x == (n+k)))=> xnk; asimpl.
by f_equal; lia.
by f_equal; lia.
Qed.
End subst_var2.
Section subst_var2p.
Context
{A : Type}
{Ids_A : Ids A}
{Rename_A : Rename A}
{Subst_A : Subst A}
{IdsLemmas_A : IdsLemmas A}
{SubstLemmas_A : SubstLemmas A}.
Context
{B : Type}
{Ids_B : Ids B}
{Rename_B : Rename B}
{Subst_B : Subst B}
{IdsLemmas_B : IdsLemmas B}
{SubstLemmas_B : SubstLemmas B}.
Context
{HSubst_AB : HSubst A B}
{HSubstLemmas_AB : HSubstLemmas A B}
{SubstHSubstComp_AB : SubstHSubstComp A B}.
Lemma subst_var_tsubst_upn_alt k x n m θ :
(upn k (subst_var2 n (ids m)) x).|[θ] = (upn k (subst_var2 n (ids m)) x).
Proof.
rewrite /subst_var2 upnP.
case (boolP (x < k)); asimpl=>//.
by case (eqn (x - k) n); asimpl.
Qed.
Corollary subst_var_tsubst_alt x n m θ :
((subst_var2 n (ids m)) x).|[θ] = subst_var2 n (ids m) x.
Proof.
exact: (subst_var_tsubst_upn_alt 0).
Qed.
Corollary subst_var_tsubst_recipe_alt θ n m :
subst_var2 n (ids m) >>| θ = subst_var2 n (ids m).
Proof.
unfold ">>|", ">>>", subst_var2.
f_ext=>x.
by rewrite subst_var_tsubst_alt.
Qed.
Corollary subst_var_tsubst_recipe_alt_2 θ n k :
upn n (subst_var2 k (ids k.+1)) >>| θ =
upn n (subst_var2 k (ids k.+1)).
Proof.
unfold ">>|", ">>>", subst_var2.
f_equal; f_ext=>x.
by rewrite subst_var_tsubst_upn_alt.
Qed.
Corollary subst_var_tsubst_recipe_alt_3 θ k :
(subst_var2 k (ids k.+1)) >>| θ =
(subst_var2 k (ids k.+1)).
Proof.
have:= subst_var_tsubst_recipe_alt_2 θ 0 k.
by rewrite upn0.
Qed.
Lemma subst_var2_miss:
forall x y u,
x < y ->
(ids y).[subst_var2 x u] = ids y.
Proof.
move=> x y u h.
rewrite /subst_var2/=.
asimpl.
case (boolP (eqn y x))=>//.
by lia.
Qed.
End subst_var2p.