Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>What's missing is a string datatype which hooks into the <code>"..."</code> notation; the <code>String</code> module contains such a notation and datatype, but you have to tell Coq to use that notation via <code>Open Scope string_scope.</code> What's also missing, however, is an implementation of <code>Case</code>, which will only show up after you fix the string problem. All of this is provided for you in the <code>Induction.v</code> file inside the "Download" tarball, but it is not included in the output <code>Induction.html</code>, possibly due to a typo in the <code>.v</code> file. The relevant code, which would be the second paragraph of the "Naming Cases" section (right after "…but a better way is to use the <code>Case</code> tactic," and right before "Here's an example of how <code>Case</code> is used…") is:</p> <pre><code>(* [Case] is not built into Coq: we need to define it ourselves. There is no need to understand how it works -- you can just skip over the definition to the example that follows. It uses some facilities of Coq that we have not discussed -- the string library (just for the concrete syntax of quoted strings) and the [Ltac] command, which allows us to declare custom tactics. Kudos to Aaron Bohannon for this nice hack! *) Require String. Open Scope string_scope. Ltac move_to_top x := match reverse goal with | H : _ |- _ =&gt; try move x after H end. Tactic Notation "assert_eq" ident(x) constr(v) := let H := fresh in assert (x = v) as H by reflexivity; clear H. Tactic Notation "Case_aux" ident(x) constr(name) := first [ set (x := name); move_to_top x | assert_eq x name; move_to_top x | fail 1 "because we are working on a different case" ]. Tactic Notation "Case" constr(name) := Case_aux Case name. Tactic Notation "SCase" constr(name) := Case_aux SCase name. Tactic Notation "SSCase" constr(name) := Case_aux SSCase name. Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name. Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name. Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name. Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name. Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name. </code></pre> <p>(A side note: When I worked through Software Foundations, I found using the provided <code>.v</code> files as my work material to be very helpful. You don't have to worry about elided code, you don't have to retype the definitions, and all the problems are right there. Your mileage may vary, of course.)</p>
    singulars
    1. This table or related slice is empty.
    1. POcoq error when trying to use Case. Example from Software Foundations book
      singulars
      1. PTQuestion
    1. PTAnswer
    1. USAntal Spector-Zabusky
    1. USAntal Spector-Zabusky
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. POcoq error when trying to use Case. Example from Software Foundations book
      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. VTAcceptedByOriginator
    3. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    1. COCool, thanks, that works perfectly. Pointing me to the induction.v file is really helpful as well, it hadn't occurred to me that there would be code in the v not in the html. So I guess what this means is that Case is not something built into the language, but something added by the SF authors for annotating a proof? Is this a common practice or something peculiar to SF's way of doing things? Also, I'm not sure I understand why the "Case" stuff is better than just a simple comment like (* case b=true *).
      singulars
      1. PO
      1. USJohn
    2. CO@quadelirus The `Case` stuff will throw an error and thereby ease debugging if something changes. Example: If you do induction over `nat`s and your base (`O`) case's tactics no longer solve that part after a change, it will throw an error on `Case "n = S n'"` instead of going on and applying the `S`-case stuff onto the (still unfinished) `O`-case.
      singulars
      1. PO
      1. USnobody
    3. CO@quadelirus These `Case`-markers can be found in developments other than the software foundations, but there are other styles as well. Personally, I prefer "Chlipala style" proving (i.e. automating to the point where the proofs are short enough that you simply don't need any `Case` markers.) -- see http://adam.chlipala.net/cpdt/ for yet another Coq book.
      singulars
      1. PO
      1. USnobody
 

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