coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Matthieu Sozeau <mattam AT mattam.org>
- To: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Program Fixpoint, measure, and simplification
- Date: Wed, 17 Sep 2008 22:18:37 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Le 17 sept. 08 à 20:28, Brian Aydemir a écrit :
Hi,
Hi,
At the end of this message, I include a snippet of code that illustrates a situation in which I am unable to simplify a function defined using Program Fixpoint. I'm using the subversion version of Coq 8.2 (r11417). The code is a simplified (somewhat silly) version of what I actually want to do, but hopefully it's not too trivial in this form. I have noted in comments variations that I've tried, to no success.
The main function of interest is [silly_subst], which is defined using [size] as a measure. I am unable to get [silly_subst] to simplify in the proof of [silly_subst_thm]. Any tips would be appreciated.
It can be indeed quite difficult to see where the computations
get stuck in this situation.
(* 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).
I've developped two tactics that try to fold/unfold such
definitions based on
[@Fix_measure_sub],
avoiding bloated goals.
For some reason I never put them in [FunctionalExtensionality] :)
The [fold_sub] tactic is only using convertibility to fold a
definition but the [unfold_sub] rewrites by a lemma using
extensionality. The calling convention is a bit weird: you have
to give the function and the function applied to the arguments
that are constant during the recursive calls to [unfold_sub] and
only the latter to [fold_sub].
<<
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.
Ltac unfold_sub f fargs :=
set (call:=fargs) ; unfold f in call ; unfold call ; clear call ;
rewrite fix_sub_measure_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig.
>>
Using these, you can avoid seeing the unfolding to [Fix_measure_sub]
while doing one unfolding. For example, at the end of your script you get:
<<
Lemma silly_subst_thm : forall (x : nat) (u e : exp) (pf : lc e),
silly_subst x u e pf = e.
Proof.
induction pf; intros; simpl in *; program_simpl.
(* Why did the first subgoal simplify away? <- program_simpl tries reflexivity *)
(* Why aren't the remaining subgoals simplified or reduced in any way? *)
unfold_sub silly_subst (silly_subst x u).
2 subgoals
x : nat
u : exp
x0 : nat
e : exp
pf : lc (open_rec 0 (fvar x0) e)
IHpf : silly_subst x u (open_rec 0 (fvar x0) e) pf = open_rec 0 (fvar x0) e
============================
silly_subst x u (open_rec 0 (fvar 7) e) (lc_rename e x0 7 pf) = abs e
subgoal 2 is:
silly_subst x u (app e1 e2) (lc_app e1 e2 pf1 pf2) = app e1 e2
>>
If you try again to reduce you'll see that [lc_rename] comes back in head position.
Hope this helps,
-- Matthieu
- [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.