The Coq mailing list

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

You need to do the induction before the intros. Consider this simplified example:

Goal forall m n, m = S n -> n < m.

intros m;induction m;intros n H. Focus 2.

(*
m : nat
IHm : forall n : nat, m = S n -> n < m (******* Good ********)
n : nat
H : S m = S n
______________________________________(1/1)
n < S m *)

Abort.

Goal forall m n, m = S n -> n < m.

intros m n H;induction m. Focus 2.

(*
m, n : nat
H : S m = S n
IHm : m = S n -> n < m (****** Bad *******)
______________________________________(1/1)
n < S m
*)

Abort.

Gaëtan Gilbert

On 06/09/2016 12:39, Samira Akili wrote:

Hi,

thanks a lot for your quick response. It really helps, especially regarding the definition of the Connection type.

You are also right with the lemma! We definitely need the distance as pathlength in the lemma, otherwise it would not be true at all. However we still get the same problem with the induction hypothesis.

H : distance x = S n IHn : distance x = n ->       {el : A_list & Connection x root el n} ______________________________________(1/1)

{el : A_list & Connection x root el (S n)}

How can I change the induction scheme to get a different x in the hypothesis and in the goal?

kind regards,

Samira

Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr> schrieb am 20:14 Montag, 5.September 2016:

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?