The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Let me suggest an alternative solution which mixes Venanzio's solution
with an inductively defined domain predicate and David's solution with
well-founded recursion.

The idea is to define the domain predicate D but on the sort Prop such
that this predicate disappears from the extracted ML program. 
Then the fixpoint is defined with a structural recursion on the domain
predicate D using the same trick as for well-founded recursion. 
It works because the domain predicate can be "inverted" it means that
we can prove lemmas 

 Lemma Deven_inv : 
  (n:nat)(D n)->(lt (1) n)->(even n)->(D (div2 n)).
such that the proof (Deven_inv n p h1 h2) of (D (div2 n)) is
structurally smaller than the proof p of (D n)

The construction is done the following way 
(* Domain definition *)
Inductive D : nat->Prop :=
   D1 : (D (1))
|  Dodd : (n:nat)(lt (1) n)->(odd n)->(D (S (mult (3) n)))->(D n)
|  Deven : (n:nat)(lt (1) n)->(even n)->(D (div2 n))->(D n).

(* Logical domain properties *)
Lemma not_D_O : (n:nat)(D n)->~O=n.
Lemma Deven_inv : 
  (n:nat)(D n)->(lt (1) n)->(even n)->(D (div2 n)).
Lemma Dodd_inv : 
  (n:nat)(D n)->(lt (1) n)->(odd n)->(D (S (mult (3) n))).

(* Some informative lemmas corresponding to the case analyses in the
program *)

Lemma odd_even_dec : (n:nat){odd n}+{even n}.
Lemma O_1_else : (n:nat){O=n}+{(1)=n}+{lt (1) n}.

Then the fixpoint can be defined the following way (the first argument
n of f is kept implicit) :

Fixpoint f [n:nat;p:(D n)] : nat := 
  if (O_1_else n) then 
     [c01:{O=n}+{(1)=n}](if c01 then [c0:O=n]<nat>Cases (not_D_O p c0) of end
                         else [c1:(1)=n](1))
  else [clt1:(lt (1) n)]
       if (odd_even_dec n) then [codd:(odd n)](S (f (Dodd_inv p clt1 codd)))
       else [ceven:(even n)](S (f (Deven_inv p clt1 ceven))).

The extraction corresponds to the expected program :
Extraction Inline O_1_else.
Extraction f.
let rec f n = match n with
  | O -> assert false (* absurd case *)
  | S n0 ->
      (match n0 with
         | O -> S O
         | S n1 ->
             (match odd_even_dec n with
                | Left -> S (f (S (mult (S (S (S O))) n)))
                | Right -> S (f (div2 n))))

Proving the termination of this program corresponds to a logical proof
of (n:nat)(le (1) n)->(D n) 

I attach the complete Coq script for this example.
Christine

Attachment: recursion.v
Description: Binary data

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 54 60       fax : (+33) (0)1 39 63 56 84