Library Lists_ext
Require Import Omega List Recdef Wf_nat Permutation.
Require Import ssreflect ssrbool ssrfun eqtype.
Require Import Arith_ext EqNat_ext.
Export List.
Require Import ssreflect ssrbool ssrfun eqtype.
Require Import Arith_ext EqNat_ext.
Export List.
find the index c of an element v of type A in a list l
Ltac Find_var A v l c :=
match l with
| @List.cons A v ?tl => constr:c
| @List.cons A ?hd ?tl => let x := eval compute in (S c) in Find_var A v tl x
| @List.nil A => constr:O
end.
match l with
| @List.cons A v ?tl => constr:c
| @List.cons A ?hd ?tl => let x := eval compute in (S c) in Find_var A v tl x
| @List.nil A => constr:O
end.
return true if the v element is in l
Ltac In_list v l :=
match l with
| @List.cons ?A v ?tl => constr:true
| @List.cons ?A ?hd ?tl => In_list v tl
| @List.nil ?A => constr:false
end.
return true if at least one element of l1 is in l2
Ltac In_list_list l1 l2 :=
match l1 with
| ?hd :: ?tl =>
let x := In_list hd l2 in
match eval compute in x with
| true => true
| false => (In_list_list tl l2)
end
| (@nil _) => false
end.
Ltac length lst :=
match lst with
| nil => O
| ?hd :: ?tl => constr:(S (length tl))
end.
Ltac compute_positions1 l k idx :=
match l with
| @List.cons ?A k ?tl =>
let new_idx := constr : (S idx) in
let new_tl := compute_positions1 tl k new_idx in
constr: (@List.cons nat idx new_tl)
| @List.cons ?A ?hd ?tl =>
let new_idx := constr : (S idx) in
compute_positions1 tl k new_idx
| _ =>
constr : (@List.nil nat)
end.
Ltac In_tac :=
match goal with
| |- In ?ELT (?ELT :: ?LT) => apply in_eq
| |- In ?ELT (?ELT' :: ?LT) => apply in_cons; In_tac
| |- In ?ELT nil => fail
end.
Ltac position elt lst cnt :=
match lst with
| nil => O
| elt :: ?tl => cnt
| ?hd :: ?tl => position elt tl (S cnt)
end.
Ltac do_n_right cnt :=
match cnt with
| O => idtac
| S ?cnt' => right; do_n_right cnt'
end.
Ltac prove_In :=
match goal with
| |- In ?x nil => fail "cannot prove In x nil"
| |- In ?x (?lst) =>
let pos := position x lst (S O) in
let len := length lst in
simpl;
match pos with
| O => fail "head does not belong to tail"
| _ =>
let cnt := eval compute in (minus pos (S O)) in
let last := eval compute in (len = pos) in
match last with
| (?n = ?n) => do_n_right (S cnt); reflexivity
| _ => do_n_right cnt; left; reflexivity
end
end
end.
Ltac incl_tac :=
match goal with
| |- incl (?HD :: ?TL) ?L =>
let tmp := In_list HD L in
match tmp with
| true => apply incl_cons ;
[ In_tac
|
incl_tac
]
| false => fail
end
| |- incl nil ?L =>
by rewrite /=
end.
Section app_ext.
Variable A : Type.
Lemma app_split : forall (l : list A) k, k <= length l ->
exists l1, exists l2, length l1 = k /\ l = l1 ++ l2.
Lemma app_app_split_L : forall (l1 l2 k1 k2 : list A),
l1 ++ l2 = k1 ++ k2 -> length l1 > length k1 -> exists k2', k2 = k2' ++ l2 /\ l1 = k1 ++ k2'.
Lemma app_app_split_R : forall (l1 l2 k1 k2 : list A),
l1 ++ l2 = k1 ++ k2 -> length l1 <= length k1 -> exists k1', k1 = l1 ++ k1' /\ l2 = k1' ++ k2.
Lemma head_app : forall (l1 l2 : list A), l1 <> nil -> head (l1 ++ l2) = head l1.
Lemma hd_nth_0 : forall (def:A) (l:list A), (O < length l)%nat -> hd def l = nth 0 l def.
Lemma tail_app : forall (lst lst' : list A), 0 < length lst ->
tail (lst ++ lst') = tail lst ++ lst'.
Lemma not_in_app : forall (l1 l2 : list A) l,
~ In l l1 -> ~ In l l2 -> ~ In l (l1 ++ l2).
Lemma not_in_app_inv : forall (x : A) l k, ~ In x (l ++ k) ->
~ In x l /\ ~ In x k.
Lemma app_inv : forall (l1 l2 k1 k2 : list A),
l1 ++ l2 = k1 ++ k2 -> length l1 = length k1 ->
l1 = k1 /\ l2 = k2.
End app_ext.
Implicit Arguments app_split [A].
Implicit Arguments app_app_split_L [A].
Implicit Arguments app_app_split_R [A].
Implicit Arguments head_app [A].
Implicit Arguments hd_nth_0 [A].
Implicit Arguments tail_app [A].
Implicit Arguments not_in_app [A].
Implicit Arguments app_inv [A].
Section various_lemmas.
Variable A : Type.
Implicit Type l : list A.
Lemma len_nil : forall l, length l = O -> l = nil.
Lemma len0 : forall l, l = nil -> length l = O.
Lemma len_not_nil : forall l, length l <> O -> l <> nil.
Lemma lst_dec' : forall l, l = nil \/ l <> nil.
Lemma lst_dec : forall l, l = nil \/ exists h, exists t, l = h ++ (t :: nil).
Lemma list_dec : (forall (a1 a2 : A), { a1 = a2 } + { a1 <> a2 }) ->
forall l1 l2, { l1 = l2 } + { l1 <> l2}.
Lemma list_last : forall l, O < length l -> exists l', exists a, l = l' ++ a :: nil.
Lemma list_last2 : forall l, 1 < length l ->
exists l', exists a, exists b, l = l' ++ a :: b :: nil.
Lemma hd_tail : forall a l, l <> nil -> l = hd a l :: tail l.
Lemma len_tail : forall l, length (tail l) = length l - 1.
Lemma not_In_cons : forall l a1 a2, ~ In a1 (a2 :: nil) -> ~ In a1 l ->
~ In a1 (a2 :: l).
Fixpoint list_flat lst : list A := if lst is h :: t then h ++ list_flat t else nil.
Lemma list_flat_app : forall (lst k : list (list A)),
list_flat (lst ++ k) = list_flat lst ++ list_flat k.
Lemma rev_inj : forall l1 l2, rev l1 = rev l2 -> l1 = l2.
Lemma rev_unit': forall l a, rev (a :: l) = (rev l) ++ a :: nil.
Lemma forallb_ext2 : forall l (f g : A -> bool),
(forall a, In a l -> f a = g a) -> forallb f l = forallb g l.
End various_lemmas.
Section ith_ext.
Fixpoint ith {A : Type} (n : nat) (l : list A) : option A :=
match n with
| O => match l with nil => None | h :: _ => Some h end
| S m => match l with nil => None | _ :: t => ith m t end
end.
Lemma ith_nil : forall {A : Type} i, ith i (@nil A) = None.
Lemma ith_In : forall {A : Type} (l : list A) n a, ith n l = Some a -> In a l.
Lemma ith_Some_inv1 : forall {A:Type} (l:list A) i v, ith i l = Some v -> i < length l.
Lemma ith_map : forall {A B : Type} (l : list A) x v,
ith x l = Some v -> forall f : A -> B, ith x (map f l) = Some (f v).
Lemma ith_Some_lt : forall {A : Type} (l :list A) n a,
ith n l = Some a -> n < length l.
Lemma ith_map_Some_inv : forall {A B : Type} (f : A -> B) l i x,
ith i (map f l) = Some x -> exists y, ith i l = Some y /\ f y = x.
Lemma ith_map_inv : forall {A B : Type} (f : A -> B) l i b,
ith i (map f l) = Some b -> exists a, ith i l = Some a /\ b = f a.
Lemma ith_Some_exists : forall {A B: Type} (l : list A) (l' : list B),
length l = length l' -> forall n f, n < length l ->
ith n l = Some f -> exists f', ith n l' = Some f'.
Lemma ith_nth : forall {A : Type} l def (a : A) i,
ith i l = Some a ->
nth i l def = a.
Lemma map_ith
: forall (A B : Type) (f : A -> B) (l : list A) (n : nat) x,
ith n l = Some x -> ith n (map f l) = Some (f x).
End ith_ext.
Section uzip.
Variables A B : Type.
Definition uzip1 (l : list (A * B)) := map (fun x => fst x) l.
Definition uzip2 (l : list (A * B)) := map (fun x => snd x) l.
Lemma ith_uzip1_inv : forall (l : list (A * B)) x v,
ith x (uzip1 l) = Some v -> exists w, ith x l = Some w /\ fst w = v.
Lemma ith_uzip1_uzip2 : forall l x (a : A) (b : B),
ith x (uzip1 l) = Some a -> ith x (uzip2 l) = Some b -> ith x l = Some (a, b).
Lemma In_uzip1 : forall l a b, In (a, b) l -> In a (uzip1 l).
Lemma uzip1_In : forall l a, In a (uzip1 l) -> exists b, In (a, b) l.
Lemma uzip1_app : forall l l', uzip1 l ++ uzip1 l' = uzip1 (l ++ l').
End uzip.
Implicit Arguments In_uzip1 [A B].
Implicit Arguments uzip1_In [A B].
Section various_lemmas2.
Variable A B : Type.
Implicit Type l : list A.
Implicit Type k : list B.
Lemma map_cons : forall {A B : Type} (f : A -> B) hd tl, map f (hd ::tl) = f hd :: map f tl.
Lemma fold_right_app_map_nil : forall l,
fold_right (@app B) nil (map (fun _ => nil) l) = nil.
Lemma fold_left_ext : forall k a (f f' : A -> B -> A),
(forall x a, In x k -> f a x = f' a x) ->
fold_left f k a = fold_left f' k a.
Lemma fold_left_ext2 : forall (k k' : list B) a (f f' : A -> B -> A),
length k = length k' -> (forall i a, i < length k ->
forall x x', ith i k = Some x -> ith i k' = Some x' -> f a x = f' a x') ->
fold_left f k a = fold_left f' k' a.
Lemma fold_right_ext2 : forall (k k' : list B) (a : A) (f f' : B -> A -> A),
length k = length k' -> (forall i a0, i < length k ->
forall x x',ith i k = Some x -> ith i k' = Some x' -> f x a0 = f' x' a0) ->
fold_right f a k = fold_right f' a k'.
Lemma fold_left_app_acc : forall k (f : B -> list A) l1 l2,
fold_left (fun a e => f e ++ a) k (l1 ++ l2) =
(fold_left (fun a e => f e ++ a) k l1) ++ l2.
Lemma fold_left_app2 : forall k (a : A) (f : B -> list A) l, In a l ->
In a (fold_left (fun (acc : list A) (e : B) => f e ++ acc) k l).
Lemma fold_left_app3 : forall k (a : A) (g : B -> list A) l,
In a (fold_left (fun l0 (e : B) => g e ++ l0) k nil) ->
In a (fold_left (fun l0 (e : B) => g e ++ l0) k l).
match l1 with
| ?hd :: ?tl =>
let x := In_list hd l2 in
match eval compute in x with
| true => true
| false => (In_list_list tl l2)
end
| (@nil _) => false
end.
Ltac length lst :=
match lst with
| nil => O
| ?hd :: ?tl => constr:(S (length tl))
end.
Ltac compute_positions1 l k idx :=
match l with
| @List.cons ?A k ?tl =>
let new_idx := constr : (S idx) in
let new_tl := compute_positions1 tl k new_idx in
constr: (@List.cons nat idx new_tl)
| @List.cons ?A ?hd ?tl =>
let new_idx := constr : (S idx) in
compute_positions1 tl k new_idx
| _ =>
constr : (@List.nil nat)
end.
Ltac In_tac :=
match goal with
| |- In ?ELT (?ELT :: ?LT) => apply in_eq
| |- In ?ELT (?ELT' :: ?LT) => apply in_cons; In_tac
| |- In ?ELT nil => fail
end.
Ltac position elt lst cnt :=
match lst with
| nil => O
| elt :: ?tl => cnt
| ?hd :: ?tl => position elt tl (S cnt)
end.
Ltac do_n_right cnt :=
match cnt with
| O => idtac
| S ?cnt' => right; do_n_right cnt'
end.
Ltac prove_In :=
match goal with
| |- In ?x nil => fail "cannot prove In x nil"
| |- In ?x (?lst) =>
let pos := position x lst (S O) in
let len := length lst in
simpl;
match pos with
| O => fail "head does not belong to tail"
| _ =>
let cnt := eval compute in (minus pos (S O)) in
let last := eval compute in (len = pos) in
match last with
| (?n = ?n) => do_n_right (S cnt); reflexivity
| _ => do_n_right cnt; left; reflexivity
end
end
end.
Ltac incl_tac :=
match goal with
| |- incl (?HD :: ?TL) ?L =>
let tmp := In_list HD L in
match tmp with
| true => apply incl_cons ;
[ In_tac
|
incl_tac
]
| false => fail
end
| |- incl nil ?L =>
by rewrite /=
end.
Section app_ext.
Variable A : Type.
Lemma app_split : forall (l : list A) k, k <= length l ->
exists l1, exists l2, length l1 = k /\ l = l1 ++ l2.
Lemma app_app_split_L : forall (l1 l2 k1 k2 : list A),
l1 ++ l2 = k1 ++ k2 -> length l1 > length k1 -> exists k2', k2 = k2' ++ l2 /\ l1 = k1 ++ k2'.
Lemma app_app_split_R : forall (l1 l2 k1 k2 : list A),
l1 ++ l2 = k1 ++ k2 -> length l1 <= length k1 -> exists k1', k1 = l1 ++ k1' /\ l2 = k1' ++ k2.
Lemma head_app : forall (l1 l2 : list A), l1 <> nil -> head (l1 ++ l2) = head l1.
Lemma hd_nth_0 : forall (def:A) (l:list A), (O < length l)%nat -> hd def l = nth 0 l def.
Lemma tail_app : forall (lst lst' : list A), 0 < length lst ->
tail (lst ++ lst') = tail lst ++ lst'.
Lemma not_in_app : forall (l1 l2 : list A) l,
~ In l l1 -> ~ In l l2 -> ~ In l (l1 ++ l2).
Lemma not_in_app_inv : forall (x : A) l k, ~ In x (l ++ k) ->
~ In x l /\ ~ In x k.
Lemma app_inv : forall (l1 l2 k1 k2 : list A),
l1 ++ l2 = k1 ++ k2 -> length l1 = length k1 ->
l1 = k1 /\ l2 = k2.
End app_ext.
Implicit Arguments app_split [A].
Implicit Arguments app_app_split_L [A].
Implicit Arguments app_app_split_R [A].
Implicit Arguments head_app [A].
Implicit Arguments hd_nth_0 [A].
Implicit Arguments tail_app [A].
Implicit Arguments not_in_app [A].
Implicit Arguments app_inv [A].
Section various_lemmas.
Variable A : Type.
Implicit Type l : list A.
Lemma len_nil : forall l, length l = O -> l = nil.
Lemma len0 : forall l, l = nil -> length l = O.
Lemma len_not_nil : forall l, length l <> O -> l <> nil.
Lemma lst_dec' : forall l, l = nil \/ l <> nil.
Lemma lst_dec : forall l, l = nil \/ exists h, exists t, l = h ++ (t :: nil).
Lemma list_dec : (forall (a1 a2 : A), { a1 = a2 } + { a1 <> a2 }) ->
forall l1 l2, { l1 = l2 } + { l1 <> l2}.
Lemma list_last : forall l, O < length l -> exists l', exists a, l = l' ++ a :: nil.
Lemma list_last2 : forall l, 1 < length l ->
exists l', exists a, exists b, l = l' ++ a :: b :: nil.
Lemma hd_tail : forall a l, l <> nil -> l = hd a l :: tail l.
Lemma len_tail : forall l, length (tail l) = length l - 1.
Lemma not_In_cons : forall l a1 a2, ~ In a1 (a2 :: nil) -> ~ In a1 l ->
~ In a1 (a2 :: l).
Fixpoint list_flat lst : list A := if lst is h :: t then h ++ list_flat t else nil.
Lemma list_flat_app : forall (lst k : list (list A)),
list_flat (lst ++ k) = list_flat lst ++ list_flat k.
Lemma rev_inj : forall l1 l2, rev l1 = rev l2 -> l1 = l2.
Lemma rev_unit': forall l a, rev (a :: l) = (rev l) ++ a :: nil.
Lemma forallb_ext2 : forall l (f g : A -> bool),
(forall a, In a l -> f a = g a) -> forallb f l = forallb g l.
End various_lemmas.
Section ith_ext.
Fixpoint ith {A : Type} (n : nat) (l : list A) : option A :=
match n with
| O => match l with nil => None | h :: _ => Some h end
| S m => match l with nil => None | _ :: t => ith m t end
end.
Lemma ith_nil : forall {A : Type} i, ith i (@nil A) = None.
Lemma ith_In : forall {A : Type} (l : list A) n a, ith n l = Some a -> In a l.
Lemma ith_Some_inv1 : forall {A:Type} (l:list A) i v, ith i l = Some v -> i < length l.
Lemma ith_map : forall {A B : Type} (l : list A) x v,
ith x l = Some v -> forall f : A -> B, ith x (map f l) = Some (f v).
Lemma ith_Some_lt : forall {A : Type} (l :list A) n a,
ith n l = Some a -> n < length l.
Lemma ith_map_Some_inv : forall {A B : Type} (f : A -> B) l i x,
ith i (map f l) = Some x -> exists y, ith i l = Some y /\ f y = x.
Lemma ith_map_inv : forall {A B : Type} (f : A -> B) l i b,
ith i (map f l) = Some b -> exists a, ith i l = Some a /\ b = f a.
Lemma ith_Some_exists : forall {A B: Type} (l : list A) (l' : list B),
length l = length l' -> forall n f, n < length l ->
ith n l = Some f -> exists f', ith n l' = Some f'.
Lemma ith_nth : forall {A : Type} l def (a : A) i,
ith i l = Some a ->
nth i l def = a.
Lemma map_ith
: forall (A B : Type) (f : A -> B) (l : list A) (n : nat) x,
ith n l = Some x -> ith n (map f l) = Some (f x).
End ith_ext.
Section uzip.
Variables A B : Type.
Definition uzip1 (l : list (A * B)) := map (fun x => fst x) l.
Definition uzip2 (l : list (A * B)) := map (fun x => snd x) l.
Lemma ith_uzip1_inv : forall (l : list (A * B)) x v,
ith x (uzip1 l) = Some v -> exists w, ith x l = Some w /\ fst w = v.
Lemma ith_uzip1_uzip2 : forall l x (a : A) (b : B),
ith x (uzip1 l) = Some a -> ith x (uzip2 l) = Some b -> ith x l = Some (a, b).
Lemma In_uzip1 : forall l a b, In (a, b) l -> In a (uzip1 l).
Lemma uzip1_In : forall l a, In a (uzip1 l) -> exists b, In (a, b) l.
Lemma uzip1_app : forall l l', uzip1 l ++ uzip1 l' = uzip1 (l ++ l').
End uzip.
Implicit Arguments In_uzip1 [A B].
Implicit Arguments uzip1_In [A B].
Section various_lemmas2.
Variable A B : Type.
Implicit Type l : list A.
Implicit Type k : list B.
Lemma map_cons : forall {A B : Type} (f : A -> B) hd tl, map f (hd ::tl) = f hd :: map f tl.
Lemma fold_right_app_map_nil : forall l,
fold_right (@app B) nil (map (fun _ => nil) l) = nil.
Lemma fold_left_ext : forall k a (f f' : A -> B -> A),
(forall x a, In x k -> f a x = f' a x) ->
fold_left f k a = fold_left f' k a.
Lemma fold_left_ext2 : forall (k k' : list B) a (f f' : A -> B -> A),
length k = length k' -> (forall i a, i < length k ->
forall x x', ith i k = Some x -> ith i k' = Some x' -> f a x = f' a x') ->
fold_left f k a = fold_left f' k' a.
Lemma fold_right_ext2 : forall (k k' : list B) (a : A) (f f' : B -> A -> A),
length k = length k' -> (forall i a0, i < length k ->
forall x x',ith i k = Some x -> ith i k' = Some x' -> f x a0 = f' x' a0) ->
fold_right f a k = fold_right f' a k'.
Lemma fold_left_app_acc : forall k (f : B -> list A) l1 l2,
fold_left (fun a e => f e ++ a) k (l1 ++ l2) =
(fold_left (fun a e => f e ++ a) k l1) ++ l2.
Lemma fold_left_app2 : forall k (a : A) (f : B -> list A) l, In a l ->
In a (fold_left (fun (acc : list A) (e : B) => f e ++ acc) k l).
Lemma fold_left_app3 : forall k (a : A) (g : B -> list A) l,
In a (fold_left (fun l0 (e : B) => g e ++ l0) k nil) ->
In a (fold_left (fun l0 (e : B) => g e ++ l0) k l).
see also Coq.Lists.List.in_map : forall (A B : Type) (f : A -> B) (l : list A) (x : A), In x l -> In (f x) (map f l)
Lemma in_map' : forall l x (f : A -> B), In x (map f l) ->
exists x', In x' l /\ x = f x'.
Lemma map_ext2 : forall l (f g : A -> B),
(forall a : A, In a l -> f a = g a) -> map f l = map g l.
Lemma map_fst_split : forall (l : list (A * B)), map (fun x => fst x) l = fst (split l).
Lemma map_snd_split : forall (l : list (A * B)), map (fun x => snd x) l = snd (split l).
Lemma len_flat_map : forall n l m (f : A -> list B),
(forall a, length (f a) = m) -> length l = n ->
length (flat_map f l) = n * m.
Lemma len_flat_map_inv : forall l q m (f : A -> list B),
length (flat_map f l) = q * m ->
(forall a, length (f a) = m) ->
m <> O ->
length l = q.
Definition injection {A B : Type} (f : A -> B) :=
forall x y, f x = f y -> x = y.
Lemma flat_map_inj : forall (f : A -> list B), injection f ->
(exists k, k <> O /\ forall a, length (f a) = k) ->
forall l1 l2, flat_map f l1 = flat_map f l2 -> l1 = l2.
End various_lemmas2.
Implicit Arguments fold_right_app_map_nil [A B].
Implicit Arguments fold_left_ext [A B].
Implicit Arguments fold_left_app2 [A B].
Implicit Arguments fold_left_app3 [A B].
Implicit Arguments fold_left_app_acc [A B].
Implicit Arguments in_map' [A B].
Implicit Arguments map_ext2 [A B].
Implicit Arguments uzip1 [A B].
Implicit Arguments uzip2 [A B].
Implicit Arguments map_fst_split [A B].
Implicit Arguments map_snd_split [A B].
Implicit Arguments len_flat_map [A B].
Implicit Arguments len_flat_map_inv [A B].
Implicit Arguments flat_map_inj [A B].
Section combine_ext.
Variables A B : Type.
Implicit Type l : list A.
Implicit Type k : list B.
Lemma In_combine_lr : forall l a b, In (a, b) (combine l l) -> a = b.
Lemma map_fst_combine : forall l k, length l = length k ->
map (fun x => fst x) (combine l k) = l.
Lemma map_snd_combine : forall l k, length l = length k ->
map (fun x => snd x) (combine l k) = k.
Lemma In_combine : forall l k x, length l = length k ->
(exists n, n < List.length l /\ ith n l = Some (fst x) /\ ith n k = Some (snd x)) ->
In x (combine l k).
Lemma len_combineC : forall l k, length (combine l k) = length (combine k l).
Variable C : Type.
Lemma combine_map_snd : forall (l : list (A * B)) (x : list C),
combine (uzip2 l) x = map (fun a_b => (snd (fst a_b), snd a_b)) (combine l x).
Lemma combine_app : forall n (l1 k1 l2 k2 : list A),
length l1 = n -> length l2 = n ->
combine (l1 ++ k1) (l2 ++ k2) = combine l1 l2 ++ combine k1 k2.
Lemma ith_combine_Some_inv : forall i a b (x : A) ( y : B),
ith i (combine a b) = Some (x, y) -> ith i a = Some x.
Lemma In_combine_com : forall l k a b, In (a, b) (combine l k) ->
In (b, a) (combine k l).
End combine_ext.
Implicit Arguments In_combine_lr [A].
Implicit Arguments map_fst_combine [A B].
Implicit Arguments map_snd_combine [A B].
Implicit Arguments In_combine [A B].
Implicit Arguments len_combineC [A B].
Implicit Arguments combine_map_snd [A B C].
Implicit Arguments combine_app [A].
Implicit Arguments ith_combine_Some_inv [A B].
Implicit Arguments In_combine_com [A B].
Section filter_ext.
Variable A : Type.
Lemma filter_app : forall (l1 l2 : list A) (p : A -> bool),
filter p (l1 ++ l2) = filter p l1 ++ filter p l2.
Lemma filter_all : forall (l : list A) (p : A -> bool),
(forall x, In x l -> p x) -> filter p l = l.
End filter_ext.
Implicit Arguments filter_app [A].
Implicit Arguments filter_all [A].
Definition fold_andb := fold_right andb true.
Lemma fold_right_andb_inv : forall l x, fold_andb l -> In x l -> x.
Lemma fold_andb_forallb : forall {A : Type} (l : list A) f, forallb f l = fold_andb (map f l).
exists x', In x' l /\ x = f x'.
Lemma map_ext2 : forall l (f g : A -> B),
(forall a : A, In a l -> f a = g a) -> map f l = map g l.
Lemma map_fst_split : forall (l : list (A * B)), map (fun x => fst x) l = fst (split l).
Lemma map_snd_split : forall (l : list (A * B)), map (fun x => snd x) l = snd (split l).
Lemma len_flat_map : forall n l m (f : A -> list B),
(forall a, length (f a) = m) -> length l = n ->
length (flat_map f l) = n * m.
Lemma len_flat_map_inv : forall l q m (f : A -> list B),
length (flat_map f l) = q * m ->
(forall a, length (f a) = m) ->
m <> O ->
length l = q.
Definition injection {A B : Type} (f : A -> B) :=
forall x y, f x = f y -> x = y.
Lemma flat_map_inj : forall (f : A -> list B), injection f ->
(exists k, k <> O /\ forall a, length (f a) = k) ->
forall l1 l2, flat_map f l1 = flat_map f l2 -> l1 = l2.
End various_lemmas2.
Implicit Arguments fold_right_app_map_nil [A B].
Implicit Arguments fold_left_ext [A B].
Implicit Arguments fold_left_app2 [A B].
Implicit Arguments fold_left_app3 [A B].
Implicit Arguments fold_left_app_acc [A B].
Implicit Arguments in_map' [A B].
Implicit Arguments map_ext2 [A B].
Implicit Arguments uzip1 [A B].
Implicit Arguments uzip2 [A B].
Implicit Arguments map_fst_split [A B].
Implicit Arguments map_snd_split [A B].
Implicit Arguments len_flat_map [A B].
Implicit Arguments len_flat_map_inv [A B].
Implicit Arguments flat_map_inj [A B].
Section combine_ext.
Variables A B : Type.
Implicit Type l : list A.
Implicit Type k : list B.
Lemma In_combine_lr : forall l a b, In (a, b) (combine l l) -> a = b.
Lemma map_fst_combine : forall l k, length l = length k ->
map (fun x => fst x) (combine l k) = l.
Lemma map_snd_combine : forall l k, length l = length k ->
map (fun x => snd x) (combine l k) = k.
Lemma In_combine : forall l k x, length l = length k ->
(exists n, n < List.length l /\ ith n l = Some (fst x) /\ ith n k = Some (snd x)) ->
In x (combine l k).
Lemma len_combineC : forall l k, length (combine l k) = length (combine k l).
Variable C : Type.
Lemma combine_map_snd : forall (l : list (A * B)) (x : list C),
combine (uzip2 l) x = map (fun a_b => (snd (fst a_b), snd a_b)) (combine l x).
Lemma combine_app : forall n (l1 k1 l2 k2 : list A),
length l1 = n -> length l2 = n ->
combine (l1 ++ k1) (l2 ++ k2) = combine l1 l2 ++ combine k1 k2.
Lemma ith_combine_Some_inv : forall i a b (x : A) ( y : B),
ith i (combine a b) = Some (x, y) -> ith i a = Some x.
Lemma In_combine_com : forall l k a b, In (a, b) (combine l k) ->
In (b, a) (combine k l).
End combine_ext.
Implicit Arguments In_combine_lr [A].
Implicit Arguments map_fst_combine [A B].
Implicit Arguments map_snd_combine [A B].
Implicit Arguments In_combine [A B].
Implicit Arguments len_combineC [A B].
Implicit Arguments combine_map_snd [A B C].
Implicit Arguments combine_app [A].
Implicit Arguments ith_combine_Some_inv [A B].
Implicit Arguments In_combine_com [A B].
Section filter_ext.
Variable A : Type.
Lemma filter_app : forall (l1 l2 : list A) (p : A -> bool),
filter p (l1 ++ l2) = filter p l1 ++ filter p l2.
Lemma filter_all : forall (l : list A) (p : A -> bool),
(forall x, In x l -> p x) -> filter p l = l.
End filter_ext.
Implicit Arguments filter_app [A].
Implicit Arguments filter_all [A].
Definition fold_andb := fold_right andb true.
Lemma fold_right_andb_inv : forall l x, fold_andb l -> In x l -> x.
Lemma fold_andb_forallb : forall {A : Type} (l : list A) f, forallb f l = fold_andb (map f l).
Additional lemmas about the standard List.incl
Section inclusion.
Variable A : Type.
Lemma incl_nil_inv : forall (l : list A), incl l nil -> l = nil.
Lemma incl_singl : forall (a : A) l, In a l -> incl (a :: nil) l.
Lemma incl_app_inv : forall (l1 l2 : list A) k, incl (l1 ++ l2) k -> incl l1 k /\ incl l2 k.
Lemma incl_cons_R : forall (x : A) l1 l2, incl l1 l2 -> incl l1 (x :: l2).
Lemma incl_cons_cons : forall (l1 l2 : list A) x, incl l1 l2 -> incl (x :: l1) (x :: l2).
Lemma incl_cons_inv_L : forall a (l : list A) k, incl (a :: l) k -> In a k /\ incl l k.
Lemma incl_filter : forall (l1 l2 : list A), incl l1 l2 -> forall f, incl (filter f l1) (filter f l2).
Lemma incl_filter_L : forall (l1 l2 : list A), incl l1 l2 -> forall f, incl (filter f l1) l2.
Lemma incl_seq_filter_imp : forall (k : list A) (p p': A -> bool ),
(forall x, In x k -> p x -> p' x ) ->
incl (filter p k) (filter p' k).
End inclusion.
Implicit Arguments incl_nil_inv [A].
Implicit Arguments incl_singl [A].
Implicit Arguments incl_app_inv [A].
Implicit Arguments incl_cons_R [A].
Implicit Arguments incl_cons_cons [A].
Implicit Arguments incl_cons_inv_L [A].
Implicit Arguments incl_filter [A].
Implicit Arguments incl_filter_L [A].
Implicit Arguments incl_seq_filter_imp [A].
Fixpoint rep (A : Type) (a : A) (n : nat) {struct n} : list A :=
match n with
| O => nil
| S m => a :: rep _ a m
end.
Implicit Arguments rep [A].
Lemma len_rep : forall (A : Type) (a : A) n, length (rep a n) = n.
Implicit Arguments len_rep [A].
Lemma rep_plus : forall {A:Type} (a:A) k l, rep a (k + l) = rep a k ++ rep a l.
Lemma rep_last : forall {A:Type} (a:A) n, rep a (S n) = rep a n ++ a :: nil.
Lemma rev_rep : forall {A : Type} n (a : A), rev (rep a n) = rep a n.
Variable A : Type.
Lemma incl_nil_inv : forall (l : list A), incl l nil -> l = nil.
Lemma incl_singl : forall (a : A) l, In a l -> incl (a :: nil) l.
Lemma incl_app_inv : forall (l1 l2 : list A) k, incl (l1 ++ l2) k -> incl l1 k /\ incl l2 k.
Lemma incl_cons_R : forall (x : A) l1 l2, incl l1 l2 -> incl l1 (x :: l2).
Lemma incl_cons_cons : forall (l1 l2 : list A) x, incl l1 l2 -> incl (x :: l1) (x :: l2).
Lemma incl_cons_inv_L : forall a (l : list A) k, incl (a :: l) k -> In a k /\ incl l k.
Lemma incl_filter : forall (l1 l2 : list A), incl l1 l2 -> forall f, incl (filter f l1) (filter f l2).
Lemma incl_filter_L : forall (l1 l2 : list A), incl l1 l2 -> forall f, incl (filter f l1) l2.
Lemma incl_seq_filter_imp : forall (k : list A) (p p': A -> bool ),
(forall x, In x k -> p x -> p' x ) ->
incl (filter p k) (filter p' k).
End inclusion.
Implicit Arguments incl_nil_inv [A].
Implicit Arguments incl_singl [A].
Implicit Arguments incl_app_inv [A].
Implicit Arguments incl_cons_R [A].
Implicit Arguments incl_cons_cons [A].
Implicit Arguments incl_cons_inv_L [A].
Implicit Arguments incl_filter [A].
Implicit Arguments incl_filter_L [A].
Implicit Arguments incl_seq_filter_imp [A].
Fixpoint rep (A : Type) (a : A) (n : nat) {struct n} : list A :=
match n with
| O => nil
| S m => a :: rep _ a m
end.
Implicit Arguments rep [A].
Lemma len_rep : forall (A : Type) (a : A) n, length (rep a n) = n.
Implicit Arguments len_rep [A].
Lemma rep_plus : forall {A:Type} (a:A) k l, rep a (k + l) = rep a k ++ rep a l.
Lemma rep_last : forall {A:Type} (a:A) n, rep a (S n) = rep a n ++ a :: nil.
Lemma rev_rep : forall {A : Type} n (a : A), rev (rep a n) = rep a n.
inb
Section BPred.
Variable A : Type.
Variable A_def : A.
Variable eq_A : A -> A -> bool.
Variable eq_A_eq : forall n m, eq_A n m -> n = m.
Variable eq_A_refl : forall n, eq_A n n.
Fixpoint inb (a : A) (lst : list A) : bool :=
match lst with
| nil => false
| hd :: tl => orb (eq_A a hd) (inb a tl)
end.
Lemma In_inb_true : forall l e, inb e l = true <-> In e l.
Lemma In_inb_false : forall l e, inb e l = false <-> ~ In e l.
Lemma inb_nth : forall l n, inb n l = true ->
exists i, i < length l /\ nth i l A_def = n.
End BPred.
Implicit Arguments inb [A].
Implicit Arguments In_inb_true [A eq_A].
Implicit Arguments In_inb_false [A eq_A].
Implicit Arguments inb_nth [A eq_A].
intersection of two lists; see also Section disjointness in seq_ext.v
Section disjunction.
Variable A : Type.
Definition disj (l1 l2 : list A) :=
forall x, (In x l1 -> ~ (In x l2)) /\ (In x l2 -> ~ (In x l1)).
Lemma disj_nil_R : forall l, disj l nil.
Lemma disj_nil_L : forall l, disj nil l.
Lemma disj_singl : forall (a b : A), a <> b -> disj (a :: nil) (b :: nil).
Lemma disj_sym : forall h1 h2, disj h1 h2 -> disj h2 h1.
Lemma disj_not_In : forall (x : A) L K, disj K L -> In x L -> ~ In x K.
Lemma disj_cons_R : forall (x : A) L K, disj K L -> ~ In x K -> disj K (x :: L).
Lemma disj_cons_L : forall (x : A) L K, disj K L -> ~ In x L -> disj (x :: K) L.
Lemma disj_in_cons_R : forall (x:A) L K, disj K L -> In x L -> disj K (x :: L).
Lemma disj_cons_inv : forall (h : A) t1 l2, disj (h :: t1) l2 -> disj t1 l2 /\ ~ In h l2.
Lemma disj_app_inv : forall (l k m : list A), disj (l ++ k) m -> disj l m /\ disj k m.
Lemma disj_app : forall (l k m : list A), disj l m /\ disj k m -> disj (l ++ k) m.
Lemma disj_incl_L : forall (l : list A) k, disj l k ->
forall l', incl l' l -> disj l' k.
Lemma disj_incl_R : forall (l : list A) k, disj l k ->
forall k', incl k' k -> disj l k'.
Lemma disj_incl_LR : forall (k k' l l' : list A), disj k' l' ->
incl k k' -> incl l l' -> disj k l.
End disjunction.
Implicit Arguments disj [A].
Implicit Arguments disj_nil_R [A].
Implicit Arguments disj_nil_L [A].
Implicit Arguments disj_singl [A].
Implicit Arguments disj_sym [A].
Implicit Arguments disj_not_In [A].
Implicit Arguments disj_cons_R [A].
Implicit Arguments disj_cons_L [A].
Implicit Arguments disj_in_cons_R [A].
Implicit Arguments disj_cons_inv [A].
Implicit Arguments disj_app_inv [A].
Implicit Arguments disj_app [A].
Implicit Arguments disj_incl_L [A].
Implicit Arguments disj_incl_R [A].
Implicit Arguments disj_incl_LR [A].
Section List_seq_ext.
Local Open Scope nat_scope.
Lemma In_seq_inv : forall l n x, In x (seq n l) -> n <= x /\ x < n + l.
Lemma not_In_seq_inv : forall l n x, ~ In x (seq n l) -> x < n \/ n + l <= x.
Lemma In_seq : forall l n x, n <= x /\ x < n + l -> In x (seq n l).
Lemma incl_seq : forall a n b m, b <= a -> n + (a - b) <= m ->
incl (seq a n) (seq b m).
Lemma nth_seq : forall l m, m < l -> forall n, nth m (seq n l) O = n + m.
Lemma seq_app : forall l n, seq n l ++ (n + l) :: nil = seq n (S l).
Lemma seq_app2 : forall n a m, seq a (n + m) = seq a n ++ seq (a + n) m.
Local Close Scope nat_scope.
Local Open Scope Z_scope.
Lemma disj_seq_singl : forall x n l, Z_of_nat x < Z_of_nat n ->
disj (seq n l) (x :: nil).
Lemma disj_seq_singl2 : forall x n l, Z_of_nat n + Z_of_nat l <= Z_of_nat x ->
disj (seq n l) (x :: nil).
Lemma disj_seq_seq : forall a l b k, Z_of_nat a + Z_of_nat l <= Z_of_nat b ->
disj (seq a l) (seq b k).
Local Close Scope Z_scope.
End List_seq_ext.
An append function that removes doubles
add an element to a list only if not already include
Fixpoint add_set (a : A) (l : list A) {struct l} : list A :=
match l with
| nil => a :: nil
| hd :: tl => if eqb hd a then l else hd :: add_set a tl
end.
Lemma In_add_set_inv : forall l a b, In a (add_set b l) -> a = b \/ In a l.
Variable eqb_refl : forall a b, eqb a b -> a = b.
Lemma In_add_set_L : forall l a, In a (add_set a l).
Lemma In_add_set_R : forall l a b, In a l -> In a (add_set b l).
Lemma incl_add_set : forall k x, incl k (add_set x k).
match l with
| nil => a :: nil
| hd :: tl => if eqb hd a then l else hd :: add_set a tl
end.
Lemma In_add_set_inv : forall l a b, In a (add_set b l) -> a = b \/ In a l.
Variable eqb_refl : forall a b, eqb a b -> a = b.
Lemma In_add_set_L : forall l a, In a (add_set a l).
Lemma In_add_set_R : forall l a b, In a l -> In a (add_set b l).
Lemma incl_add_set : forall k x, incl k (add_set x k).
append two lists using the previous functions
(adding only the elements not already included)
Fixpoint app_set l1 l2 : list A :=
match l1 with
| nil => l2
| hd :: tl => app_set tl (add_set hd l2)
end.
Lemma in_app_set_or : forall l m a, In a (app_set l m) -> In a l \/ In a m.
Lemma in_or_app_set : forall l m a, In a l \/ In a m -> In a (app_set l m).
Lemma disj_app_set : forall l k m, disj (app_set l k) m -> disj l m /\ disj k m.
Lemma In_app_set_nil : forall l x, In x (app_set l nil) -> In x l.
Lemma disj_app_set_nil : forall l k, disj l k -> disj (app_set l nil) k.
Lemma incl_app_set_L : forall l1 l2, incl l1 (app_set l1 l2).
Lemma incl_app_set_R : forall l1 l2, incl l2 (app_set l1 l2).
Lemma incl_app_set : forall l1 l2 l3,
incl l1 l3 -> incl l2 l3 -> incl (app_set l1 l2) l3.
Variable eqb_xx : forall a, eqb a a.
Lemma NoDup_add_set : forall l a, NoDup l -> NoDup (add_set a l).
Lemma NoDup_app_set : forall a b, NoDup b -> NoDup (app_set a b).
End app_set_function.
Implicit Arguments add_set [A].
Implicit Arguments In_add_set_inv [A].
Implicit Arguments In_add_set_L [A].
Implicit Arguments In_add_set_R [A].
Implicit Arguments incl_add_set [A].
Implicit Arguments app_set [A].
Implicit Arguments in_app_set_or [A].
Implicit Arguments in_or_app_set [A].
Implicit Arguments disj_app_set [A].
Implicit Arguments In_app_set_nil [A].
Implicit Arguments disj_app_set_nil [A].
Implicit Arguments incl_app_set_L [A].
Implicit Arguments incl_app_set_R [A].
Implicit Arguments incl_app_set [A].
Implicit Arguments NoDup_add_set [A].
Implicit Arguments NoDup_app_set [A].
Section remove_ext.
Variable A : Type.
Variable eq_dec : forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}.
Implicit Type l: list A.
Lemma remove_In : forall l (e e' : A), In e l -> e' <> e ->
In e (remove eq_dec e' l).
Fixpoint remove_pred l (bpred : A -> bool) : list A :=
match l with
| nil => nil
| h :: t =>
match bpred h with
| true => remove_pred t bpred
| false => h :: remove_pred t bpred
end
end.
Lemma remove_pred_filter : forall (P : pred A) (l : list A),
remove_pred l P = filter (fun x => ~~ P x) l.
Lemma In_remove_pred : forall (P : A -> bool) l a,
In a (remove_pred l P) -> In a l /\ ~ P a.
match l1 with
| nil => l2
| hd :: tl => app_set tl (add_set hd l2)
end.
Lemma in_app_set_or : forall l m a, In a (app_set l m) -> In a l \/ In a m.
Lemma in_or_app_set : forall l m a, In a l \/ In a m -> In a (app_set l m).
Lemma disj_app_set : forall l k m, disj (app_set l k) m -> disj l m /\ disj k m.
Lemma In_app_set_nil : forall l x, In x (app_set l nil) -> In x l.
Lemma disj_app_set_nil : forall l k, disj l k -> disj (app_set l nil) k.
Lemma incl_app_set_L : forall l1 l2, incl l1 (app_set l1 l2).
Lemma incl_app_set_R : forall l1 l2, incl l2 (app_set l1 l2).
Lemma incl_app_set : forall l1 l2 l3,
incl l1 l3 -> incl l2 l3 -> incl (app_set l1 l2) l3.
Variable eqb_xx : forall a, eqb a a.
Lemma NoDup_add_set : forall l a, NoDup l -> NoDup (add_set a l).
Lemma NoDup_app_set : forall a b, NoDup b -> NoDup (app_set a b).
End app_set_function.
Implicit Arguments add_set [A].
Implicit Arguments In_add_set_inv [A].
Implicit Arguments In_add_set_L [A].
Implicit Arguments In_add_set_R [A].
Implicit Arguments incl_add_set [A].
Implicit Arguments app_set [A].
Implicit Arguments in_app_set_or [A].
Implicit Arguments in_or_app_set [A].
Implicit Arguments disj_app_set [A].
Implicit Arguments In_app_set_nil [A].
Implicit Arguments disj_app_set_nil [A].
Implicit Arguments incl_app_set_L [A].
Implicit Arguments incl_app_set_R [A].
Implicit Arguments incl_app_set [A].
Implicit Arguments NoDup_add_set [A].
Implicit Arguments NoDup_app_set [A].
Section remove_ext.
Variable A : Type.
Variable eq_dec : forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}.
Implicit Type l: list A.
Lemma remove_In : forall l (e e' : A), In e l -> e' <> e ->
In e (remove eq_dec e' l).
Fixpoint remove_pred l (bpred : A -> bool) : list A :=
match l with
| nil => nil
| h :: t =>
match bpred h with
| true => remove_pred t bpred
| false => h :: remove_pred t bpred
end
end.
Lemma remove_pred_filter : forall (P : pred A) (l : list A),
remove_pred l P = filter (fun x => ~~ P x) l.
Lemma In_remove_pred : forall (P : A -> bool) l a,
In a (remove_pred l P) -> In a l /\ ~ P a.
remove an element according to a predicate on its index
Fixpoint remove_idx l (P : nat -> bool) idx :=
match l with
| nil => nil
| hd :: tl =>
match P idx with
| true => remove_idx tl P (S idx)
| false => hd :: remove_idx tl P (S idx)
end
end.
match l with
| nil => nil
| hd :: tl =>
match P idx with
| true => remove_idx tl P (S idx)
| false => hd :: remove_idx tl P (S idx)
end
end.
remove only one occurrence of an element (the Coq standard library remove function removes all of them)
Fixpoint remove1 (a : A) l :=
match l with
| nil => nil
| h :: t => if eq_dec a h then t else h :: remove1 a t
end.
Lemma remove1_In : forall l e, In e l -> S (length (remove1 e l)) = length l.
Lemma remove1_In' : forall l e x, x <> e -> In x (remove1 e l) -> In x l.
End remove_ext.
Implicit Arguments remove_pred [A].
Implicit Arguments remove_pred_filter [A].
Implicit Arguments In_remove_pred [A].
Implicit Arguments remove_idx [A].
Implicit Arguments remove1 [A].
Ltac remove_head_from_tail HD TL :=
let ISDUP := In_list HD TL in
match ISDUP with
| false => constr: (HD :: TL)
| true =>
let POSITIONS := compute_positions1 TL HD O in
let NEW_TL := eval compute in (remove_idx TL (fun x => (inb beq_nat x POSITIONS)) O) in
let NEW_HDTL := eval compute in (app NEW_TL (HD :: List.nil)) in
constr : (NEW_HDTL)
end.
Ltac remove_duplicates LST :=
match LST with
| @List.cons ?A ?HD ?TL =>
let NEW_TL := remove_duplicates TL in
remove_head_from_tail HD NEW_TL
| @List.nil ?A => LST
end.
Lemma inb_remove_idx : forall (A : eqType) (h : A) t P i,
inb (fun x y : A => x == y) h (remove_idx t P i) ->
inb (fun x y : A => x == y) h t.
match l with
| nil => nil
| h :: t => if eq_dec a h then t else h :: remove1 a t
end.
Lemma remove1_In : forall l e, In e l -> S (length (remove1 e l)) = length l.
Lemma remove1_In' : forall l e x, x <> e -> In x (remove1 e l) -> In x l.
End remove_ext.
Implicit Arguments remove_pred [A].
Implicit Arguments remove_pred_filter [A].
Implicit Arguments In_remove_pred [A].
Implicit Arguments remove_idx [A].
Implicit Arguments remove1 [A].
Ltac remove_head_from_tail HD TL :=
let ISDUP := In_list HD TL in
match ISDUP with
| false => constr: (HD :: TL)
| true =>
let POSITIONS := compute_positions1 TL HD O in
let NEW_TL := eval compute in (remove_idx TL (fun x => (inb beq_nat x POSITIONS)) O) in
let NEW_HDTL := eval compute in (app NEW_TL (HD :: List.nil)) in
constr : (NEW_HDTL)
end.
Ltac remove_duplicates LST :=
match LST with
| @List.cons ?A ?HD ?TL =>
let NEW_TL := remove_duplicates TL in
remove_head_from_tail HD NEW_TL
| @List.nil ?A => LST
end.
Lemma inb_remove_idx : forall (A : eqType) (h : A) t P i,
inb (fun x y : A => x == y) h (remove_idx t P i) ->
inb (fun x y : A => x == y) h t.
Permutations
Section Permutation_ext.
Variable A : Type.
Implicit Type l : list A.
Lemma Permutation_notin : forall l l' x, Permutation l l' -> ~ In x l -> ~ In x l'.
Lemma permut_rotate : forall (a : A) l, Permutation (a :: l) (l ++ a :: nil).
Lemma Permutation_incl_L : forall l1 l2 k, Permutation l1 l2 -> incl l1 k -> incl l2 k.
Lemma Permutation_incl_R : forall l1 l2 k, Permutation l1 l2 -> incl k l1 -> incl k l2.
Lemma incl_refl_Permutation : forall l1 l2, Permutation l1 l2 -> incl l1 l2.
Lemma Permutation_app_cons : forall l l' e, Permutation (l ++ (e :: nil) ++ l') (e :: l ++ l').
Lemma Permutation_disj_L : forall k l m, Permutation m l -> disj m k -> disj l k.
Lemma Permutation_disj_R : forall k l m, Permutation m l -> disj k m -> disj k l.
Lemma Permutation_nth : forall def l k, Permutation k (seq O (length l)) ->
Permutation l (map (fun x => nth x l def) k).
Variable B : Type.
Definition Permutation_preserving (f : list A -> list B) :=
forall l1 l2 : list A, Permutation l1 l2 ->
Permutation (f l1) (f l2).
End Permutation_ext.
Implicit Arguments Permutation_notin [A].
Implicit Arguments permut_rotate [A].
Implicit Arguments Permutation_incl_L [A].
Implicit Arguments Permutation_incl_R [A].
Implicit Arguments Permutation_app_cons [A].
Implicit Arguments incl_refl_Permutation [A].
Implicit Arguments Permutation_disj_L [A].
Implicit Arguments Permutation_disj_R [A].
Implicit Arguments Permutation_nth [A].
Implicit Arguments Permutation_preserving [A B].
Lemma Permutation_seq_inv : forall (l : list nat) n, length l <> O ->
Permutation l (seq 0 (S n)) ->
exists l1, exists l2, l = l1 ++ (n :: nil) ++ l2 /\ Permutation (l1 ++ l2) (seq O n).
Ltac Permut n :=
match goal with
| |- (Permutation ?X1 ?X1) => apply Permutation_refl
| |- (Permutation (?X1 :: ?X2) (?X1 :: ?X3)) =>
let newn := eval compute in (length X2) in
(apply perm_skip; Permut newn)
| |- (Permutation (?X1 :: ?X2) ?X3) =>
match eval compute in n with
| 1 => fail
| _ =>
let l0' := constr:(X2 ++ X1 :: nil) in
(apply (@perm_trans _ (X1 :: X2) l0' X3);
[ apply permut_rotate | compute; Permut (Peano.pred n) ])
end
end.
Ltac PermutProve :=
match goal with
| |- (Permutation ?X1 ?X2) =>
match eval compute in (length X1 = length X2) with
| (?X1 = ?X1) => Permut X1
end
end.
Section fixpoint_permutation.
Variable A : Type.
Variable eq_dec : forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}.
Lemma Permutation_remove1 : forall h1 h h2,
Permutation (remove1 eq_dec h (h1 ++ h :: h2)) (h1 ++ h2).
Fixpoint fpermut (l k : list A) :=
match (l,k) with
| (nil, nil) => true
| (h :: t, h' :: t') =>
if eq_dec h h' then
fpermut t t'
else if In_dec eq_dec h t' then
fpermut t (h' :: remove1 eq_dec h t')
else
false
| _ => false
end.
Lemma function_permut_Permutation : forall n (l k : list A),
length l = n -> fpermut l k -> Permutation l k.
End fixpoint_permutation.
Implicit Arguments function_permut_Permutation [A].
Section nth_ext.
Variable A : Type.
Implicit Type l : list A.
Lemma nth_nil : forall n a, nth n (@nil A) a = a.
Lemma nth_last: forall l n a, n = length l -> nth n l a = a.
Lemma list_tail : forall def l, 0 < length l -> nth 0 l def :: tail l = l.
Lemma list_split : forall def n l, length l = n ->
forall j, j < n -> exists l1, length l1 = j /\
exists l2, l = l1 ++ nth j l def :: nil ++ l2.
Lemma list_last_nth : forall def n l, length l = n -> O < n ->
exists l1, l = l1 ++ nth (n - 1) l def :: nil.
Lemma In_nth : forall def l n, In n l -> exists i, i < length l /\ nth i l def = n.
End nth_ext.
Implicit Arguments list_split [A].
Implicit Arguments list_last_nth [A].
Section firstn_ext.
Variable A : Type.
Implicit Type l: list A.
Lemma len_firstn : forall n l k, length l = n -> k <= n -> length (firstn k l) = k.
Lemma firstn_all : forall l n, length l <= n -> firstn n l = l.
Lemma firstn_app_new : forall n l1, n <= length l1 ->
forall l2, firstn n (l1 ++ l2) = firstn n l1.
Lemma firstn_app : forall n l1, length l1 = n ->
forall l2, firstn n (l1 ++ l2) = l1.
Lemma firstn_S : forall def l i, i < length l ->
firstn (S i) l = firstn i l ++ nth i l def :: nil.
Lemma firstn_last : forall def l i, l <> nil ->
i = length l - 1 -> l = firstn i l ++ nth i l def :: nil.
Lemma firstn_firstn : forall l n m, firstn n (firstn m l) = firstn (Min.min n m) l.
Variable B : Type.
Lemma map_firstn_com : forall (f : A -> B) l i, map f (firstn i l) = firstn i (map f l).
End firstn_ext.
Implicit Arguments len_firstn [A].
Implicit Arguments firstn_all [A].
Implicit Arguments firstn_app_new [A].
Implicit Arguments firstn_app [A].
Implicit Arguments firstn_S [A].
Implicit Arguments firstn_last [A].
Implicit Arguments firstn_firstn [A].
Implicit Arguments map_firstn_com [A B].
Section skipn_ext.
Variable A : Type.
Implicit Type l: list A.
Lemma skipn_nil : forall n, skipn n (@nil A) = nil.
Lemma len_skipn : forall n l, length (skipn n l) = length l - n.
Lemma skipn_plus : forall a b l, skipn (a + b) l = skipn b (skipn a l).
Lemma skipn_all : forall n l, length l = n -> skipn n l = nil.
Lemma skipn_all_new : forall n l, length l <= n -> skipn n l = nil.
Lemma skipn_app' : forall n l l', length l = n ->
forall k, k <= n -> skipn k (l ++ l') = (skipn k l) ++ l'.
Lemma skipn_app : forall n l l', length l = n -> skipn n (l ++ l') = l'.
Lemma skipn_S : forall def l n, n < length l ->
skipn n l = nth n l def :: skipn (S n) l.
Lemma map_nth_len_skipn : forall def m l, m <= length l ->
l = map (fun x => nth x l def) (seq O m) ++ skipn m l.
Lemma skipn_nth : forall def l n, length l = S n -> skipn n l = nth n l def :: nil.
Lemma skipn_tail : forall n l, skipn (S n) l = tail (skipn n l).
Lemma skipn_inv : forall n l, l = skipn n l -> n <> O -> l = nil.
Lemma skipn_firstn : forall l n, skipn n (firstn n l) = nil.
Lemma skipn_firstn_plus : forall l n m,
firstn m (skipn n (firstn (n + m) l)) = firstn m (skipn n l).
Lemma skipn_nth_firstn : forall def n l, S n <= length l ->
l = firstn n l ++ nth n l def :: skipn (S n) l.
Lemma nth_firstn_skipn : forall def l n m, n + m < length l ->
firstn (S n) (skipn m l) = nth m l def :: firstn n (skipn (S m) l).
Variable B : Type.
Lemma length_skipn_same : forall l (k : list B) n,
length l = length k -> length (skipn n l) = length (skipn n k).
Lemma map_skipn_com : forall l (f : A -> B) i, map f (skipn i l) = skipn i (map f l).
End skipn_ext.
Implicit Arguments skipn_nil [A].
Implicit Arguments len_skipn [A].
Implicit Arguments skipn_plus [A].
Implicit Arguments skipn_all [A].
Implicit Arguments skipn_all_new [A].
Implicit Arguments skipn_app' [A].
Implicit Arguments skipn_app [A].
Implicit Arguments skipn_S [A].
Implicit Arguments map_nth_len_skipn [A].
Implicit Arguments skipn_nth [A].
Implicit Arguments skipn_tail [A].
Implicit Arguments skipn_inv [A].
Implicit Arguments skipn_firstn [A].
Implicit Arguments skipn_firstn_plus [A].
Implicit Arguments skipn_nth_firstn [A].
Implicit Arguments nth_firstn_skipn [A].
Implicit Arguments length_skipn_same [A B].
Implicit Arguments map_skipn_com [A B].
Section repeated_firstn.
Variable A : Type.
Fixpoint firstns' (k : nat) (n : nat) (l : list A) {struct n} : list (list A) :=
match n with
| O => nil
| S m => firstn k l :: firstns' k (m - (k - 1)) (skipn k l)
end.
Definition firstns (k : nat) (l : list A) : list (list A) :=
match k with
| O => nil
| S _ => firstns' k (length l) l
end.
Lemma firstns_nil : forall n, firstns n (@nil A) = nil.
Lemma firstns_skipn : forall n (l : list A) hd tl,
firstns n l = hd :: tl -> firstns n (skipn n l) = tl.
Lemma len_firstns' : forall n (l : list A), length l = n -> forall k q,
n = q * S k -> length (firstns' (S k) n l) = q.
Lemma len_firstns : forall n (l : list A), length l = n -> forall k q,
n = q * S k -> length (firstns (S k) l) = q.
Lemma In_firstns' : forall n (l : list A), length l = n -> forall k q,
(n = q * S k) -> forall x, In x (firstns (S k) l) -> length x = (S k).
Lemma In_firstns : forall n (l : list A), length l = n -> forall k q,
(n = q * k) -> forall x, In x (firstns k l) -> length x = k.
Lemma firstns_app : forall t (H : t <> O) (a b : list A), length a = t ->
firstns t (a ++ b) = a :: firstns t b.
End repeated_firstn.
Implicit Arguments firstns' [A].
Implicit Arguments firstns [A].
Implicit Arguments firstns_nil [A].
Implicit Arguments firstns_skipn [A].
Implicit Arguments len_firstns' [A].
Implicit Arguments In_firstns' [A].
Implicit Arguments In_firstns [A].
Implicit Arguments firstns_app [A].
Fixpoint split_n (A : Type) (l : list A) (n : nat) {struct n} : prod (list A) (list A) :=
match n with
| O => (nil, l)
| S m => match l with
| nil => (nil, nil)
| hd :: tl =>
let: (one, two) := split_n A tl m in
(hd :: one, two)
end
end.
Implicit Arguments split_n [A].
Lemma split_n_app : forall (A : Type) n (l k : list A),
length l = n ->
split_n (l ++ k) n = (l, k).
Section about_substitution.
Variable A : Type.
Lemma sub_substitution : forall n s0 s1, length (s0 ++ (n :: nil) ++ s1) = S n ->
(forall x, In x (s0 ++ s1) -> (x < n)) ->
forall (def e : A) l0 l1 k,
length (l0 ++ (e :: nil) ++ l1) = S n ->
length (k ++ e :: nil) = S n ->
length l0 = length s0 ->
(forall i, i < S n ->
nth i (l0 ++ (e :: nil) ++ l1) def = nth (nth i (s0 ++ (n :: nil) ++ s1) O) (k ++ e :: nil) def) ->
(forall i, i < n ->
nth i (l0 ++ l1) def = nth (nth i (s0 ++ s1) O) k def).
Lemma substitution_Permutation : forall n s, length s = n ->
Permutation s (seq O n) ->
forall (def : A) l k, length l = n -> length k = n ->
(forall i, i < n -> nth i l def = nth (nth i s O) k def) ->
Permutation l k.
End about_substitution.
delete the nth of lst (0 <= nth < length lst)
Section index_deletion.
Variable A : Type.
Fixpoint idel (n : nat) (l : list A) { struct l } : list A :=
match l with
| nil => nil
| hd :: tl => match n with
| O => tl
| S n' => hd :: idel n' tl
end
end.
Lemma len_idel : forall (lst : list A) (n : nat), n < length lst ->
length (idel n lst) = length lst - 1.
Definition idel_last (l : list A) : list A :=
match l with
| nil => nil
| _ => idel (length l - 1) l
end.
Lemma len_idel_last : forall n (l : list A), length l = n ->
length (idel_last l) = n - 1.
Lemma len_idel_last' : forall (lst : list A),
O < length lst -> length (idel_last lst) = length lst - 1.
Lemma idel_last_exact' : forall (l : list A) (a : A),
idel (length l) (l ++ a :: nil) = l.
Lemma idel_last_exact : forall (l : list A) a, idel_last (l ++ a :: nil) = l.
Lemma idel_app : forall k (l1 : list A), length l1 = k ->
forall l a l2, l = l1 ++ a :: l2 -> idel k l = l1 ++ l2.
End index_deletion.
Implicit Arguments idel [A].
Implicit Arguments idel_last [A].
Implicit Arguments len_idel_last [A].
Implicit Arguments idel_last_exact' [A].
Implicit Arguments idel_last_exact [A].
Implicit Arguments idel_app [A].
Variable A : Type.
Fixpoint idel (n : nat) (l : list A) { struct l } : list A :=
match l with
| nil => nil
| hd :: tl => match n with
| O => tl
| S n' => hd :: idel n' tl
end
end.
Lemma len_idel : forall (lst : list A) (n : nat), n < length lst ->
length (idel n lst) = length lst - 1.
Definition idel_last (l : list A) : list A :=
match l with
| nil => nil
| _ => idel (length l - 1) l
end.
Lemma len_idel_last : forall n (l : list A), length l = n ->
length (idel_last l) = n - 1.
Lemma len_idel_last' : forall (lst : list A),
O < length lst -> length (idel_last lst) = length lst - 1.
Lemma idel_last_exact' : forall (l : list A) (a : A),
idel (length l) (l ++ a :: nil) = l.
Lemma idel_last_exact : forall (l : list A) a, idel_last (l ++ a :: nil) = l.
Lemma idel_app : forall k (l1 : list A), length l1 = k ->
forall l a l2, l = l1 ++ a :: l2 -> idel k l = l1 ++ l2.
End index_deletion.
Implicit Arguments idel [A].
Implicit Arguments idel_last [A].
Implicit Arguments len_idel_last [A].
Implicit Arguments idel_last_exact' [A].
Implicit Arguments idel_last_exact [A].
Implicit Arguments idel_app [A].
delete the nth last elements of a list
Section del_last_n_section.
Variable A : Type.
Fixpoint del_last_n (n : nat) (l:list A) : list A :=
match n with
| O => l
| S n' => match l with
| nil => nil
| _ => del_last_n n' (idel_last l)
end
end.
Lemma len_del_last_n : forall m n (l : list A), length l = n -> m <= n ->
length (del_last_n m l) = n - m.
Lemma del_last_n_last : forall def n (l : list A),
length l = S n ->
del_last_n n l = hd def l :: nil.
End del_last_n_section.
Implicit Arguments del_last_n [A].
Implicit Arguments len_del_last_n [A].
Implicit Arguments del_last_n_last [A].
Variable A : Type.
Fixpoint del_last_n (n : nat) (l:list A) : list A :=
match n with
| O => l
| S n' => match l with
| nil => nil
| _ => del_last_n n' (idel_last l)
end
end.
Lemma len_del_last_n : forall m n (l : list A), length l = n -> m <= n ->
length (del_last_n m l) = n - m.
Lemma del_last_n_last : forall def n (l : list A),
length l = S n ->
del_last_n n l = hd def l :: nil.
End del_last_n_section.
Implicit Arguments del_last_n [A].
Implicit Arguments len_del_last_n [A].
Implicit Arguments del_last_n_last [A].
list update
Fixpoint update_list (A : Type) (l : list A) (n : nat) (v : A) {struct l} : list A :=
match l with
| nil => nil
| hd :: tl => match n with
| O => v :: tl
| S n' => hd :: update_list _ tl n' v
end
end.
Implicit Arguments update_list [A].
Lemma len_update_list : forall (A : Type) n (l : list A) k (v : A),
length l = n ->
length (update_list l k v) = n.
Implicit Arguments len_update_list [A].
Lemma update_list_out : forall (A : Type) n m (l : list A),
length l <= n ->
update_list l n m = l.
Implicit Arguments update_list_out [A].
Lemma nth_update_list : forall (A: Type) n (m:A) lst def_val,
n < length lst ->
nth n (update_list lst n m) def_val = m.
Lemma nth_update_list' : forall (A: Type) lst n n' (m:A) def_val,
n <> n' ->
nth n (update_list lst n' m) def_val = nth n lst def_val.
Lemma update_list_app : forall (A: Type) n lst (v:A),
length lst <= n -> forall lst',
update_list (lst++lst') n v = lst ++ (update_list lst' (n-length lst) v).
Lemma update_list_app' : forall (A: Type) n lst (v:A),
n < length lst -> forall lst',
update_list (lst++lst') n v = (update_list lst n v) ++ lst'.
Lemma idel_update_list : forall (A : Type) (lst : list A) k m,
idel k (update_list lst k m) = idel k lst.
Lemma skipn_update_list : forall (A:Type) (l:list A) n e m,
(n < m)%nat ->
skipn m (update_list l n e) = skipn m l.
Lemma firstn_update_list : forall (A: Type) lst n (m:A),
firstn n (update_list lst n m) = firstn n lst.
Lemma eqtype_is_comparable : forall (A : eqType) (x y : A), {x = y} + {x <> y}.
simple association lists
Section assoc.
Variable A : eqType.
Variable B : Type.
Implicit Type l : list (A * B).
Fixpoint assoc_get (a : A) (m : list (A * B)) : option B :=
match m with
| (a0, b) :: t => if a == a0 then Some b else assoc_get a t
| _ => None
end.
Lemma assoc_get_Some_inv : forall (l : list (A * B)) f v, assoc_get f l = Some v ->
exists n, n < length l /\ ith n l = Some (f, v).
Lemma In_exists_assoc_get : forall (l : list (A * B)) a, In a (uzip1 l) ->
exists b, assoc_get a l = Some b.
Lemma assoc_get_In : forall (l : list (A * B)) (a : A) (b : B),
assoc_get a l = Some b -> In (a, b) l.
Lemma assoc_get_In_uzip1 : forall l a (b : B), assoc_get a l = Some b -> In a (uzip1 l).
Definition assoc_del (x : A) (l : list (A * B)) : list (A * B) :=
remove_pred l (fun y => x == (fst y)).
Lemma assoc_del_cons_eq : forall l a (b : B), assoc_del a ((a, b) :: l) = assoc_del a l.
Lemma assoc_del_cons_neq : forall l y a (b : B), y != a ->
assoc_del y ((a, b) :: l) = (a, b) :: assoc_del y l.
Lemma assoc_get_assoc_del : forall (l : list (A*B)) x y, x != y ->
assoc_get x (assoc_del y l) = assoc_get x l.
Fixpoint assoc_upd (x : A) (v : B) (l : list (A * B)) : list (A * B) :=
match l with
| nil => (x, v) :: nil
| (h1, h2) :: t => if h1 == x then (h1, v) :: t else (h1, h2) :: assoc_upd x v t
end.
Lemma assoc_get_upd_neq : forall l x y v, x <> y ->
assoc_get x (assoc_upd y v l) = assoc_get x l.
Lemma assoc_get_upd_eq : forall l x v, assoc_get x (assoc_upd x v l) = Some v.
Lemma len_assoc_upd : forall s x v, In x (uzip1 s) ->
length (assoc_upd x v s) = length s.
End assoc.
Implicit Arguments assoc_get [A B].
Implicit Arguments In_exists_assoc_get [A B].
Implicit Arguments assoc_get_In [A B].
Implicit Arguments assoc_get_In_uzip1 [A B].
Implicit Arguments assoc_del [A B].
Implicit Arguments assoc_del_cons_eq [A B].
Implicit Arguments assoc_del_cons_neq [A B].
Implicit Arguments assoc_get_assoc_del [A B].
Implicit Arguments assoc_upd [A B].
Implicit Arguments assoc_get_upd_neq [A B].
Implicit Arguments assoc_get_upd_eq [A B].
Implicit Arguments len_assoc_upd [A B].
Section find_index.
Variable A : eqType.
Implicit Type l : list A.
Fixpoint ifind' (a : A) l (idx : nat) : option nat :=
match l with
| nil => None
| hd :: tl => if a == hd then Some idx else ifind' a tl (S idx)
end.
Definition ifind a l := ifind' a l O.
Lemma ifind'_idx : forall l a idx n, ifind' a l idx = Some n -> idx <= n.
Lemma ifind'_slide : forall l k a i,
ifind' a l (S i) = Some (S k) -> ifind' a l i = Some k.
Lemma ifind'_cons_Some_inv : forall l k a idx,
ifind' a l idx = Some (idx + k) ->
forall n, n <= k -> ifind' a (skipn n l) idx = Some (idx + k - n).
Lemma ifind'_ith : forall l f idx n, ifind' f l idx = Some n ->
ith (n - idx) l = Some f.
Lemma ifind_ith : forall l f n, ifind f l = Some n -> ith n l = Some f.
Lemma ifind'_exists_ith : forall (B : Type) l (l' : list B) (f : A) (n : nat),
length l = length l' ->
forall idx, ifind' f l idx = Some n -> exists f', ith (n - idx) l' = Some f'.
Lemma ifind_exists_ith : forall (B : Type) l (l' : list B) (f : A) (n : nat),
length l = length l' -> ifind f l = Some n -> exists f', ith n l' = Some f'.
Lemma assoc_get_ifind' : forall (B : Type) (l : list (A * B)) f v i,
assoc_get f l = Some v ->
exists idx, ifind' f (uzip1 l) i = Some idx.
Lemma assoc_get_ifind : forall (B : Type) (l : list (A * B)) f v,
assoc_get f l = Some v ->
exists idx, ifind f (uzip1 l) = Some idx.
Lemma ifind'_ith_assoc_get : forall {B : Type} (l : list (A * B)) f i v idx,
ifind' f (uzip1 l) idx = Some i -> ith (i - idx) (uzip2 l) = Some v ->
assoc_get f l = Some v.
Lemma ifind_ith_assoc_get : forall {B : Type} (l : list (A * B)) f i v,
ifind f (uzip1 l) = Some i -> ith i (uzip2 l) = Some v ->
assoc_get f l = Some v.
Lemma ifind'_assoc_get : forall (B : Type) (l : list (A * B)) (f : A) (i : nat) idx,
ifind' f (uzip1 l) idx = Some i -> exists b, assoc_get f l = Some b.
Lemma ifind_assoc_get : forall (B : Type) (l : list (A * B)) (f : A) (i : nat),
ifind f (uzip1 l) = Some i -> exists b, assoc_get f l = Some b.
Lemma ifind'_assoc_get_ith : forall (B : Type)
(l : list (A * B)) (f : A) (i : nat) (v : B) idx,
ifind' f (uzip1 l) idx = Some i -> assoc_get f l = Some v ->
ith (i - idx) (uzip2 l) = Some v.
Lemma ifind_assoc_get_ith : forall (B : Type) (l : list (A * B)) (f : A) (i : nat) (v : B),
ifind f (uzip1 l) = Some i -> assoc_get f l = Some v ->
ith (i) (uzip2 l) = Some v.
Lemma ifind'_slide2 : forall l k a i,
ifind' a l i = Some k -> ifind' a l (S i) = Some (S k).
Lemma ifind_cons : forall l x h i, x <> h ->
ifind x l = Some i -> ifind x (h :: l) = Some (S i).
Lemma ifind_lt : forall l a i, ifind a l = Some i -> i < length l.
End find_index.
Implicit Arguments ifind [A].
Implicit Arguments ifind'_slide [A].
Implicit Arguments ifind'_cons_Some_inv [A].
Implicit Arguments assoc_get_ifind [A B].
Implicit Arguments ifind_ith_assoc_get [A B].
Implicit Arguments ifind_assoc_get [A B].
Implicit Arguments ifind_assoc_get_ith [A B].
Implicit Arguments ifind'_slide2 [A].
Implicit Arguments ifind_cons [A].
Implicit Arguments ifind_lt [A].
Definition iplus l := List.fold_right plus O l.
Lemma iplus_ext : forall n l l', length l = n -> length l' = n ->
(forall i x x', ith i l = Some x -> ith i l' = Some x' -> x = x') ->
iplus l = iplus l'.
Lemma lt_iplus_0 : forall l, l <> nil -> (exists x, List.In x l /\ 0 < x) -> 0 < iplus l.
Lemma iplus_app : forall a b, iplus (a ++ b) = iplus a + iplus b.
Variable A : eqType.
Variable B : Type.
Implicit Type l : list (A * B).
Fixpoint assoc_get (a : A) (m : list (A * B)) : option B :=
match m with
| (a0, b) :: t => if a == a0 then Some b else assoc_get a t
| _ => None
end.
Lemma assoc_get_Some_inv : forall (l : list (A * B)) f v, assoc_get f l = Some v ->
exists n, n < length l /\ ith n l = Some (f, v).
Lemma In_exists_assoc_get : forall (l : list (A * B)) a, In a (uzip1 l) ->
exists b, assoc_get a l = Some b.
Lemma assoc_get_In : forall (l : list (A * B)) (a : A) (b : B),
assoc_get a l = Some b -> In (a, b) l.
Lemma assoc_get_In_uzip1 : forall l a (b : B), assoc_get a l = Some b -> In a (uzip1 l).
Definition assoc_del (x : A) (l : list (A * B)) : list (A * B) :=
remove_pred l (fun y => x == (fst y)).
Lemma assoc_del_cons_eq : forall l a (b : B), assoc_del a ((a, b) :: l) = assoc_del a l.
Lemma assoc_del_cons_neq : forall l y a (b : B), y != a ->
assoc_del y ((a, b) :: l) = (a, b) :: assoc_del y l.
Lemma assoc_get_assoc_del : forall (l : list (A*B)) x y, x != y ->
assoc_get x (assoc_del y l) = assoc_get x l.
Fixpoint assoc_upd (x : A) (v : B) (l : list (A * B)) : list (A * B) :=
match l with
| nil => (x, v) :: nil
| (h1, h2) :: t => if h1 == x then (h1, v) :: t else (h1, h2) :: assoc_upd x v t
end.
Lemma assoc_get_upd_neq : forall l x y v, x <> y ->
assoc_get x (assoc_upd y v l) = assoc_get x l.
Lemma assoc_get_upd_eq : forall l x v, assoc_get x (assoc_upd x v l) = Some v.
Lemma len_assoc_upd : forall s x v, In x (uzip1 s) ->
length (assoc_upd x v s) = length s.
End assoc.
Implicit Arguments assoc_get [A B].
Implicit Arguments In_exists_assoc_get [A B].
Implicit Arguments assoc_get_In [A B].
Implicit Arguments assoc_get_In_uzip1 [A B].
Implicit Arguments assoc_del [A B].
Implicit Arguments assoc_del_cons_eq [A B].
Implicit Arguments assoc_del_cons_neq [A B].
Implicit Arguments assoc_get_assoc_del [A B].
Implicit Arguments assoc_upd [A B].
Implicit Arguments assoc_get_upd_neq [A B].
Implicit Arguments assoc_get_upd_eq [A B].
Implicit Arguments len_assoc_upd [A B].
Section find_index.
Variable A : eqType.
Implicit Type l : list A.
Fixpoint ifind' (a : A) l (idx : nat) : option nat :=
match l with
| nil => None
| hd :: tl => if a == hd then Some idx else ifind' a tl (S idx)
end.
Definition ifind a l := ifind' a l O.
Lemma ifind'_idx : forall l a idx n, ifind' a l idx = Some n -> idx <= n.
Lemma ifind'_slide : forall l k a i,
ifind' a l (S i) = Some (S k) -> ifind' a l i = Some k.
Lemma ifind'_cons_Some_inv : forall l k a idx,
ifind' a l idx = Some (idx + k) ->
forall n, n <= k -> ifind' a (skipn n l) idx = Some (idx + k - n).
Lemma ifind'_ith : forall l f idx n, ifind' f l idx = Some n ->
ith (n - idx) l = Some f.
Lemma ifind_ith : forall l f n, ifind f l = Some n -> ith n l = Some f.
Lemma ifind'_exists_ith : forall (B : Type) l (l' : list B) (f : A) (n : nat),
length l = length l' ->
forall idx, ifind' f l idx = Some n -> exists f', ith (n - idx) l' = Some f'.
Lemma ifind_exists_ith : forall (B : Type) l (l' : list B) (f : A) (n : nat),
length l = length l' -> ifind f l = Some n -> exists f', ith n l' = Some f'.
Lemma assoc_get_ifind' : forall (B : Type) (l : list (A * B)) f v i,
assoc_get f l = Some v ->
exists idx, ifind' f (uzip1 l) i = Some idx.
Lemma assoc_get_ifind : forall (B : Type) (l : list (A * B)) f v,
assoc_get f l = Some v ->
exists idx, ifind f (uzip1 l) = Some idx.
Lemma ifind'_ith_assoc_get : forall {B : Type} (l : list (A * B)) f i v idx,
ifind' f (uzip1 l) idx = Some i -> ith (i - idx) (uzip2 l) = Some v ->
assoc_get f l = Some v.
Lemma ifind_ith_assoc_get : forall {B : Type} (l : list (A * B)) f i v,
ifind f (uzip1 l) = Some i -> ith i (uzip2 l) = Some v ->
assoc_get f l = Some v.
Lemma ifind'_assoc_get : forall (B : Type) (l : list (A * B)) (f : A) (i : nat) idx,
ifind' f (uzip1 l) idx = Some i -> exists b, assoc_get f l = Some b.
Lemma ifind_assoc_get : forall (B : Type) (l : list (A * B)) (f : A) (i : nat),
ifind f (uzip1 l) = Some i -> exists b, assoc_get f l = Some b.
Lemma ifind'_assoc_get_ith : forall (B : Type)
(l : list (A * B)) (f : A) (i : nat) (v : B) idx,
ifind' f (uzip1 l) idx = Some i -> assoc_get f l = Some v ->
ith (i - idx) (uzip2 l) = Some v.
Lemma ifind_assoc_get_ith : forall (B : Type) (l : list (A * B)) (f : A) (i : nat) (v : B),
ifind f (uzip1 l) = Some i -> assoc_get f l = Some v ->
ith (i) (uzip2 l) = Some v.
Lemma ifind'_slide2 : forall l k a i,
ifind' a l i = Some k -> ifind' a l (S i) = Some (S k).
Lemma ifind_cons : forall l x h i, x <> h ->
ifind x l = Some i -> ifind x (h :: l) = Some (S i).
Lemma ifind_lt : forall l a i, ifind a l = Some i -> i < length l.
End find_index.
Implicit Arguments ifind [A].
Implicit Arguments ifind'_slide [A].
Implicit Arguments ifind'_cons_Some_inv [A].
Implicit Arguments assoc_get_ifind [A B].
Implicit Arguments ifind_ith_assoc_get [A B].
Implicit Arguments ifind_assoc_get [A B].
Implicit Arguments ifind_assoc_get_ith [A B].
Implicit Arguments ifind'_slide2 [A].
Implicit Arguments ifind_cons [A].
Implicit Arguments ifind_lt [A].
Definition iplus l := List.fold_right plus O l.
Lemma iplus_ext : forall n l l', length l = n -> length l' = n ->
(forall i x x', ith i l = Some x -> ith i l' = Some x' -> x = x') ->
iplus l = iplus l'.
Lemma lt_iplus_0 : forall l, l <> nil -> (exists x, List.In x l /\ 0 < x) -> 0 < iplus l.
Lemma iplus_app : forall a b, iplus (a ++ b) = iplus a + iplus b.