Require Export List.
Require Export Arith.
Require Export Permutation.

Lemma gt_neq : forall x y:nat, y < x -> x <> y.

Lemma lt_neq : forall x y:nat, x < y -> x <> y.

Lemma plus_minus_S_S : forall n m p, p + S n - S m = p + n - m.

Lemma minus_S : forall n m, n - S m = n - m - 1.

Definition sign (n:nat) :=
  match n with
  | O => 0
  | S _ => 1
  end.

Lemma sign_mon : forall i j, i <= j -> sign i <= sign j.

Lemma sign_lt : forall i j, sign i < sign j -> i < j.

Lemma nat_compare_eq_rev : forall n, nat_compare n n = Eq.

Lemma nat_compare_sym_lt : forall m n, nat_compare m n = Lt -> nat_compare n m = Gt.

Lemma nat_compare_sym_gt : forall m n, nat_compare m n = Gt -> nat_compare n m = Lt.

Lemma nat_compare_trans : forall m n o, nat_compare m n = Lt -> nat_compare n o = Lt ->
                                        nat_compare m o = Lt.

Lemma nil_length : forall A, forall l:list A, length l = 0 -> l = nil.

Lemma is_nil_dec : forall A, forall l:list A, {l=nil}+{l<>nil}.

Theorem list_length_induction : forall A, forall P:list A -> Prop,
        P nil ->
        (forall n, (forall l, length l = n -> P l) ->
                   (forall l, length l = (S n) -> P l)) ->
        forall l, P l.

Lemma all_in_dec : forall A B:Type, forall B_dec : (forall x y:B, {x=y}+{x<>y}),
                   forall f:A->B, forall l l',
                      {forall x, In x l -> In (f x) l'} +
                        {~(forall x, In x l -> In (f x) l')}.

Lemma ext_map : forall (A B : Type)(f g:A->B), forall l, map f l = map g l ->
                forall a, In a l -> f a = g a.

Lemma nth_ok_length : forall A, forall l:list A, forall n x,
      n < length l -> nth_ok n l x = true.

Lemma length_nth_ok : forall A, forall l:list A, forall n x,
      nth_ok n l x = true -> n < length l.

Fixpoint change (n:nat) (A:Type) (l:list A) (x:A) : list A :=
    match n, l with
      | O, nil => nil
      | O, y :: l' => x :: l'
      | S m, nil => nil
      | S m, y :: l' => y :: change m A l' x
    end.

Lemma change_len : forall n A l x, length (change n A l x) = length l.

Lemma change_In : forall n A l x y, In y (change n A l x) -> (x = y) \/ In y l.

Lemma change_nth_k : forall A x n a l, n < length l ->
                       nth n (change n A l x) a = x.

Lemma change_nth_neq : forall A:Type, forall x:A, forall k n a l,
                       n < length l -> k <> n ->
                       nth k (change n A l x) a = nth k l a.

Lemma list_eq : forall P Q, length P = length Q ->
               (forall i x, i < length P -> nth (A:=nat) i P x = nth i Q x) ->
                P = Q.

Theorem nth_In_Prop : forall A, forall P:A -> Prop, forall l, forall k:nat,
                      k < length l -> (forall x, In x l -> P x) ->
                      forall a, P (nth k l a).

Lemma In_char : forall A, (forall x y:A, {x=y} + {x<>y}) -> forall l:list A,
                          forall x y, In x l -> {i | i < length l & nth i l y = x}.

Lemma In_suff : forall A, (forall x y:A, {x=y} + {x<>y}) -> forall l:list A,
                          forall x y i, i < length l -> nth i l y = x -> In x l.

Lemma map_in : forall A B, forall f:A->B, forall l y,
                           In y (map f l) -> exists x, f x = y /\ In x l.

Section Remove.

Variable A:Type.
Hypothesis A_dec : forall x y:A, {x=y} + {x <> y}.

Lemma remove_app : forall l l' x,
                   remove A_dec x (l++l') = remove A_dec x l ++ remove A_dec x l'.

Lemma remove_not_in : forall l x, ~In x l -> remove A_dec x l = l.

Lemma in_remove : forall l x y, In x l -> x <> y -> In x (remove A_dec y l).

Lemma remove_out : forall l x y, ~(In x l) -> ~(In x (remove A_dec y l)).

Lemma remove_In_neq : forall l x y, In x (remove A_dec y l) -> In x l.

Lemma remove_length : forall l x, length (remove A_dec x l) <= length l.

Lemma remove_length_In : forall l x, In x l ->
                                     length (remove A_dec x l) < length l.

Lemma count_length : forall l x, count_occ A_dec l x <= length l.

Lemma count_remove : forall l x y, x <> y -> count_occ A_dec l x =
                                             count_occ A_dec (remove A_dec y l) x.

Lemma remove_count_length : forall l x, length (remove A_dec x l) =
                                        length l - count_occ A_dec l x.

Lemma count_occ_zero : forall l x, ~In x l -> count_occ A_dec l x = 0.

Lemma zero_count : forall l x, count_occ A_dec l x = 0 -> ~In x l.

Lemma Permutation_NoDup : forall A, forall P Q: list A, Permutation P Q ->
                                                        NoDup P -> NoDup Q.

Lemma NoDup_dec : forall l:list A, {NoDup l} + {~NoDup l}.

Lemma NoDup_remove : forall l a, NoDup l -> NoDup (remove A_dec a l).

Lemma NoDup_append : forall l, forall a:A, NoDup (a::l) -> NoDup (l ++ a :: nil).

Lemma NoDup_char_1 : forall l:list A,
                    (forall i j x, i < length l -> j < length l ->
                                   i<>j -> nth i l x <> nth j l x) -> NoDup l.

Lemma NoDup_char_2 : forall l:list A, NoDup l ->
                     forall i j x, i < length l -> j < length l ->
                                   i<>j -> nth i l x <> nth j l x.

Lemma NoDup_char_3 : forall l:list A, NoDup l ->
                     forall i j x, i < length l -> j < length l ->
                                   nth i l x = nth j l x -> i=j.

Lemma NoDup_count : forall l x, NoDup l -> In x l -> count_occ A_dec l x = 1.

Lemma count_NoDup : forall l, (forall x, count_occ A_dec l x <= 1) -> NoDup l.

Lemma NoDup_count_length_le : forall l: list A, NoDup l ->
                              forall l', (forall x, In x l -> In x l') ->
                                          length l <= length l'.

Lemma NoDup_count_length_lt : forall l: list A, NoDup l ->
                              forall l', (forall x, In x l -> In x l') ->
                              forall y, count_occ A_dec l' y > 1 ->
                                        length l < length l'.

Lemma NoDup_count_occ : forall l x, NoDup l -> count_occ A_dec l x <= 1.

Lemma NoDup_lemma : forall l l':list A, length l = length l' -> NoDup l ->
                               (forall x, In x l -> In x l') -> NoDup l'.

Lemma NoDup_app : forall l l':list A, NoDup l -> NoDup l' ->
                 (forall x, In x l -> ~In x l') -> NoDup (l++l').

End Remove.

Section FindAndRemove.

Variable A:Type.
Hypothesis A_dec : forall x y:A, {x = y} + {x <> y}.

Fixpoint remove_fst (x:A) (l:list A) : list A :=
  match l with
  | nil => nil
  | y :: l' => match (A_dec x y) with
               | left _ => l'
               | right _ => y :: remove_fst x l'
               end
  end.

Lemma remove_fst_NoDup : forall l, NoDup l -> forall x, remove_fst x l = remove A_dec x l.

Lemma remove_fst_not_In : forall l x, ~In x l -> remove_fst x l = remove A_dec x l.

Lemma remove_fst_length_In : forall l x, In x l ->
                             length (remove_fst x l) < length l.

Fixpoint find_and_remove (a b:bool) (l:list A) (x y:A)
  : bool * bool * (list A) :=
  match (a,b,l) with
  | (true,true,_) => (true,true,l)
  | (_,_,nil) => (a,b,nil)
  | (false,true,z::l') => match (A_dec x z) with
      | left _ => (true,true,z::l')
      | right _ => let (t1,t2) := find_and_remove a b l' x y
                   in (t1,z::t2)
      end
  | (true,false,z::l') => match (A_dec y z) with
          | left _ => (true,true,l')
          | right _ => let (t1,t2) := find_and_remove a b l' x y
                       in (t1,z::t2)
          end
  | (false,false,z::l') => match (A_dec x z) with
      | left _ => let (t1,t2) := find_and_remove true b l' x y
                  in (t1,z::t2)
      | right _ => match (A_dec y z) with
          | left _ => find_and_remove a true l' x y
          | right _ => let (t1,t2) := find_and_remove a b l' x y
                       in (t1,z::t2)
          end
      end
  end.

Lemma find_and_remove_true_true : forall l x y, find_and_remove true true l x y = (true,true,l).

Lemma find_and_remove_1_true : forall l b x y, fst (fst (find_and_remove true b l x y)) = true.

Lemma find_and_remove_1 : forall l a b x y,
      fst (fst (find_and_remove a b l x y)) = false -> ~In x l.

Lemma find_and_remove_1a : forall l b x y,
      fst (fst (find_and_remove false b l x y)) = true -> In x l.

Lemma find_and_remove_2_true : forall l a x y, snd (fst (find_and_remove a true l x y)) = true.

Lemma find_and_remove_2 : forall l a b x y, x <> y ->
      snd (fst (find_and_remove a b l x y)) = false -> ~In y l.

Lemma find_and_remove_2a : forall l a x y,
      snd (fst (find_and_remove a false l x y)) = true -> In y l.

Lemma find_and_remove_3a : forall l a x y,
      snd (find_and_remove a true l x y) = l.

Lemma find_and_remove_3b : forall l a x y, x <> y ->
      snd (find_and_remove a false l x y) = remove_fst y l.

Lemma find_and_remove_not_in : forall l a b x y, x <> y -> ~In y l ->
      snd (find_and_remove a b l x y) = l.

Lemma find_and_remove_3c : forall l a x y, x <> y ->
  NoDup l ->
  snd (find_and_remove a false l x y) = remove A_dec y l.

Lemma find_and_remove_le : forall l l' a a' b b' x y,
      find_and_remove a b l x y = (a',b',l') -> length l' <= length l.

Lemma find_and_remove_smaller : forall l l' x y a a',
      find_and_remove a false l x y = (a',true,l') -> length l' < length l.

End FindAndRemove.

Section Split.

Variable A:Type.
Variable A_dec : forall x y : A, {x = y} + {x <> y}.

Fixpoint split (x:A) (l:list A) : list A * list A :=
  match l with
  | nil => (nil,nil)
  | y :: l' => match A_dec x y with
               | left _ => (nil,l')
               | right _ => let (w,w') := (split x l')
                            in (y :: w, w')
               end
  end.

Lemma split_char_in : forall x l, In x l -> forall w w', split x l = (w,w') ->
                      w ++ w' = remove_fst A A_dec x l.

Lemma split_char_out : forall x l, ~In x l -> split x l = (l,nil).

Lemma split_length_1 : forall x l, In x l ->
                       forall w w', split x l = (w,w') -> length w < length l.

Lemma split_length_2 : forall x l, In x l ->
                       forall w w', split x l = (w,w') -> length w' < length l.

Lemma In_split : forall x l y, x <> y ->
                 forall w w', split x l = (w,w') -> In y l -> In y (w++w').

End Split.


Section RemoveAll.

Variable A:Type.
Variable A_dec : forall x y : A, {x = y} + {x <> y}.

Fixpoint remove_all (l w:list A) :=
  match l with
  | nil => w
  | x :: l' => match w with
            | nil => nil
            | y::w' => match (A_dec x y) with
                       | left _ => remove_all l' w'
                       | right _ => y :: remove_all l w'
                       end
            end
  end.

Lemma remove_all_length_le : forall l w, length (remove_all l w) <= length w.

Lemma remove_all_length_lt : forall x l w, In x w -> length (remove_all (x::l) w) < length w.

Lemma remove_all_in : forall l w x, In x (remove_all l w) -> In x w.

Lemma remove_all_nil : forall l, remove_all l nil = nil.

Lemma remove_all_NoDup : forall l w, NoDup w -> NoDup (remove_all l w).

Lemma remove_all_not_in : forall l w x, In x w -> ~In x (remove_all l w) -> In x l.

End RemoveAll.