The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Sun, 7 Aug 2011 14:40:55 +0800,
Hongjin Liang 
<lianghongjin AT gmail.com>
 a écrit :

> Hi all,
> 
> I defined a coinductive property and tried to prove a lemma about it.
> When I applied the hypothesis, the proof violates the guarded
> condition. But if I wrote the same hypothesis as a case in the
> coinductive definition, then I can complete the proof. I'm not
> familiar with coq, but I'm really curious about the reasons behind
> the results and hope somebody could help me. My code is given below
> (it itself does not have special meanings).
> 
> *****************************************************************************
> CoInductive LList : Set :=
>     LNil : LList
>   | LCons : nat -> LList -> LList.
> 
> CoInductive my_Inf : LList -> Prop :=
>     My_Inf_Lcons : forall l, my_Inf (LCons 0 l) -> my_Inf l.
> 
> Hypothesis foo : forall l, my_Inf l -> my_Inf (LCons 0 l).
> 
> Lemma foo_test :  forall l, my_Inf l.
> Proof.
>   cofix H. intros. apply My_Inf_Lcons. apply foo. apply H. Guarded.
> ------------------------------------------------------------------------------------------------
> The error message:
> Recursive definition of H is ill-formed.
> In environment
> H : forall l : LList, my_Inf l
> l : LList
> Sub-expression "foo l (H l)" not in guarded form (should be a
> constructor, an
> abstraction, a match, a cofix or a recursive call).
> Recursive definition is: "fun l : LList => My_Inf_Lcons l (foo l (H
> l))".
> 
> *****************************************************************************
> Then I merged the coinductive definition my_Inf and the hypothesis
> foo to be a new coinductive definition:
> 
> CoInductive my_Inf : LList -> Prop :=
>     My_Inf_Lcons : forall l, my_Inf (LCons 0 l) -> my_Inf l
>   | foo : forall l, my_Inf l -> my_Inf (LCons 0 l).
> 
> Lemma foo_test :  forall l, my_Inf l.
> Proof.
>   cofix H. intros. apply My_Inf_Lcons. apply foo. apply H. Guarded.
> Qed.
> 
> The proof is completed and foo_test is defined.
> *****************************************************************************
> 
> I'm really curious about the differences between the above two ways to
> define and prove coinductive properties. Could anyone give me some
> hints about the reasons behind the results please? Thanks a lot!
> 
> - Hongjin

I am not used to CoInductives, so it takes me some time to understand
the problem; consider this variation (just an instantiation of foo)
======================================================================
CoInductive LList : Set :=
    LNil : LList
  | LCons : nat -> LList -> LList.

CoInductive my_Inf : LList -> Prop :=
    My_Inf_Lcons : forall l, my_Inf (LCons 0 l) -> my_Inf l.

Lemma foo : forall l, my_Inf l -> my_Inf (LCons 0 l).
 now intros l [].
Defined.

(*Hypothesis foo : forall l, my_Inf l -> my_Inf (LCons 0 l).*)

Lemma foo_test :  forall l, my_Inf l.
Proof.
intros l.
cofix H.
Guarded.
set (term := My_Inf_Lcons l (foo l H)).
unfold foo in term.
======================================================================
Now what would mean this proof?
That is I assume my final result by coinduction then destruct it then
rebuild it, so that there is a constructor at head of term.
But the truth is that really "built something" the coinduction doesn't
hold.
I did this artificial example, which roughly follows what you did:

CoInductive dummy : Set :=
 Dummy: False -> dummy.

(*
CoFixpoint dummy_wrong: dummy.
 cofix H.
 (* apply H. Guarded. *)
 apply Dummy.
 Guarded.
 destruct H.
 Guarded.
*)

Hypothesis foo: dummy -> False.
 (* you can instantiate it with destructing the argument. *)
(*Lemma foo: dummy -> False. now intros []. Qed.*)
Lemma foo_test : dummy.
 cofix H.
 apply Dummy.
 apply foo.
 apply H.
 Guarded.

The guardness condition requires that the corecursive call is not
inspected; so it cannot be argument of an opaque function or a
transparent inspecting function.

In your second definition, there is no inspection, only a sequence of
constructor and it is ok.

To convince you, try to write manually the first constructors of your
first definition (you won't be able to do so).

Your second attempt gives a term of the form

My_Inf_Lcons l (foo (Lcons 0 l) (My_Inf_Lcons (Lcons 0 …)))

foo is no more an hypothesis, but a constructor