Library Coq.Lists.List
Basics: definition of polymorphic lists and some operations
The definition of
list is now in
Init/Datatypes,
as well as the definitions of
length and
app
Open Scope list_scope.
Standard notations for lists.
In a special module to avoid conflicts.
Head and tail
The In predicate
Generic facts
Discrimination
Destruction
Facts about app
Discrimination
Concat with nil
app is associative
app commutes with cons
Facts deduced from the result of a concatenation
Compatibility with other operations
Facts about In
Characterization of
In
Theorem in_eq :
forall (
a:
A) (
l:
list A),
In a (
a :: l).
Theorem in_cons :
forall (
a b:
A) (
l:
list A),
In b l -> In b (
a :: l).
Theorem not_in_cons (
x a :
A) (
l :
list A):
~ In x (
a::l)
<-> x<>a /\ ~ In x l.
Theorem in_nil :
forall a:
A,
~ In a [].
Lemma in_app_or :
forall (
l m:
list A) (
a:
A),
In a (
l ++ m)
-> In a l \/ In a m.
Lemma in_or_app :
forall (
l m:
list A) (
a:
A),
In a l \/ In a m -> In a (
l ++ m).
Lemma in_app_iff :
forall l l' (
a:
A),
In a (
l++l')
<-> In a l \/ In a l'.
Theorem in_split :
forall x (
l:
list A),
In x l -> exists l1 l2, l = l1++x::l2.
Lemma in_elt :
forall (
x:
A)
l1 l2,
In x (
l1 ++ x :: l2).
Lemma in_elt_inv :
forall (
x y :
A)
l1 l2,
In x (
l1 ++ y :: l2)
-> x = y \/ In x (
l1 ++ l2).
Inversion
Decidability of In
Theorem in_dec :
(forall x y:
A,
{x = y} + {x <> y}) ->
forall (
a:
A) (
l:
list A),
{In a l} + {~ In a l}.
End Facts.
Hint Resolve app_assoc app_assoc_reverse:
datatypes.
Hint Resolve app_comm_cons app_cons_not_nil:
datatypes.
Hint Immediate app_eq_nil:
datatypes.
Hint Resolve app_eq_unit app_inj_tail:
datatypes.
Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app:
datatypes.
Operations on the elements of a list
Section Elts.
Variable A :
Type.
Fixpoint nth (
n:
nat) (
l:
list A) (
default:
A) {
struct l} :
A :=
match n,
l with
|
O,
x :: l' =>
x
|
O,
other =>
default
|
S m,
[] =>
default
|
S m,
x :: t =>
nth m t default
end.
Fixpoint nth_ok (
n:
nat) (
l:
list A) (
default:
A) {
struct l} :
bool :=
match n,
l with
|
O,
x :: l' =>
true
|
O,
other =>
false
|
S m,
[] =>
false
|
S m,
x :: t =>
nth_ok m t default
end.
Lemma nth_in_or_default :
forall (
n:
nat) (
l:
list A) (
d:
A),
{In (
nth n l d)
l} + {nth n l d = d}.
Lemma nth_S_cons :
forall (
n:
nat) (
l:
list A) (
d a:
A),
In (
nth n l d)
l -> In (
nth (
S n) (
a :: l)
d) (
a :: l).
Fixpoint nth_error (
l:
list A) (
n:
nat) {
struct n} :
option A :=
match n,
l with
|
O,
x :: _ =>
Some x
|
S n,
_ :: l =>
nth_error l n
|
_,
_ =>
None
end.
Definition nth_default (
default:
A) (
l:
list A) (
n:
nat) :
A :=
match nth_error l n with
|
Some x =>
x
|
None =>
default
end.
Lemma nth_default_eq :
forall n l (
d:
A),
nth_default d l n = nth n l d.
Results about nth
Lemma nth_In :
forall (
n:
nat) (
l:
list A) (
d:
A),
n < length l -> In (
nth n l d)
l.
Lemma In_nth l x d :
In x l ->
exists n, n < length l /\ nth n l d = x.
Lemma nth_overflow :
forall l n d,
length l <= n -> nth n l d = d.
Lemma nth_indep :
forall l n d d',
n < length l -> nth n l d = nth n l d'.
Lemma app_nth1 :
forall l l' d n,
n < length l -> nth n (
l++l')
d = nth n l d.
Lemma app_nth2 :
forall l l' d n,
n >= length l -> nth n (
l++l')
d = nth (
n-length l)
l' d.
Lemma app_nth2_plus :
forall l l' d n,
nth (
length l + n) (
l ++ l')
d = nth n l' d.
Lemma nth_middle :
forall l l' a d,
nth (
length l) (
l ++ a :: l')
d = a.
Lemma nth_split n l d :
n < length l ->
exists l1, exists l2, l = l1 ++ nth n l d :: l2 /\ length l1 = n.
Lemma nth_ext :
forall l l' d d',
length l = length l' ->
(forall n,
n < length l -> nth n l d = nth n l' d') -> l = l'.
Results about nth_error
Results directly relating nth and nth_error
Last element of a list
last l d returns the last element of the list
l,
or the default value
d if
l is empty.
removelast l remove the last element of l
Hypothesis eq_dec :
forall x y :
A,
{x = y}+{x <> y}.
Fixpoint remove (
x :
A) (
l :
list A) :
list A :=
match l with
|
[] =>
[]
|
y::tl =>
if (
eq_dec x y)
then remove x tl else y::(remove x tl)
end.
Lemma remove_cons :
forall x l,
remove x (
x :: l)
= remove x l.
Lemma remove_app :
forall x l1 l2,
remove x (
l1 ++ l2)
= remove x l1 ++ remove x l2.
Theorem remove_In :
forall (
l :
list A) (
x :
A),
~ In x (
remove x l).
Lemma notin_remove:
forall l x,
~ In x l -> remove x l = l.
Lemma in_remove:
forall l x y,
In x (
remove y l)
-> In x l /\ x <> y.
Lemma in_in_remove :
forall l x y,
x <> y -> In x l -> In x (
remove y l).
Lemma remove_remove_comm :
forall l x y,
remove x (
remove y l)
= remove y (
remove x l).
Lemma remove_remove_eq :
forall l x,
remove x (
remove x l)
= remove x l.
Lemma remove_length_le :
forall l x,
length (
remove x l)
<= length l.
Lemma remove_length_lt :
forall l x,
In x l -> length (
remove x l)
< length l.
Counting occurrences of an element
Compatibility of count_occ with operations on list
Compatibility with other operations
An alternative tail-recursive definition for reverse
Reverse Induction Principle on Lists
Decidable equality on lists
Applying functions to the elements of a list
Map
Section Map.
Variables (
A :
Type) (
B :
Type).
Variable f :
A -> B.
Fixpoint map (
l:
list A) :
list B :=
match l with
|
[] =>
[]
|
a :: t =>
(f a) :: (map t)
end.
Lemma map_cons (
x:
A)(
l:
list A) :
map (
x::l)
= (f x) :: (map l).
Lemma in_map :
forall (
l:
list A) (
x:
A),
In x l -> In (
f x) (
map l).
Lemma in_map_iff :
forall l y,
In y (
map l)
<-> exists x, f x = y /\ In x l.
Lemma map_length :
forall l,
length (
map l)
= length l.
Lemma map_nth :
forall l d n,
nth n (
map l) (
f d)
= f (
nth n l d).
Lemma map_nth_error :
forall n l d,
nth_error l n = Some d -> nth_error (
map l)
n = Some (
f d).
Lemma map_app :
forall l l',
map (
l++l')
= (map l)++(map l').
Lemma map_last :
forall l a,
map (
l ++ [a])
= (map l) ++ [f a].
Lemma map_rev :
forall l,
map (
rev l)
= rev (
map l).
Lemma map_eq_nil :
forall l,
map l = [] -> l = [].
Lemma map_eq_cons :
forall l l' b,
map l = b :: l' -> exists a tl, l = a :: tl /\ f a = b /\ map tl = l'.
Lemma map_eq_app :
forall l l1 l2,
map l = l1 ++ l2 -> exists l1' l2', l = l1' ++ l2' /\ map l1' = l1 /\ map l2' = l2.
map and count of occurrences
flat_map
Definition flat_map (
f:
A -> list B) :=
fix flat_map (
l:
list A) :
list B :=
match l with
|
nil =>
nil
|
cons x t =>
(f x)++(flat_map t)
end.
Lemma flat_map_app :
forall f l1 l2,
flat_map f (
l1 ++ l2)
= flat_map f l1 ++ flat_map f l2.
Lemma in_flat_map :
forall (
f:
A->list B)(
l:
list A)(
y:
B),
In y (
flat_map f l)
<-> exists x, In x l /\ In y (
f x).
End Map.
Lemma flat_map_concat_map :
forall A B (
f :
A -> list B)
l,
flat_map f l = concat (
map f l).
Lemma concat_map :
forall A B (
f :
A -> B)
l,
map f (
concat l)
= concat (
map (
map f)
l).
Lemma remove_concat A (
eq_dec :
forall x y :
A,
{x = y}+{x <> y}) :
forall l x,
remove eq_dec x (
concat l)
= flat_map (
remove eq_dec x)
l.
Lemma map_id :
forall (
A :
Type) (
l :
list A),
map (
fun x =>
x)
l = l.
Lemma map_map :
forall (
A B C:
Type)(
f:
A->B)(
g:
B->C)
l,
map g (
map f l)
= map (
fun x =>
g (
f x))
l.
Lemma map_ext_in :
forall (
A B :
Type)(
f g:
A->B)
l,
(forall a,
In a l -> f a = g a) -> map f l = map g l.
Lemma ext_in_map :
forall (
A B :
Type)(
f g:
A->B)
l,
map f l = map g l -> forall a,
In a l -> f a = g a.
Lemma map_ext_in_iff :
forall (
A B :
Type)(
f g:
A->B)
l,
map f l = map g l <-> forall a,
In a l -> f a = g a.
Lemma map_ext :
forall (
A B :
Type)(
f g:
A->B),
(forall a,
f a = g a) -> forall l,
map f l = map g l.
Lemma flat_map_ext :
forall (
A B :
Type)(
f g :
A -> list B),
(forall a,
f a = g a) -> forall l,
flat_map f l = flat_map g l.
Lemma nth_nth_nth_map A :
forall (
l :
list A)
n d ln dn,
n < length ln \/ length l <= dn ->
nth (
nth n ln dn)
l d = nth n (
map (
fun x =>
nth x l d)
ln)
d.
Left-to-right iterator on lists
Right-to-left iterator on lists
(list_power x y) is y^x, or the set of sequences of elts of y
indexed by elts of x, sorted in lexicographic order.
Boolean operations over lists
find whether a boolean function can be satisfied by an
elements of the list.
find whether a boolean function is satisfied by
all the elements of a list.
filter
find
partition
Fixpoint partition (
l:
list A) :
list A * list A :=
match l with
|
nil =>
(nil, nil)
|
x :: tl =>
let (
g,
d) :=
partition tl in
if f x then (x::g,d) else (g,x::d)
end.
Theorem partition_cons1 a l l1 l2:
partition l = (l1, l2) ->
f a = true ->
partition (
a::l)
= (a::l1, l2).
Theorem partition_cons2 a l l1 l2:
partition l = (l1, l2) ->
f a=false ->
partition (
a::l)
= (l1, a::l2).
Theorem partition_length l l1 l2:
partition l = (l1, l2) ->
length l = length l1 + length l2.
Theorem partition_inv_nil (
l :
list A):
partition l = ([], []) <-> l = [].
Theorem elements_in_partition l l1 l2:
partition l = (l1, l2) ->
forall x:
A,
In x l <-> In x l1 \/ In x l2.
End Bool.
Section Filtering.
Variables (
A :
Type).
Lemma filter_map :
forall (
f g :
A -> bool) (
l :
list A),
filter f l = filter g l <-> map f l = map g l.
Lemma filter_ext_in :
forall (
f g :
A -> bool) (
l :
list A),
(forall a,
In a l -> f a = g a) -> filter f l = filter g l.
Lemma ext_in_filter :
forall (
f g :
A -> bool) (
l :
list A),
filter f l = filter g l -> (forall a,
In a l -> f a = g a).
Lemma filter_ext_in_iff :
forall (
f g :
A -> bool) (
l :
list A),
filter f l = filter g l <-> (forall a,
In a l -> f a = g a).
Lemma filter_ext :
forall (
f g :
A -> bool),
(forall a,
f a = g a) -> forall l,
filter f l = filter g l.
Remove by filtering
Counting occurrences by filtering
Operations on lists of pairs or lists of lists
split derives two lists from a list of pairs
Fixpoint split (
l:
list (
A*B)) :
list A * list B :=
match l with
|
[] =>
([], [])
|
(x,y) :: tl =>
let (
left,
right) :=
split tl in (x::left, y::right)
end.
Lemma in_split_l :
forall (
l:
list (
A*B))(
p:
A*B),
In p l -> In (
fst p) (
fst (
split l)).
Lemma in_split_r :
forall (
l:
list (
A*B))(
p:
A*B),
In p l -> In (
snd p) (
snd (
split l)).
Lemma split_nth :
forall (
l:
list (
A*B))(
n:
nat)(
d:
A*B),
nth n l d = (nth n (
fst (
split l)) (
fst d)
, nth n (
snd (
split l)) (
snd d)
).
Lemma split_length_l :
forall (
l:
list (
A*B)),
length (
fst (
split l))
= length l.
Lemma split_length_r :
forall (
l:
list (
A*B)),
length (
snd (
split l))
= length l.
combine is the opposite of split.
Lists given to combine are meant to be of same length.
If not, combine stops on the shorter list
Fixpoint combine (
l :
list A) (
l' :
list B) :
list (
A*B) :=
match l,
l' with
|
x::tl,
y::tl' =>
(x,y)::(combine tl tl')
|
_,
_ =>
nil
end.
Lemma split_combine :
forall (
l:
list (
A*B)),
let (
l1,
l2) :=
split l in combine l1 l2 = l.
Lemma combine_split :
forall (
l:
list A)(
l':
list B),
length l = length l' ->
split (
combine l l')
= (l,l').
Lemma in_combine_l :
forall (
l:
list A)(
l':
list B)(
x:
A)(
y:
B),
In (x,y) (
combine l l')
-> In x l.
Lemma in_combine_r :
forall (
l:
list A)(
l':
list B)(
x:
A)(
y:
B),
In (x,y) (
combine l l')
-> In y l'.
Lemma combine_length :
forall (
l:
list A)(
l':
list B),
length (
combine l l')
= min (
length l) (
length l').
Lemma combine_nth :
forall (
l:
list A)(
l':
list B)(
n:
nat)(
x:
A)(
y:
B),
length l = length l' ->
nth n (
combine l l')
(x,y) = (nth n l x, nth n l' y).
list_prod has the same signature as combine, but unlike
combine, it adds every possible pairs, not only those at the
same position.
Miscellaneous operations on lists
Length order of lists
Section SetIncl.
Variable A :
Type.
Definition incl (
l m:
list A) :=
forall a:
A,
In a l -> In a m.
Hint Unfold incl :
core.
Lemma incl_nil_l :
forall l,
incl nil l.
Lemma incl_l_nil :
forall l,
incl l nil -> l = nil.
Lemma incl_refl :
forall l:
list A,
incl l l.
Hint Resolve incl_refl :
core.
Lemma incl_tl :
forall (
a:
A) (
l m:
list A),
incl l m -> incl l (
a :: m).
Hint Immediate incl_tl :
core.
Lemma incl_tran :
forall l m n:
list A,
incl l m -> incl m n -> incl l n.
Lemma incl_appl :
forall l m n:
list A,
incl l n -> incl l (
n ++ m).
Hint Immediate incl_appl :
core.
Lemma incl_appr :
forall l m n:
list A,
incl l n -> incl l (
m ++ n).
Hint Immediate incl_appr :
core.
Lemma incl_cons :
forall (
a:
A) (
l m:
list A),
In a m -> incl l m -> incl (
a :: l)
m.
Hint Resolve incl_cons :
core.
Lemma incl_cons_inv :
forall (
a:
A) (
l m:
list A),
incl (
a :: l)
m -> In a m /\ incl l m.
Lemma incl_app :
forall l m n:
list A,
incl l n -> incl m n -> incl (
l ++ m)
n.
Hint Resolve incl_app :
core.
Lemma incl_app_app :
forall l1 l2 m1 m2:
list A,
incl l1 m1 -> incl l2 m2 -> incl (
l1 ++ l2) (
m1 ++ m2).
Lemma incl_app_inv :
forall l1 l2 m :
list A,
incl (
l1 ++ l2)
m -> incl l1 m /\ incl l2 m.
Lemma incl_filter f l :
incl (
filter f l)
l.
Lemma remove_incl (
eq_dec :
forall x y :
A,
{x = y} + {x <> y}) :
forall l1 l2 x,
incl l1 l2 -> incl (
remove eq_dec x l1) (
remove eq_dec x l2).
End SetIncl.
Lemma incl_map A B (
f :
A -> B)
l1 l2 :
incl l1 l2 -> incl (
map f l1) (
map f l2).
Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons
incl_app incl_map:
datatypes.
Cutting a list at some position
Section Cutting.
Variable A :
Type.
Fixpoint firstn (
n:
nat)(
l:
list A) :
list A :=
match n with
| 0 =>
nil
|
S n =>
match l with
|
nil =>
nil
|
a::l =>
a::(firstn n l)
end
end.
Lemma firstn_nil n:
firstn n [] = [].
Lemma firstn_cons n a l:
firstn (
S n) (
a::l)
= a :: (firstn n l).
Lemma firstn_all l:
firstn (
length l)
l = l.
Lemma firstn_all2 n:
forall (
l:
list A),
(length l) <= n -> firstn n l = l.
Lemma firstn_O l:
firstn 0
l = [].
Lemma firstn_le_length n:
forall l:
list A,
length (
firstn n l)
<= n.
Lemma firstn_length_le:
forall l:
list A,
forall n:
nat,
n <= length l -> length (
firstn n l)
= n.
Lemma firstn_app n:
forall l1 l2,
firstn n (
l1 ++ l2)
= (firstn n l1) ++ (firstn (
n - length l1)
l2).
Lemma firstn_app_2 n:
forall l1 l2,
firstn (
(length l1) + n) (
l1 ++ l2)
= l1 ++ firstn n l2.
Lemma firstn_firstn:
forall l:
list A,
forall i j :
nat,
firstn i (
firstn j l)
= firstn (
min i j)
l.
Fixpoint skipn (
n:
nat)(
l:
list A) :
list A :=
match n with
| 0 =>
l
|
S n =>
match l with
|
nil =>
nil
|
a::l =>
skipn n l
end
end.
Lemma firstn_skipn_comm :
forall m n l,
firstn m (
skipn n l)
= skipn n (
firstn (
n + m)
l).
Lemma skipn_firstn_comm :
forall m n l,
skipn m (
firstn n l)
= firstn (
n - m) (
skipn m l).
Lemma skipn_O :
forall l,
skipn 0
l = l.
Lemma skipn_nil :
forall n,
skipn n (
[] :
list A)
= [].
Lemma skipn_cons n a l:
skipn (
S n) (
a::l)
= skipn n l.
Lemma skipn_all :
forall l,
skipn (
length l)
l = nil.
#[
deprecated(
since="8.12",
note="Use skipn_all instead.")]
Notation skipn_none :=
skipn_all.
Lemma skipn_all2 n:
forall l,
length l <= n -> skipn n l = [].
Lemma firstn_skipn :
forall n l,
firstn n l ++ skipn n l = l.
Lemma firstn_length :
forall n l,
length (
firstn n l)
= min n (
length l).
Lemma skipn_length n :
forall l,
length (
skipn n l)
= length l - n.
Lemma skipn_app n :
forall l1 l2,
skipn n (
l1 ++ l2)
= (skipn n l1) ++ (skipn (
n - length l1)
l2).
Lemma firstn_skipn_rev:
forall x l,
firstn x l = rev (
skipn (
length l - x) (
rev l)).
Lemma firstn_rev:
forall x l,
firstn x (
rev l)
= rev (
skipn (
length l - x)
l).
Lemma skipn_rev:
forall x l,
skipn x (
rev l)
= rev (
firstn (
length l - x)
l).
Lemma removelast_firstn :
forall n l,
n < length l ->
removelast (
firstn (
S n)
l)
= firstn n l.
Lemma removelast_firstn_len :
forall l,
removelast l = firstn (
pred (
length l))
l.
Lemma firstn_removelast :
forall n l,
n < length l ->
firstn n (
removelast l)
= firstn n l.
End Cutting.
Combining pairs of lists of possibly-different lengths
Predicate for List addition/removal (no need for decidability)
Effective computation of a list without duplicates
Alternative characterisations of being without duplicates,
thanks to nth_error and nth
Having NoDup hypotheses bring more precise facts about incl.
NoDup and map
NB: the reciprocal result holds only for injective functions,
see FinFun.v
Sequence of natural numbers
seq computes the sequence of len contiguous integers
that starts at start. For instance, seq 2 3 is 2::3::4::nil.
Existential and universal predicates over lists
Variable A:
Type.
Section One_predicate.
Variable P:
A->Prop.
Inductive Exists :
list A -> Prop :=
|
Exists_cons_hd :
forall x l,
P x -> Exists (
x::l)
|
Exists_cons_tl :
forall x l,
Exists l -> Exists (
x::l).
Hint Constructors Exists :
core.
Lemma Exists_exists (
l:
list A) :
Exists l <-> (exists x, In x l /\ P x).
Lemma Exists_nth l :
Exists l <-> exists i d, i < length l /\ P (
nth i l d).
Lemma Exists_nil :
Exists nil <-> False.
Lemma Exists_cons x l:
Exists (
x::l)
<-> P x \/ Exists l.
Lemma Exists_app l1 l2 :
Exists (
l1 ++ l2)
<-> Exists l1 \/ Exists l2.
Lemma Exists_rev l :
Exists l -> Exists (
rev l).
Lemma Exists_dec l:
(forall x:
A,
{P x} + { ~ P x }) ->
{Exists l} + {~ Exists l}.
Lemma Exists_fold_right l :
Exists l <-> fold_right (
fun x =>
or (
P x))
False l.
Lemma incl_Exists l1 l2 :
incl l1 l2 -> Exists l1 -> Exists l2.
Inductive Forall :
list A -> Prop :=
|
Forall_nil :
Forall nil
|
Forall_cons :
forall x l,
P x -> Forall l -> Forall (
x::l).
Hint Constructors Forall :
core.
Lemma Forall_forall (
l:
list A):
Forall l <-> (forall x,
In x l -> P x).
Lemma Forall_nth l :
Forall l <-> forall i d,
i < length l -> P (
nth i l d).
Lemma Forall_inv :
forall (
a:
A)
l,
Forall (
a :: l)
-> P a.
Theorem Forall_inv_tail :
forall (
a:
A)
l,
Forall (
a :: l)
-> Forall l.
Lemma Forall_app l1 l2 :
Forall (
l1 ++ l2)
<-> Forall l1 /\ Forall l2.
Lemma Forall_elt a l1 l2 :
Forall (
l1 ++ a :: l2)
-> P a.
Lemma Forall_rev l :
Forall l -> Forall (
rev l).
Lemma Forall_rect :
forall (
Q :
list A -> Type),
Q [] -> (forall b l,
P b -> Q (
b :: l)
) -> forall l,
Forall l -> Q l.
Lemma Forall_dec :
(forall x:
A,
{P x} + { ~ P x }) ->
forall l:
list A,
{Forall l} + {~ Forall l}.
Lemma Forall_fold_right l :
Forall l <-> fold_right (
fun x =>
and (
P x))
True l.
Lemma incl_Forall l1 l2 :
incl l2 l1 -> Forall l1 -> Forall l2.
End One_predicate.
Lemma map_ext_Forall B :
forall (
f g :
A -> B)
l,
Forall (
fun x =>
f x = g x)
l -> map f l = map g l.
Theorem Exists_impl :
forall (
P Q :
A -> Prop),
(forall a :
A,
P a -> Q a) ->
forall l,
Exists P l -> Exists Q l.
Lemma Exists_or :
forall (
P Q :
A -> Prop)
l,
Exists P l \/ Exists Q l -> Exists (
fun x =>
P x \/ Q x)
l.
Lemma Exists_or_inv :
forall (
P Q :
A -> Prop)
l,
Exists (
fun x =>
P x \/ Q x)
l -> Exists P l \/ Exists Q l.
Lemma Forall_impl :
forall (
P Q :
A -> Prop),
(forall a,
P a -> Q a) ->
forall l,
Forall P l -> Forall Q l.
Lemma Forall_and :
forall (
P Q :
A -> Prop)
l,
Forall P l -> Forall Q l -> Forall (
fun x =>
P x /\ Q x)
l.
Lemma Forall_and_inv :
forall (
P Q :
A -> Prop)
l,
Forall (
fun x =>
P x /\ Q x)
l -> Forall P l /\ Forall Q l.
Lemma Forall_Exists_neg (
P:
A->Prop)(
l:
list A) :
Forall (
fun x =>
~ P x)
l <-> ~(Exists P l).
Lemma Exists_Forall_neg (
P:
A->Prop)(
l:
list A) :
(forall x,
P x \/ ~P x) ->
Exists (
fun x =>
~ P x)
l <-> ~(Forall P l).
Lemma neg_Forall_Exists_neg (
P:
A->Prop) (
l:
list A) :
(forall x:
A,
{P x} + { ~ P x }) ->
~ Forall P l ->
Exists (
fun x =>
~ P x)
l.
Lemma Forall_Exists_dec (
P:
A->Prop) :
(forall x:
A,
{P x} + { ~ P x }) ->
forall l:
list A,
{Forall P l} + {Exists (
fun x =>
~ P x)
l}.
Lemma incl_Forall_in_iff l l' :
incl l l' <-> Forall (
fun x =>
In x l')
l.
End Exists_Forall.
Hint Constructors Exists :
core.
Hint Constructors Forall :
core.
Lemma exists_Forall A B :
forall (
P :
A -> B -> Prop)
l,
(exists k, Forall (
P k)
l) -> Forall (
fun x =>
exists k, P k x)
l.
Lemma Forall_image A B :
forall (
f :
A -> B)
l,
Forall (
fun y =>
exists x, y = f x)
l <-> exists l', l = map f l'.
Lemma concat_nil_Forall A :
forall (
l :
list (
list A)),
concat l = nil <-> Forall (
fun x =>
x = nil)
l.
Lemma in_flat_map_Exists A B :
forall (
f :
A -> list B)
x l,
In x (
flat_map f l)
<-> Exists (
fun y =>
In x (
f y))
l.
Lemma notin_flat_map_Forall A B :
forall (
f :
A -> list B)
x l,
~ In x (
flat_map f l)
<-> Forall (
fun y =>
~ In x (
f y))
l.
Section Forall2.
Forall2: stating that elements of two lists are pairwise related.
ForallPairs : specifies that a certain relation should
always hold when inspecting all possible pairs of elements of a list.
ForallOrdPairs : we still check a relation over all pairs
of elements of a list, but now the order of elements matters.
ForallPairs implies ForallOrdPairs. The reverse implication is true
only when R is symmetric and reflexive.
Sum of elements of a list of nat: list_sum
Max of elements of a list of nat: list_max
Inversion of predicates over lists based on head symbol
Ltac is_list_constr c :=
match c with
|
nil =>
idtac
| (
_::_) =>
idtac
|
_ =>
fail
end.
Ltac invlist f :=
match goal with
|
H:
f ?
l |-
_ =>
is_list_constr l;
inversion_clear H;
invlist f
|
H:
f _ ?
l |-
_ =>
is_list_constr l;
inversion_clear H;
invlist f
|
H:
f _ _ ?
l |-
_ =>
is_list_constr l;
inversion_clear H;
invlist f
|
H:
f _ _ _ ?
l |-
_ =>
is_list_constr l;
inversion_clear H;
invlist f
|
H:
f _ _ _ _ ?
l |-
_ =>
is_list_constr l;
inversion_clear H;
invlist f
|
_ =>
idtac
end.
Exporting hints and tactics