Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>Look at your <code>estack</code>, what does it do? Generalize! <code>element</code> is just a relation (<code>A -&gt; A -&gt; Set</code>), <code>tag</code> is just a <code>Set</code>. What do you get?</p> <pre><code>Inductive RTList {I : Set} (X : Rel I) : Rel I := | RTNil : forall {i : I}, RTList X i i | RTCons : forall {i j k : I}, X i j -&gt; RTList X j k -&gt; RTList X i k. </code></pre> <p>(<code>Rel</code> ist just a Definition with <code>Rel I = I -&gt; I -&gt; Set</code>.)</p> <p>Reflexive-transitive closure! That <em>is</em> common, reusable and modular. Or so you'd think.</p> <p>The only implementation I found in Coq's libs is in <code>Coq.Relations.Relation_Operators</code>, named <a href="http://coq.inria.fr/stdlib/Coq.Relations.Relation_Operators.html#clos_refl_trans" rel="nofollow"><code>clos_refl_trans</code></a>, differently structured and locked into <code>Prop</code> (all according to the docs, didn't try it).</p> <p>You'll probably have to re-implement that or find a library somewhere. At least, you'll only have to do this once (or up to three times for <code>Set</code>, <code>Prop</code> and <code>Type</code>).</p> <hr> <p>Your other idea will probably be harder to manage. Look at <a href="http://coq.inria.fr/stdlib/Coq.Lists.List.html#NoDup" rel="nofollow"><code>NoDup</code></a> for something that's similar to your description, you might be able to reuse the pattern. If you really want that. <a href="http://coq.inria.fr/stdlib/Coq.Lists.List.html#NoDup" rel="nofollow"><code>NoDup</code></a> uses <a href="http://coq.inria.fr/stdlib/Coq.Lists.List.html#In" rel="nofollow"><code>In</code></a>, which is a function that checks if an element is in a list. The last time I tried using it, I found it considerably harder to solve proofs involving <code>In</code>. You can't just <code>destruct</code> but have to apply helper lemmas, you have to carefully unfold exactly $n levels, folding back is hard etc. etc. I'd suggest that unless it's truly necessary, you'd better stick with data types for <code>Prop</code>s.</p>
    singulars
    1. This table or related slice is empty.
    1. PODecoupling the data to be manipulated from the proofs that the manipulations are justified
      singulars
      1. PTQuestion
    1. PTAnswer
    1. USnobody
    1. USnobody
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. PODecoupling the data to be manipulated from the proofs that the manipulations are justified
      singulars
      1. PTQuestion
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    3. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTAcceptedByOriginator
    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