The Coq mailing list

["Harley D. Eades III" <harley.eades AT gmail.com>]

Hi Auger.

On Fri, Mar 16, 2012 at 5:36 AM, AUGER Cédric <sedrikov AT gmail.com> wrote:

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.

I agree.  I don't see any profound theoretical reason for this.  It doesn't seem to compromise

consistency.  Maybe it has to do with making "Function" definitions as simple to reason about as possible.  I am 

not sure.

 

>
> 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.

I didn't know of this before now.  Thanks for telling me!  Your example

below helped a ton.  After reading this i went and read a bunch on accessibility 

predicates.  I managed to get my function defined using "Program Fixpoint" and 

then actually understanding what I was supposed to do.  :-)

 

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).

Right, I know that now.  Thanks again for this.  It helped a lot!

Thanks,

Harley

 

>
> 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)