The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 18 sept. 08 à 00:39, Brian Aydemir a écrit :

> On Sep 17, 2008, at 16:18, Matthieu Sozeau wrote:
>
> > > (* too lazy to prove this right now *)
> > > (* as noted below, I don't actually need this lemma for the  
> > > problem to appear *)
> > > Axiom lc_rename : forall x y e,
> > > lc (open_rec 0 (fvar x) e) ->
> > > lc (open_rec 0 (fvar y) e).
> >
> > That's why it blocks, at the recursive call in the [lc_abs] case,
> > you give this axiom which makes reduction stop right after, on a
> > [match (lc_rename e x0 7 pf) with ...]. You can see that by doing
> > some unfolding and simplification (and wait a bit because the
> > resulting term is huge).
>
> Right.  That makes sense, and I expected reduction to get stuck  
> there.  What confused me is that reduction seemed to get stuck  
> before I reached that point.  I'll use the [app] case as an example,  
> since it doesn't depend on [lc_rename].  In the goal, I see
>
>         silly_subst x u (app e1 e2) (lc_app e1 e2 pf1 pf2) = app e1 e2
>
> If I look at my definition of [silly_subst], I see that it does a  
> [match] on the fourth argument.  The fourth argument here has a  
> constructor at its head, so I expected that the application should  
> somehow reduce to
>
>         app (silly_subst x u e1 pf1) (silly_subst x u e2 pf2) = app e1 e2.

Definitions made using measures are structurally recursive on a proof  
of well-foundedness
of the naturals that's hidden inside the [silly_subst] definition here.
[unfold silly_subst, Fix_measure_sub.]
In the app case, the real argument that is matched is [lt_wf (size  
(app e1 e2))],
and for some reason, [simpl] won't try to reduce it (probably because  
it's not seen
as recursive, I'm not sure).
You can try and put it in hnf:
<<
 match goal with
   | [ |- context C [ lt_wf ?x ] ] =>
     let prf := eval hnf in (lt_wf x) in
     let gl' := context C [ prf ] in
       change gl'
 end.
>>

Now you see an [Acc_intro] constructor at the head of the proof so  
[Fix_measure_F_sub]
can unfold at least once. This time [simpl] will reduce but it cannot  
do the usual trick
of folding back the fixpoint in the reduced term, as the fixpoint is  
local to the definition
of [silly_subst]. In this case, I think if [simpl] was called before  
the unfoldings it would
consider the goal is not in good shape and just fail, making no  
progress, even if the [lt_wf]
proof did unfold. Even by hand, it's not clear how to fold back the  
recursive calls at this point
because [simpl] does too much reductions in the [lt_wf] proof and the  
functional itself. That's
why I use a lemma instead.

> It looks like what I want is [fold_sub] and [unfold_sub].  I think  
> was expecting [program_simpl] to do the equivalent thing for this  
> function that [simpl] would do for functions defined by normal  
> structural recursion.  (-:

My bad, [program_simpl] is supposed to simplify the goal, by  
destructuring objects in subsets,
simplifying the correponding projections and the like, not to be a  
variant of [simpl].

> > <<
> > Ltac fold_sub f :=
> > match goal with
> >   | [ |- ?T ] =>
> >     match T with
> >       appcontext C [ @Fix_measure_sub _ _ _ _ ?arg ] =>
> >       let app := context C [ f arg ] in
> >        change app
> >     end
> > end.
> > >>
>
> Is this intended work with my version of Coq ( svn:// 
> scm.gforge.inria.fr/svn/coq/branches/v8.2 , r11417 )?  Coq is  
> complaining: "Error: The reference appcontext was not found in the  
> current environment."  The syntax is unfamiliar to me, as well.

Indeed, it seems I did not backport this code yet. appcontext is just  
a variant of context
that allows to match partial applications.

-- Matthieu