Require Import Datatypes.
Require Import Bool.Bool.
Require Import Coq.Arith.Arith_base.
Require Import Coq.Lists.List.

Definition set := list nat.

Open Scope list_scope.

Fixpoint member (n : nat) (l : list nat) : bool :=
   match l with
     | nil => false
     | x :: xs => match beq_nat x n with
                     | true => true
                     | false => member n xs
                  end
   end.

Fixpoint check (s : set) : bool :=
   match s with
     | nil => true
     | x :: xs => andb (negb (member x xs)) (check xs)
   end.

Fixpoint union (s1 s2 : set) : set :=
   match s1 with
     | nil => s2
     | x :: xs => match member x s2 with
                    | true => union xs s2
                    | false => x :: (union xs s2)
                  end
   end.

Fixpoint intersection (s1 s2 : set) : set :=
   match s1 with
     | nil => nil
     | x :: xs => match member x s2 with
                     | true => x :: intersection xs s2
                     | false => intersection xs s2
                  end
   end.
Fixpoint difference (s1 s2 : set) : set :=
   match s1 with
     | nil => nil
     | x :: xs => match member x s2 with
                     | true => difference xs s2
                     | false => x :: difference xs s2
                  end
   end.

Fixpoint cardinality (s : set) : nat :=
   match s with
     | nil => O
     | _ :: xs => S (cardinality xs)
   end.

Fixpoint ble_nat (n1 n2 : nat) : bool :=
   match n1 with
     | O => true
     | S n1' => match n2 with
                  | O => false
                  | S n2' => ble_nat n1' n2'
                end
   end.

Lemma union_empty_r : forall (s : set), union s nil = s.
Proof.
  intros s.
  induction s. reflexivity.
  simpl. f_equal. apply IHs.
Qed.

Lemma ble_nat_refl : forall n, ble_nat n n = true.
Proof.
  intros n.
  induction n. reflexivity. simpl. rewrite IHn. reflexivity.
Qed.

Theorem union_card_l : forall (s1 s2 : set), ble_nat (cardinality s1) (cardinality (union s1 s2)) = true.
Proof.
Admitted.