Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Re: trying to use Init.Wf.Fix .

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: trying to use Init.Wf.Fix .


chronological Thread 
  • 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






Archive powered by MhonArc 2.6.16.

Top of Page