Library Exercise_3_3_1_5

Require Import Utf8.
Require Import Common Graph.

Set Implicit Arguments.

Generalizable All Variables.


Section Exercise_3_3_1_5.


Let V be a set. Suppose we just draw the elements of V as vertices and have no arrows between them. Is this a graph?
Given V, is there any other ``canonical'' or somehow automatic non-random procedure for generating a graph with those vertices?

  Variable V : Type.

  Local Open Scope type_scope.

  Definition ConstantGraph (E : Type) : Graph
    := {| Vertex := V;
          Edge := (fun _ _ E) |}.

  Definition ExtendedConstantGraph (E_same E_diff : Type) : Graph
    := {| Vertex := V;
          Edge := (fun s d ((s = d) × E_same) + ((s d) × E_diff)) |}.
  Definition DiscreteGraph := ConstantGraph .
  Definition CompleteGraph := ExtendedConstantGraph unit.
End Exercise_3_3_1_5.