The Coq mailing list

[Helmut Brandl <helmut.brandl AT gmx.net>]

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