Set Implicit Arguments.
Require Import MyTactics.
Lifting.
lift_var k x should be read: lift the indices greater than or
equal to k within x.
Definition lift_var (
k :
nat) (
x :
nat) :
nat :=
if le_gt_dec k x then 1 +
x else x.
Substitution.
subst_var a k x should be read as: substitute a for k in x.
Definition subst_var A (
var :
nat ->
A) (
a :
A) (
k :
nat) (
x :
nat) :
A :=
match lt_eq_lt_dec x k with
|
inleft (
left _) =>
var x
|
inleft (
right _) =>
a
|
inright _ =>
var (
x - 1)
end.
Basic lemmas.
A reformulation of the definition of lift_var.
Lemma lift_var_recent:
forall k x,
k >
x ->
lift_var k x =
x.
Proof.
intros. unfold lift_var. by_cases; easy.
Qed.
Lemma lift_var_old:
forall k x,
k <=
x ->
lift_var k x =
S x.
Proof.
intros. unfold lift_var. by_cases; easy.
Qed.
Lemma lift_var_succ:
forall k x,
lift_var (
S k) (
S x) =
S (
lift_var k x).
Proof.
unfold lift_var. intros. by_cases; easy.
Qed.
lift_var is injective.
Lemma lift_var_injective:
forall k x1 x2,
lift_var k x1 =
lift_var k x2 ->
x1 =
x2.
Proof.
intros ? ? ?. unfold lift_var. by_cases; easy.
Qed.
Definition lift_injective A (
lift :
nat ->
A ->
A) :=
forall a1 k a2,
lift k a1 =
lift k a2 ->
a1 =
a2.
Substituting a for k in k yields a.
Lemma subst_var_identity:
forall A (
var :
nat ->
A) (
a :
A) (
k :
nat),
subst_var var a k k =
a.
Proof.
intros. unfold subst_var. inspect_cases; intro.
false; omega.
auto.
false; omega.
Qed.
Substituting for a variable that doesn't exist has no effect.
Lemma subst_var_miss_1:
forall A (
var :
nat ->
A) (
a :
A) (
k x :
nat),
k >
x ->
subst_var var a k x =
var x.
Proof.
intros. unfold subst_var. inspect_cases; intro; auto; false; omega.
Qed.
Lemma subst_var_miss_2:
forall A (
var :
nat ->
A) (
a :
A) (
k x :
nat),
k <
x ->
subst_var var a k x =
var (
x - 1).
Proof.
intros. unfold subst_var. inspect_cases; intro; auto; false; omega.
Qed.
Definition subst_lift A B (
lift :
nat ->
B ->
B) (
subst :
A ->
nat ->
B ->
B) :=
forall b k a,
subst a k (
lift k b) =
b.
Lemma subst_lift_var:
forall A (
var :
nat ->
A)
k a x,
subst_var var a k (
lift_var k x) =
var x.
Proof.
intros. unfold lift_var, subst_var. by_cases; easy.
Qed.
Punning is the sequence of lifting, which introduces a new variable,
and substitution, which replaces a pre-existing variable with the new
variable (pun_1) or replaces the new variable with a pre-existing
one (pun_2).
Definition pun_1 A B (
var:
nat ->
A) (
lift:
nat ->
B ->
B) (
subst:
A ->
nat ->
B ->
B) :=
forall b k,
subst (
var k) (
S k) (
lift k b) =
b.
Lemma pun_1_var:
forall A (
var :
nat ->
A)
k x,
subst_var var (
var k) (
S k) (
lift_var k x) =
var x.
Proof.
intros. unfold subst_var, lift_var. inspect_cases; inspect_cases; intros; f_equal; omega.
Qed.
Definition pun_2 A B (
var:
nat ->
A) (
lift:
nat ->
B ->
B) (
subst:
A ->
nat ->
B ->
B) :=
forall b k,
subst (
var k)
k (
lift (
S k)
b) =
b.
Lemma pun_2_var:
forall A (
var :
nat ->
A)
k x,
subst_var var (
var k)
k (
lift_var (
S k)
x) =
var x.
Proof.
intros. unfold subst_var, lift_var. inspect_cases; inspect_cases; intros; f_equal; omega.
Qed.
Commutation of lift with itself.
Definition lift_lift A (
lift :
nat ->
A ->
A) :=
forall a k1 s1,
k1 <=
s1 ->
lift k1 (
lift s1 a) =
lift (
S s1) (
lift k1 a).
Definition lift_zero_lift A (
lift :
nat ->
A ->
A) :=
forall a s1,
lift 0 (
lift s1 a) =
lift (
S s1) (
lift 0
a).
Lemma lift_lift_var:
lift_lift lift_var.
Proof.
unfold lift_lift, lift_var. intros. by_cases; easy.
Qed.
This tactic tries to identify an occurrence of lift 0 (lift k) a, and
rewrites it via a lift_lift lemma, whose name must be provided. The task
is somewhat tricky, because we don't want k to be the constant 0. Indeed,
if the goal is the form lift 0 (lift 0 (lift k a)), we would like the inner
redex to be selected, not the outer one.
Ltac lzl lift lift_zero_lift :=
match goal with
| |-
context[
lift 0 (
lift (
S ?
k1) ?
t)] =>
rewrite (
lift_zero_lift t (
S k1))
|
h: ?
k1 <= ?
s1 |-
context[
lift 0 (
lift ?
k1 ?
t)] =>
rewrite (
lift_zero_lift t k1)
|
h: ?
s1 <= ?
k1 |-
context[
lift 0 (
lift ?
k1 ?
t)] =>
rewrite (
lift_zero_lift t k1)
end.
Commutation of lift with subst.
Definition lift_subst_1 A B (
liftA :
nat ->
A ->
A) (
liftB :
nat ->
B ->
B) (
subst :
A ->
nat ->
B ->
B) :=
forall u k1 t s1,
k1 <=
s1 ->
liftB k1 (
subst t s1 u) =
subst (
liftA k1 t) (
S s1) (
liftB k1 u).
Lemma lift_subst_var_1:
forall A (
var :
nat ->
A) (
lift :
nat ->
A ->
A) (
k1 s1 :
nat) (
t :
A) (
u :
nat),
(
forall k x,
lift k (
var x) =
var (
lift_var k x)) ->
k1 <=
s1 ->
lift k1 (
subst_var var t s1 u) =
subst_var var (
lift k1 t) (
S s1) (
lift_var k1 u).
Proof.
introv h. unfold lift_var, subst_var. by_cases; easy;
rewrite h; unfold lift_var; by_cases; easy.
Qed.
Definition lift_subst_2 A B (
liftA :
nat ->
A ->
A) (
liftB :
nat ->
B ->
B) (
subst :
A ->
nat ->
B ->
B) :=
forall u k1 t s1,
k1 <=
s1 ->
liftB s1 (
subst t k1 u) =
subst (
liftA s1 t)
k1 (
liftB (
S s1)
u).
Lemma lift_subst_var_2:
forall A (
var :
nat ->
A) (
lift :
nat ->
A ->
A) (
k1 s1 :
nat) (
t :
A) (
u :
nat),
(
forall k x,
lift k (
var x) =
var (
lift_var k x)) ->
k1 <=
s1 ->
lift s1 (
subst_var var t k1 u) =
subst_var var (
lift s1 t)
k1 (
lift_var (
S s1)
u).
Proof.
introv h. unfold lift_var, subst_var. by_cases; easy;
rewrite h; unfold lift_var; by_cases; easy.
Qed.
Commutation of subst with itself.
Definition subst_subst A B (
lift :
nat ->
A ->
A) (
substA :
A ->
nat ->
A ->
A) (
substB :
A ->
nat ->
B ->
B) :=
forall v k1 t u s1,
k1 <=
s1 ->
substB t s1 (
substB u k1 v) =
substB (
substA t s1 u)
k1 (
substB (
lift k1 t) (
S s1)
v).
Lemma subst_subst_var:
forall A (
var :
nat ->
A) (
lift :
nat ->
A ->
A) (
subst :
A ->
nat ->
A ->
A) (
k1 s1 :
nat) (
t u :
A) (
v :
nat),
(
forall a k x,
subst a k (
var x) =
subst_var var a k x) ->
subst_lift lift subst ->
k1 <=
s1 ->
subst t s1 (
subst_var var u k1 v) =
subst (
subst t s1 u)
k1 (
subst_var var (
lift k1 t) (
S s1)
v).
Proof.
introv h sl. unfold subst_var. by_cases; repeat (rewrite h; unfold subst_var; by_cases; easy).
Qed.
Hints, to be used by eauto when proving lemmas about de Bruijn
indices.
Hint Resolve subst_lift_var :
subst_lift_db.
Hint Extern 1 =>
f_equal :
subst_lift_db.
Hint Extern 1 => (
subst;
apply lift_lift_var) :
lift_lift_db.
Hint Extern 1 =>
f_equal :
lift_subst_1_db.
Hint Extern 1 => (
subst;
apply lift_subst_var_1;
intuition eauto) :
lift_subst_1_db.
Hint Extern 1 =>
subst :
lift_subst_1_db.
Hint Extern 1 =>
f_equal :
lift_subst_2_db.
Hint Extern 1 => (
subst;
apply lift_subst_var_2;
intuition eauto) :
lift_subst_2_db.
Hint Extern 1 =>
subst :
lift_subst_2_db.
Hint Extern 1 =>
f_equal :
subst_subst_db.
Hint Extern 1 => (
subst;
apply subst_subst_var;
intuition eauto) :
subst_subst_db.
Hint Extern 1 =>
subst :
subst_subst_db.
Tactics for proving the standard lemmas.
Ltac subst_lift_tac :=
intro b;
induction b;
simpl;
intros;
eauto with subst_lift_db.
Ltac lift_lift_tac :=
intro a;
induction a;
intros;
simpl;
f_equal;
eauto with lift_lift_db.
Ltac lift_zero_lift_tac :=
unfold lift_zero_lift;
eauto.
Ltac lift_subst_1_tac :=
intro u;
induction u;
simpl;
intros;
eauto with lift_subst_1_db.
Ltac lift_subst_2_tac :=
intro u;
induction u;
simpl;
intros;
eauto with lift_subst_2_db.
Ltac subst_subst_tac :=
intro v;
induction v;
simpl;
intros;
eauto with subst_subst_db.
Ltac pun_tac :=
intro t;
induction t;
simpl;
intros;
f_equal;
eauto using pun_1_var,
pun_2_var.
Ltac invert_lift_equality :=
match goal with
|
h:
_ =
_ _ ?
v |-
_ =>
destruct v;
simpl in h;
depelim h
end.
Ltac invert_subst_equality :=
match goal with
|
h:
_ =
_ _ _ ?
v |-
_ =>
destruct v;
simpl in h;
depelim h
end.
Ltac invert_subst_var_equality :=
match goal with
|
h:
_ =
subst_var ?
var _ _ ?
v |-
_ =>
generalize h;
clear h;
unfold subst_var;
by_cases;
eauto;
match goal with
|
i:
var _ =
var _ |-
_ =>
injection i;
eauto
end
end.
Ltac lift_injective_tac :=
intro v;
induction v;
simpl;
intros;
invert_lift_equality;
f_equal;
eauto using lift_var_injective.
This is a definition of closedness.
When the syntax of objects is known, one can give a direct definition of
closedness as an inductive predicate. However, this duplicates the syntax
of objects. It seems preferable to view an object as closed when it is
invariant under lifting. We show that this implies that it is also invariant
under substitution.
Definition well_scoped_lift B (
lift:
nat ->
B ->
B) (
k :
nat) (
b :
B) :=
forall j,
j >=
k ->
lift j b =
b.
Definition well_scoped_subst A B (
lift:
nat ->
B ->
B) (
subst:
A ->
nat ->
B ->
B) (
k :
nat) (
b :
B) :=
forall j,
j >=
k ->
forall a,
subst a j b =
b.
Lemma well_scoped_lift_subst:
forall A B (
lift:
nat ->
B ->
B) (
subst:
A ->
nat ->
B ->
B),
subst_lift lift subst ->
forall k b,
well_scoped_lift lift k b ->
well_scoped_subst lift subst k b.
Proof.
unfold well_scoped_lift, well_scoped_subst. introv sl wsl jk. intro.
rewrite <- (wsl _ jk) at 1. auto.
Qed.
Definition closed B (
lift:
nat ->
B ->
B) (
b :
B) :=
forall k,
well_scoped_lift lift k b.
Lemma well_scoped_lift_monotonic:
forall B (
lift:
nat ->
B ->
B) (
k1 k2 :
nat) (
b :
B),
k1 <=
k2 ->
well_scoped_lift lift k1 b ->
well_scoped_lift lift k2 b.
Proof.
unfold well_scoped_lift. intros. eauto.
Qed.
Rotation of indices.
rotate n maps 0 to n, n to n-1, ..., 1 to 0.
Definition rotate A (
var :
nat ->
A) (
lift :
nat ->
A ->
A) (
subst :
A ->
nat ->
A ->
A) (
n :
nat) (
x :
A) :
A :=
subst (
var n) 0 (
lift (
S n)
x).
Definition rotate_var :
nat ->
nat ->
nat :=
let var x :=
x in
rotate var lift_var (
subst_var var).
Lemma rotate_var_characterization:
forall n k,
(
k = 0 ->
rotate_var n k =
n) /\
(
k > 0 ->
k <=
n ->
rotate_var n k =
k - 1) /\
(
k >
n ->
rotate_var n k =
k).
Proof.
In particular, rotate 1 exchanges the indices 0 and 1.
Definition rotate1_self_inverse A (
var :
nat ->
A) (
lift :
nat ->
A ->
A) (
subst :
A ->
nat ->
A ->
A) :=
forall x :
A,
rotate var lift subst 1 (
rotate var lift subst 1
x) =
x.
Lemma rotate1_self_inverse_holds:
forall A (
var :
nat ->
A) (
lift :
nat ->
A ->
A) (
subst :
A ->
nat ->
A ->
A),
(
forall k x,
lift k (
var x) =
var (
lift_var k x)) ->
(
forall y k x,
subst y k (
var x) =
subst_var var y k x) ->
lift_lift lift ->
lift_subst_2 lift lift subst ->
subst_subst lift subst subst ->
pun_2 var lift subst ->
rotate1_self_inverse var lift subst.
Proof.
introv lv sv ll ls ss pun.
intro.
unfold rotate.
We are looking at a subst-lift-subst-lift composition.
Permute the central lift/subst pair, to obtain subst-subst-lift-lift.
rewrite ls;
eauto.
Simplify.
rewrite lv.
unfold lift_var;
simpl.
Permute the two lifts.
rewrite <-
ll;
eauto.
Permute the two substs.
rewrite ss;
eauto.
rewrite sv.
rewrite lv.
unfold lift_var,
subst_var;
simpl.
De-simplify to prepare the next rewriting step.
replace (
var 2)
with (
lift 1 (
var 1)); [
idtac |
rewrite lv;
auto ].
Permute the central subst-lift.
rewrite <-
ls;
eauto.
Identify two puns, and we are done.
rewrite pun.
rewrite pun.
reflexivity.
In summary, we have done this:
substA-liftA-substB-liftB
substA-substB-liftA-liftB
substB-substA-liftB-liftA
substB-liftB-substA-liftA
This algebraic proof was admittedly quite tricky and obscure. Perhaps
one could come up with a simpler approach.
Qed.