The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Just a comment:

As Cedric showed, the hypothesis foo is useless.

First, an informal argument :
If you look at my_Inf, it defines the "biggest" set X of possibly  
infinite lists such that if Lcons 0 x belongs to X then x belongs to X.

Since the type LList is such a set, and is clearly the biggest one,
the predicate  my_Inf characterizes  all the elements of LList.

If you put it in Coq, you obtain the following proof.

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 L : forall l, my_Inf l.
cofix.
split;apply L.
Qed.

Pierre




Quoting 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