Require Export misc sets.

Section Lists0.
  Variable A : Type.

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

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

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

  Lemma length_firstn_less : ∀(l : list A)(n : nat),
    n ≤ length l → length (firstn n l) = n.

  Lemma firstn_whole : ∀(l : list A)(n : nat),
    n ≥ length l → firstn n l = l.

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

  Lemma firstn_append_right : ∀(l1 l2 : list A)(n : nat),
    n ≥ length l1 → firstn 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 : A → B)(l : list A)(n : nat),
    map f (firstn n l) = firstn n (map f l).

  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 l → skipn n l = [].

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

  Lemma skipn_append_right : ∀(l1 l2 : list A)(n : nat),
    n ≥ length l1 → skipn 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 : A → B)(l : list A)(n : nat),
    map f (skipn n l) = skipn n (map f l).

End Lists0.

Section Lists1.

  Variable A : Type.

   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 : A → B)(l : list A)(n : nat),
       map f (cutout_nth l n) = cutout_nth (map f l) n.

  Lemma forallb_cons : ∀(f : A → bool)(a : A)(l : list A),
    forallb f (a :: l) = true ↔ ((f a = true) ∧ forallb f l = true).

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

  Lemma partition_result : ∀(f : A → bool)(l : list A),
    forallb f (fst (partition f l)) = true ∧
    forallb (fun a ⇒ negb (f a)) (snd (partition f l)) = true.

  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 : A → B)(l : list A),
    (∀(a1 a2 : A), In a1 l → In a2 l → f a1 = f a2 → a1 = a2) →
    NoDup l →
      NoDup (map f l).

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

  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 l → A with
      | [] ⇒ fun(H : n < length []) ⇒ nth_0_nil_tcc n H _
      | a :: r ⇒ fun(H : n < length (a :: r)) ⇒
        match n return n < length (a :: r) → A with
          | 0 ⇒ fun _ ⇒ a
          | S p ⇒ fun(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 l1 → n - 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 < n1 → n2 < 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 l → n2 < 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 : A → B)(l : list A)(n : nat)
          (n_less_map : n < length (map f l)),
      n < length l.

  Lemma nth_map :
    ∀(B : Type)(f : A → B)(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 : A → B)(l : list A)(n : nat)(n_less : n < length l),
      n < length (map f l).

  Lemma nth_map_inv :
    ∀(B : Type)(f : A → B)(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).

  Fixpoint flatten(ll : list (list A)) : list A :=
    match ll with
      | [] ⇒ []
      | l :: ll ⇒ l ++ (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.

  Fixpoint member(a_eq : eq_type A)(a : A)(l : list A) : bool :=
    match l with
      | [] ⇒ false
      | b :: l ⇒ if 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).

  Lemma in_map_reverse :
    ∀{B : Type}(f : A → B)(l : list A)(a2 : A),
      (∀(a1 : A), In a1 l → f a1 = f a2 → a1 = 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.

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

  Lemma every_nth_empty : ∀(P : A → Prop),
    every_nth P [].

  Lemma every_nth_mono : ∀(P Q : set A)(l : list A),
    subset P Q → every_nth P l → every_nth Q l.

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

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

  Lemma every_nth_cons : ∀(P : A → Prop)(a : A)(l : list A),
    P a → every_nth P l → every_nth P (a :: l).

  Lemma every_nth_append : ∀(P : A → Prop)(l1 l2 : list A),
    every_nth P l1 → every_nth P l2 → every_nth P (l1 ++ l2).

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

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

  Lemma every_nth_In : ∀(P : A → Prop)(l : list A)(a : A),
    every_nth P l → In a l → P a.

  Lemma every_nth_In_rev : ∀(P : A → Prop)(l : list A),
    (∀(a : A), In a l → P a) →
       every_nth P l.

  Lemma forallb_every_nth : ∀(f : A → bool)(l : list A),
    forallb f l = true ↔ every_nth (fun a ⇒ f a = true) l.

  Lemma every_nth_cutout_nth : ∀(P : A → Prop)(l : list A)(n : nat),
    every_nth P l → every_nth P (cutout_nth l n).

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

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

  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).

  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).

  Fixpoint nat_list_sum(l : list nat) : nat :=
    match l with
      | [] ⇒ 0
      | n :: l ⇒ n + (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).

  Fixpoint nat_list_max(l : list nat) : nat :=
    match l with
      | [] ⇒ 0
      | n :: l ⇒ max 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 m ⇒ n < m)
                                              n_less (length l2) len_eq))
      → nat_list_max l1 ≤ nat_list_max l2.

  Fixpoint list_search(l : list A)(count : nat)(pred : A → bool)
                                                               : 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 : A → bool)
          (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 : A → bool)(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 : A → bool)(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 : A → bool)(n : nat),
      list_search l 0 test = Some n →
        n < length l.

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

  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 : B → Prop)(f : A → B)(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) l → nat_list_max l ≤ n.

Lemma nat_list_max_le_inv : ∀(l : list nat)(n : nat),
  nat_list_max l ≤ n → every_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 : X → Y)(g : Z → Y → Z)(l : list X)(z : Z),
    fold_left g (map f l) z = fold_left (fun z x ⇒ g z (f x)) l z.