The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 11/15/2011 05:31 PM, AUGER Cedric wrote:
> 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.


You don't need to clear the mutual functions before running Guarded. 
This advice is more to prevent automated tactics from doing stupid 
things with general recursive hypotheses.

The guard checker is indeed very optimistic and consider as guarded any 
term of the form (?n t1 .. tn) even if you do illegal recursive calls in 
terms t1..tn. It assumes that such bad arguments will not be used by the 
?n subgoal variable. So, to answer Randy's initial concern, Guarded 
should (most of the time) only break when any possible continuation of 
the proof fails to pass the guard. I can see 2 exceptions:
- the one Randy ran into: the guard checker is eager to find the 
abstraction corresponding to the recursive argument, and dies if it 
cannot find it. This could be fixed, but I think it's not critical. I 
would bet that doing intros before Guarded works.
- other elimination operators (like match) are not supported: a proof term
fix F x {struct x} :=
  match ?n with
  | 0 => 0
  | S k => F x
  end.
is rejected but refining subgoal ?n with 0 produces a valid proof (but 
we're walking a tightrope here!)

Bruno.

--
Bruno Barras                    Typical team - INRIA Saclay
LIX - Ecole Polytechnique       91128 Palaiseau Cedex - France
Tel: +33 1 69 33 40 57          Fax: +33 1 69 33 30 14