The Coq mailing list

[David Nowak <David.Nowak AT lsv.ens-cachan.fr>]

Hi,

With the solution proposed by Venanzio, even if we assume the axiom

  (n:nat)(le (1) n)->(Df n)

we cannot run the extracted function in O'Caml:

let rec f n = function
  | Df1 -> S O
  | Dfe (n', h') -> S (f (div2 n') h')
  | Dfo (n', h') -> S (f (S (mult (S (S (S O))) n')) h')

Another way is to use well founded recursion.

Require Arith.
Require Even.
Require Div2.

We first define the following relation:

Inductive R : nat->nat->Prop :=
  r1 : (n:nat)(le (1) n)->(odd n)->(R (S (mult (3) n)) n)
| r2 : (n:nat)(le (1) n)->(even n)->(R (div2 n) n).

We assume it is well founded (by the way, can anyone remind me the name of this 
conjecture ?):

Axiom R_wf : (well_founded nat R).

We define the function by proof:

Definition f [n:nat] : (le (1) n)->nat.
Proof.
Change (n:nat)([p:nat](le (1) p)->nat n) .
Apply (well_founded_induction nat R R_wf).
Intro n.
Case n.
Intros.
Apply False_rec.
Inversion H0.

Intro n'.
Case n'.
Intros.
Exact (1).

Intro n''.
Case (even_odd_dec n'').
Intros.
Refine (S (H (div2 (S (S n''))) ? ?)).
Apply r2.
Assumption.

Auto with arith.

Generalize e H0.
Clear e H0.
Simpl.
Auto with arith.

Intros.
Refine (S (H (S (mult (3) (S (S n'')))) ? ?)).
Apply r1.
Assumption.

Auto with arith.

Auto with arith.
Defined.

Lemma le_1_3 : (le (1) (3)).
Proof.
Auto.
Defined.

The extracted function can be run in O'Caml:

let f x =
  let rec acc_rect x0 _ =
    match x0 with
      | O -> assert false (* absurd case *)
      | S n' ->
          (match n' with
             | O -> S O
             | S n'' ->
                 (match even_odd_dec n'' with
                    | Left -> S (acc_rect (div2 (S (S n''))) ())
                    | Right -> S
                        (acc_rect (S (mult (S (S (S O))) (S (S n''))))
                          ())))

Regards,

David.

--
David Nowak
LSV - CNRS UMR 8643 - ENS de Cachan
61, av. du Président Wilson, 94235 Cachan Cedex
tél: +33 1 47 40 55 69   fax: +33 1 47 40 24 64
http://www.lsv.ens-cachan.fr/~nowak/