Library Basic

Require Export List.
Require Export Arith.
Require Export ZArith.

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

Lemma compare_Lt_dec : forall C, {C = Lt} + {C <> Lt}.

Lemma compare_Gt_dec : forall C, {C = Gt} + {C <> Gt}.

Lemma compare_Eq_dec : forall C, {C = Eq} + {C <> Eq}.

End Compare.

Section NatCompare.

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.

End NatCompare.

Section Z_stuff.

Open Scope Z_scope.

Lemma Zabs_le_1 : forall z, Z.abs z <= 1 ->
  {z = 0} + {z = 1} + {z = -1}.
Lemma Zabs_diff_le_1 : forall z z', Z.abs (z - z') <= 1 ->
  {z = z'} + {z = z' + 1} + {z' = z + 1}.

End Z_stuff.

Section RemoveAll.

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

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

Lemma remove_not_In : forall y l, ~(In y l) -> remove A_dec y l = l.

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

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

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

Lemma remove_all_orig : forall l w x,
  In x w -> In x l \/ In x (remove_all l w).

End RemoveAll.


Definition list_subset (A:Type) (l1 l2:list A) := forall x, In x l1 -> In x l2.