coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Thery Laurent <thery AT ns.di.univaq.it>
- To: dehlinge AT dpt-info.u-strasbg.fr
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Re: trying to use Init.Wf.Fix .
- Date: Tue, 11 May 2004 10:09:19 +0200 (CEST)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
using Yves and Jean-Christophe's solutions you can get
a function that both computes and extracts well
everytime you can find a measure for the recursive
calls of the function.
For this you just need that your well founded proof
simplifies. With Jean-Christophe's solution it just needs
to evaluate to the maximum number of recursive calls.
Here is the code:
Require Export Arith.
Require Export Even.
Require Export Peano_dec.
Definition even_odd_dec: forall n, ({ even n }) + ({ odd n }).
Proof.
induction n.
auto with arith.
elim IHn; auto with arith.
Defined.
(* Now even_odd_dec computes *)
Eval compute in (even_odd_dec 6).
Definition well_founded_ltof:
forall (A : Set) (f : A -> nat), well_founded (fun x y => f x < f y).
Proof.
intros A f; red.
cut (forall n (a : A), f a < n -> Acc (fun (x y : A) => f x < f y) a).
intros H a; apply (H (S (f a))); auto with arith.
induction n.
intros; absurd (f a < 0); auto with arith.
intros a ltSma.
apply Acc_intro.
intros b ltfafb.
apply IHn.
apply lt_le_trans with (f a); auto with arith.
Defined.
(* Now well_founded_ltof computes *)
Eval compute in (well_founded_ltof _ (fun x => x) 1).
(* The weight function ensures termination*)
Definition weight :=
fun (x : nat) =>
match even_odd_dec x with left _ => x + 2 | right _ => x end.
(* The first recursion *)
Theorem rec1: forall (n : nat), ~ n = 1 -> even n -> (weight (S n) < weight
n).
intros n H; unfold weight.
case (even_odd_dec (S n)); case (even_odd_dec n); simpl; auto.
intros; case (not_even_and_odd (S n)); auto with arith.
intros; case (not_even_and_odd n); auto with arith.
rewrite plus_comm; simpl; auto.
intros; case (not_even_and_odd n); auto with arith.
Qed.
(* The second recursion *)
Theorem rec2: forall (n : nat), ~ n = 1 -> odd n -> (weight (n - 3) < weight
n).
intros n Diff Odd.
unfold weight; simpl.
assert (Hn: le 3 n).
generalize Diff Odd; case n; simpl; auto with arith.
intros; case (not_even_and_odd 0); auto with arith.
intros n1; case n1; simpl.
intros H1; case H1; auto.
intros n2; case n2; simpl; [idtac | auto with arith].
intros; case (not_even_and_odd 2); auto with arith.
case (even_odd_dec (n - 3)); case (even_odd_dec n); simpl; auto.
intros; case (not_even_and_odd n); auto with arith.
intros; pattern n at 2; rewrite (le_plus_minus 3 n); auto with arith.
rewrite (plus_comm 3); auto with arith.
intros; case (not_even_and_odd n); auto with arith.
intros; apply lt_minus; auto with arith.
Qed.
(* Definition of f *)
Definition f: nat -> nat.
refine (Fix
(well_founded_ltof _ weight) (fun (_ : nat) => nat)
(fun n f =>
match eq_nat_dec n 1 with
left _ => 0
| right _ =>
match even_odd_dec n with
left _ => f (S n) _
| right _ => f (n - 3) _
end
end)).
apply rec1; auto.
apply rec2; auto.
Defined.
(* Computation works fine *)
Eval compute in (f 5).
(* Rewriting works fine *)
Theorem f_correct:
forall (n : nat),
f n = match eq_nat_dec n 1 with
left _ => 0
| right _ =>
match even_odd_dec n with left _ => f (S n)
| right _ => f (n - 3) end
end.
intros n.
refine (Fix_eq _ (fun (_ : nat) => nat) _ _ n).
intros x f0 g H.
case (eq_nat_dec x 1); simpl; auto.
intros H1.
case (even_odd_dec x); auto.
Qed.
(* Extraction works fine *)
Extraction Inline Fix Fix_F.
Extraction "test.ml" f.
--
Laurent Thery
- [Coq-Club] Re: trying to use Init.Wf.Fix ., dehlinge
- Re: [Coq-Club] Re: trying to use Init.Wf.Fix .,
Thery Laurent
- Re: [Coq-Club] Re: trying to use Init.Wf.Fix ., Jean-Christophe Filliatre
- Re: [Coq-Club] Re: trying to use Init.Wf.Fix ., Thery Laurent
- Re: [Coq-Club] Re: trying to use Init.Wf.Fix .,
Thery Laurent
Archive powered by MhonArc 2.6.16.