The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 14 Nov 2011 17:49:44 -0500,
Randy Pollack 
<rpollack AT inf.ed.ac.uk>
 a écrit :

> 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

I guess some time, I'll have to write a tutorial on it…

My way to combine "Guarded" with Fixpoint is to:
1. destruct the inductive term.
2. generalize the application to the given subterms and the mutual
   functions.
3. clear mutual functions from the environnement.
4. run "Guarded."
5. continue the proof without using Guarded anymore.

Example (not tested, so there may be some typos):

Inductive A: Set := X : B -> A | Y : A
with B: Set := U : A -> B.

Fixpoint a_length (a:A) {struct a}: nat
with     b_length (b:B) {struct b}: nat.
Proof.
  destruct a as [b|]. (* step 1 *)
   (*case X*)
   assert (IHa := length_b b). (* step 2 *)
   clear length_a length_b. (* step 3 *)
   Guarded. (* step 4 *)
   exact (S IHa). (* step 5 *)
  (*case Y*)
  exact (O).
Proof.
  destruct b as [a]. (* step 1 *)
  (*case U*)
  assert (IHb := length_a a). (* step 2 *)
  clear length_a length_b. (* step 3 *)
  Guarded. (* step 4 *)
  exact (S IHb). (* step 5 *)
Defined.

Why such a way to proceed?
=> if Guarded reports an error,
   then as there is no "unguarded" function in the
   environment (we have cleared them),
   that is you have done an illegal call to a recursive function
   and you can stop your proof to understand immediately why.
=> if Guarded succeeds, then as you have removed all
   "unguarded" functions, there is no way Guarded will fail later
   AFAIK, so for the continuation of the proof, you can do whatever
   tactic you want (as far as you do not introduce a new fixpoint),
   it will be ok (it is not the case for example if you keep
   your recursive functions and use "auto" somewhere).

Of course I am aware that some times it is not that easy to do,
you may have lot of things to do before running a destruct on
the wished argument, and may introduce a lot of problems,
but for simple case, it is quite efficient to do so;
for complex case, there is also a way to do that, but not always that
easy.

If you provide more information on your inductive type, I can show you
on your example how to do so. Also, if I am to write a tutorial on
that, I would also be interested in relevant examples, so if it is not
too big, you can send me your file (with axioms and parameters instead
of complicate stuff which is orthogonal).