Add info about customization of Lean

IntroLean.qmd

@@ -15,7 +15,7 @@ Suppose $P \to (Q \to R)$.  Then $\neg R \to (P \to \neg Q)$.
 Suppose $\neg R$.  Suppose $P$.  Since $P$ and $P \to (Q \to R)$, it follows that $Q \to R$.  But then, since $\neg R$, we can conclude $\neg Q$.  Thus, $P \to \neg Q$.  Therefore $\neg R \to (P \to \neg Q)$. [ □]{.excl}\qedhere
 :::
 
-And here is how we would write the proof in Lean.  (If you are reading this book online, then Lean examples like the one below will appear in gray boxes.  You can copy the example to your clipboard by clicking in the upper-right corner of the box, and then you can paste it into a file in VS Code to try it out.)
+And here is how we would write the proof in Lean.^[Experienced Lean users will notice that the Lean proofs in this book look somewhat different from standard Lean proofs.  This is because our proofs use a number of custom tactics.  These tactics are designed to make our Lean proofs more readable and to bring Lean into closer agreement with *HTPI*.  These custom tactics are defined in the file "HTPIDefs.lean", which is in the folder "HTPILib" in the Lean package that accompanies this book.  The appendix includes advice about transitioning from the Lean in this book to standard Lean.]  (If you are reading this book online, then Lean examples like the one below will appear in gray boxes.  You can copy the example to your clipboard by clicking in the upper-right corner of the box, and then you can paste it into a file in VS Code to try it out.)
 
 ```lean
 theorem Example_3_2_4

docs/IntroLean.html

@@ -267,7 +267,7 @@ <h2 class="anchored" data-anchor-id="a-first-example">A First Example</h2>
 <div class="proof">
 <p><span class="proof-title"><em>Proof</em>. </span>Suppose <span class="math inline">\(\neg R\)</span>. Suppose <span class="math inline">\(P\)</span>. Since <span class="math inline">\(P\)</span> and <span class="math inline">\(P \to (Q \to R)\)</span>, it follows that <span class="math inline">\(Q \to R\)</span>. But then, since <span class="math inline">\(\neg R\)</span>, we can conclude <span class="math inline">\(\neg Q\)</span>. Thus, <span class="math inline">\(P \to \neg Q\)</span>. Therefore <span class="math inline">\(\neg R \to (P \to \neg Q)\)</span>. <span class="excl">&nbsp;□</span></p>
 </div>
-<p>And here is how we would write the proof in Lean. (If you are reading this book online, then Lean examples like the one below will appear in gray boxes. You can copy the example to your clipboard by clicking in the upper-right corner of the box, and then you can paste it into a file in VS Code to try it out.)</p>
+<p>And here is how we would write the proof in Lean.<a href="#fn1" class="footnote-ref" id="fnref1" role="doc-noteref"><sup>1</sup></a> (If you are reading this book online, then Lean examples like the one below will appear in gray boxes. You can copy the example to your clipboard by clicking in the upper-right corner of the box, and then you can paste it into a file in VS Code to try it out.)</p>
 <div class="sourceCode" id="cb1"><pre class="sourceCode lean code-with-copy"><code class="sourceCode lean"><span id="cb1-1"><a href="#cb1-1" aria-hidden="true" tabindex="-1"></a><span class="kw">theorem</span> Example_3_2_4</span>
 <span id="cb1-2"><a href="#cb1-2" aria-hidden="true" tabindex="-1"></a>    (P Q R : <span class="kw">Prop</span>) (h : P → (Q → R)) : ¬R → (P → ¬Q) := <span class="kw">by</span></span>
 <span id="cb1-3"><a href="#cb1-3" aria-hidden="true" tabindex="-1"></a>  <span class="kw">assume</span> h2 : ¬R</span>
@@ -622,6 +622,12 @@ <h2 class="anchored" data-anchor-id="types">Types</h2>
 <p>In this version of the theorem, we have introduced a new variable <code>U</code>, whose type is … <code>Type</code>! So <code>U</code> can stand for any type. You can think of the variable <code>U</code> as playing the role of the universe of discourse, an idea that was introduced in Section 1.3 of <em>HTPI</em>. The sets <code>B</code> and <code>C</code> contain elements from that universe of discourse, and <code>a</code> belongs to the universe. You can prove the new version of the theorem by using exactly the same sequence of tactics as before.</p>
 
 
+</section>
+<section id="footnotes" class="footnotes footnotes-end-of-document" role="doc-endnotes">
+<hr>
+<ol>
+<li id="fn1"><p>Experienced Lean users will notice that the Lean proofs in this book look somewhat different from standard Lean proofs. This is because our proofs use a number of custom tactics. These tactics are designed to make our Lean proofs more readable and to bring Lean into closer agreement with <em>HTPI</em>. These custom tactics are defined in the file “HTPIDefs.lean”, which is in the folder “HTPILib” in the Lean package that accompanies this book. The appendix includes advice about transitioning from the Lean in this book to standard Lean.<a href="#fnref1" class="footnote-back" role="doc-backlink">↩︎</a></p></li>
+</ol>
 </section>
 
 </main> <!-- /main -->

docs/index.html

@@ -229,6 +229,7 @@ <h2 class="anchored" data-anchor-id="about-this-book">About This Book</h2>
 <h2 class="anchored" data-anchor-id="about-lean">About Lean</h2>
 <p><a href="https://leanprover.github.io">Lean</a> is a kind of software package called a <em>proof assistant</em>. What that means is that Lean can help you to write proofs. As we will see over the course of this book, there are several ways in which Lean can be helpful. First of all, if you type a proof into Lean, then Lean can check the correctness of the proof and point out errors. As you are typing a proof into Lean, it will keep track of what has been accomplished so far in the proof and what remains to be done to finish the proof, and it will display that information for you. That can keep you moving in the right direction as you are figuring out a proof. And sometimes Lean can fill in small details of the proof for you.</p>
 <p>Of course, to make this possible, you must type your proof in a format that Lean understands. Much of this book will be taken up with explaining how to write a proof so that Lean will understand it.</p>
+<p>Note that this book uses a customized version of Lean. The customization is designed to make Lean proofs more readable and to bring Lean into closer agreement with <em>HTPI</em>. The appendix includes advice about transitioning from the Lean in this book to standard Lean.</p>
 </section>
 <section id="installing-lean" class="level2">
 <h2 class="anchored" data-anchor-id="installing-lean">Installing Lean</h2>

docs/search.json

@@ -18,7 +18,7 @@
     "href": "index.html#about-lean",
     "title": "How To Prove It With Lean",
     "section": "About Lean",
-    "text": "About Lean\nLean is a kind of software package called a proof assistant. What that means is that Lean can help you to write proofs. As we will see over the course of this book, there are several ways in which Lean can be helpful. First of all, if you type a proof into Lean, then Lean can check the correctness of the proof and point out errors. As you are typing a proof into Lean, it will keep track of what has been accomplished so far in the proof and what remains to be done to finish the proof, and it will display that information for you. That can keep you moving in the right direction as you are figuring out a proof. And sometimes Lean can fill in small details of the proof for you.\nOf course, to make this possible, you must type your proof in a format that Lean understands. Much of this book will be taken up with explaining how to write a proof so that Lean will understand it."
+    "text": "About Lean\nLean is a kind of software package called a proof assistant. What that means is that Lean can help you to write proofs. As we will see over the course of this book, there are several ways in which Lean can be helpful. First of all, if you type a proof into Lean, then Lean can check the correctness of the proof and point out errors. As you are typing a proof into Lean, it will keep track of what has been accomplished so far in the proof and what remains to be done to finish the proof, and it will display that information for you. That can keep you moving in the right direction as you are figuring out a proof. And sometimes Lean can fill in small details of the proof for you.\nOf course, to make this possible, you must type your proof in a format that Lean understands. Much of this book will be taken up with explaining how to write a proof so that Lean will understand it.\nNote that this book uses a customized version of Lean. The customization is designed to make Lean proofs more readable and to bring Lean into closer agreement with HTPI. The appendix includes advice about transitioning from the Lean in this book to standard Lean."
   },
   {
     "objectID": "index.html#installing-lean",
@@ -81,7 +81,7 @@
     "href": "IntroLean.html#a-first-example",
     "title": "Introduction to Lean",
     "section": "A First Example",
-    "text": "A First Example\nWe’ll start with Example 3.2.4 in How To Prove It. Here is how the theorem and proof in that example appear in HTPI (HTPI p. 110; consult HTPI if you want to see how this proof was constructed):\n\nSuppose \\(P \\to (Q \\to R)\\). Then \\(\\neg R \\to (P \\to \\neg Q)\\).\n\n\nProof. Suppose \\(\\neg R\\). Suppose \\(P\\). Since \\(P\\) and \\(P \\to (Q \\to R)\\), it follows that \\(Q \\to R\\). But then, since \\(\\neg R\\), we can conclude \\(\\neg Q\\). Thus, \\(P \\to \\neg Q\\). Therefore \\(\\neg R \\to (P \\to \\neg Q)\\).  □\n\nAnd here is how we would write the proof in Lean. (If you are reading this book online, then Lean examples like the one below will appear in gray boxes. You can copy the example to your clipboard by clicking in the upper-right corner of the box, and then you can paste it into a file in VS Code to try it out.)\ntheorem Example_3_2_4\n    (P Q R : Prop) (h : P → (Q → R)) : ¬R → (P → ¬Q) := by\n  assume h2 : ¬R\n  assume h3 : P\n  have h4 : Q → R := h h3\n  contrapos at h4            --Now h4 : ¬R → ¬Q\n  show ¬Q from h4 h2\n  done\nLet’s go through this Lean proof line-by-line and see what it means. The first line tells Lean that we are going to prove a theorem, and it gives the theorem a name, Example_3_2_4. The next line states the theorem. In the theorem as stated in HTPI, the letters \\(P\\), \\(Q\\), and \\(R\\) are used to stand for statements that are either true or false. In logic, such statements are often called propositions. The expression (P Q R : Prop) on the second line tells Lean that P, Q, and R will be used in this theorem to stand for propositions. The next parenthetical expression, (h : P → (Q → R)), states the hypothesis of the theorem and gives it the name h; the technical term that Lean uses is that h is an identifier for the hypothesis. Assigning an identifier to the hypothesis gives us a way to refer to it when it is used later in the proof. Almost any string of characters that doesn’t begin with a digit can be used as an identifier, but it is traditional to use identifiers beginning with the letter h for hypotheses. After the statement of the hypothesis there is a colon followed by the conclusion of the theorem, ¬R → (P → ¬Q). Finally, at the end of the second line, the expression := by signals the beginning of the proof.\nEach of the remaining lines is a step in the proof. The first line of the proof introduces the assumption ¬R and gives it the identifier h2. Of course, this corresponds precisely to the first sentence of the proof in HTPI. Similarly, the second line, corresponding to the second sentence of the HTPI proof, assigns the identifier h3 to the assumption P. The next line makes the inference Q → R, giving it the identifier h4. The inference is justified by combining statements h and h3—that is, the statements P → (Q → R) and P—exactly as in the third sentence of the proof in HTPI.\nThe next step of the proof in HTPI combines the statements \\(Q \\to R\\) and \\(\\neg R\\) to draw the inference \\(\\neg Q\\). This reasoning is justified by the contrapositive law, which says that \\(Q \\to R\\) is equivalent to its contrapositive, \\(\\neg R \\to \\neg Q\\). In the Lean proof, this inference is broken up into two steps. In the fourth line of the proof, we ask Lean to rewrite statement h4—that is, Q → R—using the contrapositive law. Two hyphens in a row tell Lean that the rest of the line is a comment. Lean ignores comments and displays them in green. The comment on line four serves as a reminder that h4 now stands for the statement ¬R → ¬Q. Finally, in the last step of the proof, we combine the new h4 with h2 to infer ¬Q. There is no need to give this statement an identifier, because it completes the proof. In the proof in HTPI, there are a couple of final sentences explaining why this completes the proof, but Lean doesn’t require this explanation."
+    "text": "A First Example\nWe’ll start with Example 3.2.4 in How To Prove It. Here is how the theorem and proof in that example appear in HTPI (HTPI p. 110; consult HTPI if you want to see how this proof was constructed):\n\nSuppose \\(P \\to (Q \\to R)\\). Then \\(\\neg R \\to (P \\to \\neg Q)\\).\n\n\nProof. Suppose \\(\\neg R\\). Suppose \\(P\\). Since \\(P\\) and \\(P \\to (Q \\to R)\\), it follows that \\(Q \\to R\\). But then, since \\(\\neg R\\), we can conclude \\(\\neg Q\\). Thus, \\(P \\to \\neg Q\\). Therefore \\(\\neg R \\to (P \\to \\neg Q)\\).  □\n\nAnd here is how we would write the proof in Lean.1 (If you are reading this book online, then Lean examples like the one below will appear in gray boxes. You can copy the example to your clipboard by clicking in the upper-right corner of the box, and then you can paste it into a file in VS Code to try it out.)\ntheorem Example_3_2_4\n    (P Q R : Prop) (h : P → (Q → R)) : ¬R → (P → ¬Q) := by\n  assume h2 : ¬R\n  assume h3 : P\n  have h4 : Q → R := h h3\n  contrapos at h4            --Now h4 : ¬R → ¬Q\n  show ¬Q from h4 h2\n  done\nLet’s go through this Lean proof line-by-line and see what it means. The first line tells Lean that we are going to prove a theorem, and it gives the theorem a name, Example_3_2_4. The next line states the theorem. In the theorem as stated in HTPI, the letters \\(P\\), \\(Q\\), and \\(R\\) are used to stand for statements that are either true or false. In logic, such statements are often called propositions. The expression (P Q R : Prop) on the second line tells Lean that P, Q, and R will be used in this theorem to stand for propositions. The next parenthetical expression, (h : P → (Q → R)), states the hypothesis of the theorem and gives it the name h; the technical term that Lean uses is that h is an identifier for the hypothesis. Assigning an identifier to the hypothesis gives us a way to refer to it when it is used later in the proof. Almost any string of characters that doesn’t begin with a digit can be used as an identifier, but it is traditional to use identifiers beginning with the letter h for hypotheses. After the statement of the hypothesis there is a colon followed by the conclusion of the theorem, ¬R → (P → ¬Q). Finally, at the end of the second line, the expression := by signals the beginning of the proof.\nEach of the remaining lines is a step in the proof. The first line of the proof introduces the assumption ¬R and gives it the identifier h2. Of course, this corresponds precisely to the first sentence of the proof in HTPI. Similarly, the second line, corresponding to the second sentence of the HTPI proof, assigns the identifier h3 to the assumption P. The next line makes the inference Q → R, giving it the identifier h4. The inference is justified by combining statements h and h3—that is, the statements P → (Q → R) and P—exactly as in the third sentence of the proof in HTPI.\nThe next step of the proof in HTPI combines the statements \\(Q \\to R\\) and \\(\\neg R\\) to draw the inference \\(\\neg Q\\). This reasoning is justified by the contrapositive law, which says that \\(Q \\to R\\) is equivalent to its contrapositive, \\(\\neg R \\to \\neg Q\\). In the Lean proof, this inference is broken up into two steps. In the fourth line of the proof, we ask Lean to rewrite statement h4—that is, Q → R—using the contrapositive law. Two hyphens in a row tell Lean that the rest of the line is a comment. Lean ignores comments and displays them in green. The comment on line four serves as a reminder that h4 now stands for the statement ¬R → ¬Q. Finally, in the last step of the proof, we combine the new h4 with h2 to infer ¬Q. There is no need to give this statement an identifier, because it completes the proof. In the proof in HTPI, there are a couple of final sentences explaining why this completes the proof, but Lean doesn’t require this explanation."
   },
   {
     "objectID": "IntroLean.html#term-mode",

index.qmd

@@ -18,6 +18,8 @@ If you are reading this book online, then at the end of the title in the left ma
 
 Of course, to make this possible, you must type your proof in a format that Lean understands.  Much of this book will be taken up with explaining how to write a proof so that Lean will understand it.
 
+Note that this book uses a customized version of Lean.  The customization is designed to make Lean proofs more readable and to bring Lean into closer agreement with *HTPI*.  The appendix includes advice about transitioning from the Lean in this book to standard Lean.
+
 ## Installing Lean
 
 These instructions are based on the installation procedure that is described [here](https://lean-lang.org/lean4/doc/quickstart.html).  Alternative installation procedures can be found [here](https://leanprover-community.github.io/get_started.html).