[Coq-Club] Extracting runnable relations

[Kakadu]

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

[Xuanrui Qi]

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

Post by Kakadu
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

[Cao Qinxiang]

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

Post by Xuanrui Qi
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

Post by Kakadu
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

[Sylvain Boulmé]

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.

Post by Cao Qinxiang
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
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

Post by Kakadu
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

[Dominique Larchey-Wendling]

Dear Qinxiang Cao,

With JF Monin from Verimag, we recently proposed a solution which
applies easily to the very problem you are mentioning:

https://members.loria.fr/DLarchey/files/papers/TYPES_2018_paper_19.pdf

It was presented at TYPES 2018.

The basic idea is that the graph G : X -> Y -> Prop of an algorithm induces a
well-founded relation on the domain D : X -> Prop of the algorithm which you
can then use to realize the algo. as a term

f : forall x, D x -> { y | G x y } (where D x := exists y, G x y)

term which is extracted to what you want (you have to respect the
computational content of the algorithm when you implement f).

Notice that you have to find another inductive representation of D
(i.e. other than exists x, G x y) to use it for the fixpoint construction.
There is a general way explained in the paper.

On your example, this gives you something like the following

Best regards,

Dominique Larchey-Wendling
-----------------

Require Import Arith Wellfounded Omega Extraction.

Set Implicit Arguments.

Section measure_rect.

Variables (X : Type) (m : X -> nat) (P : X -> Type)
(HP : forall x, (forall y, m y < m x -> P y) -> P x).

Theorem measure_rect : forall x, P x.
Proof.
apply (@well_founded_induction_type _ (fun x y => m x < m y)); auto.
apply wf_inverse_image, lt_wf.
Qed.

End measure_rect.

Definition measure_rec X m (P : X -> Set) := @measure_rect X m P.
Definition measure_ind X m (P : X -> Prop) := @measure_rect X m P.

Fixpoint div2 n :=
match n with
| S (S n) => S (div2 n)
| _ => 0
end.

Fixpoint div2_lt n : { n <= 1 } + { 1 <= div2 n < n }.
Proof.
destruct n as [ | [ | n ] ]; simpl; auto.
right.
specialize (div2_lt n).
destruct div2_lt.
+ destruct n as [ | [] ]; simpl in *; omega.
+ omega.
Qed.

Fact div2_zero n : div2 n = 0 -> n <= 1.
Proof.
destruct n as [ | [ |]]; simpl; auto; discriminate.
Qed.

Inductive g_log2: nat -> nat -> Prop :=
| g_log2_base: g_log2 1 0
| g_log2_step: forall n k, g_log2 (div2 n) k -> g_log2 n (S k).

Fact g_log2_zero n k : g_log2 n k -> n <> 0.
Proof.
induction 1 as [ | n k H ].
+ discriminate.
+ contradict H; subst; auto.
Qed.

Fact g_log2_fun n k1 k2 : g_log2 n k1 -> g_log2 n k2 -> k1 = k2.
Proof.
intros H; revert H k2.
induction 1; inversion 1; subst; auto.
+ apply g_log2_zero in H0; destruct H0; auto.
+ apply g_log2_zero in H; destruct H; auto.
Qed.

Section log2.

Let log2_full n : n <> 0 -> { k | g_log2 n k }.
Proof.
induction n as [ n IHn ] using (measure_rect (fun n => n)).
case_eq n.
+ intros _ []; trivial.
+ intros p E1 _.
case_eq p.
* intro; subst; exists 0; constructor.
* intros m E2; subst p.
refine (let (k,Hk) := IHn (div2 n) _ _ in _).
- destruct (div2_lt n); omega.
- subst; simpl; discriminate.
- exists (S k); rewrite <- E1.
constructor; auto.
Qed.

Definition log2 n Hn := proj1_sig (@log2_full n Hn).
Fact log2_spec n Hn : g_log2 n (@log2 n Hn).
Proof. apply (proj2_sig _). Qed.

End log2.

Arguments log2 : clear implicits.

Fact log2_fix_0 H : log2 1 H = 0.
Proof.
apply g_log2_fun with (1 := log2_spec _); constructor.
Qed.

Fact log2_fix_1 n H1 H2 : log2 n H1 = S (log2 (div2 n) H2).
Proof.
apply g_log2_fun with (1 := log2_spec _).
constructor; apply log2_spec.
Qed.

Extraction Inline measure_rect.
Recursive Extraction log2.

Envoyé: Vendredi 26 Octobre 2018 08:27:03
Objet: Re: [Coq-Club] Extracting runnable relations
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

Post by Xuanrui Qi
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

Post by Kakadu
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

[mukesh tiwari]

I am not sure, but I think relation-extraction [1] plugin does the same
thing. I haven't used it, so I am wondering if someone having more
familiarity could shed some more insights about this plugin.

Best,
Mukesh

[1] https://github.com/coq-contribs/relation-extraction

On Fri, Oct 26, 2018 at 8:50 PM Dominique Larchey-Wendling <

Post by Dominique Larchey-Wendling
Dear Qinxiang Cao,
With JF Monin from Verimag, we recently proposed a solution which
https://members.loria.fr/DLarchey/files/papers/TYPES_2018_paper_19.pdf
It was presented at TYPES 2018.
The basic idea is that the graph G : X -> Y -> Prop of an algorithm induces a
well-founded relation on the domain D : X -> Prop of the algorithm which you
can then use to realize the algo. as a term
f : forall x, D x -> { y | G x y } (where D x := exists y, G x y)
term which is extracted to what you want (you have to respect the
computational content of the algorithm when you implement f).
Notice that you have to find another inductive representation of D
(i.e. other than exists x, G x y) to use it for the fixpoint construction.
There is a general way explained in the paper.
On your example, this gives you something like the following
Best regards,
Dominique Larchey-Wendling
-----------------
Require Import Arith Wellfounded Omega Extraction.
Set Implicit Arguments.
Section measure_rect.
Variables (X : Type) (m : X -> nat) (P : X -> Type)
(HP : forall x, (forall y, m y < m x -> P y) -> P x).
Theorem measure_rect : forall x, P x.
Proof.
apply wf_inverse_image, lt_wf.
Qed.
End measure_rect.
Fixpoint div2 n :=
match n with
| S (S n) => S (div2 n)
| _ => 0
end.
Fixpoint div2_lt n : { n <= 1 } + { 1 <= div2 n < n }.
Proof.
destruct n as [ | [ | n ] ]; simpl; auto.
right.
specialize (div2_lt n).
destruct div2_lt.
+ destruct n as [ | [] ]; simpl in *; omega.
+ omega.
Qed.
Fact div2_zero n : div2 n = 0 -> n <= 1.
Proof.
destruct n as [ | [ |]]; simpl; auto; discriminate.
Qed.
Inductive g_log2: nat -> nat -> Prop :=
| g_log2_base: g_log2 1 0
| g_log2_step: forall n k, g_log2 (div2 n) k -> g_log2 n (S k).
Fact g_log2_zero n k : g_log2 n k -> n <> 0.
Proof.
induction 1 as [ | n k H ].
+ discriminate.
+ contradict H; subst; auto.
Qed.
Fact g_log2_fun n k1 k2 : g_log2 n k1 -> g_log2 n k2 -> k1 = k2.
Proof.
intros H; revert H k2.
induction 1; inversion 1; subst; auto.
+ apply g_log2_zero in H0; destruct H0; auto.
+ apply g_log2_zero in H; destruct H; auto.
Qed.
Section log2.
Let log2_full n : n <> 0 -> { k | g_log2 n k }.
Proof.
induction n as [ n IHn ] using (measure_rect (fun n => n)).
case_eq n.
+ intros _ []; trivial.
+ intros p E1 _.
case_eq p.
* intro; subst; exists 0; constructor.
* intros m E2; subst p.
refine (let (k,Hk) := IHn (div2 n) _ _ in _).
- destruct (div2_lt n); omega.
- subst; simpl; discriminate.
- exists (S k); rewrite <- E1.
constructor; auto.
Qed.
Proof. apply (proj2_sig _). Qed.
End log2.
Arguments log2 : clear implicits.
Fact log2_fix_0 H : log2 1 H = 0.
Proof.
apply g_log2_fun with (1 := log2_spec _); constructor.
Qed.
Fact log2_fix_1 n H1 H2 : log2 n H1 = S (log2 (div2 n) H2).
Proof.
apply g_log2_fun with (1 := log2_spec _).
constructor; apply log2_spec.
Qed.
Extraction Inline measure_rect.
Recursive Extraction log2.
------------------------------
*Envoyé: *Vendredi 26 Octobre 2018 08:27:03
*Objet: *Re: [Coq-Club] Extracting runnable relations
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

Post by Xuanrui Qi
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

Post by Kakadu
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