The Coq mailing list

[Hongjin Liang <lhj1018 AT mail.ustc.edu.cn>]

Yes, foo_test could be proved directly, without using the hypothesis foo. I just intended to know why I cannot apply the hypothesis when proving foo_test (so the example seems inappropriate). I got another example, which originates from proving safety of programs with loops. The safety is defined coinductively, as shown below. 

-------------------------------------------------------------------------------------------

Variable Prog : Type.     (* The type of programs C *)

Variable Seq : Prog -> Prog -> Prog.    (* Sequential composition: C1;C2 *)

Variable Loop : Prog -> Prog.    (* Loop C is like  while true do C. *)

Variable Next : Prog -> Prog -> Prop.    (* Next step: C is executed to C' after a step *)

Hypothesis LoopStep : forall C, Next (Loop C) (Seq C (Loop C)).  

CoInductive Safe : Prog -> Prop :=

  | safeStep : forall C C', Next C C' -> Safe C' -> Safe C. 

(* Assume safety is compositional w.r.t. sequential compositions. *)

Hypothesis SeqSafe : forall C1 C2, Safe C1 -> Safe C2 -> Safe (Seq C1 C2). 

(* I want to prove safety is compositional w.r.t loops. *)

Lemma LoopSafe : 

  forall C, Safe C -> Safe (Loop C).  

Proof. 

  cofix H. intros. 

  apply safeStep with (C' := Seq C (Loop C)).

  apply LoopStep. 

  apply SeqSafe. assumption. apply H. assumption. Guarded. 

------------------------------------------------------------------------------------------------

The error message: 

Recursive definition of H is ill-formed.

In environment

H : forall C : Prog, Safe C -> Safe (Loop C)

C : Prog

H0 : Safe C

Sub-_expression_ "SeqSafe C (Loop C) H0 (H C H0)" not in guarded form (should

be a constructor, an abstraction, a match, a cofix or a recursive

call).

Recursive definition is:

"fun (C : Prog) (H0 : Safe C) =>

 safeStep (Loop C) (Seq C (Loop C)) (LoopStep C)

   (SeqSafe C (Loop C) H0 (H C H0))".

------------------------------------------------------------------------------------------------

Since SeqSafe is not a constructor, I cannot apply it to prove LoopSafe. Then how can I prove it? Do I need to define another coinductive Safe with SeqSafe as a constructor in it (like in the previous example, writing foo as a constructor in my_Inf)? 

- Hongjin

2011/8/7 Pierre Casteran <pierre.casteran AT labri.fr>

Le 07/08/2011 16:51, Pierre Casteran a écrit :

Just a comment:

As Cedric showed, the hypothesis foo is useless.

First, an informal argument :

I'm afraid this argument was a bit too informal :-)
Let's try to be more precise.


Let's have a look at your definition of my_Inf. We can assocaite to it a set (predicate) transformer
F(X) = {y:LList | exists x : LList, x In X /\  x = Lcons 0 y}.

We prove easily that LList is a subset of F(LList)  : Let's take some LList y, then consider the list
(LCons 0 y). Obviously (but not needed) we have also F(LList) = LList.

Thus LList is a fixpoint of F, and clearly the greatest one.

ouf!

Note that the Coq proof below is much shorter than the text above.

Pierre






(*) I use the same notation for the type LList and the set of all its inhabitants.

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