coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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:
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 thensome_expressionelsesome_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 withtrue => 0| false => some_function (n-1) _ + 1end)....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
- [Coq-Club] Axiomatize ocaml integers, Helmut Brandl, 10/13/2017
- Re: [Coq-Club] Axiomatize ocaml integers, Abhishek Anand, 10/15/2017
- Re: [Coq-Club] Axiomatize ocaml integers, Helmut Brandl, 10/18/2017
- Re: [Coq-Club] Axiomatize ocaml integers, Abhishek Anand, 10/15/2017
Archive powered by MHonArc 2.6.18.