Update Tue Jul 12 14:35:34 EDT 2022

02_Using_Polyrith.html

@@ -78,6 +78,11 @@
 
   <section id="using-polyrith">
 <span id="id1"></span><h1><span class="section-number">2. </span>Using polyrith<a class="headerlink" href="#using-polyrith" title="Permalink to this headline">&#61633;</a></h1>
+<p>This section and <a class="reference internal" href="03_Nonsingularity_of_Curves.html#projective-curves"><span class="std std-ref">the next</span></a> can be read independently. They present a
+series of extended examples, showing how to transform problems into nails which the <code class="docutils literal notranslate"><span class="pre">polyrith</span></code>
+hammer can hit.</p>
+<p>The focus in this section is on making sure that <code class="docutils literal notranslate"><span class="pre">polyrith</span></code> has all the hypotheses it needs to
+solve a problem.</p>
 <section id="chebyshev-polynomials">
 <span id="chebyshev"></span><h2><span class="section-number">2.1. </span>Chebyshev polynomials<a class="headerlink" href="#chebyshev-polynomials" title="Permalink to this headline">&#61633;</a></h2>
 <p>The Chebyshev polynomials (of the first kind) are a sequence of polynomials <span class="math notranslate nohighlight">\(T_n(x)\)</span> defined
@@ -196,7 +201,7 @@
 right factor vanishes).</p>
 <p>We present the skeleton of this argument in Lean below, with the exercise indicated above left as a
 sorry.  A tricky point is that <code class="docutils literal notranslate"><span class="pre">linear_combination</span></code>/<code class="docutils literal notranslate"><span class="pre">polyrith</span></code>
-does not know facts specific to the ring of complex numbers, such as that <span class="math notranslate nohighlight">\(i^2=1\)</span> or that
+does not know facts specific to the ring of complex numbers, such as that <span class="math notranslate nohighlight">\(i^2=-1\)</span> or that
 <span class="math notranslate nohighlight">\(\overline{i}=-i\)</span>.  You can state any needed such facts explicitly and prove them using
 <code class="docutils literal notranslate"><span class="pre">norm_num</span></code> (of course, there are lemmas for this, but why bother memorizing them?).  Then you can
 rewrite by these facts, or just include them in the context for <code class="docutils literal notranslate"><span class="pre">polyrith</span></code> to pick up.</p>

03_Nonsingularity_of_Curves.html

@@ -194,8 +194,14 @@
 </section>
 <section id="weierstrass-form-elliptic-curve">
 <span id="weierstrass"></span><h2><span class="section-number">3.3. </span>Weierstrass-form elliptic curve<a class="headerlink" href="#weierstrass-form-elliptic-curve" title="Permalink to this headline">&#61633;</a></h2>
-<p>Next, we consider an elliptic curve in Weierstrass normal form <span class="math notranslate nohighlight">\(zy^2 = x^3 + pxz^2 + qz^3\)</span>.
-We fix the parameters <span class="math notranslate nohighlight">\(p\)</span> and <span class="math notranslate nohighlight">\(q\)</span> explicitly.</p>
+<p>Next, we consider an elliptic curve in Weierstrass normal form <span class="math notranslate nohighlight">\(zy^2 = x^3 + pxz^2 + qz^3\)</span>.</p>
+<figure class="align-default" id="id2">
+<a class="reference internal image-reference" href="_images/cubic.png"><img alt="a Weierstrass-normal-form elliptic curve" src="_images/cubic.png" style="width: 320.0px; height: 320.0px;" /></a>
+<figcaption>
+<p><span class="caption-number">Fig. 3.2 </span><span class="caption-text">A Weierstrass-normal-form elliptic curve with positive discriminant.</span><a class="headerlink" href="#id2" title="Permalink to this image">&#61633;</a></p>
+</figcaption>
+</figure>
+<p>We fix the parameters <span class="math notranslate nohighlight">\(p\)</span> and <span class="math notranslate nohighlight">\(q\)</span> explicitly.</p>
 <div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variables</span> <span class="o">(</span><span class="n">p</span> <span class="n">q</span> <span class="o">:</span> <span class="n">K</span><span class="o">)</span>
 </pre></div>
 </div>

04_Combining_Tactics.html

@@ -44,7 +44,7 @@
 <li class="toctree-l1"><a class="reference internal" href="02_Using_Polyrith.html">2. Using polyrith</a></li>
 <li class="toctree-l1"><a class="reference internal" href="03_Nonsingularity_of_Curves.html">3. Nonsingularity of algebraic curves</a></li>
 <li class="toctree-l1 current"><a class="current reference internal" href="#">4. Combining tactics</a><ul>
-<li class="toctree-l2"><a class="reference internal" href="#basics-of-field-simp">4.1. Basics of field_simp</a></li>
+<li class="toctree-l2"><a class="reference internal" href="#basics-of-the-field-simp-tactic">4.1. Basics of the field_simp tactic</a></li>
 <li class="toctree-l2"><a class="reference internal" href="#stereographic-projection">4.2. Stereographic projection</a></li>
 <li class="toctree-l2"><a class="reference internal" href="#a-binomial-coefficient-identity">4.3. A binomial coefficient identity</a></li>
 </ul>
@@ -86,8 +86,8 @@
 (<span class="math notranslate nohighlight">\(\mathbb{N}\)</span>, <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>, <span class="math notranslate nohighlight">\(\mathbb{Q}\)</span>, <span class="math notranslate nohighlight">\(\mathbb{R}\)</span>,
 <span class="math notranslate nohighlight">\(\mathbb{C}\)</span>) and with <code class="docutils literal notranslate"><span class="pre">(n)linarith</span></code> (to prove inequalities).  But we will not give a
 detailed description of these other tactics.</p>
-<section id="basics-of-field-simp">
-<span id="field-simp"></span><h2><span class="section-number">4.1. </span>Basics of field_simp<a class="headerlink" href="#basics-of-field-simp" title="Permalink to this headline">&#61633;</a></h2>
+<section id="basics-of-the-field-simp-tactic">
+<span id="field-simp"></span><h2><span class="section-number">4.1. </span>Basics of the field_simp tactic<a class="headerlink" href="#basics-of-the-field-simp-tactic" title="Permalink to this headline">&#61633;</a></h2>
 <p>Let us turn to <code class="docutils literal notranslate"><span class="pre">field_simp</span></code>.  Given a ring expression with division or inversion, this tactic
 will clear any denominators for which there is a proof in context that that denominator is nonzero.</p>
 <p>Here is an example: we prove that if <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> are rational numbers, with <span class="math notranslate nohighlight">\(a\)</span>
@@ -100,7 +100,11 @@
 <span class="kd">end</span>
 </pre></div>
 </div>
-<p>In the following problem we prove that the unit circle admits a rational parametrization.  Notice
+<p>In the following problem we prove that the unit circle admits a rational parametrization:</p>
+<div class="math notranslate nohighlight">
+\[\left(\frac{m ^ 2 - n ^ 2} {m ^ 2 + n ^ 2}\right) ^ 2
++ \left(\frac{2 m n} {m ^ 2 + n ^ 2}\right) ^ 2 = 1.\]</div>
+<p>Notice
 the use of contraposition and of <code class="docutils literal notranslate"><span class="pre">(n)linarith</span></code> in proving the nonzeroness hypothesis; these are
 both common ingredients. Again, check that if you comment out the justification that
 <span class="math notranslate nohighlight">\(m ^ 2 + n ^ 2 \ne 0\)</span>, then <code class="docutils literal notranslate"><span class="pre">field_simp</span></code> fails to trigger.</p>

_sources/02_Using_Polyrith.rst.txt

@@ -3,6 +3,14 @@
 Using polyrith
 ==============
 
+This section and :ref:`the next<projective_curves>` can be read independently. They present a
+series of extended examples, showing how to transform problems into nails which the ``polyrith``
+hammer can hit.
+
+The focus in this section is on making sure that ``polyrith`` has all the hypotheses it needs to
+solve a problem.
+
+
 .. include:: 02_Using_Polyrith/01_chebyshev.inc
 .. include:: 02_Using_Polyrith/02_isometry_plane.inc
 .. include:: 02_Using_Polyrith/03_double_cover.inc

index.html

@@ -109,7 +109,7 @@ <h1>Algebraic computations in Lean<a class="headerlink" href="#algebraic-computa
 </ul>
 </li>
 <li class="toctree-l1"><a class="reference internal" href="04_Combining_Tactics.html">4. Combining tactics</a><ul>
-<li class="toctree-l2"><a class="reference internal" href="04_Combining_Tactics.html#basics-of-field-simp">4.1. Basics of field_simp</a></li>
+<li class="toctree-l2"><a class="reference internal" href="04_Combining_Tactics.html#basics-of-the-field-simp-tactic">4.1. Basics of the field_simp tactic</a></li>
 <li class="toctree-l2"><a class="reference internal" href="04_Combining_Tactics.html#stereographic-projection">4.2. Stereographic projection</a></li>
 <li class="toctree-l2"><a class="reference internal" href="04_Combining_Tactics.html#a-binomial-coefficient-identity">4.3. A binomial coefficient identity</a></li>
 </ul>