The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

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 <dominique.larchey-wendling AT loria.fr> wrote:

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.
 

---

De: "Cao Qinxiang" <caoqinxiang AT gmail.com>
À: coq-club AT inria.fr
Cc: "danya berezun" <danya.berezun AT gmail.com>
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

On Thu, Oct 25, 2018 at 2:20 PM Xuanrui Qi <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

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