The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Hello,

Sorry but on this subject, I feel the need to advertise on the works of 
our team in Verimag at Grenoble ;-)

One major application of programming with "relations" is to invoke 
external OCaml oracles from Coq code. Indeed, an OCaml function is 
possibly non-deterministic from Coq eyes, and needs thus to be encoded 
as a relation. Moreover, any Coq function invoking such a 
non-deterministic function is itself non-deterministic.

On way to extract (some) relations into runnable programs, is to 
axiomatize the predicate type transformer:
   P(B) = B -> Prop.

The good news is that P(.) as naturally the structure of a monad, and is 
thus fully compatible with functional programming.

Thus, we can axiomatize P(B) as a type ??B using a monad structure 
providing a "~~>" relation of type  ?? B -> P(B).

NB: given k:??B and x:B,  "k ~~> x" is read "k may return x".

In this view, a binary relation of A -> B -> Prop is encoded as a 
function of A -> ?? B.

At extraction "?? B" is simply extracted like "B"

See details of the axioms in

https://github.com/boulme/ImpureDemo/blob/master/coq_src/Impure/ImpMonads.v

Some applications of this idea:

 - Verified Polyhedra Library:
   https://github.com/VERIMAG-Polyhedra/VPL

 - satans-cert: a Coq-certified tool that wraps state-of-the-art 
Boolean SAT-solvers and checks their result.
   https://github.com/boulme/satans-cert



To have more details on this idea (still under development):

  - https://github.com/boulme/ImpureDemo

  - my slides on the Coq Workshop 2018:

https://coqworkshop2018.inria.fr/files/2018/07/coq2018_talk_boulme.pdf

  - the original paper where this idea has appeared:
  https://hal.archives-ouvertes.fr/hal-00991853


Rem: of course, we could imagine other extraction scheme, like 
extracting "?? B" on "'b Lazy.t" or "'b list" ...



Best regards,

Sylvain.



Le 26/10/2018 à 08:27, Cao Qinxiang a écrit :
> This is an interesting idea.
>
> Coq requires functions to terminate (and we have to shows its 
> termination by kind of structure recursion) but ocaml does not require 
> that. A ``function'' may be more convenient to be formalized as a 
> relation instead of a function in Coq. And it will be amazing if those 
> relations can be extracted as functions.
>
> Here is an example,
>
> Inductive log2: nat -> nat -> Prop :=
> | log2_base: log2 1 0
> | log2_step: forall n k, log2 (div2 n) k -> log2 n (S k).
>
>
> Qinxiang Cao
> Tenure Track Assistant Professor
> Shanghai Jiao Tong University, John Hopcroft Center
> Room 1102-2, SJTUSE Building
> 800 Dongchuan Road, Shanghai, China, 200240
>
>
>
> On Thu, Oct 25, 2018 at 2:20 PM Xuanrui Qi <xqi01 AT cs.tufts.edu 
> <mailto:xqi01 AT cs.tufts.edu>> wrote:
>
>     Hello Kakadu,
>
>     This would look interesting to me. I can envision a miniKanren-style
>     program relation correct w/ respect to some specification, and then
>     extract the relation to miniKanren, e.g. for program synthesis.
>
>     I do not know if Will Byrd is on this list, but I guess he would be a
>     person to approach.
>
>     -Ray
>
>     -- 
>     Xuanrui "Ray" Qi
>
>     Department of Computer Science
>     Tufts University
>     161 College Ave, Halligan Hall
>     Medford, MA 02144, USA
>
>     Email: 
> xqi01 AT cs.tufts.edu
>  
> <mailto:xqi01 AT cs.tufts.edu>
>
>     On Thu, 2018-10-25 at 10:52 +0000, Kakadu wrote:
>      > Hello,
>      >
>      >
>      > AFAIU, proving something in terms of relations is convenient but it's
>      > difficult to extract them to runnable code. Let's say we can extract
>      > them to a logical programming language embedded into OCaml. How
>      > useful can it be? Can you easily imagine any concrete use cases?
>      >
>      >
>      > Happy hacking,
>      > Kakadu
>      >
>      >