Databases
StackOverflow2013
Postsdbo
POWhat does `true = false` mean in Coq?
 

Note that there are some explanatory texts on larger screens.

plurals
  1. POWhat does `true = false` mean in Coq?
    primarykey
    data
    text
    <p>[I am not sure this is appropriate for stack overflow, but there are many other Coq questions here so perhaps someone can help.]</p> <p>I am working through the following from <a href="http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab28" rel="noreferrer">http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab28</a> (just below where Case is introduced). Note that I am a complete beginner at this, and am working at home - I am not a student.</p> <pre><code>Theorem andb_true_elim1 : forall b c : bool, andb b c = true -&gt; b = true. Proof. intros b c H. destruct b. Case "b = true". reflexivity. Case "b = false". rewrite &lt;- H. reflexivity. Qed. </code></pre> <p>and I am looking at what the rewrite does:</p> <pre><code> Case := "b = false" : String.string c : bool H : andb false c = true ============================ false = true </code></pre> <p>then <code>rewrite &lt;- H.</code> is applied:</p> <pre><code> Case := "b = false" : String.string c : bool H : andb false c = true ============================ false = andb false c </code></pre> <p>and it's clear how the proof will succeed.</p> <p>I can see how in terms of manipulating symbols in a mechanical way I am arriving at a proof. That's fine. But I am disturbed by the "meaning". In particular, how can I have <code>false = true</code> in the middle of a proof?</p> <p>It seems like I am making some kind of argument with contradictions, but I am not sure what. I feel like I have been blindly following rules and have somehow arrived at a point where I am typing nonsense.</p> <p>What am I <em>doing</em> above?</p> <p>I hope the question is clear.</p>
    singulars
    1. PO
      singulars
      1. PTAnswer
    1. This table or related slice is empty.
    1. PTQuestion
    1. This table or related slice is empty.
    1. USandrew cooke
    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
    2. PO
      singulars
      1. PTAnswer
    1. VO
      singulars
      1. POWhat does `true = false` mean in Coq?
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. POWhat does `true = false` mean in Coq?
      1. USLambdageek
      1. VTFavorite
    3. VO
      singulars
      1. POWhat does `true = false` mean in Coq?
      1. This table or related slice is empty.
      1. VTUpMod
    1. COYou could try using: [`discriminate`](http://www.fing.edu.uy/inco/grupos/mf/man/Coq/node.1.2.8.html). (I see it's an old post)
      singulars
      1. POWhat does `true = false` mean in Coq?
      1. USguest
 

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