Library CoLoR.Util.List.ListUtil
CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
- Stephane Le Roux, 2006-10-17
- Adam Koprowski, 2006-04-28
- Solange Coupet-Grimal and William Delobel, 2006-01-09
- Frederic Blanqui, 2005-02-03, 2009-07-06
- Sebastien Hinderer, 2004-05-25
Set Implicit Arguments.
Require Import LogicUtil EqUtil Setoid SetoidList RelMidex RelUtil BoolUtil
NatUtil.
Require Export List.
Require Program.
Ltac elt_type l := match type of l with list ?A => A end.
Infix "[=" := incl (at level 70).
Properties of In (membership predicate on lists).
Section In.
Variable A : Type.
Lemma in_app : forall l m (x : A), In x (l ++ m) <-> In x l \/ In x m.
Lemma notin_app : forall l m (x : A), ~In x (l ++ m) <-> ~In x l /\ ~In x m.
Lemma in_appl : forall (x : A) l1 l2, In x l1 -> In x (l1 ++ l2).
Lemma in_appr : forall (x : A) l1 l2, In x l2 -> In x (l1 ++ l2).
Lemma in_app_com : forall (x : A) l1 l2 l3,
In x ((l1 ++ l3) ++ l2) -> In x ((l1 ++ l2) ++ l3).
Lemma in_elim : forall (x : A) l,
In x l -> exists l1, exists l2, l = l1 ++ x :: l2.
Variable eqA_dec : forall x y : A, {x=y}+{~x=y}.
Lemma in_elim_dec : forall (x : A) l,
In x l -> exists m, exists p, l = m ++ x :: p /\ ~In x m.
Lemma In_midex : eq_midex A -> forall (x : A) l, In x l \/ ~In x l.
Lemma In_elim_right : eq_midex A -> forall (x : A) l,
In x l -> exists l', exists l'', l = l'++x::l'' /\ ~In x l''.
Lemma In_cons : forall (x a : A) l, In x (a::l) <-> a=x \/ In x l.
Lemma In_InA_eq : forall (x : A) l, In x l <-> InA eq x l.
End In.
Implicit Arguments in_elim [A x l].
Implicit Arguments in_elim_dec [A x l].
Ltac intac := repeat (apply in_eq || apply in_cons).
Ltac list_ok := let x := fresh in intro x;
match goal with
| |- In _ ?l => vm_compute; destruct x; tauto
end.
Properties of incl
(non-order-preserving inclusion predicate on lists).
Instance incl_PreOrder A : PreOrder (@incl A).
Instance app_incl A : Proper (incl ==> incl ==> incl) (@app A).
Section incl.
Variable A : Type.
Lemma incl_nil_elim : forall l : list A, l [= nil <-> l = nil.
Lemma incl_nil : forall l : list A, nil [= l.
Lemma incl_cons_l : forall (a : A) l m, a :: l [= m -> In a m /\ l [= m.
Lemma incl_cons_l_in : forall (x : A) l m, x :: l [= m -> In x m.
Lemma incl_cons_l_incl : forall (x : A) l m, x :: l [= m -> l [= m.
Lemma incl_app_elim : forall l1 l2 l3 : list A,
l1 ++ l2 [= l3 -> l1 [= l3 /\ l2 [= l3.
Lemma incl_appr_incl : forall l1 l2 l3 : list A, l1 ++ l2 [= l3 -> l1 [= l3.
Lemma incl_appl_incl : forall l1 l2 l3 : list A, l1 ++ l2 [= l3 -> l2 [= l3.
Lemma appl_incl : forall l l2 l2' : list A, l2 [= l2' -> l ++ l2 [= l ++ l2'.
Lemma appr_incl : forall l l1 l1' : list A, l1 [= l1' -> l1 ++ l [= l1' ++ l.
Lemma app_com_incl : forall l1 l2 l3 l4 : list A,
(l1 ++ l3) ++ l2 [= l4 -> (l1 ++ l2) ++ l3 [= l4.
Lemma incl_cons_r : forall x : A, forall m l, l [= x :: m -> In x l \/ l [= m.
Variable eqA_dec : forall x y : A, {x=y}+{~x=y}.
Lemma not_incl : forall l m, ~ l [= m <-> exists x:A, In x l /\ ~In x m.
End incl.
Implicit Arguments incl_app_elim [A l1 l2 l3].
Strict inclusion.
Definition strict_incl A (l m : list A) := l [= m /\ ~m [= l.
Infix "[" := strict_incl (at level 70).
Lemma strict_incl_tran : forall A (l m n : list A), l [ m -> m [ n -> l [ n.
Instance strict_incl_rel A : Transitive (@strict_incl A).
Equivalence (i.e. having the same elements).
Definition lequiv {A} (l1 l2 : list A) := l1 [= l2 /\ l2 [= l1.
Infix "[=]" := lequiv (at level 70).
Instance lequiv_rel A : Equivalence (@lequiv A).
Instance app_lequiv A : Proper (lequiv ==> lequiv ==> lequiv) (@app A).
Instance incl_lequiv1 A1 B (f : list A1 -> relation B) :
Proper (incl ==> inclusion) f -> Proper (lequiv ==> same_rel) f.
Instance incl_lequiv2 A1 A2 B (f : list A1 -> list A2 -> relation B) :
Proper (incl ==> incl ==> inclusion) f ->
Proper (lequiv ==> lequiv ==> same_rel) f.
Properties of the empty list.
Section nil.
Variable A : Type.
Lemma list_empty_dec : forall l : list A, {l = nil} + {l <> nil}.
Definition is_empty (l : list A) : bool :=
match l with
| nil => true
| _ => false
end.
End nil.
Properties of cons.
Instance cons_incl A : Proper (eq ==> incl ==> incl) (@cons A).
Instance cons_lequiv A : Proper (eq ==> lequiv ==> lequiv) (@cons A).
Section cons.
Variable A : Type.
Lemma cons_eq : forall x x' : A, forall l l',
x = x' -> l = l' -> x :: l = x' :: l'.
Lemma head_eq : forall x x' : A, forall l, x = x' -> x :: l = x' :: l.
Lemma tail_eq : forall x : A, forall l l', l = l' -> x :: l = x :: l'.
End cons.
Properties of app (concatenation).
Section app.
Variable A : Type.
Lemma length_app : forall l m : list A, length (l ++ m) = length l + length m.
Lemma app_nil : forall l1 l2 : list A, l1 = nil -> l2 = nil -> l1 ++ l2 = nil.
Lemma app_eq : forall l1 l2 l1' l2' : list A,
l1 = l1' -> l2 = l2' -> l1 ++ l2 = l1' ++ l2'.
Lemma appl_eq : forall l1 l2 l1' : list A, l1 = l1' -> l1 ++ l2 = l1' ++ l2.
Lemma appr_eq : forall l1 l2 l2' : list A, l2 = l2' -> l1 ++ l2 = l1 ++ l2'.
Lemma list_app_first_last : forall l m (a : A),
(l ++ a::nil) ++ m = l ++ a::m.
Lemma list_app_last : forall l m n (a : A),
l ++ m = n ++ a::nil -> m <> nil -> In a m.
Lemma list_drop_last : forall l m n (a : A),
l ++ m = n ++ a::nil -> m <> nil -> exists2 w, w [= m & l ++ w = n.
Lemma last_intro : forall l : list A, length l > 0 ->
exists m, exists a, l = m ++ a :: nil /\ length m = length l - 1.
End app.
Properties of length.
Section length.
Variable A : Type.
Lemma length_0 : forall l : list A, length l = 0 -> l = nil.
End length.
Implicit Arguments length_0 [A l].
Properties of head and tail.
Section head_tail.
Variable A : Type.
Lemma head_app : forall (l l': list A) (lne: l <> nil),
head (l ++ l') = head l.
Lemma length_tail : forall l : list A, length (tail l) <= length l.
Lemma tail_in : forall (x: A) l, In x (tail l) -> In x l.
Lemma tail_cons_tail : forall (l1 l2: list A),
l1 <> nil -> tail l1 ++ l2 = tail (l1 ++ l2).
Lemma length_tail_minus : forall (l : list A), length (tail l) = length l - 1.
Lemma list_decompose_head : forall (l : list A) el (lne: l <> nil),
head l = Some el -> l = el :: tail l.
Lemma in_head_tail : forall a (l : list A),
In a l -> Some a = head l \/ In a (tail l).
Lemma head_notNil : forall (l : list A) (lne : l <> nil),
{a : A | head l = Some a}.
Lemma head_of_notNil : forall (l : list A) a (lne: l <> nil),
head l = Some a -> proj1_sig (head_notNil lne) = a.
End head_tail.
Hint Resolve tail_in tail_cons_tail head_app : datatypes.
Hint Rewrite head_app length_app : datatypes.
Iteration of tail.
Section tail_nth.
Variable A : Type.
Fixpoint tail_nth (l : list A) (n : nat) : option (list A) :=
match l, n with
| _, 0 => Some l
| a :: l', S n' => tail_nth l' n'
| _, _ => None
end.
End tail_nth.
Function selecting the elements that satisfy some predicate.
Section select.
Context {A: Type} {f : A->Prop}.
Variable (f_dec : forall x, {f x}+{~f x}).
Fixpoint select (l : list A) :=
match l with
| nil => nil
| cons a l' =>
match f_dec a with
| left _ => a :: select l'
| right _ => select l'
end
end.
Lemma incl_select : forall l, select l [= l.
Lemma select_correct : forall l x, In x (select l) -> In x l /\ f x.
Lemma select_complete : forall l x, In x l -> f x -> In x (select l).
End select.
Select the elements of a list wrt a boolean function.
Section filter.
Variables (A : Type) (f : A -> bool).
Lemma filter_app : forall l m, filter f (l ++ m) = filter f l ++ filter f m.
Lemma filter_incl : forall l, filter f l [= l.
Variable eq_dec : forall x y : A, {x=y}+{~x=y}.
Lemma notIn_filter : forall x l,
~In x (filter f l) <-> ~In x l \/ (In x l /\ f x = false).
End filter.
Section filter_opt.
Variables (A B : Type) (f : A -> option B).
Fixpoint filter_opt (l : list A) : list B :=
match l with
| nil => nil
| cons a m =>
match f a with
| Some b => cons b (filter_opt m)
| _ => filter_opt m
end
end.
End filter_opt.
Boolean function testing membership.
Section Inb.
Variables (A : Type) (eq_dec : forall x y : A, {x=y}+{~x=y}).
Fixpoint Inb (x : A) (l : list A) : bool :=
match l with
| nil => false
| cons y l' =>
match eq_dec x y with
| left _ => true
| _ => Inb x l'
end
end.
Lemma Inb_true : forall x l, Inb x l = true -> In x l.
Lemma Inb_false : forall x l, Inb x l = false -> In x l -> False.
Lemma Inb_intro : forall x l, In x l -> Inb x l = true.
Lemma Inb_elim : forall x l, ~In x l -> Inb x l = false.
Lemma Inb_correct : forall x l, In x l <-> Inb x l = true.
Lemma Inb_incl : forall x l l', l [= l' -> Inb x l = true -> Inb x l' = true.
Lemma Inb_equiv : forall x l l', lequiv l l' -> Inb x l = Inb x l'.
Definition Inclb (l1 l2 : list A) := forallb (fun x => Inb x l2) l1.
Lemma Inclb_ok : forall l1 l2, Inclb l1 l2 = true <-> l1 [= l2.
End Inb.
Ltac inbtac :=
match goal with
| _ : In ?x ?l |- _ =>
let H0 := fresh "H" in
(assert (H0 : Inb x l = true); apply Inb_intro; hyp; rewrite H0)
end.
Remove an element from a list.
Section remove.
Variables (A : Type) (eq_dec : forall x y : A, {x=y}+{~x=y}).
Fixpoint remove (y : A) (l : list A) : list A :=
match l with
| nil => nil
| cons x l' =>
match eq_dec x y with
| left _ => remove y l'
| right _ => cons x (remove y l')
end
end.
Lemma length_remove : forall (x : A) l, length (remove x l) <= length l.
Lemma In_length_remove : forall (x : A) l,
In x l -> length (remove x l) < length l.
Lemma In_remove : forall (x y : A) l, x <> y -> In y l -> In y (remove x l).
Lemma incl_remove : forall (x : A) l m, ~In x l -> l [= m -> l [= remove x m.
Lemma incl_remove2 (x : A) : forall l, remove x l [= l.
Lemma notin_remove : forall x l, In x (remove x l) -> False.
Lemma remove_In : forall a x l, In a (remove x l) -> In a l.
Lemma remove_eq : forall a x l, In a (remove x l) <-> a <> x /\ In a l.
Lemma remove_notin (x : A) : forall l, ~In x l -> remove x l = l.
End remove.
Removes a list of elements from a list.
Section removes.
Variable (A : Type) (eqdec : forall x y : A, {x=y}+{x<>y}).
Notation In_dec := (In_dec eqdec).
Fixpoint removes (l m : list A) : list A :=
match m with
| nil => nil
| x :: m' =>
match In_dec x l with
| left _ => removes l m'
| right _ => x :: removes l m'
end
end.
Lemma incl_removes : forall l m, removes l m [= m.
Lemma incl_removes_app : forall l m, m [= removes l m ++ l.
Lemma In_removes : forall x l m, In x (removes l m) <-> In x m /\ ~In x l.
End removes.
Properties of map.
Section map.
Variable (A B : Type) (f : A->B).
Lemma map_app : forall l1 l2, map f (l1 ++ l2) = (map f l1) ++ map f l2.
Lemma in_map_elim : forall x l, In x (map f l) -> exists y, In y l /\ x = f y.
Lemma map_eq : forall (g : A->B) l,
(forall x, In x l -> f x = g x) -> map f l = map g l.
End map.
Implicit Arguments in_map_elim [A B f x l].
Lemma map_eq_id : forall A (f:A->A) l,
(forall x, In x l -> f x = x) -> map f l = l.
Properties of flat_map.
Section flat_map.
Variables (A B : Type) (f : A -> list B).
Lemma In_flat_map_intro : forall x l y,
In y l -> In x (f y) -> In x (flat_map f l).
Lemma In_flat_map_elim : forall l y,
In y (flat_map f l) -> exists x, In x l /\ In y (f x).
Lemma flat_map_app : forall l m,
flat_map f (l ++ m) = flat_map f l ++ flat_map f m.
End flat_map.
Concatenation of a list of lists.
Section flat.
Variable A : Type.
Fixpoint flat (l : list (list A)) : list A :=
match l with
| nil => nil
| cons x l' => x ++ flat l'
end.
Lemma In_incl_flat : forall x l, In x l -> x [= flat l.
Lemma incl_flat_In : forall x c cs l,
In x c -> In c cs -> flat cs [= l -> In x l.
End flat.
Implicit Arguments In_incl_flat [A x l].
Position of an element in a list (the result is meaningful only if
the element occurs in the list).
Section pos.
Variables (A : Type) (eq_dec : forall x y : A, {x=y}+{~x=y}).
Section def.
Variable x : A.
Fixpoint pos l :=
match l with
| nil => 0
| a :: l' => if eq_dec a x then 0 else S (pos l')
end.
Lemma nth_pos d : forall l, In x l -> nth (pos l) l d = x.
Lemma pos_lt_length : forall l, In x l -> pos l < length l.
End def.
Lemma inj_pos x y : forall l, In x l -> pos x l = pos y l -> x = y.
End pos.
Element at a position (starting from 0) and its replacement.
Section Element_At_List.
Variable A : Type.
Fixpoint element_at (l : list A) (p : nat) : option A :=
match l with
| nil => None
| h :: t =>
match p with
| 0 => Some h
| S p' => element_at t p'
end
end.
Notation "l '[' p ']'" := (element_at l p) (at level 50).
Fixpoint replace_at (l : list A) (p : nat) (a : A) : list A :=
match l with
| nil => nil
| h :: t =>
match p with
| 0 => a :: t
| S p' => h :: (replace_at t p' a)
end
end.
Notation "l '[' p ':=' a ']'" := (replace_at l p a) (at level 50).
Lemma element_at_exists : forall l p,
p < length l <-> ex (fun a => l[p] = Some a).
Lemma element_at_replaced : forall l p a, p < length l -> l[p:=a][p] = Some a.
Lemma element_at_not_replaced : forall l p q a, p <> q -> l[p] = l[q:=a][p].
Lemma in_exists_element_at :
forall l a, In a l -> ex (fun p => l[p] = Some a).
Lemma exists_element_at_in :
forall l a, ex (fun p => l[p] = Some a) -> In a l.
Lemma element_at_in : forall (x:A) l n, l[n] = Some x -> In x l.
Lemma element_at_in2 :
forall (x:A) l n, l[n] = Some x -> In x l /\ n < length l.
Lemma element_at_app_r : forall l l' p,
p >= length l -> (l ++ l') [p] = l' [p - length l].
Lemma replace_at_app_r : forall l l' p a,
p >= length l -> (l ++ l') [p := a] = l ++ l' [p - length l := a].
End Element_At_List.
Implicit Arguments element_at_in [A x l n].
Implicit Arguments element_at_in2 [A x l n].
Implicit Arguments in_exists_element_at [A l a].
Implicit Arguments element_at_exists [A l p].
Notation "l '[' p ']'" := (element_at l p) (at level 50) : list_scope.
Notation "l '[' p ':=' a ']'" := (replace_at l p a) (at level 50) : list_scope.
Precidate saying that an element a in a list has been replaced
by an element a' such that r a a' where r is a relation.
Section one_less.
Variables (A : Type) (r : relation A).
Inductive one_less : relation (list A) :=
| one_less_cons : forall (l l' : list A) (p : nat) (a a' : A),
r a a' -> l[p] = Some a -> l' = l[p:=a'] -> one_less l l'.
Lemma one_less_length : forall l l', one_less l l' -> length l = length l'.
End one_less.
Implicit Arguments one_less [A].
Implicit Arguments one_less_cons [A].
Properties of rev.
Section reverse.
Variable A : Type.
Lemma in_rev : forall (x : A) l, In x l -> In x (rev l).
Lemma incl_rev : forall l : list A, l [= rev l.
Lemma rev_incl : forall l : list A, rev l [= l.
Lemma incl_rev_intro : forall l l' : list A, rev l [= rev l' -> l [= l'.
End reverse.
Tail-recursive reserve function.
Section reverse_tail_recursive.
Variable A : Type.
Fixpoint rev_append (l' l : list A) : list A :=
match l with
| nil => l'
| a :: l => rev_append (a :: l') l
end.
Notation rev' := (rev_append nil).
Lemma rev_append_rev : forall l l', rev_append l' l = rev l ++ l'.
Lemma rev_append_app : forall l l' acc : list A,
rev_append acc (l ++ l') = rev_append (rev_append acc l) l'.
Lemma rev'_app : forall l l' : list A, rev' (l ++ l') = rev' l' ++ rev' l.
Lemma rev'_rev : forall l : list A, rev' l = rev l.
Lemma rev'_rev' : forall l : list A, rev' (rev' l) = l.
Lemma rev'_cons : forall a (l : list A), rev' (a::l) = rev' l ++ (a::nil).
End reverse_tail_recursive.
Notation rev' := (rev_append nil).
Given a list l and a position n in l, return the pair of
lists l1 and l2 such that l = l1 ++ l2.
Section split.
Variable A : Type.
Fixpoint split_aux (acc l : list A) (n : nat) : option (list A * list A) :=
match l, n with
| _, 0 => Some (rev' acc, l)
| a :: l', S n' => split_aux (a::acc) l' n'
| _, _ => None
end.
Lemma split_aux_correct : forall l n l1 l2 acc,
split_aux acc l n = Some (l1, l2) -> rev' acc ++ l = l1 ++ l2.
Implicit Arguments split_aux_correct [l n l1 l2].
Notation split := (split_aux nil).
Lemma split_correct : forall l n l1 l2,
split l n = Some (l1, l2) -> l = l1 ++ l2.
End split.
Notation split := (split_aux nil).
Implicit Arguments split_correct [A l n l1 l2].
Last element of a list.
Section last.
Variable A : Type.
Lemma last_nth : forall (d : A) l, last l d = nth (length l - 1) l d.
Lemma last_default : forall (d1 : A) d2 l, l <> nil -> last l d1 = last l d2.
End last.
Implicit Arguments last_intro [A l].
Properties of partition.
Section partition.
Variables (A : Type) (f : A -> bool) (a : A) (l : list A).
Lemma partition_complete : let p := partition f l in
In a l -> In a (fst p) \/ In a (snd p).
Lemma partition_inleft : In a (fst (partition f l)) -> In a l.
Lemma partition_inright : In a (snd (partition f l)) -> In a l.
Lemma partition_left : In a (fst (partition f l)) -> f a = true.
Lemma partition_right : In a (snd (partition f l)) -> f a = false.
End partition.
Section partition_by_prop.
Variables (A : Type) (P : A -> Prop) (P_dec : forall x, {P x}+{~P x}).
Definition partition_by_prop a :=
match P_dec a with
| left _ => true
| right _ => false
end.
Lemma partition_by_prop_true : forall a, partition_by_prop a = true -> P a.
End partition_by_prop.
Section partition_by_rel.
Variables (A : Type) (R : relation A) (R_dec : rel_dec R).
Definition partition_by_rel p :=
if R_dec (fst p) (snd p) then true else false.
Lemma partition_by_rel_true : forall a b,
partition_by_rel (a, b) = true -> R a b.
End partition_by_rel.
Select the elements of a list according to a list of booleans.
Section ListFilter.
Variable A : Type.
Fixpoint listfilter (L : list A) l :=
match L with
| nil => nil
| a :: Q =>
match l with
| nil => nil
| true :: q => a :: listfilter Q q
| false :: q => listfilter Q q
end
end.
Lemma listfilter_in : forall L l i x,
L[i]=Some x -> l[i]=Some true -> In x (listfilter L l) .
End ListFilter.
Properties of nth and nth_error.
Section ListsNth.
Variable A: Type.
Lemma In_nth : forall A d (x : A) l,
In x l -> exists i, i < length l /\ nth i l d = x.
Lemma nth_error_In : forall (l : list A) i,
{a : A | nth_error l i = Some a} + {nth_error l i = None}.
Lemma nth_some_in :
forall (l : list A) i a, nth_error l i = Some a -> In a l.
Lemma list_In_nth : forall (l : list A) a,
In a l -> exists p: nat, nth_error l p = Some a.
Lemma nth_app_left : forall (l m: list A) i,
i < length l -> nth_error (l ++ m) i = nth_error l i.
Lemma nth_app_right : forall (l m: list A) i, i >= length l ->
nth_error (l ++ m) i = nth_error m (i - length l).
Lemma nth_app : forall (l m: list A) a i, nth_error (l ++ m) i = Some a ->
(nth_error l i = Some a /\ i < length l) \/
(nth_error m (i - length l) = Some a /\ i >= length l).
Lemma nth_beyond : forall (l : list A) i,
i >= length l -> nth_error l i = None.
Lemma nth_beyond_idx : forall (l : list A) i,
nth_error l i = None -> i >= length l.
Lemma nth_in : forall (l : list A) i,
nth_error l i <> None <-> i < length l.
Lemma nth_some : forall (l : list A) n a,
nth_error l n = Some a -> n < length l.
Lemma nth_map_none : forall (l : list A) i (f: A -> A),
nth_error l i = None -> nth_error (map f l) i = None.
Lemma nth_map_none_rev : forall (l : list A) i (f: A -> A),
nth_error (map f l) i = None -> nth_error l i = None.
Lemma nth_map_some : forall (l : list A) i (f: A -> A) a,
nth_error l i = Some a -> nth_error (map f l) i = Some (f a).
Lemma nth_map_some_rev : forall (l : list A) i (f: A -> A) a,
nth_error (map f l) i = Some a ->
exists a', nth_error l i = Some a' /\ f a' = a.
Lemma nth_error_singleton_in : forall (a b: A) i,
nth_error (a :: nil) i = Some b -> a = b /\ i = 0.
End ListsNth.
Implicit Arguments In_nth [A x l].
Total function returning the ith element of a list ŀ
if i < length l.
Section ith.
Variable A : Type.
Fixpoint ith (l : list A) : forall i, i < length l -> A :=
match l as l return forall i, i < length l -> A with
| nil => fun i H => False_rect A (lt_n_O H)
| cons x m => fun i =>
match i return i < S (length m) -> A with
| O => fun _ => x
| S j => fun H => ith (lt_S_n H)
end
end.
Lemma ith_In : forall l i (h : i < length l), In (ith h) l.
Lemma ith_eq : forall l i (hi : i < length l) j (hj : j < length l),
i = j -> ith hi = ith hj.
Lemma ith_eq_app : forall m l i (hi : i < length (l++m))
j (hj : j < length l), i = j -> ith hi = ith hj.
End ith.
Implicit Arguments ith_In [A l i].
Given a function f:nat->A and j:nat, values f j returns the
list f (j-1); ..; f 0 of the j first values of f starting from
0 in reverse order.
Section values.
Variables (A : Type) (f : nat -> A).
Fixpoint values j : list A :=
match j with
| 0 => nil
| S k => f k :: values k
end.
End values.
Given a function n:nat and f:forall i, i<n -> A, pvalues n f
returns the list f 0; ..; f (n-1) of the n first values of f
starting from 0.
Section pvalues.
Variable A : Type.
Fixpoint pvalues n : (forall i, i < n -> A) -> list A :=
match n as n return (forall i, i < n -> A) -> list A with
| 0 => fun _ => nil
| S k => fun f =>
f 0 (lt_O_Sn k) :: pvalues (fun i h => f (S i) (lt_n_S h))
end.
Lemma pvalues_eq : forall n (f g : forall i, i < n -> A),
(forall i (hi : i < n), f i hi = g i hi) -> pvalues f = pvalues g.
End pvalues.
Section pvalues_map.
Variables (A B : Type) (f : A -> B).
Definition f_ith (l : list A) i (hi : i < length l) := f (ith hi).
Lemma pvalues_ith_eq_map : forall l, pvalues (@f_ith l) = map f l.
End pvalues_map.
First element satisfying some boolean function.
Section first.
Variable (A : Type) (f : A -> bool).
Fixpoint first l :=
match l with
| nil => None
| x :: l' => if f x then Some x else first l'
end.
End first.
Properties of fold_left.
Instance transpose_inclusion A B :
Proper (inclusion ==> eq ==> impl) (@transpose A B).
Instance transpose_same_rel A B :
Proper (same_rel ==> eq ==> iff) (@transpose A B).
Section fold_left.
Variables (A : Type) (eqA : relation A) (B : Type) (eqB : relation B).
Definition feq f f' :=
forall a a', eqA a a' -> forall b b', eqB b b' -> eqA (f a b) (f' a' b').
Global Instance fold_left_m_ext :
Proper (feq ==> eqlistA eqB ==> eqA ==> eqA) (@fold_left A B).
End fold_left.
Section fold_left_list.
Variables (A B : Type) (f : list A -> B -> list A).
Variable g : B -> list A.
Variable hyp : forall l b, f l b = g b ++ l.
Lemma fold_left_flat_map : forall bs l,
fold_left f bs l = flat_map g (rev bs) ++ l.
Lemma In_fold_left : forall a bs l,
In a (fold_left f bs l) <-> (In a l \/ exists b, In b bs /\ In a (g b)).
End fold_left_list.
Implicit Arguments fold_left_flat_map [A B f].
Implicit Arguments In_fold_left [A B f].
lookup el default l takes an association list of pairs of keys
and values, and returns v such that (el, v) belongs to the list,
or default if there is no element with key equal to el.
Section lookup.
Variable (A B : Type).
Variable (eqA_dec : forall x y : A, {x = y} + {x <> y}).
Variable (el : A).
Variable (default : B).
Fixpoint lookup (l : list (A * B)) : B :=
match l with
| nil => default
| (el', v)::l' =>
if @eqA_dec el el' then
v
else
lookup l'
end.
Variable P : B -> Prop.
Lemma lookup_prop l :
(forall x, In x l -> P (snd x)) -> P default -> P (lookup l).
End lookup.
lookup_dep is equivalent to lookup above but works on lists of
dependent pairs instead.
Section lookup_dep.
Variable (A : Type) (B : A -> Type).
Variable (eqA_dec : forall x y : A, {x = y} + {x <> y}).
Variable (el : A).
Variable (default : forall a : A, B a).
Program Fixpoint lookup_dep (l : list { el : A & B el}) : B el :=
match l with
| nil => @default el
| x::l' =>
let (el', v) := x in
if @eqA_dec el el' then
v
else
lookup_dep l'
end.
Variable P : forall a : A, B a -> Prop.
Lemma lookup_dep_prop (l : list {el : A & B el}) :
(forall x, In x l -> P (projT2 x)) ->
(forall a : A, P (@default a)) -> P (lookup_dep l).
End lookup_dep.
Properties of forallb.
Section forallb.
Variables (A : Type) (P : A -> Prop)
(f : A -> bool) (f_ok : forall x, f x = true <-> P x).
Lemma forallb_false : forall l,
forallb f l = false <-> exists x, In x l /\ f x = false.
Lemma forallb_neg : forall l,
forallb f l = false <-> exists x, In x l /\ ~P x.
Variables (As : list A) (As_ok : forall x, In x As).
Lemma forallb_ok_fintype : forallb f As = true <-> forall x, P x.
End forallb.
sub_list l k n is the sublist of l of length n starting at
position k.
Section sub_list.
Variable A : Type.
Fixpoint sub_list l k n : list A :=
match l, k, n with
| _ :: l', S k', _ => sub_list l' k' n
| x :: l', 0, S n' => x :: sub_list l' 0 n'
| _, _, _ => nil
end.
Functional Scheme sub_list_ind := Induction for sub_list Sort Prop.
Lemma sub_list_ok : forall l k n i,
k < length l -> k+n <= length l -> i < n ->
element_at (sub_list l k n) i = element_at l (k+i).
Lemma length_sub_list : forall l k n,
k < length l -> k+n <= length l -> length (sub_list l k n) = n.
Lemma eq_app_elim_l : forall l1 l l2,
l = l1 ++ l2 -> l1 = sub_list l 0 (length l1).
Lemma eq_app_elim_r : forall l1 l l2,
l = l1 ++ l2 -> l2 = sub_list l (length l1) (length l2).
Lemma sub_list_0 : forall l k, sub_list l k 0 = nil.
Lemma sub_list_length : forall l, sub_list l 0 (length l) = l.
Lemma app_eq_sub_list : forall l1 l2, l1++l2 =
sub_list (l1++l2) 0 (length l1)
++ sub_list (l1++l2) (length l1) (length l2).
End sub_list.
Implicit Arguments eq_app_elim_l [A l1 l l2].
Implicit Arguments eq_app_elim_r [A l1 l l2].