The Coq mailing list

[Hongjin Liang <lianghongjin AT gmail.com>]

Yes, this solves my problem!  Thanks very much!

Hongjin

On Sat, Jan 10, 2015 at 5:16 PM, Xavier Leroy <Xavier.Leroy AT inria.fr> wrote:

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