Contribution: GraphBasics

Library GraphBasics.Trees

Require Export Acyclic.
Require Export Connected.

Section TREE.

Inductive Tree : V_set -> A_set -> Set :=
| T_root : forall r : Vertex, Tree (V_single r) A_empty
| T_leaf :
forall (v : V_set) (a : A_set) (t : Tree v a) (f n : Vertex),
v n -> ~ v f -> Tree (V_union (V_single f) v) (A_union (E_set n f) a)
| T_eq :
forall (v v' : V_set) (a a' : A_set),
v = v' -> a = a' -> Tree v a -> Tree v' a'.

Lemma Tree_isa_graph : forall (v : V_set) (a : A_set), Tree v a -> Graph v a.
Proof.
intros v a t; elim t; intros.
apply G_eq with (v := V_union (V_single r) V_empty) (a := A_empty).
rewrite V_union_commut; apply V_union_neutral.

trivial.

apply G_vertex.
apply G_empty.

compute in |- *. tauto.

apply G_edge.
apply G_vertex; trivial.

apply V_in_right; trivial.

apply V_in_left; apply V_in_single.

red in |- *; intros He; elim n0.
rewrite <- He; trivial.

red in |- *; intro; elim n0; apply (G_ina_inv2 v0 a0 H n f); trivial.

red in |- *; intro; elim n0; apply (G_ina_inv1 v0 a0 H f n); trivial.

apply G_eq with (v := v0) (a := a0); trivial.
Defined.

Lemma Tree_isa_connected :
forall (v : V_set) (a : A_set), Tree v a -> Connected v a.
Proof.
intros v a t; elim t; intros.
apply C_isolated.

apply C_leaf; auto.

apply C_eq with (v := v0) (a := a0); trivial.
Qed.

Lemma Tree_isa_acyclic :
forall (v : V_set) (a : A_set), Tree v a -> Acyclic v a.
Proof.
intros v a t; elim t; intros.
apply AC_eq with (v := V_union (V_single r) V_empty) (a := A_empty).
rewrite V_union_commut; apply V_union_neutral.

trivial.

apply AC_vertex.
apply AC_empty.

compute in |- *. tauto.

apply AC_leaf; auto.

apply AC_eq with (v := v0) (a := a0); trivial.
Qed.

End TREE.

Section CONNECTED_AND_ACYCLIC.

Lemma Acyclic_connected_isa_tree :
forall (v : V_set) (a : A_set), Acyclic v a -> Connected v a -> Tree v a.
Proof.
intros v a ac; elim ac; intros.
elim (Connected_not_empty _ _ H); auto.

apply T_eq with (v := V_single x) (a := A_empty).
symmetry in |- *; apply (C_minus_isolated_left _ _ H0 x).
apply V_in_left; apply V_in_single.

intros; red in |- *; intros; elim n.
apply (AC_ina_inv1 _ _ _ _ ac0 H1).

symmetry in |- *; apply (C_minus_isolated_right _ _ H0 x).
apply V_in_left; apply V_in_single.

intros; red in |- *; intros; elim n.
apply (AC_ina_inv1 _ _ _ _ ac0 H1).

apply T_root.

apply T_leaf.
apply H.
apply (C_minus_pendant _ _ H0 x y).
apply V_in_right; trivial.

apply V_in_left; apply V_in_single.

intros.
inversion H1.
inversion H2; trivial.

elim n; apply (AC_ina_inv1 _ _ y z ac0 H2).

trivial.

trivial.

red in |- *; intros H1; elim n; apply (AC_ina_inv2 _ _ x y ac0 H1).

red in |- *; intros H1; elim n; apply (AC_ina_inv1 _ _ y x ac0 H1).

trivial.

trivial.

trivial.

apply T_eq with (v := v0) (a := a0).
trivial.

trivial.

apply H; apply C_eq with (v := v') (a := a'); auto.
Qed.

End CONNECTED_AND_ACYCLIC.