The Coq mailing list

[Ivan Scagnetto <scagnett AT dimi.uniud.it>]

Hello,

we are facing a strange error with proofs of Coinductive predicates,
involving names.  In the following, we will explain it in a very
simple and useless case, but the same problem arises in a real (and
MUCH MORE complex) case.

--- beginning of Coq V6.1 code
(* Let's take a nonempty set *)
Parameter N : Set.
Axiom     x : N.

(* and define a coinductive predicate, whose only constructors takes
 * a proof of A over all N
 *)

CoInductive A : Prop :=
  a: ((n:N)A) -> A.

(* We can prove without problems the following lemma, which let us
 * to prove an universal quantification by proving an existential one
 *)
Lemma WEIRD : (Ex [n:N]A) -> (n:N)A. 
Intros; Inversion_clear H; Assumption.
Qed.

(* Now, we want to prove the following lemma *)
Lemma FOO : A.
Cofix; Apply a; Intro.

(* 1 subgoal
 
  FOO : A
  n : N
  ============================
   A
 
 The shortest way would be

Apply FOO.
Qed.

 which would lead to

 FOO = CoFix FOO{FOO : A := a [_:N]FOO}
     : A

 But we take a longer way (because in the real case we are facing,
 there is no choice): we reduce the universal quantification to the
 existential one, and then give it a witness.
 *)

Apply WEIRD with 2:=n.

(* 1 subgoal
 
  FOO : A
  n : N
  ============================
   (Ex [_:N]A)
*)

Exists x.

(* 1 subgoal
 
  FOO : A
  n : N
  ============================
   A

  And now, like before, we try to close with FOO.
*)

Apply FOO.
Qed.

(* But Coq loudly complains about a non-guarded occurrence of FOO:

(Cofix; Apply a; Intro).
Apply WEIRD with 2:=n.
Exists  x.
Apply FOO.
 
Error: Definition not in guarded form
        The recursive definition 
       (a [n:N](WEIRD (ex_intro N [_:N]A n FOO) n)) is not well-formed
during command
Save.

*)

--- end of Coq listing



Actually, the proof can be carried out as desired if we do not prove
WEIRD as a separate lemma, but rather inside the main proof: we
introduce it by means of a Cut, and prove it like in the lemma:


--- begin of Coq listing
(* As before... *)
Parameter N : Set.
Axiom     x : N.
CoInductive A : Prop :=
  a: ((n:N)A) -> A.

Lemma FOO : A.
Cofix; Apply a; Intro.

Cut (Ex [n:N]A).

(* 2 subgoals

  FOO : A
  n : N
  ============================
   (Ex [_:N]A)->A

subgoal 2 is:
 (Ex [_:N]A)

First goal is the former WEIRD lemma *)

Intro; Inversion_clear H; Assumption.

(* Second goal is the last part of FOO *)

Exists x.

(* 1 subgoal
 
  FOO : A
  n : N
  ============================
   A

  And now we close with FOO.
*)

Apply FOO.
Qed.

Print FOO.
(*
FOO = CoFix FOO{FOO : A := a [_:N]FOO}
     : A
*)
--- end of Coq listing


So, why does Coq complain if we use a "named" lemma, instead of an
"unnamed" one? Does this mean that we cannot use lemmata in proving
(some) coinductive predicates? And what in the case WEIRD is an axiom,
instead of a lemma? In such case, there would be no proof to "expand"
within another one - there would be no solution at all...


Thanks in advance,

Ivan and Marino