Lists

In the end, every theorem boils down to a property of lists. This is not always true, but often enough. I need a lot of definitions, that are not in the Coq library, most notably, a partial nth and every_nth. I also need a lot of additional results on the definitions in the standard library, for instance about firstn, skipn and In.
Note that a lot of list material is in different files for modularization and better compilation speed. See the files reorder, list_set, list_support, assoc, list_multiset, some_nth and some_neg.

Require Export misc sets.

Section Lists0.
  Variable A : Type.

misc stuff


  Lemma append_single_rev : (a : A)(l : list A), a :: l = [a] ++ l.

nonempty lists


  Definition nonempty_list(l : list A) : Prop :=
    match l with
      | []False
      | _True
    end.

  Lemma nonempty_list_tcc :
    (X : Type), nonempty_list []X.

firstn lemmas



  Lemma length_firstn_less : (l : list A)(n : nat),
    n length llength (firstn n l) = n.

  Lemma firstn_whole : (l : list A)(n : nat),
    n length lfirstn n l = l.

  Lemma firstn_append_left : (l1 l2 : list A)(n : nat),
    n length l1firstn n (l1 ++ l2) = firstn n l1.

  Lemma firstn_append_right : (l1 l2 : list A)(n : nat),
    n length l1firstn n (l1 ++ l2) = l1 ++ (firstn (n - length l1) l2).

  Lemma firstn_firstn_less :
    (l : list A)(n1 n2 : nat),
      n1 n2
      n2 length l
        firstn n1 (firstn n2 l) = firstn n1 l.

  Lemma map_firstn : (B : Type)(f : AB)(l : list A)(n : nat),
    map f (firstn n l) = firstn n (map f l).

skipn lemmas



  Lemma length_skipn : (l : list A)(n : nat),
    length (skipn n l) = length l - n.

  Lemma skipn_whole : (l : list A)(n : nat),
    n length lskipn n l = [].

  Lemma skipn_append_left : (l1 l2 : list A)(n : nat),
    n length l1skipn n (l1 ++ l2) = (skipn n l1) ++ l2.

  Lemma skipn_append_right : (l1 l2 : list A)(n : nat),
    n length l1skipn n (l1 ++ l2) = skipn (n - length l1) l2.

  Lemma skipn_skipn : (l : list A)(n1 n2 : nat),
    skipn n1 (skipn n2 l) = skipn (n1 + n2) l.

  Lemma skipn_firstn : (l : list A)(n1 n2 : nat),
    n1 n2
    n2 length l
      skipn n1 (firstn n2 l) = firstn (n2 - n1) (skipn n1 l).

  Lemma map_skipn : (B : Type)(f : AB)(l : list A)(n : nat),
    map f (skipn n l) = skipn n (map f l).

End Lists0.

Section Lists1.

  Variable A : Type.

cutout_nth


   Definition cutout_nth{A : Type}(l : list A)(n : nat) : list A :=
     (firstn n l) ++ (skipn (1 + n) l).

   Lemma cutout_nth_cons_0 :
     (a : A)(l : list A), cutout_nth (a :: l) 0 = l.

   Lemma cutout_nth_cons_succ : (a : A)(l : list A)(n : nat),
     cutout_nth (a :: l) (S n) = a :: cutout_nth l n.

   Lemma map_cutout_nth :
     {A B : Type}(f : AB)(l : list A)(n : nat),
       map f (cutout_nth l n) = cutout_nth (map f l) n.

forallb


  Lemma forallb_cons : (f : Abool)(a : A)(l : list A),
    forallb f (a :: l) = true ((f a = true) forallb f l = true).

combine


   Lemma in_combine_same : (l : list A)(a b : A),
     In (a, b) (combine l l) → a = b In a l.

partition


  Lemma partition_result : (f : Abool)(l : list A),
    forallb f (fst (partition f l)) = true
    forallb (fun anegb (f a)) (snd (partition f l)) = true.

NoDup


  Lemma NoDup_tail : (a : A)(l : list A),
    NoDup (a :: l) → NoDup l.

  Lemma NoDup_head : (a : A)(l : list A),
    NoDup (a :: l) → ¬ In a l.

  Lemma NoDup_map : (B : Type)(f : AB)(l : list A),
    ((a1 a2 : A), In a1 lIn a2 lf a1 = f a2a1 = a2) →
    NoDup l
      NoDup (map f l).

  Lemma NoDup_map_injective : (B : Type)(f : AB)(l : list A),
    injective f
    NoDup l
      NoDup (map f l).


nth as partial function


  Lemma nth_0_nil_tcc :
    (n : nat)(inside : n < length (@nil A))(X : Type), X.

  Lemma nth_succ_tcc : (n : nat)(a : A)(l : list A),
    S n < length (a :: l) → n < length l.

  Fixpoint nth(l : list A)(n : nat)(inside : n < length l) : A :=
    match l return n < length lA with
      | []fun(H : n < length []) ⇒ nth_0_nil_tcc n H _
      | a :: rfun(H : n < length (a :: r)) ⇒
        match n return n < length (a :: r) → A with
          | 0 ⇒ fun _a
          | S pfun(H0 : S p < length (a :: r)) ⇒
              nth r p (nth_succ_tcc p a r H0)
        end H
    end inside.

  Lemma nth_tail :
    (a : A)(l : list A)(n : nat)(n_less : S n < length (a :: l)),
      nth (a :: l) (S n) n_less = nth l n (nth_succ_tcc _ _ _ n_less).

  Lemma nth_tcc_irr :
    (l : list A)(n : nat)(inside_1 inside_2 : n < length l),
      nth l n inside_1 = nth l n inside_2.

  Lemma list_equal_nth_char : (l1 l2 : list A),
    length l1 = length l2
    ((n : nat)(n1_less : n < length l1)(n2_less : n < length l2),
               nth l1 n n1_less = nth l2 n n2_less) →
      l1 = l2.

  Lemma nth_head_tcc : (l : list A), length l = 1 → 0 < length l.

  Lemma nth_append_left :
    (l1 l2 : list A)(n : nat)
          (n_less_app : n < length (l1 ++ l2))
          (n_less_l1 : n < length l1),
      nth (l1 ++ l2) n n_less_app = nth l1 n n_less_l1.

  Lemma nth_append_right_tcc : (l1 l2 : list A)(n : nat),
    n < length(l1 ++ l2) → n length l1n - length l1 < length l2.

  Lemma nth_append_right_ind :
    (l1 l2 : list A)(n : nat)
          (n_less : n < length(l1 ++ l2))(n_greater : n length l1)
          (n_min_less : n - length l1 < length l2),
      nth (l1 ++ l2) n n_less = nth l2 (n - length l1) n_min_less.

  Lemma nth_append_right :
    (l1 l2 : list A)(n : nat)
          (n_less : n < length(l1 ++ l2))(n_greater : n length l1),
      nth (l1 ++ l2) n n_less =
        nth l2 (n - length l1) (nth_append_right_tcc l1 l2 n n_less n_greater).

  Lemma nth_firstn_tcc : (l : list A)(n1 n2 : nat),
    n2 < length (firstn n1 l) → n2 < n1n2 < length l.

  Lemma nth_firstn :
    (l : list A)(n1 n2 : nat)
          (n2_less_firstn : n2 < length (firstn n1 l))(n2_less_n1 : n2 < n1),
      nth (firstn n1 l) n2 n2_less_firstn =
        nth l n2 (nth_firstn_tcc l n1 n2 n2_less_firstn n2_less_n1).

  Lemma nth_skipn_tcc :
    (l : list A)(n1 n2 : nat),
      n1 length ln2 < length (skipn n1 l) → n1 + n2 < length l.

  Lemma nth_skipn :
    (l : list A)(n1 n2 : nat)
          (n1_less : n1 length l)(n2_less : n2 < length (skipn n1 l)),
      nth (skipn n1 l) n2 n2_less =
        nth l (n1 + n2) (nth_skipn_tcc l n1 n2 n1_less n2_less).

  Lemma cons_nth_skipn :
    (l : list A)(n : nat)(inside : n < length l),
      (nth l n inside) :: (skipn (1 + n) l) = (skipn n l).

  Lemma list_split_at_n :
    (l : list A)(n : nat)(n_less : n < length l),
      l = (firstn n l) ++ (nth l n n_less) :: (skipn (1 + n) l).

  Lemma list_split_n_equal :
    (l : list A)(a : A)(n : nat)(n_less : n < length l),
      nth l n n_less = a
        (firstn n l) ++ a :: (skipn (1 + n) l) = l.

  Lemma list_split_at_n2 :
    (l : list A)(n1 n2 : nat)
          (n1_less : n1 < length l)(n2_less : n2 < length l),
      n1 n2
        (ll lm lr : list A)(al ar : A),
          l = ll ++ al :: lm ++ ar :: lr
          ((al = nth l n1 n1_less ar = nth l n2 n2_less)
           (al = nth l n2 n2_less ar = nth l n1 n1_less)).

End Lists1.

Implicit Arguments nonempty_list [A].
Implicit Arguments nonempty_list_tcc [A X].
Implicit Arguments length_firstn_less [A].
Implicit Arguments firstn_whole [A].
Implicit Arguments skipn_whole [A].
Implicit Arguments cutout_nth [A].
Implicit Arguments partition_result [A].
Implicit Arguments NoDup_tail [A].
Implicit Arguments nth_0_nil_tcc [A].
Implicit Arguments nth_succ_tcc [A].
Implicit Arguments nth [A].
Implicit Arguments nth_tcc_irr [A].
Implicit Arguments nth_head_tcc [A].
Implicit Arguments nth_append_left [A].
Implicit Arguments nth_append_right_tcc [A].
Implicit Arguments nth_append_right [A].
Implicit Arguments nth_skipn [A].
Implicit Arguments list_split_n_equal [A].
Implicit Arguments list_split_at_n2 [A].

Section Lists2.
  Variable A : Type.

  Lemma nth_map_tcc :
    (B : Type)(f : AB)(l : list A)(n : nat)
          (n_less_map : n < length (map f l)),
      n < length l.

  Lemma nth_map :
    (B : Type)(f : AB)(l : list A)(n : nat)
          (n_less_map : n < length (map f l)),
      nth (map f l) n n_less_map = f (nth l n (nth_map_tcc B f l n n_less_map)).

  Lemma nth_map_inv_tcc :
    (B : Type)(f : AB)(l : list A)(n : nat)(n_less : n < length l),
      n < length (map f l).

  Lemma nth_map_inv :
    (B : Type)(f : AB)(l : list A)(n : nat)(n_less : n < length l),
      f (nth l n n_less) = nth (map f l) n (nth_map_inv_tcc _ f _ _ n_less).

flatten


  Fixpoint flatten(ll : list (list A)) : list A :=
    match ll with
      | [][]
      | l :: lll ++ (flatten ll)
    end.

  Lemma flatten_append : (ll1 ll2 : list (list A)),
    flatten (ll1 ++ ll2) = (flatten ll1) ++ (flatten ll2).

  Lemma flatten_map_singleton_id : (l : list A),
     flatten (map (fun(a : A) ⇒ [a]) l) = l.

member


  Fixpoint member(a_eq : eq_type A)(a : A)(l : list A) : bool :=
    match l with
      | []false
      | b :: lif a_eq a b then true else member a_eq a l
    end.

  Lemma member_In : (a_eq : eq_type A)(a : A)(l : list A),
    member a_eq a l = true In a l.

  Lemma member_In_false : (a_eq : eq_type A)(a : A)(l : list A),
    member a_eq a l = false ¬ In a l.

  Lemma member_append : (a_eq : eq_type A)(a : A)(l1 l2 : list A),
    member a_eq a (l1 ++ l2) = true
      member a_eq a l1 = true member a_eq a l2 = true.

  Lemma member_append_left :
    (a_eq : eq_type A)(a : A)(l1 l2 : list A),
      member a_eq a l1 = true
        member a_eq a (l1 ++ l2) = true.

  Lemma member_append_right :
    (a_eq : eq_type A)(a : A)(l1 l2 : list A),
      member a_eq a l2 = true
        member a_eq a (l1 ++ l2) = true.



  Lemma In_flatten :
    (ll : list (list A))(a : A),
      In a (flatten ll) →
        (n : nat), n_less # n < length ll /#\
          In a (nth ll n n_less).

In


  Lemma in_map_reverse :
    {B : Type}(f : AB)(l : list A)(a2 : A),
      ((a1 : A), In a1 lf a1 = f a2a1 = a2) →
      In (f a2) (map f l) →
        In a2 l.

  Lemma In_nth :
    (a : A)(l : list A),
      In a l
        (n : nat), n_less # n < length l /#\ nth l n n_less = a.

  Lemma In_nth_rev :
    (a : A)(l : list A)(n : nat)(n_less : n < length l),
      a = nth l n n_less
        In a l.

End Lists2.

Implicit Arguments In_flatten [A].

Section Lists3.

  Variable A : Type.

every via nth


  Definition every_nth(P : AProp)(l : list A) : Prop :=
    (n : nat)(n_less : n < length l), P (nth l n n_less).

  Lemma every_nth_empty : (P : AProp),
    every_nth P [].

  Lemma every_nth_mono : (P Q : set A)(l : list A),
    subset P Qevery_nth P levery_nth Q l.

  Lemma every_nth_head : (P : AProp)(a : A)(l : list A),
    every_nth P (a :: l) → P a.

  Lemma every_nth_tail : (P : AProp)(a : A)(l : list A),
    every_nth P (a :: l) → every_nth P l.

  Lemma every_nth_cons : (P : AProp)(a : A)(l : list A),
    P aevery_nth P levery_nth P (a :: l).

  Lemma every_nth_append : (P : AProp)(l1 l2 : list A),
    every_nth P l1every_nth P l2every_nth P (l1 ++ l2).

  Lemma every_nth_append_left : (P : AProp)(l1 l2 : list A),
    every_nth P (l1 ++ l2) → every_nth P l1.

  Lemma every_nth_append_right : (P : AProp)(l1 l2 : list A),
    every_nth P (l1 ++ l2) → every_nth P l2.

  Lemma every_nth_In : (P : AProp)(l : list A)(a : A),
    every_nth P lIn a lP a.

  Lemma every_nth_In_rev : (P : AProp)(l : list A),
    ((a : A), In a lP a) →
       every_nth P l.

  Lemma forallb_every_nth : (f : Abool)(l : list A),
    forallb f l = true every_nth (fun af a = true) l.

  Lemma every_nth_cutout_nth : (P : AProp)(l : list A)(n : nat),
    every_nth P levery_nth P (cutout_nth l n).

map


  Lemma map_id : (l : list A), map id l = l.

  Lemma restricted_map_ext :
    (B : Type)(f g : AB)(l : list A),
      (every_nth (fun(a : A) ⇒ f a = g a) l) →
        map f l = map g l.

remove


  Lemma length_remove :
    (a_eq : eq_type A)(a : A)(l : list A),
      length (remove a_eq a l) length l.

  Lemma length_remove_In :
    (a_eq : eq_type A)(a : A)(l : list A),
      In a l
        length (remove a_eq a l) < length l.

  Lemma In_remove_other :
    (a_eq : eq_type A)(a1 a2 : A)(l : list A),
      In a1 l
      a1 a2
        In a1 (remove a_eq a2 l).

seq


  Lemma nth_seq :
    (n l i : nat)(i_less : i < length (seq n l)),
      nth (seq n l) i i_less = n + i.

  Lemma NoDup_seq : (n len : nat), NoDup (seq n len).

nat list sum


  Fixpoint nat_list_sum(l : list nat) : nat :=
    match l with
      | [] ⇒ 0
      | n :: ln + (nat_list_sum l)
    end.

  Lemma nat_list_sum_append : (l1 l2 : list nat),
    nat_list_sum(l1 ++ l2) = (nat_list_sum l1) + (nat_list_sum l2).

nat maximum


  Fixpoint nat_list_max(l : list nat) : nat :=
    match l with
      | [] ⇒ 0
      | n :: lmax n (nat_list_max l)
    end.


  Lemma nat_list_max_pairwise_le :
    (l1 l2 : list nat)(len_eq : length l1 = length l2),
      ((n : nat)(n_less : n < length l1),
         nth l1 n n_less nth l2 n (eq_rect (length l1) (fun mn < m)
                                              n_less (length l2) len_eq))
      → nat_list_max l1 nat_list_max l2.

list search


  Fixpoint list_search(l : list A)(count : nat)(pred : Abool)
                                                               : option nat :=
    match l with
      | []None
      | a :: r
        if pred a then Some count
        else list_search r (1 + count) pred
    end.

  Lemma list_search_none :
    (l : list A)(count : nat)(pred : Abool)
          (n : nat)(n_less : n < length l),
      list_search l count pred = None
        pred (nth l n n_less) = false.

  Lemma list_search_some_ind :
    (l : list A)(count : nat)(test : Abool)(n : nat),
      list_search l count test = Some n
        n count
        n_less # (n - count < length l) /#\
            test (nth l (n - count) n_less) = true.

  Lemma list_search_some :
    (l : list A)(test : Abool)(n : nat),
      list_search l 0 test = Some n
        n_less # n < length l /#\
            test (nth l n n_less) = true.

  Lemma list_search_some_less :
    (l : list A)(test : Abool)(n : nat),
      list_search l 0 test = Some n
        n < length l.

  Lemma list_search_some_test :
    (l : list A)(test : Abool)(n : nat)
          (H : list_search l 0 test = Some n),
      test (nth l n (list_search_some_less l test n H)) = true.

swap list of pairs


  Definition swap_pairs(B : Type)(l : list (A × B)) : list (B × A) :=
    map swap_pair l.

End Lists3.

Implicit Arguments nth_map_tcc [A B].
Implicit Arguments nth_map [A B].
Implicit Arguments flatten [A].
Implicit Arguments member [A].
Implicit Arguments member_In [A].
Implicit Arguments member_append [A].
Implicit Arguments in_map_reverse [A B].
Implicit Arguments every_nth [A].
Implicit Arguments every_nth_empty [A].
Implicit Arguments every_nth_mono [A].
Implicit Arguments every_nth_cons [A].
Implicit Arguments every_nth_head [A].
Implicit Arguments every_nth_tail [A].
Implicit Arguments every_nth_In [A].
Implicit Arguments list_split_at_n [A].
Implicit Arguments list_search [A].
Implicit Arguments list_search_some [A].
Implicit Arguments list_search_none [A].
Implicit Arguments list_search_some_less [A].
Implicit Arguments list_search_some_test [A].
Implicit Arguments swap_pairs [A B].

Lemma every_nth_map :
  (A B : Type)(P : BProp)(f : AB)(l : list A),
    every_nth P (map f l) every_nth (fun(a : A) ⇒ P (f a)) l.

Lemma nat_list_max_le : (l : list nat)(n : nat),
  every_nth (fun(m : nat) ⇒ m n) lnat_list_max l n.

Lemma nat_list_max_le_inv : (l : list nat)(n : nat),
  nat_list_max l nevery_nth (fun(m : nat) ⇒ m n) l.

Lemma nat_list_max_lub : (l : list nat),
  every_nth (fun(n : nat) ⇒ n nat_list_max l) l.

Lemma fold_left_map :
  {X Y Z : Type}(f : XY)(g : ZYZ)(l : list X)(z : Z),
    fold_left g (map f l) z = fold_left (fun z xg z (f x)) l z.