Library ListFunctions
This file is part of
A Formal Definition of JML in Coq
and its Application to Runtime Assertion Checking
Ph.D. Thesis by Hermann Lehner
Online available at jmlcoq.info
Authors:
- Hermann Lehner
- David Pichardie (Bicolano)
- Andreas Kaegi (Syntax Rewritings, Implementation of ADTs)
Useful functions on lists, not part of the Coq standard library.
Most functions are taken from the Haskell standard libary module Data.List.
Make a singleton list from the given element a.
Drop all prefix elements of l that satisfy p.
Fixpoint dropWhile (p:A->bool) (l:list A) {struct l} : list A :=
match l with
| nil => nil
| (x::xs) => if p x then dropWhile p xs else xs
end.
match l with
| nil => nil
| (x::xs) => if p x then dropWhile p xs else xs
end.
Concatenate all given lists into a flat list.
Maximum element of the given list of natural numbers.
Fixpoint maximum (e:nat) (l:list nat) {struct l} : nat :=
match l with
| nil => e
| (x::xs) => max x (maximum e xs)
end.
match l with
| nil => e
| (x::xs) => max x (maximum e xs)
end.
Like fold_left but take e for the empty list. e is not used for a non-empty list.
Definition fold_left1 (op:A->A->A) (l:list A) (e:A) : A :=
match l with
| nil => e
| x::xs => fold_left op xs x
end.
match l with
| nil => e
| x::xs => fold_left op xs x
end.
Like fold_right but take e for the empty list. e is not used for a non-empty list.
Fixpoint fold_right1 (op:A->A->A) (l:list A) (e:A) : A :=
match l with
| nil => e
| x::nil => x
| x::xs => op x (fold_right1 op xs e)
end.
End ListFunctions.
Implicit Arguments singleton [A].
Implicit Arguments dropWhile [A].
Implicit Arguments concat [A].
Implicit Arguments fold_left1 [A].
Implicit Arguments fold_right1 [A].
Inductive Expr : Set :=
| Lit : nat -> Expr
| Add : Expr -> Expr -> Expr.
Section Proofs.
Variable A : Type.
match l with
| nil => e
| x::nil => x
| x::xs => op x (fold_right1 op xs e)
end.
End ListFunctions.
Implicit Arguments singleton [A].
Implicit Arguments dropWhile [A].
Implicit Arguments concat [A].
Implicit Arguments fold_left1 [A].
Implicit Arguments fold_right1 [A].
Inductive Expr : Set :=
| Lit : nat -> Expr
| Add : Expr -> Expr -> Expr.
Section Proofs.
Variable A : Type.
For every element y in the result list (concat l), there exists a list x in l that contains y.
Lemma in_concat : forall (l:list (list A)) (y:A),
In y (concat l) <-> exists x, In x l /\ In y x.
Proof.
apply (in_flat_map (fun x:list A => x)).
Qed.
In y (concat l) <-> exists x, In x l /\ In y x.
Proof.
apply (in_flat_map (fun x:list A => x)).
Qed.
e is the maximum of the empty list.
Lemma maximum_e_nil : forall (e:nat) (l:list nat), l=nil -> maximum e l=e.
Proof.
intros e l H.
rewrite H.
simpl.
reflexivity.
Qed.
Proof.
intros e l H.
rewrite H.
simpl.
reflexivity.
Qed.
maximum is composable using max and cons.
Lemma maximum_e_cons : forall (e:nat) (x:nat) (l:list nat),
maximum e (x::l) = max x (maximum e l).
Proof.
intros e x l.
simpl.
reflexivity.
Qed.
maximum e (x::l) = max x (maximum e l).
Proof.
intros e x l.
simpl.
reflexivity.
Qed.
fold_left1 op nil e = e
Lemma fold_left1_e_nil : forall (op:A->A->A) (e:A) (l:list A),
l=nil ->
fold_left1 op l e = e.
Proof.
intros op e l H.
rewrite H.
simpl.
reflexivity.
Qed.
l=nil ->
fold_left1 op l e = e.
Proof.
intros op e l H.
rewrite H.
simpl.
reflexivity.
Qed.
fold_left1 op (x::l) e = fold_left1 op l x,
e vanishes for a non-empty list.
Lemma fold_left1_fold_left : forall (op:A->A->A) (e:A) (x:A) (l:list A),
fold_left1 op (x::l) e = fold_left op l x.
Proof.
intros op e x l.
simpl.
reflexivity.
Qed.
fold_left1 op (x::l) e = fold_left op l x.
Proof.
intros op e x l.
simpl.
reflexivity.
Qed.
The element found by find satisfies predicate p.