The Coq mailing list

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

Hi Arthur,

2012/3/16 Arthur Charguéraud <arthur AT chargueraud.org>

Hi Harley,

If you are happy to use non-constructive definitions, you may use the "Optimal Fixed Point Combinator" for your definitions.
For the ackermann function, you can construct the fix point and then prove a fixed point equation that allows unfolding the body of the function when needed. My Coq script is as follows.

Definition Ack ack m n :=
  If m = 0 then n+1 else 
  If n = 0 then ack (m-1) 1 else
  ack (m-1) (ack m (n-1)).

Definition ack := FixFun2 Ack.

Ltac emaths := eauto with maths.

Lemma fix_ack : forall m n,
  ack m n = Ack ack m n.
Proof.
  applys~ (FixFun2_fix (lexico2 (@lt nat _) (@lt nat _))).
  introv IH. unfolds. case_if~. case_if~. 
  apply IH. emaths. 
  rewrite IH. fequals~. emaths. emaths.
Qed.

You can find more details from: http://arthur.chargueraud.org/projects/fix/

I didn't know about this.  Thanks for the example and the link.  I don't think it will work for my purposes, but I will definitely remember it.

 

PS: If you need to remain constructive, you will probably need to use "Program Fixpoint" and give you definition a dependent type that captures enough of the specification of the function for you to be able to justify termination. I am not aware of any recursive functions for which the dependent-type approach is impossible to use.

Yes, this is what I ended up doing.  I do want to remain constructive.  I managed to get it defined use this and proving the obligations.  The only question I have is is it harder to reason about functions defined this way?

Thanks,

Harley

 

 

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.  

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.

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.  

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

Thanks,

Harley