The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

If I'm reading it right that lemma says for any point x and any n, there is a path of length n between x and root. This seems unlikely to be true.

You might want something like

forall x, v x -> {el : A_list & Connection x root el (distance x)}

for path_to_root, which says that for any point x there is a path of length (distance x) between x and root.

Then you can modify it to

forall n, forall x, v x -> distance x = n -> {el : A_list & Connection x root el n }

and then you can do induction on n.

Additional remarks:

I'm not familiar with this library but it seems like it would be cleaner to have (g : Graph v a) and (propRoot : v root) as section variables.

In the definition of Connection, why is the inductive argument to step [Connection y z el (S n)] and not [Connection y z el n]? Doesn't this make it impossible to define any Connection of nonzero length?

The parent_exists axiom is strange, I would have expected something like forall c, v c -> v (parent c).

Gaëtan Gilbert

On 05/09/2016 17:50, Samira Akili wrote:

Hi everyone,

we are using the graph library GraphBasics and want to show that if some self-defined properties are true for all vertices of a graph the resulting graph is a tree.
First, we want to show the connectivity by proving that there is a path between any vertex and the root by induction over the pathlength, which is descibed by the following lemma.
Lemma path_to_root_inductive: forall (g : Graph v a)(x :Component)(prop1: v x) (prop2: v root)(n:nat),
{el : A_list & Connection x root el n}.

We use these axioms and definitions:
Definition Component := Vertex.
Variable v: U_Set Component. Variable a: A_set. Variable root: Component.
Definition distance: Component -> nat. Axiom distance_root : distance root = 0. Axiom distance_prop : forall (c:Component)(a:A_set)(v:V_set)(g: Graph v a) (prop :v c), c <>root -> distance c = distance (parent c) + 1.
Definition parent : Component -> Component. Axiom parent_root := parent root = root. Axiom parent_exists : forall (c :Component)(g: Graph v a)(prop: v c),
exists (k: Component), v k -> parent c = k.
(*Connection is an undirected path consisting of edges that are induced by the parent relation, each path has its that has a length*)
Inductive Connection:  Component -> Component -> A_list -> nat -> Set :=   | self : forall x:Vertex,  v x -> Connection x x  A_nil 0   | step : forall (x y z : Vertex)(el : A_list)(n:nat),            Connection y z el (S n) -> v x  -> parent x = y
          -> a (A_ends x (parent x))  -> a (A_ends (parent x) x)
          -> ~ In (A_ends x (parent x))  el -> ~ In (A_ends (parent x) x)  el           -> Connection x z ((A_ends (parent x) x ) :: el) (S(S n)).

We try to prove the lemma path_to_root_inductive by induction over n. Our induction hypothesis looks like this:
IHn : {el : A_list & Connection x root el n}
and our goal like this
{el : A_list & Connection x root el (S n)}
What we need instead is an induction hypothesis that looks like this:
IHn : {el : A_list & Connection y root el n} with (y = parent x)

How can we change the induction scheme to fit our purpose?