The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

As far as I understand the Guarded command, it basically tries to
check the Guard condition on the current partial proof term. Since
here the partial proof term only says that the two lemmas are mutually
recursive, without any information, Guarded cannot check that there is
a decreasing argument (conditions for proper termination), hence the
failure. I would therefore say it's a feature :) I think the idea of
Guarded is more to use it after applying one of the lemma, of using
refine, to convince yourself you're not doing something stupid.

My 2c.
Alexandre

On Mon, Nov 14, 2011 at 5:49 PM, Randy Pollack 
<rpollack AT inf.ed.ac.uk>
 wrote:
> I have 2 mutual lemmas:
>
> Lemma lower_free_eval : forall r t tl v tl',
>  lower_free_env r ->
>  lower_free_tm t ->
>  eval r t tl v tl' ->
>  lower_free_val v
> with lower_free_ueval : forall r t tl u tl',
>  lower_free_env r ->
>  lower_free_tm t ->
>  ueval r t tl u tl' ->
>  lower_free_uval u.
> Proof. Guarded.
>
> The "Guarded" is not accepted, even though no induction has yet been 
> attempted:
>
> Error:
> Recursive definition of lower_free_eval is ill-formed.
> In environment
> lower_free_eval :
> forall (r : env) (t : tm) (tl : lab) (v : val) (tl' : lab),
> lower_free_env r -> lower_free_tm t -> eval r t tl v tl' -> lower_free_val v
> lower_free_ueval :
> forall (r : env) (t : tm) (tl : lab) (u : uval) (tl' : lab),
> lower_free_env r ->
> lower_free_tm t -> ueval r t tl u tl' -> lower_free_uval u
> Not enough abstractions in the definition.
> Recursive definition is: "?1 lower_free_eval lower_free_ueval".
>
> Yet, If I remove only the "Guarded" command, I have a proof of this
> lemma that is accepted, including the Qed.
>
> The reason I was playing with Guarded is that a slight variant of the
> development causes the proof of these lemmas to be rejected at the Qed
> with:
>
>  Error: Cannot guess decreasing argument of fix.
>
> Thanks for any help.
>
> Randy
>