coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: dehlinge AT dpt-info.u-strasbg.fr
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] trying to use Init.Wf.Fix .
- Date: Wed, 5 May 2004 17:34:42 +0200 (CEST)
- Importance: Normal
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi all,
I'm trying to translate the following function into Coq :
f n = 0 if n=1
f n = n+1 if n is even
f n = n-3 if n is odd
Obviously, a simple Fixpoint with n as the variable will not work, as n
isn't structurally decreasing. So I tried to use the Fix function,
defined in the Wf library.
Set Implicit Arguments.
Require Export Arith.
Require Export Even.
Require Export Peano_dec.
Require Export Wf_nat.
(* creating a well-founded relation between the argument value of a
recursive call and the original value*)
Inductive l : nat -> nat -> Prop :=
L : forall n : nat, (even n)->(l (S n) n)
| L2 : forall n : nat, n<>1->(odd n)->(l (n-3) n).
Lemma WFL :
well_founded l.
Proof.
intro n.
apply (lt_wf_ind n (Acc l)).
clear n.
intros n rec.
constructor.
intros y l1.
inversion l1.
generalize l1.
rewrite <- H0.
rewrite H1.
clear H1 H0 H n0 l1 y.
unfold next in |- *.
elim (even_odd_dec n); intros.
constructor.
intros.
inversion H.
unfold next in |- *.
elim (even_odd_dec (S n)); intros.
elim (not_even_and_odd (S n)); auto with arith.
apply rec.
destruct n.
elim H0.
auto.
unfold lt in |- *.
rewrite minus_Sn_m.
simpl in |- *.
rewrite <- minus_n_O.
apply le_S.
apply le_n.
do 2 apply le_n_S.
destruct n.
inversion a.
inversion H4.
apply le_n_S.
apply le_O_n.
apply rec.
destruct n.
inversion b.
unfold lt in |- *.
apply le_n_S.
simpl in |- *.
apply le_minus.
Defined.
Definition f : nat->nat := Fix WFL (fun _ => nat)
(fun (x:nat) (rec:(forall y : nat, l y x -> nat)) =>
match (eq_nat_dec x 1) with
(left _) => 0
| (right neqx1) =>
(match (even_odd_dec x) with
(left e) => rec _ (L e)
| (right o) => rec _ (L2 neqx1 o)
end)
end).
Now I've got my function. My question is : how do I use it ? I tried
Eval compute (f 1).
as well as other flag combinations, but the only computations that occur
are within f itself; there is no fixpoint reduction with 1 and (WFL 1),
and I can't see why. Note that this computation doesn't even need any
recursive calls.
Thanks for any insight.
Christophe Dehlinger
LSIIT, UMR 7005, CNRS & Louis-Pasteur University (Strasbourg 1),
Pole Technologique, Boulevard S. Brant, BP 10413, 67412 Illkirch
- [Coq-Club] trying to use Init.Wf.Fix ., dehlinge
- Re: [Coq-Club] trying to use Init.Wf.Fix ., Robert R Schneck-McConnell
Archive powered by MhonArc 2.6.16.