The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

The solution that you propose,


Fixpoint ack2 (x:dom_ack) : nat :=
   match x with
      | existS 0 n
      => n+1
      | existS (S m) n
      => ack2 (existS B m (n+1))
      | existS (S m) (S n)
      => ack2 (existS B m (ack2 (existS B (S m) n)))
      end.

cannot be applied, because the standard way of checking whether a 
recursive definition are well-formed requires that recursive calls 
are only performed on (structural) subterms of the initial argument.

When (existS (S m) n) is the initial argument, (existS m (n+1)) is not
a subterm, so this simple way to check whether a recursive function is
well-formed does not apply.

Now, your proof is slightly more complex than what I would like to 
read, so here is a solution to make the whole code definition shorter.

Require Import Wf.
Require Import Relation_Operators.
Require Import Lexicographic_Product.

Definition A : Set := nat.
Definition B (_: A) := nat.
Definition ltA : A -> A -> Prop := lt.
Definition ltB  (x:A) : B x -> B x -> Prop := lt.

Definition lex_ord_n2 := (lexprod A B ltA ltB).

Definition dom_ack : Set := sigS B.
Definition dom_inj (m n:nat) : dom_ack := existS B m n.

Require Import Wf_nat.

Axiom wf_lt : well_founded lt.

Axiom wf_ack : well_founded (A:=dom_ack) lex_ord_n2.

Axiom case2 : forall x y:A,lex_ord_n2 (dom_inj x y) (dom_inj x (S y)).

Axiom case2_ : forall (x0:dom_ack) (x y:A),
   x0 = dom_inj x (S y) -> lex_ord_n2 (dom_inj x y) x0.


Axiom case1 : forall x y z:A,lex_ord_n2 (dom_inj x y) (dom_inj (S x) z).

Axiom case1_ : forall (x0 : dom_ack) (z:A),projS1 x0 > 0 ->
               lex_ord_n2 (dom_inj (pred (projS1 x0)) z) x0.


(* Here is my contribution. *)

Definition F (x:dom_ack):(forall y:dom_ack, lex_ord_n2 y x -> nat) -> nat :=
 match x return
    (forall y:dom_ack, lex_ord_n2 y x -> nat) -> nat with
   existS O n => fun f => (S n)
 | existS (S m) 0 => 
     fun f => (f (dom_inj m 1) (case1 m 1 0))
 | existS (S m) (S n) =>
     fun f =>
       let v := f (dom_inj (S m) n) (case2 (S m) n) in
       f (dom_inj m v) (case1 m v (S n))
 end.

Definition ack (m n : nat) : nat :=
  Fix wf_ack (fun _: dom_ack => nat) F (dom_inj m n).


Now, my definition essentially does the same as yours (and I do reuse 
your lemmas, which I just took as axioms here).  When defining the
function "F", the function "f" is used for the recursive calls, and 
every recursive call has its extra argument to explain that the 
recursive call is licit.   The one very tricky bit is the fact that I 
choose the structure of the function to start with a dependent 
pattern matching construct over x before abstracting over f, as you 
do.  This makes it possible to identify x with the various cases
(like "existS (S m) 0"), and this needed because x is mentioned in 
the type of f.  If you wanted to write all the type information, you 
would have to write the following:


Definition F (x:dom_ack):(forall y:dom_ack, lex_ord_n2 y x -> nat) -> nat :=
 match x return
    (forall y:dom_ack, lex_ord_n2 y x -> nat) -> nat with
   existS O n => fun f => (S n)
 | existS (S m) 0 => 
     fun f: forall y:dom_ack, lex_ord_n2 y (existS B (S m) 0) -> nat 
      => (f (dom_inj m 1) (case1 m 1 0))
 | existS (S m) (S n) =>
     fun f: forall y:dom_ack, lex_ord_n2 y (existS B (S m) (S n)) -> nat =>
       let v := f (dom_inj (S m) n) (case2 (S m) n) in
       f (dom_inj m v) (case1 m v (S n))
 end.


A last point: you defined your function "F" by a proof and this proof 
is rather long, but this is because you have a beginner's style, a 
little cleaning on the proof would give a short, readable proof where 
the algorithmic content still is perceived:

Definition F (x:dom_ack)(f:forall y:dom_ack, lex_ord_n2 y x -> nat) : nat.
intros.
induction x as (m,n).
 induction m.
   exact (S n).

   induction n.
     (* recursive call. *)
     apply (f (dom_inj m 1)).
     (* justification for the recursive call. *)
     change (lex_ord_n2 (dom_inj m 1) (dom_inj (S m) 0)).
     apply case1.

     (* first the justification for the inner recursive call. *)
     assert (H':lex_ord_n2 (dom_inj (S m) n) (dom_inj (S m) (S n))).
       apply case2.
     (* This is the outer recursive call, the inner recursive call is
        given in full, with its justification H' *)
     apply (f (dom_inj m (f (dom_inj (S m) n) H'))).
     (* This is the justification for the outer recursive call. *)
     change (lex_ord_n2 (dom_inj m (f (dom_inj (S m) n) H')) 
                   (dom_inj (S m) (S n))).
     apply case1.
Qed.

In this proof, the "change ..." tactics replace the "assert ..." 
tactics that you used.

As a conclusion, it is true that you have to "prove" your function as
you define it, but you can organize your data so that one definition
contains only the algorithmic part and references to auxiliary lemmas
for the justification that are needed for the recursive calls.  There
is a difficulty when you have nested recursion, as in the Ackermann
function, because you need to refer to other results of recursive
calls when providing some recursive arguments.  For this you need to
use a local definition that gives the justification, which you can 
use several times.

In the Coq'Art, we tried to describe a solution where people write the 
recursive equation in a simpler subset of the calculus of 
constructions (basically avoiding dependent pattern matching), and 
then derive the function from the recursive equation (see sect. 15.3) 
but the solution as described in the book does not apply well to 
Ackermann, because of the nested recursion.  The solution can be 
extended, but the paper where we describe the extension is currently 
being written.

Yves




-- 
Yves.Bertot AT inria.fr
  Tel: (+33/0)4 92 38 77 39  Fax: (+33/0)4 92 38 50 60
INRIA Sophia-Antipolis 2004, route des lucioles, B.P. 93,
06902 Sophia Antipolis Cedex (France).
http://www.inria.fr/lemme/Yves.Bertot