Databases
StackOverflow2013
Postsdbo
POHow to optimize a search in coq
 

Note that there are some explanatory texts on larger screens.

plurals
  1. POHow to optimize a search in coq
    primarykey
    data
    text
    <p>I have a simple search function for a property that I am interested in, and a proof that the function is correct. I want to evaluate the function, and use the correctness proof to get the theorem for the original property. Unfortunately, evaluation in coq is very slow. As a trivial example, consider looking for square roots:</p> <pre><code>(* Coq 8.4 A simple example to demonstrate searching. Timings are rough and approximate. *) Require Import Peano_dec. Definition SearchSqrtLoop := fix f i n := if eq_nat_dec (i * i) n then i else match i with | 0 =&gt; 0 (* ~ Square n \/ n = 0 *) | S j =&gt; f j n end . Definition SearchSqrt n := SearchSqrtLoop n n. (* Compute SearchSqrt 484. takes about 30 seconds. *) Theorem sqrt_484a : SearchSqrt 484 = 22. apply eq_refl. (* 100 seconds *) Qed. (* 50 seconds *) Theorem sqrt_484b : SearchSqrt 484 = 22. vm_compute. (* 30 seconds *) apply eq_refl. Qed. (* 30 seconds *) Theorem sqrt_484c (a : nat) : SearchSqrt 484 = 22. apply eq_refl. (* 100 seconds *) Qed. (* 50 seconds *) Theorem sqrt_484d (a : nat) : SearchSqrt 484 = 22. vm_compute. (* 60 seconds *) apply eq_refl. Qed. (* 60 seconds *) </code></pre> <p>Now try the corresponding function in Python:</p> <pre><code>def SearchSqrt(n): for i in range(n, -1, -1): if i * i == n: return i return 0 </code></pre> <p>or slightly more literally</p> <pre><code>def SearchSqrtLoop(i, n): if i * i == n: return i if i == 0: return 0 return SearchSqrtLoop(i - 1, n) def SearchSqrt(n): return SearchSqrtLoop(n, n) </code></pre> <p>The function is nearly instant in Python, but takes minutes in coq, depending on exactly how you try to call it. Also curious is that putting an extra variable in makes vm_compute take twice as long.</p> <p>I understand that everything is done symbolically in coq, and thus slow, but it would be very useful if I could directly evaluate simple functions. Is there a way to do it? Just using native integers instead of linked lists would probably help a lot.</p>
    singulars
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. PTQuestion
    1. This table or related slice is empty.
    1. USscubed
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. PO
      singulars
      1. PTAnswer
    1. This table or related slice is empty.
    1. This table or related slice is empty.
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload