Skip to Content.
Sympa Menu

coq-club - [Coq-Club]

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]


Chronological Thread 
  • From: Samira Akili <claire_sari AT yahoo.de>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: [Coq-Club]
  • Date: Mon, 5 Sep 2016 15:50:56 +0000 (UTC)
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=claire_sari AT yahoo.de; spf=Pass smtp.mailfrom=claire_sari AT yahoo.de; spf=None smtp.helo=postmaster AT nm31-vm4.bullet.mail.ir2.yahoo.com
  • Ironport-phdr: 9a23:2zYe6RbSpSDvl/2Gg35LBV7/LSx+4OfEezUN459isYplN5qZpcuzbnLW6fgltlLVR4KTs6sC0LuP9f2wEj1ZqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2atc+p26ie8oHeKwxOgz+0ZaI6bE/v7Fb8s9EKkMN5N6wzxxDV6jsRI6UFjV9vcBiYmA+57cOt9rZi9T5RsrQv7YQIBa79ZuEzSaFSJDUgKWE8osPx40r5QBOL90cbB14flxtSCkDs7xD+X9+luS/zt/Bw7zKTJ8zeXLk0XjPk46o9GzHyjyJSDDc88XvewuVzjaZa6EaqoxV+2YPje4iPNdJvd6PaepUWSDwSDY5qSyVdD9bkPMM0BO0bMLMD9oQ=

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?

 







Archive powered by MHonArc 2.6.18.

Top of Page