Section Lists.

Lists of Real Numbers

In some contexts we will need to work with nested existential quantified formulas of the form exists n exists x1,...,xn P(x1,..,xn). One way of formalizing this kind of statement is through quantifying over lists. In this file we provide some tools for manipulating lists.

Notice that some of the properties listed below only make sense in the context within which we are working. Unlike in the other lemma files, no care has been taken here to state the lemmas in their most general form, as that would make them very unpractical to use.

We start by defining maximum and minimum of lists of reals and two membership predicates. The value of these functions for the empty list is arbitrarily set to 0, but it will be irrelevant, as we will never work with empty lists.

Fixpoint maxlist (l : list IR) : IR :=
  match l with
  | nil => 0
  | cons x nil => x
  | cons x m => Max x (maxlist m)
  end.

Fixpoint minlist (l : list IR) : IR :=
  match l with
  | nil => 0
  | cons x nil => x
  | cons x m => Min x (minlist m)
  end.

Fixpoint member (x : IR) (l : list IR) {struct l} : CProp :=
  match l with
  | nil => ⊥
  | cons y m => member x m or x [=] y
  end.

Sometimes the length of the list has to be restricted; the next definition provides an easy way to do that.

Definition length_leEq (A : Type) (l : list A) (n : N) := length l <= n.

Length is preserved by mapping.

Lemma map_pres_length : forall (A B : Set) (l : list A) (f : A -> B),
length l = length (map f l).

Often we want to map partial functions through a list; this next operator provides a way to do that, and is proved to be correct.

Definition map2 (F : PartIR) (l : list IR) :
(forall y, member y l -> Dom F y) -> list IR.
Defined.

Lemma map2_wd : forall F l H H' x,
member x (map2 F l H) -> member x (map2 F l H').

Lemma map2_pres_member : forall (F : PartIR) x Hx l H,
member x l -> member (F x Hx) (map2 F l H).

As maxlist and minlist are generalizations of Max and Min to finite sets of real numbers, they have the expected properties:

Lemma maxlist_greater : forall l x, member x l -> x [<=] maxlist l.

Lemma maxlist_leEq_eps : forall l : list IR, {x : IR | member x l} ->
forall e, 0 [<] e -> {x : IR | member x l | maxlist l[-]e [<=] x}.

Lemma maxlist_less : forall x l,
0 < length l -> (forall y, member y l -> y [<] x) -> maxlist l [<] x.

Lemma maxlist_leEq : forall y l,
0 < length l -> (forall x, member x l -> x [<=] y) -> maxlist l [<=] y.

Lemma minlist_smaller : forall l x, member x l -> minlist l [<=] x.

Lemma minlist_leEq_eps : forall l : list IR, {x : IR | member x l} ->
forall e, 0 [<] e -> {x : IR | member x l | x [<=] minlist l[+]e}.

Lemma less_minlist : forall x l,
0 < length l -> (forall y, member y l -> x [<] y) -> x [<] minlist l.

Lemma leEq_minlist : forall x l,
0 < length l -> (forall y, member y l -> x [<=] y) -> x [<=] minlist l.

End Lists.