The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 16 Mar 2012 01:45:58 -0500,
"Harley D. Eades III" 
<harley.eades AT gmail.com>
 a écrit :

> Hello.
> 
> I am trying to define a function using the well-founded annotation for
> function definitions.
> 
> Here is a simple example illustrating both my problem and what I am
> attempting:
> 
> Inductive ord : (nat * nat) -> (nat * nat) -> Prop :=
>   | ord_red1 : forall n n' m m',
>     n < m -> ord (n, n') (m, m')
>   | ord_red2 : forall n n' m',
>     n' < m' -> ord (n, n') (n, m').
> 
> Function ack (p : nat*nat) {wf ord p } : nat :=
>   match p with
>     | (0, n) => (S n)
>     | (S m, 0) => ack (m,1)
>     | (S m, S n) => ack(m, ack(S m, n))
>   end.
> 
> Keep in mind that this is just an example.  The function I ultimately
> want to define is more complex
> than this example.
> 
> The main problem is that the above function is rejected by Coq.  I
> believe it is because I am not allowed
> to use nested recursive calls in the body of a function; as in the
> last branch of ack.

At least that is the error message, althought I don't see particular
reason to forbid it.

> 
> My question is, does anyone know of a way around this?  I really want
> to be able to use the well-founded annotation, because
> the function I really want to define would be very difficult any
> other way.

Do you know of the Acc predicate? In fact, it is what is behind "wf
annotations"; so using it explicitly can help.

If you don't know of this predicate, you should take a look at it.

> 
> In this case I might be able to use 'fix' to get around the above
> problem, but I am wondering if there are any other ways, because
> doing it using 'fix' essentially makes using the wf-annotation
> pointless.  Also, my ultimate goal is not possible using 'fix', at
> least I think it is.

At each place you use "wf annotations", you can use "fix"; in fact,
"Function" is not part of the Coq "core" language, it is something
built using fix (and the Acc predicate).

> 
> If anyone wants to know what this "ultimate" function is I will post
> it.
> 
> Thanks,
> Harley

So with Acc, that would give:
=============================================

Set Implicit Arguments.

Inductive ord : (nat * nat) -> (nat * nat) -> Prop :=
  | ord_red1 : forall n n' m m',
    n < m -> ord (n, n') (m, m')
  | ord_red2 : forall n n' m',
    n' < m' -> ord (n, n') (n, m').

Fixpoint ack (p : nat*nat) (H:Acc ord p) : nat :=
  let ack := match H with Acc_intro H => fun p Ho => ack (H p Ho) end in
  match p as p0 return (forall p, ord p p0 -> nat) -> nat with
    | (0, n) => fun _ => (S n)
    | (S m, 0) => fun ack => ack (m,1) (ord_red1 _ _ (le_n _))
    | (S m, S n) => fun ack =>
       ack (m, ack (S m, n) (ord_red2 _ (le_n _))) (ord_red1 _ _ (le_n
_)) end ack.

Lemma rec : forall p, Acc ord p.
Proof.
 assert (K : forall y, (forall z, z < y -> forall n, Acc ord (z, n)) ->
             forall n, Acc ord (y, n)).
  intros.
  induction n; split; intros; inversion H0; clear H0; subst; auto.
   inversion H3.
  assert (K := le_S_n _ _ H3); clear H3.
  induction K; auto.
  apply IHK; clear - IHn; destruct IHn; apply H; right; left.
 intros [m]; induction m; apply K; clear K; intros;
 inversion H; clear H; subst; auto.
 now destruct (IHm 0); apply H; left.
Qed.

Definition Ack := fun p => ack (rec p).
================================================

If you find "ack" definition being ugly, you can also use tactics to
manage the proof handling.

Fixpoint ack (p : nat*nat) (H:Acc ord p) : nat.
refine (
  let ack := _ in
  match p as p0 return (forall p, ord p p0 -> nat) -> nat with
    | (0, n) => fun _ => (S n)
    | (S m, 0) => fun ack => ack (m,1) _
    | (S m, S n) => fun ack =>
       ack (m, ack (S m, n) _) _
  end ack
).
Proof.
 (*Your proofs here*)
Defined.

Some last remarks:
→ if you want to compute "rec" must be transparent
  (ie. Defined terminated, not Qed terminated)
→ If you build terms using tactics, I strongly recommend:
  → build only Prop habitants with tactics
    (ie. avoid « Definition zero : nat. left. Defined. »)
  → if you want to compute/unfold definitions, abstract
    the Prop contents of the term you are building
    (using the abstract tactic)
  → Try to apply the previous two points to the "rec"
    definition.
→ if you use the abstract tactic, clean your hypothesis
  before (in particular, never keep a fixpoint not
  fully applied before proceding, since it will
  be generalized, and will make guardedness fail)