Library Coq.Lists.List
Basics: definition of polymorphic lists and some operations
#[local] Open Scope bool_scope.
Open Scope list_scope.
Standard notations for lists.
In a special module to avoid conflicts.
Module ListNotations.
Notation "[ ]" := nil (format "[ ]") : list_scope.
Notation "[ x ]" := (cons x nil) : list_scope.
Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..))
(format "[ '[' x ; '/' y ; '/' .. ; '/' z ']' ]") : list_scope.
End ListNotations.
Import ListNotations.
Section Lists.
Variable A : Type.
Notation "[ ]" := nil (format "[ ]") : list_scope.
Notation "[ x ]" := (cons x nil) : list_scope.
Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..))
(format "[ '[' x ; '/' y ; '/' .. ; '/' z ']' ]") : list_scope.
End ListNotations.
Import ListNotations.
Section Lists.
Variable A : Type.
Head and tail
Definition hd (default:A) (l:list A) :=
match l with
| [] => default
| x :: _ => x
end.
Definition hd_error (l:list A) :=
match l with
| [] => None
| x :: _ => Some x
end.
Definition tl (l:list A) :=
match l with
| [] => nil
| a :: m => m
end.
The In predicate
Fixpoint In (a:A) (l:list A) : Prop :=
match l with
| [] => False
| b :: m => b = a \/ In a m
end.
End Lists.
Section Facts.
Variable A : Type.
match l with
| [] => False
| b :: m => b = a \/ In a m
end.
End Lists.
Section Facts.
Variable A : Type.
Destruction
Theorem destruct_list (l : list A) : {x:A & {tl:list A | l = x::tl}}+{l = []}.
Lemma hd_error_tl_repr l (a:A) r :
hd_error l = Some a /\ tl l = r <-> l = a :: r.
Lemma hd_error_some_nil l (a:A) : hd_error l = Some a -> l <> nil.
Theorem length_zero_iff_nil (l : list A):
length l = 0 <-> l = [].
Theorem hd_error_nil : hd_error (@nil A) = None.
Theorem hd_error_cons (l : list A) (x : A) : hd_error (x::l) = Some x.
Concat with nil
app is associative
app commutes with cons
Facts deduced from the result of a concatenation
Theorem app_eq_nil (l l':list A) : l ++ l' = [] -> l = [] /\ l' = [].
Lemma app_eq_cons x y z (a : A):
x ++ y = a :: z -> (x = nil /\ y = a :: z) \/ exists x', x = a :: x' /\ z = x' ++ y.
Theorem app_eq_unit (x y:list A) (a:A) :
x ++ y = [a] -> x = [] /\ y = [a] \/ x = [a] /\ y = [].
Lemma elt_eq_unit l1 l2 (a b : A) :
l1 ++ a :: l2 = [b] -> a = b /\ l1 = [] /\ l2 = [].
Theorem app_eq_app X (x1 x2 y1 y2: list X) : x1++x2 = y1++y2 ->
exists l, (x1 = y1++l /\ y2 = l++x2) \/ (y1 = x1++l /\ x2 = l++y2).
Lemma app_inj_tail :
forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b.
Lemma app_inj_tail_iff :
forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] <-> x = y /\ a = b.
Compatibility with other operations
Lemma length_app : forall l l' : list A, length (l++l') = length l + length l'.
Lemma last_length : forall (l : list A) a, length (l ++ a :: nil) = S (length l).
Lemma app_inv_head_iff:
forall l l1 l2 : list A, l ++ l1 = l ++ l2 <-> l1 = l2.
Lemma app_inv_head:
forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2.
Lemma app_inv_tail:
forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2.
Lemma app_inv_tail_iff:
forall l l1 l2 : list A, l1 ++ l = l2 ++ l <-> l1 = l2.
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).
Lemma app_inj_pivot x1 x2 y1 y2 (a : A): x1 ++ a :: x2 = y1 ++ a :: y2 ->
((In a x1 /\ In a y2) \/ (In a x2 /\ In a y1)) \/ (x1 = y1 /\ x2 = y2).
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.
#[global]
Hint Resolve app_assoc app_assoc_reverse_deprecated: datatypes.
#[global]
Hint Resolve app_comm_cons app_cons_not_nil: datatypes.
#[global]
Hint Immediate app_eq_nil: datatypes.
#[global]
Hint Resolve app_eq_unit app_inj_tail: datatypes.
#[global]
Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes.
Local Ltac Tauto.intuition_solver ::= auto with datatypes.
(forall x y:A, {x = y} + {x <> y}) ->
forall (a:A) (l:list A), {In a l} + {~ In a l}.
End Facts.
#[global]
Hint Resolve app_assoc app_assoc_reverse_deprecated: datatypes.
#[global]
Hint Resolve app_comm_cons app_cons_not_nil: datatypes.
#[global]
Hint Immediate app_eq_nil: datatypes.
#[global]
Hint Resolve app_eq_unit app_inj_tail: datatypes.
#[global]
Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes.
Local Ltac Tauto.intuition_solver ::= auto with datatypes.
Fixpoint nth (n:nat) (l:list A) (default:A) {struct l} : A :=
match n, l with
| O, x :: l' => x
| O, [] => 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, [] => 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
Lemma nth_error_In l n x : nth_error l n = Some x -> In x l.
Lemma In_nth_error l x : In x l -> exists n, nth_error l n = Some x.
Lemma In_iff_nth_error l x : In x l <-> exists n, nth_error l n = Some x.
Lemma nth_error_None l n : nth_error l n = None <-> length l <= n.
Lemma nth_error_Some l n : nth_error l n <> None <-> n < length l.
Lemma nth_error_split l n a : nth_error l n = Some a ->
exists l1, exists l2, l = l1 ++ a :: l2 /\ length l1 = n.
Lemma nth_error_app1 l l' n : n < length l ->
nth_error (l++l') n = nth_error l n.
Lemma nth_error_app2 l l' n : length l <= n ->
nth_error (l++l') n = nth_error l' (n-length l).
Lemma nth_error_app l l' n : nth_error (l ++ l') n =
if Nat.ltb n (length l)
then nth_error l n
else nth_error l' (n - length l).
Lemma nth_error_ext l l':
(forall n, nth_error l n = nth_error l' n) -> l = l'.
Lemma unfold_nth_error l n
: nth_error l n
= match n, l with
| O, x :: _ => Some x
| S n, _ :: l => nth_error l n
| _, _ => None
end.
Lemma nth_error_nil n : nth_error nil n = None.
Lemma nth_error_cons x xs n
: nth_error (x :: xs) n
= match n with
| O => Some x
| S n => nth_error xs n
end.
Lemma nth_error_O l
: nth_error l O = hd_error l.
Lemma nth_error_S l n
: nth_error l (S n) = nth_error (tl l) n.
Lemma nth_error_cons_0 x l : nth_error (cons x l) 0 = Some x.
Lemma nth_error_cons_succ x l n :
nth_error (cons x l) (S n) = nth_error l n.
Results directly relating nth and nth_error
Lemma nth_error_nth : forall (l : list A) (n : nat) (x d : A),
nth_error l n = Some x -> nth n l d = x.
Lemma nth_error_nth' : forall (l : list A) (n : nat) (d : A),
n < length l -> nth_error l n = Some (nth n l d).
Lemma nth_error_nth_None (l : list A) (n : nat) (d : A) :
nth_error l n = None -> nth n l d = d.
Last element of a list
Fixpoint last (l:list A) (d:A) : A :=
match l with
| [] => d
| [a] => a
| a :: l => last l d
end.
Lemma last_last : forall l a d, last (l ++ [a]) d = a.
removelast l remove the last element of l
Fixpoint removelast (l:list A) : list A :=
match l with
| [] => []
| [a] => []
| a :: l => a :: removelast l
end.
Lemma app_removelast_last :
forall l d, l <> [] -> l = removelast l ++ [last l d].
Lemma exists_last :
forall l, l <> [] -> { l' : (list A) & { a : A | l = l' ++ [a]}}.
Lemma removelast_app :
forall l l', l' <> [] -> removelast (l++l') = l ++ removelast l'.
Lemma removelast_last : forall l a, removelast (l ++ [a]) = 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.
Fixpoint count_occ (l : list A) (x : A) : nat :=
match l with
| [] => 0
| y :: tl =>
let n := count_occ tl x in
if eq_dec y x then S n else n
end.
Compatibility of count_occ with operations on list
Theorem count_occ_In l x : In x l <-> count_occ l x > 0.
Theorem count_occ_not_In l x : ~ In x l <-> count_occ l x = 0.
Lemma count_occ_nil x : count_occ [] x = 0.
Theorem count_occ_inv_nil l :
(forall x:A, count_occ l x = 0) <-> l = [].
Lemma count_occ_cons_eq l x y :
x = y -> count_occ (x::l) y = S (count_occ l y).
Lemma count_occ_cons_neq l x y :
x <> y -> count_occ (x::l) y = count_occ l y.
Lemma count_occ_app l1 l2 x :
count_occ (l1 ++ l2) x = count_occ l1 x + count_occ l2 x.
Lemma count_occ_elt_eq l1 l2 x y : x = y ->
count_occ (l1 ++ x :: l2) y = S (count_occ (l1 ++ l2) y).
Lemma count_occ_elt_neq l1 l2 x y : x <> y ->
count_occ (l1 ++ x :: l2) y = count_occ (l1 ++ l2) y.
Lemma count_occ_bound x l : count_occ l x <= length l.
End Elts.
Theorem count_occ_not_In l x : ~ In x l <-> count_occ l x = 0.
Lemma count_occ_nil x : count_occ [] x = 0.
Theorem count_occ_inv_nil l :
(forall x:A, count_occ l x = 0) <-> l = [].
Lemma count_occ_cons_eq l x y :
x = y -> count_occ (x::l) y = S (count_occ l y).
Lemma count_occ_cons_neq l x y :
x <> y -> count_occ (x::l) y = count_occ l y.
Lemma count_occ_app l1 l2 x :
count_occ (l1 ++ l2) x = count_occ l1 x + count_occ l2 x.
Lemma count_occ_elt_eq l1 l2 x y : x = y ->
count_occ (l1 ++ x :: l2) y = S (count_occ (l1 ++ l2) y).
Lemma count_occ_elt_neq l1 l2 x y : x <> y ->
count_occ (l1 ++ x :: l2) y = count_occ (l1 ++ l2) y.
Lemma count_occ_bound x l : count_occ l x <= length l.
End Elts.
Fixpoint rev (l:list A) : list A :=
match l with
| [] => []
| x :: l' => rev l' ++ [x]
end.
Lemma rev_app_distr : forall x y:list A, rev (x ++ y) = rev y ++ rev x.
Remark rev_unit : forall (l:list A) (a:A), rev (l ++ [a]) = a :: rev l.
Lemma rev_involutive : forall l:list A, rev (rev l) = l.
Lemma rev_inj (l1 l2: list A):
rev l1 = rev l2 -> l1 = l2.
Lemma rev_eq_app : forall l l1 l2, rev l = l1 ++ l2 -> l = rev l2 ++ rev l1.
Reverse Induction Principle on Lists
Lemma rev_list_ind : forall P:list A-> Prop,
P [] ->
(forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) ->
forall l:list A, P (rev l).
Theorem rev_ind : forall P:list A -> Prop,
P [] ->
(forall (x:A) (l:list A), P l -> P (l ++ [x])) -> forall l:list A, P l.
Compatibility with other operations
Lemma in_rev : forall l x, In x l <-> In x (rev l).
Lemma length_rev : forall l, length (rev l) = length l.
Lemma rev_nth : forall l d n, n < length l ->
nth n (rev l) d = nth (length l - S n) l d.
Lemma nth_error_rev n l : nth_error (rev l) n =
if Nat.ltb n (length l) then nth_error l (length l - S n) else None.
An alternative tail-recursive definition for reverse
Fixpoint rev_append (l l': list A) : list A :=
match l with
| [] => l'
| a::l => rev_append l (a::l')
end.
Definition rev' l : list A := rev_append l [].
Lemma rev_append_rev : forall l l', rev_append l l' = rev l ++ l'.
Lemma rev_alt : forall l, rev l = rev_append l [].
Fixpoint concat (l : list (list A)) : list A :=
match l with
| nil => nil
| cons x l => x ++ concat l
end.
Lemma concat_nil : concat nil = nil.
Lemma concat_cons : forall x l, concat (cons x l) = x ++ concat l.
Lemma concat_app : forall l1 l2, concat (l1 ++ l2) = concat l1 ++ concat l2.
Lemma in_concat : forall l y,
In y (concat l) <-> exists x, In x l /\ In y x.
Hypothesis eq_dec : forall (x y : A), {x = y}+{x <> y}.
Lemma list_eq_dec : forall l l':list A, {l = l'} + {l <> l'}.
Lemma count_occ_rev l x : count_occ eq_dec (rev l) x = count_occ eq_dec l x.
End ListOps.
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 length_map : 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 nth_error_map : forall n l,
nth_error (map l) n = option_map f (nth_error l n).
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
Hypothesis decA: forall x1 x2 : A, {x1 = x2} + {x1 <> x2}.
Hypothesis decB: forall y1 y2 : B, {y1 = y2} + {y1 <> y2}.
Hypothesis Hfinjective: forall x1 x2: A, (f x1) = (f x2) -> x1 = x2.
Theorem count_occ_map x l:
count_occ decA l x = count_occ decB (map l) (f x).
End Map.
flat_map
Definition flat_map :=
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_concat_map l :
flat_map l = concat (map f l).
Lemma flat_map_app l1 l2 :
flat_map (l1 ++ l2) = flat_map l1 ++ flat_map l2.
Lemma in_flat_map l y :
In y (flat_map l) <-> exists x, In x l /\ In y (f x).
End FlatMap.
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.
Arguments ext_in_map [A B f g l].
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.
Arguments map_ext_in_iff {A B f g l}.
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
Section Fold_Left_Recursor.
Variables (A : Type) (B : Type).
Variable f : A -> B -> A.
Fixpoint fold_left (l:list B) (a0:A) : A :=
match l with
| nil => a0
| cons b t => fold_left t (f a0 b)
end.
Lemma fold_left_app : forall (l l':list B)(i:A),
fold_left (l++l') i = fold_left l' (fold_left l i).
End Fold_Left_Recursor.
Lemma fold_left_S_O :
forall (A:Type)(l:list A), fold_left (fun x _ => S x) l 0 = length l.
Right-to-left iterator on lists
Section Fold_Right_Recursor.
Variables (A : Type) (B : Type).
Variable f : B -> A -> A.
Variable a0 : A.
Fixpoint fold_right (l:list B) : A :=
match l with
| nil => a0
| cons b t => f b (fold_right t)
end.
End Fold_Right_Recursor.
Lemma fold_right_app : forall (A B:Type)(f:A->B->B) l l' i,
fold_right f i (l++l') = fold_right f (fold_right f i l') l.
Lemma fold_left_rev_right : forall (A B:Type)(f:A->B->B) l i,
fold_right f i (rev l) = fold_left (fun x y => f y x) l i.
Theorem fold_symmetric :
forall (A : Type) (f : A -> A -> A),
(forall x y z : A, f x (f y z) = f (f x y) z) ->
forall (a0 : A), (forall y : A, f a0 y = f y a0) ->
forall (l : list A), fold_left f l a0 = fold_right f a0 l.
(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.
Fixpoint list_power (A B:Type)(l:list A) (l':list B) :
list (list (A * B)) :=
match l with
| nil => cons nil nil
| cons x t =>
flat_map (fun f:list (A * B) => map (fun y:B => cons (x, y) f) l')
(list_power t l')
end.
find whether a boolean function can be satisfied by an
elements of the list.
Fixpoint existsb (l:list A) : bool :=
match l with
| nil => false
| a::l => f a || existsb l
end.
Lemma existsb_exists :
forall l, existsb l = true <-> exists x, In x l /\ f x = true.
Lemma existsb_nth : forall l n d, n < length l ->
existsb l = false -> f (nth n l d) = false.
Lemma existsb_app : forall l1 l2,
existsb (l1++l2) = existsb l1 || existsb l2.
find whether a boolean function is satisfied by
all the elements of a list.
Fixpoint forallb (l:list A) : bool :=
match l with
| nil => true
| a::l => f a && forallb l
end.
Lemma forallb_forall :
forall l, forallb l = true <-> (forall x, In x l -> f x = true).
Lemma forallb_app :
forall l1 l2, forallb (l1++l2) = forallb l1 && forallb l2.
filter
Fixpoint filter (l:list A) : list A :=
match l with
| nil => nil
| x :: l => if f x then x::(filter l) else filter l
end.
Lemma filter_In : forall x l, In x (filter l) <-> In x l /\ f x = true.
Lemma filter_app (l l':list A) :
filter (l ++ l') = filter l ++ filter l'.
Lemma concat_filter_map : forall (l : list (list A)),
concat (map filter l) = filter (concat l).
Lemma forallb_filter l: forallb (filter l) = true.
Lemma forallb_filter_id l: forallb l = true -> filter l = l.
find
Fixpoint find (l:list A) : option A :=
match l with
| nil => None
| x :: tl => if f x then Some x else find tl
end.
Lemma find_some l x : find l = Some x -> In x l /\ f x = true.
Lemma find_none l : find l = None -> forall x, In x l -> f x = false.
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_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_map : forall (f g : A -> bool) (l : list A),
filter f l = filter g l <-> map f l = map g l.
Lemma filter_ext : forall (f g : A -> bool),
(forall a, f a = g a) -> forall l, filter f l = filter g l.
Lemma partition_as_filter f (l : list A) : partition f l = (filter f l, filter (fun x => negb (f x)) l).
Corollary filter_length f (l : list A) : length (filter f l) + length (filter (fun x => negb (f x)) l) = length l.
Corollary filter_length_le f (l : list A): length (filter f l) <= length l.
Lemma filter_length_forallb f (l : list A): length (filter f l) = length l -> forallb f l = true.
Remove by filtering
Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
Definition remove' (x : A) : list A -> list A :=
filter (fun y => if eq_dec x y then false else true).
Lemma remove_alt (x : A) (l : list A) : remove' x l = remove eq_dec x l.
Counting occurrences by filtering
Definition count_occ' (l : list A) (x : A) : nat :=
length (filter (fun y => if eq_dec y x then true else false) l).
Lemma count_occ_alt (l : list A) (x : A) :
count_occ' l x = count_occ eq_dec l x.
End Filtering.
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 length_fst_split : forall (l:list (A*B)),
length (fst (split l)) = length l.
Lemma length_snd_split : 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)),
forall l1 l2, split l = (l1, l2) -> 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 length_combine : 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.
Fixpoint list_prod (l:list A) (l':list B) :
list (A * B) :=
match l with
| nil => nil
| cons x t => (map (fun y:B => (x, y)) l')++(list_prod t l')
end.
Lemma in_prod_aux :
forall (x:A) (y:B) (l:list B),
In y l -> In (x, y) (map (fun y0:B => (x, y0)) l).
Lemma in_prod :
forall (l:list A) (l':list B) (x:A) (y:B),
In x l -> In y l' -> In (x, y) (list_prod l l').
Lemma in_prod_iff :
forall (l:list A)(l':list B)(x:A)(y:B),
In (x,y) (list_prod l l') <-> In x l /\ In y l'.
Lemma length_prod : forall (l:list A)(l':list B),
length (list_prod l l') = (length l) * (length l').
End ListPairs.
Section length_order.
Variable A : Type.
Definition lel (l m:list A) := length l <= length m.
Variables a b : A.
Variables l m n : list A.
Lemma lel_refl : lel l l.
Lemma lel_trans : lel l m -> lel m n -> lel l n.
Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m).
Lemma lel_cons : lel l m -> lel l (b :: m).
Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m.
Lemma lel_nil : forall l':list A, lel l' nil -> nil = l'.
End length_order.
#[global]
Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons:
datatypes.
Section SetIncl.
Variable A : Type.
Definition incl (l m:list A) := forall a:A, In a l -> In a m.
#[local]
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.
#[local]
Hint Resolve incl_refl : core.
Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m).
#[local]
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).
#[local]
Hint Immediate incl_appl : core.
Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n).
#[local]
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.
#[local]
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.
#[local]
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).
#[global]
Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons
incl_app incl_map: datatypes.
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 nth_error_firstn n l i
: nth_error (firstn n l) i = if Nat.ltb i n then nth_error l i else None.
Lemma nth_firstn (n : nat) (l : list A) (i : nat) (d : A) :
nth i (firstn n l) d = if i <? n then nth i l d else d.
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 nth_error_skipn n l i : nth_error (skipn n l) i = nth_error l (n + i).
Lemma nth_skipn n l i d : nth i (skipn n l) d = nth (n + i) l d.
Lemma hd_error_skipn n l : hd_error (skipn n l) = nth_error l n.
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.
Lemma skipn_all2 n: forall l, length l <= n -> skipn n l = [].
Lemma skipn_all_iff n l : length l <= n <-> skipn n l = nil.
Lemma skipn_skipn : forall x y l, skipn x (skipn y l) = skipn (x + y) l.
Lemma firstn_skipn : forall n l, firstn n l ++ skipn n l = l.
Lemma firstn_skipn_middle n l x :
nth_error l n = Some x ->
firstn n l ++ x :: skipn (S n) l = l.
Lemma length_firstn : forall n l, length (firstn n l) = min n (length l).
Lemma length_skipn 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.
Section CuttingMap.
Variables A B : Type.
Variable f : A -> B.
Lemma firstn_map : forall n l,
firstn n (map f l) = map f (firstn n l).
Lemma skipn_map : forall n l,
skipn n (map f l) = map f (skipn n l).
End CuttingMap.
Section Combining.
Variables (A B : Type).
Lemma combine_nil : forall (l : list A),
combine l (@nil B) = @nil (A*B).
Lemma combine_firstn_l : forall (l : list A) (l' : list B),
combine l l' = combine l (firstn (length l) l').
Lemma combine_firstn_r : forall (l : list A) (l' : list B),
combine l l' = combine (firstn (length l') l) l'.
Lemma combine_firstn : forall (l : list A) (l' : list B) (n : nat),
firstn n (combine l l') = combine (firstn n l) (firstn n l').
End Combining.
Section Add.
Variable A : Type.
Inductive Add (a:A) : list A -> list A -> Prop :=
| Add_head l : Add a l (a::l)
| Add_cons x l l' : Add a l l' -> Add a (x::l) (x::l').
Lemma Add_app a l1 l2 : Add a (l1++l2) (l1++a::l2).
Lemma Add_split a l l' :
Add a l l' -> exists l1 l2, l = l1++l2 /\ l' = l1++a::l2.
Lemma Add_in a l l' : Add a l l' ->
forall x, In x l' <-> In x (a::l).
Lemma Add_length a l l' : Add a l l' -> length l' = S (length l).
Lemma Add_inv a l : In a l -> exists l', Add a l' l.
Lemma incl_Add_inv a l u v :
~In a l -> incl (a::l) v -> Add a u v -> incl l u.
End Add.
Section ReDun.
Variable A : Type.
Inductive NoDup : list A -> Prop :=
| NoDup_nil : NoDup nil
| NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l).
Lemma NoDup_Add a l l' : Add a l l' -> (NoDup l' <-> NoDup l /\ ~In a l).
Lemma NoDup_remove l l' a :
NoDup (l++a::l') -> NoDup (l++l') /\ ~In a (l++l').
Lemma NoDup_remove_1 l l' a : NoDup (l++a::l') -> NoDup (l++l').
Lemma NoDup_remove_2 l l' a : NoDup (l++a::l') -> ~In a (l++l').
Theorem NoDup_cons_iff a l:
NoDup (a::l) <-> ~ In a l /\ NoDup l.
Lemma NoDup_app (l1 l2 : list A):
NoDup l1 -> NoDup l2 -> (forall a, In a l1 -> ~ In a l2) ->
NoDup (l1 ++ l2).
Lemma NoDup_app_remove_l l l' : NoDup (l++l') -> NoDup l'.
Lemma NoDup_app_remove_r l l' : NoDup (l++l') -> NoDup l.
Lemma NoDup_rev l : NoDup l -> NoDup (rev l).
Lemma NoDup_filter f l : NoDup l -> NoDup (filter f l).
Effective computation of a list without duplicates
Hypothesis decA: forall x y : A, {x = y} + {x <> y}.
Fixpoint nodup (l : list A) : list A :=
match l with
| [] => []
| x::xs => if in_dec decA x xs then nodup xs else x::(nodup xs)
end.
Lemma nodup_fixed_point (l : list A) :
NoDup l -> nodup l = l.
Lemma nodup_In l x : In x (nodup l) <-> In x l.
Lemma nodup_incl l1 l2 : incl l1 (nodup l2) <-> incl l1 l2.
Lemma NoDup_nodup l: NoDup (nodup l).
Lemma nodup_inv k l a : nodup k = a :: l -> ~ In a l.
Theorem NoDup_count_occ l:
NoDup l <-> (forall x:A, count_occ decA l x <= 1).
Theorem NoDup_count_occ' l:
NoDup l <-> (forall x:A, In x l -> count_occ decA l x = 1).
Alternative characterisations of being without duplicates,
thanks to nth_error and nth
Lemma NoDup_nth_error l :
NoDup l <->
(forall i j, i<length l -> nth_error l i = nth_error l j -> i = j).
Lemma NoDup_nth l d :
NoDup l <->
(forall i j, i<length l -> j<length l ->
nth i l d = nth j l d -> i = j).
Having NoDup hypotheses bring more precise facts about incl.
Lemma NoDup_incl_length l l' :
NoDup l -> incl l l' -> length l <= length l'.
Lemma NoDup_length_incl l l' :
NoDup l -> length l' <= length l -> incl l l' -> incl l' l.
Lemma NoDup_incl_NoDup (l l' : list A) : NoDup l ->
length l' <= length l -> incl l l' -> NoDup l'.
End ReDun.
NoDup and map
NB: the reciprocal result holds only for injective functions,
see FinFun.v
seq computes the sequence of len contiguous integers
that starts at start. For instance, seq 2 3 is 2::3::4::nil.
Fixpoint seq (start len:nat) : list nat :=
match len with
| 0 => nil
| S len => start :: seq (S start) len
end.
Lemma cons_seq : forall len start, start :: seq (S start) len = seq start (S len).
Lemma length_seq : forall len start, length (seq start len) = len.
Lemma seq_nth : forall len start n d,
n < len -> nth n (seq start len) d = start+n.
Lemma seq_shift : forall len start,
map S (seq start len) = seq (S start) len.
Lemma in_seq len start n :
In n (seq start len) <-> start <= n < start+len.
Lemma seq_NoDup len start : NoDup (seq start len).
Lemma seq_app : forall len1 len2 start,
seq start (len1 + len2) = seq start len1 ++ seq (start + len1) len2.
Lemma seq_S : forall len start, seq start (S len) = seq start len ++ [start + len].
Lemma nth_error_seq start len n :
nth_error (seq start len) n =
if Nat.ltb n len then Some (start + n) else None.
End NatSeq.
Section Compare.
Variable A : Type.
Variable cmp : A -> A -> comparison.
Fixpoint list_compare (xs ys : list A) : comparison :=
match xs, ys with
| nil , nil => Eq
| nil , _ => Lt
| _ , nil => Gt
| x :: xs, y :: ys =>
match cmp x y with
| Eq => list_compare xs ys
| c => c
end
end%list.
Section Lemmas.
Variable Hcmp : forall x y, cmp x y = Eq <-> x = y.
Lemma list_compare_cons (x : A) (xs ys : list A) :
list_compare (x :: xs) (x :: ys) = list_compare xs ys.
Lemma list_compare_app (xs ys zs : list A) :
list_compare (xs ++ ys) (xs ++ zs) = list_compare ys zs.
Lemma prefix_eq {prefix1 prefix2 xs1 xs2 ys1 ys2 : list A} {x1 x2 y1 y2 : A} :
prefix1 ++ x1 :: xs1 = prefix2 ++ x2 :: xs2 ->
prefix1 ++ y1 :: ys1 = prefix2 ++ y2 :: ys2 ->
x1 <> y1 ->
x2 <> y2 ->
prefix1 = prefix2.
#[local] Ltac list_auto :=
repeat lazymatch goal with
| |- ?x = ?x =>
reflexivity
| H : ?xs = ?xs ++ _ |- _ =>
rewrite <-(app_nil_r xs) in H at 1
| H : ?xs ++ _ = ?xs |- _ =>
symmetry in H
| H : ?xs ++ _ = ?xs ++ _ |- _ =>
apply app_inv_head in H
| H : _ :: _ = _ :: _ |- _ =>
injection H; intros; clear H; subst
| H : [] = _ :: _ |- _ =>
inversion H
| H : cmp ?x ?x = Lt |- _ =>
rewrite (proj2 (Hcmp _ _) eq_refl) in H; discriminate
| H : cmp ?x ?x = Gt |- _ =>
rewrite (proj2 (Hcmp _ _) eq_refl) in H; discriminate
| H1 : ?p1 ++ _ :: _ = ?p2 ++ _ :: _,
H2 : ?p2 ++ _ :: _ = ?p1 ++ _ :: _ |- _ =>
symmetry in H2
| H1 : ?p1 ++ ?x1 :: ?xs1 = ?p2 ++ ?x2 :: ?xs2,
H2 : ?p1 ++ ?y1 :: ?ys1 = ?p2 ++ ?y2 :: ?ys2 |- _ =>
assert (p1 = p2) as Hp;
[ eapply (prefix_eq H1 H2); intros Heq; subst
| subst; apply app_inv_head in H1, H2 ]
| H : cmp ?x ?x = _ |- _ =>
rewrite (proj2 (Hcmp _ _) eq_refl) in H; try discriminate H
| H1 : cmp ?x1 ?x2 = _,
H2 : cmp ?x1 ?x2 = _ |- _ =>
rewrite H1 in H2; discriminate H2
| Htrans : forall (x y z : A) (c : comparison), cmp x y = c -> cmp y z = c -> cmp x z = c,
H1 : cmp ?x1 ?x2 = ?c,
H2 : cmp ?x2 ?x3 = ?c |- _ =>
pose proof (Htrans x1 x2 x3 c H1 H2); clear H1 H2
| Hcmp_opp : (forall x y, cmp y x = CompOpp (cmp x y)),
H1 : cmp ?x1 ?x2 = ?c, H2 : cmp ?x2 ?x1 = ?c |- _ =>
rewrite Hcmp_opp, H2 in H1; simpl in H1; discriminate H1
end.
Inductive ListCompareSpec (xs ys : list A) : forall (c : comparison), Prop :=
| ListCompareEq :
xs = ys ->
ListCompareSpec xs ys Eq
| ListCompareShorter y ys' :
ys = xs ++ y :: ys' ->
ListCompareSpec xs ys Lt
| ListCompareLonger x xs' :
xs = ys ++ x :: xs' ->
ListCompareSpec xs ys Gt
| ListCompareLt prefix x xs' y ys' :
xs = prefix ++ x :: xs' ->
ys = prefix ++ y :: ys' ->
cmp x y = Lt ->
ListCompareSpec xs ys Lt
| ListCompareGt prefix x xs' y ys' :
xs = prefix ++ x :: xs' ->
ys = prefix ++ y :: ys' ->
cmp x y = Gt ->
ListCompareSpec xs ys Gt.
Lemma list_compareP (xs ys : list A) :
ListCompareSpec xs ys (list_compare xs ys).
Lemma list_compare_refl (xs ys : list A) :
list_compare xs ys = Eq <-> xs = ys.
Lemma list_compare_antisym (xs ys : list A) :
(forall x y, cmp y x = CompOpp (cmp x y)) ->
list_compare ys xs = CompOpp (list_compare xs ys).
Lemma list_compare_trans (xs ys zs : list A) (c : comparison) :
(forall x y z c, cmp x y = c -> cmp y z = c -> cmp x z = c) ->
(forall x y, cmp y x = CompOpp (cmp x y)) ->
list_compare xs ys = c -> list_compare ys zs = c -> list_compare xs zs = c.
Lemma list_compare_spec_complete (xs ys : list A) (c : comparison) :
ListCompareSpec xs ys c -> list_compare xs ys = c.
End Lemmas.
End Compare.
Section Exists_Forall.
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).
#[local]
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).
#[local]
Hint Constructors Forall : core.
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_nil_iff : Forall [] <-> True.
Lemma Forall_cons_iff : forall (a:A) l, Forall (a :: l) <-> P a /\ Forall l.
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_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.
#[global]
Hint Constructors Exists : core.
#[global]
Hint Constructors Forall : core.
Lemma Exists_map A B (f : A -> B) P l :
Exists P (map f l) <-> Exists (fun x => P (f x)) l.
Lemma Exists_concat A P (ls : list (list A)) :
Exists P (concat ls) <-> Exists (Exists P) ls.
Lemma Exists_flat_map A B P ls (f : A -> list B) :
Exists P (flat_map f ls) <-> Exists (fun d => Exists P (f d)) ls.
Lemma Forall_map A B (f : A -> B) P l :
Forall P (map f l) <-> Forall (fun x => P (f x)) l.
Lemma Forall_concat A P (ls : list (list A)) :
Forall P (concat ls) <-> Forall (Forall P) ls.
Lemma Forall_flat_map A B P ls (f : A -> list B) :
Forall P (flat_map f ls) <-> Forall (fun d => Forall P (f d)) ls.
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.
Variables A B : Type.
Variable R : A -> B -> Prop.
Inductive Forall2 : list A -> list B -> Prop :=
| Forall2_nil : Forall2 [] []
| Forall2_cons : forall x y l l',
R x y -> Forall2 l l' -> Forall2 (x::l) (y::l').
#[local]
Hint Constructors Forall2 : core.
#[deprecated(since = "8.18", note = "Use Forall2_nil instead.")]
Theorem Forall2_refl : Forall2 [] [].
Theorem Forall2_cons_iff : forall x y l l',
Forall2 (x :: l) (y :: l') <-> R x y /\ Forall2 l l'.
Theorem Forall2_length : forall l l',
Forall2 l l' -> length l = length l'.
Theorem Forall2_app_inv_l : forall l1 l2 l',
Forall2 (l1 ++ l2) l' ->
exists l1' l2', Forall2 l1 l1' /\ Forall2 l2 l2' /\ l' = l1' ++ l2'.
Theorem Forall2_app_inv_r : forall l1' l2' l,
Forall2 l (l1' ++ l2') ->
exists l1 l2, Forall2 l1 l1' /\ Forall2 l2 l2' /\ l = l1 ++ l2.
Theorem Forall2_app : forall l1 l2 l1' l2',
Forall2 l1 l1' -> Forall2 l2 l2' -> Forall2 (l1 ++ l2) (l1' ++ l2').
Theorem Forall_Exists_exists_Forall2 l1 l2 :
Forall (fun a => Exists (R a) l2) l1 ->
exists l2', Forall2 l1 l2' /\ incl l2' l2.
End Forall2.
Lemma Forall2_impl (A B : Type) (R1 R2 : A -> B -> Prop) : (forall a b, R1 a b -> R2 a b) ->
forall l1 l2, Forall2 R1 l1 l2 -> Forall2 R2 l1 l2.
Lemma Forall2_flip (A B : Type) (R : A -> B -> Prop) l1 l2 :
Forall2 R l1 l2 -> Forall2 (fun b a => R a b) l2 l1.
#[global]
Hint Constructors Forall2 : core.
Section ForallPairs.
ForallPairs : specifies that a certain relation should
always hold when inspecting all possible pairs of elements of a list.
Variable A : Type.
Variable R : A -> A -> Prop.
Definition ForallPairs l :=
forall a b, In a l -> In b l -> R a b.
ForallOrdPairs : we still check a relation over all pairs
of elements of a list, but now the order of elements matters.
Inductive ForallOrdPairs : list A -> Prop :=
| FOP_nil : ForallOrdPairs nil
| FOP_cons : forall a l,
Forall (R a) l -> ForallOrdPairs l -> ForallOrdPairs (a::l).
#[local]
Hint Constructors ForallOrdPairs : core.
Lemma ForallOrdPairs_In : forall l,
ForallOrdPairs l ->
forall x y, In x l -> In y l -> x=y \/ R x y \/ R y x.
ForallPairs implies ForallOrdPairs. The reverse implication is true
only when R is symmetric and reflexive.
Lemma ForallPairs_ForallOrdPairs l: ForallPairs l -> ForallOrdPairs l.
Lemma ForallOrdPairs_ForallPairs :
(forall x, R x x) ->
(forall x y, R x y -> R y x) ->
forall l, ForallOrdPairs l -> ForallPairs l.
End ForallPairs.
Lemma NoDup_iff_ForallOrdPairs [A] (l: list A):
NoDup l <-> ForallOrdPairs (fun a b => a <> b) l.
Lemma NoDup_map_NoDup_ForallPairs [A B] (f: A->B) (l: list A) :
ForallPairs (fun x y => f x = f y -> x = y) l -> NoDup l -> NoDup (map f l).
Lemma NoDup_concat [A] (L: list (list A)):
Forall (@NoDup A) L ->
ForallOrdPairs (fun l1 l2 => forall a, In a l1 -> ~ In a l2) L ->
NoDup (concat L).
Section Repeat.
Variable A : Type.
Fixpoint repeat (x : A) (n: nat ) :=
match n with
| O => []
| S k => x::(repeat x k)
end.
Theorem repeat_length x n:
length (repeat x n) = n.
Theorem repeat_spec n x y:
In y (repeat x n) -> y=x.
Lemma repeat_cons n a :
a :: repeat a n = repeat a n ++ (a :: nil).
Lemma repeat_app x n m :
repeat x (n + m) = repeat x n ++ repeat x m.
Lemma repeat_eq_app x n l1 l2 :
repeat x n = l1 ++ l2 -> repeat x (length l1) = l1 /\ repeat x (length l2) = l2.
Lemma repeat_eq_cons x y n l :
repeat x n = y :: l -> x = y /\ repeat x (pred n) = l.
Lemma repeat_eq_elt x y n l1 l2 :
repeat x n = l1 ++ y :: l2 -> x = y /\ repeat x (length l1) = l1 /\ repeat x (length l2) = l2.
Lemma Forall_eq_repeat x l :
Forall (eq x) l -> l = repeat x (length l).
Hypothesis decA : forall x y : A, {x = y}+{x <> y}.
Lemma count_occ_repeat_eq x y n : x = y -> count_occ decA (repeat y n) x = n.
Lemma count_occ_repeat_neq x y n : x <> y -> count_occ decA (repeat y n) x = 0.
Lemma count_occ_unique x l : count_occ decA l x = length l -> l = repeat x (length l).
Lemma count_occ_repeat_excl x l :
(forall y, y <> x -> count_occ decA l y = 0) -> l = repeat x (length l).
Lemma count_occ_sgt l x : l = x :: nil <->
count_occ decA l x = 1 /\ forall y, y <> x -> count_occ decA l y = 0.
Lemma nth_repeat a m n :
nth n (repeat a m) a = a.
Lemma nth_repeat_lt a m n d :
n < m ->
nth n (repeat a m) d = a.
Lemma nth_error_repeat a m n :
n < m -> nth_error (repeat a m) n = Some a.
End Repeat.
Lemma repeat_to_concat A n (a:A) :
repeat a n = concat (repeat [a] n).
Lemma map_repeat A B (a:A) n (f : A -> B):
map f (repeat a n) = repeat (f a) n.
Lemma rev_repeat A n (a:A):
rev (repeat a n) = repeat a n.
Sum of elements of a list of nat: list_sum
Definition list_sum l := fold_right plus 0 l.
Lemma list_sum_app : forall l1 l2,
list_sum (l1 ++ l2) = list_sum l1 + list_sum l2.
Lemma length_concat A l:
length (concat l) = list_sum (map (@length A) l).
Lemma length_flat_map A B (f: A -> list B) l:
length (flat_map f l) = list_sum (map (fun x => length (f x)) l).
Corollary flat_map_constant_length A B c (f: A -> list B) l:
(forall x, In x l -> length (f x) = c) -> length (flat_map f l) = (length l) * c.
Lemma length_list_power (A B:Type)(l:list A) (l':list B):
length (list_power l l') = (length l')^(length l).
Max of elements of a list of nat: list_max
Definition list_max l := fold_right max 0 l.
Lemma list_max_app : forall l1 l2,
list_max (l1 ++ l2) = max (list_max l1) (list_max l2).
Lemma list_max_le : forall l n,
list_max l <= n <-> Forall (fun k => k <= n) l.
Lemma list_max_lt : forall l n, l <> nil ->
list_max l < n <-> Forall (fun k => k < n) l.
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.
Global Hint Rewrite
rev_involutive
rev_unit
map_nth
length_map
length_seq
length_app
length_rev
app_nil_r
: list.
Ltac simpl_list := autorewrite with list.
Ltac ssimpl_list := autorewrite with list using simpl.