The Coq mailing list

[Hongjin Liang <lianghongjin AT gmail.com>]

Hi all, 

I use two ways (co-inductive predicates) to define the property that there is an infinite path starting from a node, where one predicate explicitly records the trace (an infinite list of all the nodes that will go through) and the other does not.   As shown in the following code, InfPath(x) tries to specify that there is an infinite path starting from node x, and InfPathWithTrace(x, T) tries to also describe the infinite trace T.   I am wondering if it is possible to prove the lemma "infPath_existTrace", which says that such T must exist if InfPath(x) holds. 

(**********************************)

Require Import Relations. 

Variable Node : Type. 

Variable edge : relation Node. 

CoInductive InfPath : Node -> Prop := 

  | infpath : forall x y, 

               edge x y ->

               InfPath y ->

               InfPath x. 

CoInductive Trace : Type := 

  | cons : Node -> Trace -> Trace. 

CoInductive InfPathWithTrace : Node -> Trace -> Prop := 

  | infpathtr : forall x y T, 

                edge x y ->

                InfPathWithTrace y T ->

                InfPathWithTrace x (cons x T).

Lemma infPath_existTrace : 

  forall x, InfPath x -> exists T, InfPathWithTrace x T. 

Proof.  

Admitted.

(***********************************)

In my intuition, the proof of this lemma would be infinite. If (InfPath x) holds, then there must exist a node y such that (edge x y) and (InfPath y) hold.  If we could prove 

   InfPath y -> exists T', InfPathWithTrace y T'       (*)

then we could let T be (cons x T') and get (InfPathWithTrace x T).    But (*) looks the same as our original goal "infPath_existTrace". 

So it sounds like that we need to do co-induction. The problem is, we are required to find an instance of T before doing co-induction. But we cannot find it before "assuming the goal is correct". 

Perhaps this lemma is actually incorrect?  Any idea or suggestion is greatly appreciated. 

Hongjin