Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Axiomatize ocaml integers

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Axiomatize ocaml integers


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Axiomatize ocaml integers
  • Date: Sun, 15 Oct 2017 00:55:26 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f178.google.com
  • Ironport-phdr: 9a23:nE5FNRbtxyJq6M1Jfpvo2jD/LSx+4OfEezUN459isYplN5qZpsuybnLW6fgltlLVR4KTs6sC0LWG9f24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i76vnYuHUD0MhMwLeDoEMaGhMOukuu25pf7YgNShTP7b6kkfzusqgCEn8MWgJBiJ6V54x3ApHcAL+1cxWJzJV+Q2R/678G8up9i7yt4tPco9soGWqL/KfdrBYdEBSgrZjhmrPbgsgPOGFOC

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


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





Archive powered by MHonArc 2.6.18.

Top of Page