coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Brian Aydemir <baydemir AT cis.upenn.edu>
- To: Matthieu Sozeau <mattam AT mattam.org>
- Cc: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Program Fixpoint, measure, and simplification
- Date: Wed, 17 Sep 2008 18:39:43 -0400
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] Program Fixpoint, measure, and simplification, Brian Aydemir
- Re: [Coq-Club] Program Fixpoint, measure, and simplification,
Matthieu Sozeau
- Re: [Coq-Club] Program Fixpoint, measure, and simplification, Brian Aydemir
- Re: [Coq-Club] Program Fixpoint, measure, and simplification,
Matthieu Sozeau
- [Coq-Club] Type-checking & Evaluation, Thery Laurent
- Re: [Coq-Club] Program Fixpoint, measure, and simplification,
Matthieu Sozeau
- Re: [Coq-Club] Program Fixpoint, measure, and simplification, Brian Aydemir
- Re: [Coq-Club] Program Fixpoint, measure, and simplification,
Matthieu Sozeau
Archive powered by MhonArc 2.6.16.