Set Implicit Arguments.
Require Import MyTactics.
Require Import Programs.
Some predicates and functions over lists of values.
-------------------------------------------------------------------------
Existence of an element that satisfies a property P.
Fixpoint some (
P :
value ->
Prop) (
vs :
values) :
Prop :=
match vs with
|
VNil =>
False
|
VCons v vs =>
P v \/
some P vs
end.
-------------------------------------------------------------------------
Membership.
Definition member v vs :=
some (
fun w =>
v =
w)
vs.
-------------------------------------------------------------------------
Length.
Fixpoint count (
vs :
values) :=
match vs with
|
VNil =>
0
|
VCons _ vs =>
1 +
count vs
end.
-------------------------------------------------------------------------
Map.
Fixpoint vmap (
f :
value ->
value) (
vs :
values) :=
match vs with
|
VNil =>
VNil
|
VCons v vs =>
VCons (
f v) (
vmap f vs)
end.
-------------------------------------------------------------------------
Removal of an element.
We remove just one copy of the element, even if it occurs multiple times.
This is because we use our lists of values as multisets of the inhabitants
of a region.
Fixpoint remove v vs :=
match vs with
|
VNil =>
VNil
|
VCons hd tl =>
if eq_value_dec v hd then tl else VCons hd (
remove v tl)
end.
This lemma proves that the definition satisfies our intuitive idea.
Lemma remove_cases:
forall vh v vs,
(
vh =
v /\
remove vh (
VCons v vs) =
vs) \/
(
vh <>
v /\
remove vh (
VCons v vs) =
VCons v (
remove vh vs)).
Proof.
intros.
simpl.
destruct (
eq_value_dec vh v);
intuition congruence.
Qed.
-------------------------------------------------------------------------
Lemmas.
A list of length 1 contains a single element.
Lemma singleton_list:
forall vs,
count vs = 1 ->
exists v,
vs =
VCons v VNil.
Proof.
intros [| v [ | ]]; simpl; intros.
false; omega.
intuition eauto.
false; omega.
Qed.
This tactic exploits the knowledge that a list has length 1 to replace it
with a list of a single element.
Ltac singleton_list :=
match goal with h: ?
rk = ?
rk ->
count ?
vs = 1 |-
_ =>
unpack (
singleton_list _ (
h eq_refl));
subst vs;
clear h
end.
If some element of a singleton list satisfies P, then the unique
element satisfies P.
Lemma some_singleton:
forall P v,
some P (
VCons v VNil) ->
P v.
Proof.
simpl. tauto.
Qed.
Lemma singleton_some:
forall (
P :
value ->
Prop)
v,
P v ->
some P (
VCons v VNil).
Proof.
simpl. tauto.
Qed.
Lemma member_singleton:
forall v1 v2,
member v1 (
VCons v2 VNil) ->
v2 =
v1.
Proof.
unfold member. simpl. symmetry. tauto.
Qed.
The head of a list is a member of the list.
Lemma head_member:
forall v vs,
member v (
VCons v vs).
Proof.
unfold member. simpl. auto.
Qed.
A member of the tail is a member of the list.
Lemma member_tail:
forall v1 v2 vs,
member v1 vs ->
member v1 (
VCons v2 vs).
Proof.
unfold member. simpl. tauto.
Qed.
A member of the list is a member of the tail, if it differs from the head.
Lemma member_further:
forall vh v vs,
member vh (
VCons v vs) ->
vh <>
v ->
member vh vs.
Proof.
unfold member; simpl. tauto.
Qed.
To prove that every member of a list satisfies P, one must prove that
the head satisfies P and that every member of the tail satisfies P.
Lemma member_cons_elim:
forall (
P :
value ->
Prop)
vh vs,
P vh ->
(
forall v,
member v vs ->
P v) ->
(
forall v,
member v (
VCons vh vs) ->
P v).
Proof.
introv ? ? [ ? | ? ]. congruence. auto.
Qed.
A correspondence (both ways) between member and some.
Lemma some_member:
forall P vs,
some P vs ->
exists v,
member v vs /\
P v.
Proof.
induction vs;
simpl.
tauto.
intros [ ? | ? ].
intuition eauto using head_member.
forwards:
IHvs.
auto.
unpack.
intuition eauto using member_tail.
Qed.
Lemma member_some:
forall (
P :
value ->
Prop)
v vs,
member v vs ->
P v ->
some P vs.
Proof.
induction vs; unfold member; simpl. tauto. intros [ ? | ? ] ?; subst; tauto.
Qed.
If some element of remove v vs satisfies P, then some element of vs
satisfies P.
Lemma some_remove:
forall (
P :
value ->
Prop)
v vs,
some P (
remove v vs) ->
some P vs.
Proof.
induction vs;
simpl;
intro.
tauto.
destruct (
eq_value_dec v v0);
subst;
simpl in *;
tauto.
Qed.
If vh is a member of vs, then the lists vs and VCons vh
(remove vh vs) have the same elements, which we express by saying
that they cannot be distinguished by some P.
Lemma reordering_1:
forall P vh vs,
some P vs ->
member vh vs ->
some P (
VCons vh (
remove vh vs)).
Proof.
unfold member.
induction vs;
simpl;
introv spvs mvh.
tauto.
destruct mvh.
Sub-case: vh is v. Obvious.
subst.
case (
eq_value_dec v v);
tauto.
Sub-case: vh is not v. Simplify, then distinguish two further sub-cases:
case (
eq_value_dec vh v);
intro.
subst;
tauto.
destruct spvs.
Sub-case: v satisfies P. Obvious.
simpl.
tauto.
Sub-case: some further element satisfies P. Use the induction hypothesis and conclude.
forwards ih:
IHvs;
auto.
destruct ih;
simpl;
tauto.
Qed.
Lemma reordering_2:
forall P vh vs,
some P (
VCons vh (
remove vh vs)) ->
member vh vs ->
some P vs.
Proof.