The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

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