Update Tue Dec 19 05:11:31 EST 2023

hrmacbeth · Dec 19, 2023 · ba7e663 · ba7e663
1 parent 495c7c3
commit ba7e663
Show file tree

Hide file tree

Showing 27 changed files with 420 additions and 354 deletions.
diff --git a/.buildinfo b/.buildinfo
@@ -1,4 +1,4 @@
 # Sphinx build info version 1
 # This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
-config: 7e05cf3a855125a920132587baee20c0
+config: 7b220ab85f5c2c3aa0ee3577fe0afed2
 tags: 645f666f9bcd5a90fca523b33c5a78b7
diff --git a/00_Introduction.html b/00_Introduction.html
diff --git a/01_Proofs_by_Calculation.html b/01_Proofs_by_Calculation.html
diff --git a/02_Proofs_with_Structure.html b/02_Proofs_with_Structure.html
@@ -30,7 +30,7 @@
     <nav data-toggle="wy-nav-shift" class="wy-nav-side">
       <div class="wy-side-scroll">
         <div class="wy-side-nav-search" >
-            <a href="index.html" class="icon icon-home"> The mechanics of proof
+            <a href="index.html" class="icon icon-home"> The Mechanics of Proof
           </a>
 <div role="search">
   <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
@@ -41,7 +41,7 @@
 </div>
         </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
               <ul>
-<li class="toctree-l1"><a class="reference internal" href="00_Introduction.html">Introduction</a></li>
+<li class="toctree-l1"><a class="reference internal" href="00_Introduction.html">Preface</a></li>
 </ul>
 <ul class="current">
 <li class="toctree-l1"><a class="reference internal" href="01_Proofs_by_Calculation.html">1. Proofs by calculation</a></li>
@@ -119,7 +119,7 @@
 
     <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
           <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
-          <a href="index.html">The mechanics of proof</a>
+          <a href="index.html">The Mechanics of Proof</a>
       </nav>
 
       <div class="wy-nav-content">
@@ -157,7 +157,7 @@
 <p>Every proof we&#8217;ve seen so far has been a single calculation.  More typically, though, a proof will
 have a more complex structure, with facts established at an early stage which are not used immediately,
 but instead brought in later.</p>
-<p>For example, here&#8217;s the algebra problem from <a class="reference internal" href="01_Proofs_by_Calculation.html#id20"><span class="std std-numref">Example 1.3.3</span></a>.</p>
+<p>For example, here&#8217;s the algebra problem from <a class="reference internal" href="01_Proofs_by_Calculation.html#id22"><span class="std std-numref">Example 1.3.3</span></a>.</p>
 <div class="admonition-problem admonition">
 <p class="admonition-title">Problem</p>
 <p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be real numbers and suppose that <span class="math notranslate nohighlight">\(a-5b=4\)</span>
@@ -321,7 +321,7 @@ <h3><span class="section-number">2.1.2. </span>Example<a class="headerlink" href
 </section>
 <section id="id3">
 <h3><span class="section-number">2.1.3. </span>Example<a class="headerlink" href="#id3" title="Permalink to this headline">&#61633;</a></h3>
-<p>Let&#8217;s redo another example, this time <a class="reference internal" href="01_Proofs_by_Calculation.html#id33"><span class="std std-numref">Example 1.4.2</span></a>.  The problem was:</p>
+<p>Let&#8217;s redo another example, this time <a class="reference internal" href="01_Proofs_by_Calculation.html#id35"><span class="std std-numref">Example 1.4.2</span></a>.  The problem was:</p>
 <div class="admonition-problem admonition">
 <p class="admonition-title">Problem</p>
 <p>Let <span class="math notranslate nohighlight">\(r\)</span> and <span class="math notranslate nohighlight">\(s\)</span> be rational numbers, and suppose that
@@ -436,7 +436,7 @@ <h3><span class="section-number">2.1.6. </span>Example<a class="headerlink" href
 <p>We conclude the section with some exercises translating prose proofs into Lean proofs.  The
 difficult part with these problems is to pick out, from the text, what the intermediate statements
 are.</p>
-<p>First, we redo one more example, this time <a class="reference internal" href="01_Proofs_by_Calculation.html#id31"><span class="std std-numref">Example 1.4.1</span></a>.  The problem was:</p>
+<p>First, we redo one more example, this time <a class="reference internal" href="01_Proofs_by_Calculation.html#id33"><span class="std std-numref">Example 1.4.1</span></a>.  The problem was:</p>
 <div class="admonition-problem admonition">
 <p class="admonition-title">Problem</p>
 <p>Let <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> be integers, and suppose that
@@ -695,6 +695,16 @@ <h3><span class="section-number">2.2.4. </span>Exercises<a class="headerlink" hr
 </pre></div>
 </div>
 </li>
+<li><p>Let <span class="math notranslate nohighlight">\(s\)</span> be a rational number for which <span class="math notranslate nohighlight">\(3s &#8804; -6\)</span> and
+<span class="math notranslate nohighlight">\(2s \ge -4\)</span>. Show that <span class="math notranslate nohighlight">\(s=-2\)</span>.</p>
+<p>You will probably use the lemma <code class="docutils literal notranslate"><span class="pre">le_antisymm</span></code>, stating if <span class="math notranslate nohighlight">\(x\le y\)</span> and
+<span class="math notranslate nohighlight">\(x\ge y\)</span> then <span class="math notranslate nohighlight">\(x = y\)</span>.</p>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="c">/-</span><span class="cm"> 5 points -/</span>
+<span class="kd">theorem</span> <span class="n">problem2</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">}</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">s</span> <span class="bp">&#8804;</span> <span class="bp">-</span><span class="mi">6</span><span class="o">)</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">s</span> <span class="bp">&#8805;</span> <span class="bp">-</span><span class="mi">4</span><span class="o">)</span> <span class="o">:</span> <span class="n">s</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+</pre></div>
+</div>
+</li>
 </ol>
 <p class="rubric">Footnotes</p>
 <dl class="footnote brackets">
@@ -1215,7 +1225,7 @@ <h3><span class="section-number">2.4.3. </span>Example<a class="headerlink" href
 <p>It also sometimes happens that the goal of a problem features an &#8220;and&#8221; statement.  For example, you
 might be given a system of simultaneous equations, and asked to determine the values of all the
 variables appearing.  Here&#8217;s a system of simultaneous equations we saw before in
-<a class="reference internal" href="01_Proofs_by_Calculation.html#id20"><span class="std std-numref">Example 1.3.3</span></a>, but the problem statement has been tweaked to ask us to find the
+<a class="reference internal" href="01_Proofs_by_Calculation.html#id22"><span class="std std-numref">Example 1.3.3</span></a>, but the problem statement has been tweaked to ask us to find the
 values of both <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span>.</p>
 <div class="admonition-problem admonition">
 <p class="admonition-title">Problem</p>
@@ -1682,12 +1692,18 @@ <h3><span class="section-number">2.5.9. </span>Exercises<a class="headerlink" hr
 </pre></div>
 </div>
 </li>
-<li><p>Let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span> and <span class="math notranslate nohighlight">\(c\)</span> be nonnegative real numbers, and suppose that
+<li><p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer.
+Show that there exists an integer <span class="math notranslate nohighlight">\(a\)</span>, such that <span class="math notranslate nohighlight">\(2a^3 &#8805; na+7\)</span>.</p>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">a</span><span class="o">,</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">&#8805;</span> <span class="n">n</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">7</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+</pre></div>
+</div>
+</li>
+<li><p>Let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span> and <span class="math notranslate nohighlight">\(c\)</span> be real numbers, and suppose that
 <span class="math notranslate nohighlight">\(a\le b+c\)</span>, <span class="math notranslate nohighlight">\(b\le a+c\)</span> and <span class="math notranslate nohighlight">\(c\le a+b\)</span>.  Show that there exist nonnegative
 real numbers <span class="math notranslate nohighlight">\(x\)</span>, <span class="math notranslate nohighlight">\(y\)</span> and <span class="math notranslate nohighlight">\(z\)</span> such that <span class="math notranslate nohighlight">\(a=y+z\)</span>, <span class="math notranslate nohighlight">\(b=x+z\)</span> and
 <span class="math notranslate nohighlight">\(c=x+y\)</span>.</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8804;</span> <span class="n">b</span> <span class="bp">+</span> <span class="n">c</span><span class="o">)</span> <span class="o">(</span><span class="n">hb</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">&#8804;</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">c</span><span class="o">)</span> <span class="o">(</span><span class="n">hc</span> <span class="o">:</span> <span class="n">c</span> <span class="bp">&#8804;</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">b</span><span class="o">)</span>
-    <span class="o">(</span><span class="n">ha&#39;</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">a</span><span class="o">)</span> <span class="o">(</span><span class="n">hb&#39;</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">b</span><span class="o">)</span> <span class="o">(</span><span class="n">hc&#39;</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&#8804;</span> <span class="n">c</span><span class="o">)</span> <span class="o">:</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8804;</span> <span class="n">b</span> <span class="bp">+</span> <span class="n">c</span><span class="o">)</span> <span class="o">(</span><span class="n">hb</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">&#8804;</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">c</span><span class="o">)</span> <span class="o">(</span><span class="n">hc</span> <span class="o">:</span> <span class="n">c</span> <span class="bp">&#8804;</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">b</span><span class="o">)</span> <span class="o">:</span>
     <span class="bp">&#8707;</span> <span class="n">x</span> <span class="n">y</span> <span class="n">z</span><span class="o">,</span> <span class="n">x</span> <span class="bp">&#8805;</span> <span class="mi">0</span> <span class="bp">&#8743;</span> <span class="n">y</span> <span class="bp">&#8805;</span> <span class="mi">0</span> <span class="bp">&#8743;</span> <span class="n">z</span> <span class="bp">&#8805;</span> <span class="mi">0</span> <span class="bp">&#8743;</span> <span class="n">a</span> <span class="bp">=</span> <span class="n">y</span> <span class="bp">+</span> <span class="n">z</span> <span class="bp">&#8743;</span> <span class="n">b</span> <span class="bp">=</span> <span class="n">x</span> <span class="bp">+</span> <span class="n">z</span> <span class="bp">&#8743;</span> <span class="n">c</span> <span class="bp">=</span> <span class="n">x</span> <span class="bp">+</span> <span class="n">y</span> <span class="o">:=</span> <span class="kd">by</span>
   <span class="gr">sorry</span>
 </pre></div>

diff --git a/03_Parity_and_Divisibility.html b/03_Parity_and_Divisibility.html
@@ -30,7 +30,7 @@
     <nav data-toggle="wy-nav-shift" class="wy-nav-side">
       <div class="wy-side-scroll">
         <div class="wy-side-nav-search" >
-            <a href="index.html" class="icon icon-home"> The mechanics of proof
+            <a href="index.html" class="icon icon-home"> The Mechanics of Proof
           </a>
 <div role="search">
   <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
@@ -41,7 +41,7 @@
 </div>
         </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
               <ul>
-<li class="toctree-l1"><a class="reference internal" href="00_Introduction.html">Introduction</a></li>
+<li class="toctree-l1"><a class="reference internal" href="00_Introduction.html">Preface</a></li>
 </ul>
 <ul class="current">
 <li class="toctree-l1"><a class="reference internal" href="01_Proofs_by_Calculation.html">1. Proofs by calculation</a></li>
@@ -126,7 +126,7 @@
 
     <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
           <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
-          <a href="index.html">The mechanics of proof</a>
+          <a href="index.html">The Mechanics of Proof</a>
       </nav>
 
       <div class="wy-nav-content">
@@ -1261,6 +1261,15 @@ <h3><span class="section-number">3.4.5. </span>Exercises<a class="headerlink" hr
 </pre></div>
 </div>
 </li>
+<li><p>Let <span class="math notranslate nohighlight">\(a\)</span> be an integer for which <span class="math notranslate nohighlight">\(a\equiv 3\mod 4\)</span>.
+Show that <span class="math notranslate nohighlight">\(a^3+4a^2+2\equiv 1\mod 4\)</span>.</p>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="c">/-</span><span class="cm"> 4 points -/</span>
+<span class="kd">theorem</span> <span class="n">problem4</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">])</span> <span class="o">:</span>
+    <span class="n">a</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">+</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">]</span> <span class="o">:=</span>
+  <span class="gr">sorry</span>
+</pre></div>
+</div>
+</li>
 <li><p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be integers.  Show that <span class="math notranslate nohighlight">\((a + b)^3\equiv a^3+b^3\mod 3\)</span>.</p>
 <div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="n">b</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">&#8801;</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span>
   <span class="gr">sorry</span>
@@ -1273,6 +1282,13 @@ <h3><span class="section-number">3.4.5. </span>Exercises<a class="headerlink" hr
 </pre></div>
 </div>
 </li>
+<li><p>Show that there exists an integer <span class="math notranslate nohighlight">\(k\)</span>, such that <span class="math notranslate nohighlight">\(5k\equiv 6\mod 8\)</span>.</p>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="c">/-</span><span class="cm"> 4 points -/</span>
+<span class="kd">theorem</span> <span class="n">problem5</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">k</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">,</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">&#8801;</span> <span class="mi">6</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">8</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+</pre></div>
+</div>
+</li>
 <li><p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer.  Show that <span class="math notranslate nohighlight">\(5n^2+3n+7\equiv 1\mod 2\)</span>.</p>
 <div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">7</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
   <span class="gr">sorry</span>