The Coq mailing list

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

Le Wed, 16 Nov 2011 16:16:34 +0100,
Bruno Barras 
<bruno.barras AT inria.fr>
 a écrit :

> 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.

I know that, but I prefer to use "Guarded" only once!
If you do Guarded before cleaning, then you have no guarantee that
later you won't have a guardedness error, if you do it after, then
(unless if you use the fix tactic or a fixpoint refine later) you have
some guarantee not to have a guardedness error, AFAI understand the
system.

> 
> 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.
>