The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Coq's termination check is very simple: "_" must be of the form  (or reduce to) "All_ints_next ....".

I would suggest using the Function mechanism, which is much more semantic:

https://coq.inria.fr/refman/Reference-Manual004.html#sec78

Here is a potential way to write your function:

Require Import  Recdef.

Parameter one: int.

Function some_function (n:int) {wf (fun a b => int_ltb a b = true)}: int :=

  match int_eqb n min_int with

    true => zero

  | false => some_function (int_minus n one)

  end.

Coq will throw two proof obligations at you. You can prove them in *whatever way you like*. 

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, Oct 12, 2017 at 6:36 PM, Helmut Brandl <helmut.brandl AT gmx.net> wrote:

Hi,

I want to use coq to extract code to ocaml and use ocaml ints.

I ocaml I can write the following recursive function which certainly terminates:

  let rec some_function (i:int) (a:'a): 'a =

    if i = min_int then

      some_expression

    else

      some_function (i-1) (some_g a)

I want to write a function in coq which extracts to such an ocaml function. I have tried some axiomatizations, but I have not yet achieved the desired result.

Parameter min_int: int.

Parameter max_int: int.

Parameter int_eqb: int -> int -> bool.

Parameter int_leb: int -> int -> bool.

Parameter int_ltb: int -> int -> bool.

Parameter int_plus:  int -> int -> int.

Parameter int_minus: int -> int -> int.

.. (* some more parameters to have le, lt, .. and the corresponding axioms *)

Inductive all_ints: int -> Prop :=

  All_ints_base: all_ints min_int

| All_ints_next: forall i, all_ints i -> i <> max_int -> all_ints (i+1).

Axiom all_ints_in_all_ints: forall i:int, all_ints i.

I wanted to use the the inductive set ‘all_ints’ to control termination and e.g. write a recursive function like the following.

Fixpoint some_function (n:int) (p:all_ints n) {struct p}: int.

Proof.

  refine (

  match n =? min_int with

    true => 0

  | false => some_function (n-1) _ + 1

  end).

  ...

Defined.

But I could not find a way to construct the missing _expression_ such that coq accepts it as a decreasing argument. There must be a possibility since the above axiom states that all ints are in an inductively definded set. I assume that some dependent pattern matching can do the job. But I have not yet enough expert knowledge to find this _expression_.

Can anybody help me or give me a hint on how to do this?

Thanks in advance.

Helmut