Module ValueLists

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.

-------------------------------------------------------------------------

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.

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.

Lemma singleton_some:
  forall (P : value -> Prop) v,
  P v ->
  some P (VCons v VNil).

Proof.

Lemma member_singleton:
  forall v1 v2,
  member v1 (VCons v2 VNil) ->
  v2 = v1.

Proof.

The head of a list is a member of the list.

Lemma head_member:
forall v vs,
member v (VCons v vs).

Proof.

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.

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.

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.

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.

Lemma member_some:
  forall (P : value -> Prop) v vs,
  member v vs ->
  P v ->
  some P vs.

Proof.

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.

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.

Lemma reordering_2:
  forall P vh vs,
  some P (VCons vh (remove vh vs)) ->
  member vh vs ->
  some P vs.

Proof.