The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

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.


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


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


In any event, your explanation was helpful.  Thank you!

--Brian