Contribution: GraphBasics

# Library GraphBasics.Enumerated

Require Export Sets.
Require Export List.

Section ENUMERATION.

Variable U : Set.

Hypothesis U_separable : forall x y : U, {x = y} + {x <> y}.

Definition U_list := list U.

Definition U_enumerable (E : U_set U) :=
{ul : U_list | forall x : U, E x -> In x ul}.

Inductive U_canon : U_list -> Prop :=
| U_canon_nil : U_canon nil
| U_canon_cons :
forall (x : U) (ul : U_list),
U_canon ul -> ~ In x ul -> U_canon (x :: ul).

Lemma U_in_dec : forall (x : U) (ul : U_list), {In x ul} + {~ In x ul}.
Proof.
simple induction ul; intros.
right; red in |- *; intros; inversion H.

case (U_separable x a); intros.
left; rewrite e; simpl in |- *; auto.

case H; intros.
left; simpl in |- *; auto.

right; red in |- *; intros; inversion H0.
elim n; auto.

elim n0; auto.
Qed.

Variable f : U -> nat.

Fixpoint U_sum (ul : U_list) : nat :=
match ul with
| nil => 0
| x :: ul' => f x + U_sum ul'
end.

Lemma U_enumerable_sum : forall E : U_set U, U_enumerable E -> nat.
Proof.
intros; elim H; intros.
apply (U_sum x).
Defined.

End ENUMERATION.