The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On 10/01/15 05:04, Hongjin Liang wrote:
> (**********************************)
> 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. 

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

As a general guideline,
induction lets you prove statements of the shape
          inductive-hypothesis -> ...
and coinduction lets you prove statements of the shape
          ... -> coinductive-conclusion
Your lemma has shape
          coinductive-hypothesis -> inductive-conclusion
so neither induction nor coinduction will help.

The trick is to explicitly construct (with a CoFixpoint) the trace T
such that InfPathWithTrace x T holds:

CoFixpoint TraceofInfPath (x: Node) (ip: InfPath x) : Trace := ...

Lemma infPath_trace:
  forall x (ip: InfPath x), InfPathWithTrace x (TraceofInfPath x ip).
Proof ... Qed.

Lemma infPath_existTrace :
  forall x, InfPath x -> exists T, InfPathWithTrace x T.
Proof.
  intros x ip. exists (TraceofInfPath x ip). apply infPath_trace.
Qed.

The construction of the trace is not obvious because InfPath is in
Prop while Trace is in Type.

Solution #1: put InfPath in Type.

CoInductive InfPath : Node -> Type :=
  | infpath : forall x y,
               edge x y ->
               InfPath y ->
               InfPath x.

CoFixpoint TraceofInfPath (x: Node) (ip: InfPath x) : Trace :=
  match ip with
  | infpath x y edge inf => cons x (TraceofInfPath y inf)
  end.

Solution #2: use classical logic, e.g. an axiom of description.

Require Import ClassicalEpsilon.

Definition invertInfPath (x: Node) (ip: InfPath x)
                       : { y | edge x y /\ InfPath y }.
Proof.
  apply constructive_indefinite_description.
  inversion ip; subst. exists y; auto.
Qed.

CoFixpoint TraceofInfPath (x: Node) (ip: InfPath x) : Trace :=
  match invertInfPath x ip with
  | exist y (conj edg inf) => cons x (TraceofInfPath y inf)
  end.

Hope this helps,

- Xavier Leroy