Fixing the Algebra section copy paste error

kenmonks · Aug 2, 2024 · 1797e06 · 1797e06
1 parent 7ee1486
commit 1797e06
Show file tree

Hide file tree

Showing 2 changed files with 44 additions and 9 deletions.
diff --git a/help/cicm/cicm-soln.lurch b/help/cicm/cicm-soln.lurch
@@ -4,7 +4,7 @@
                 <script language="javascript">
                     const link = document.querySelector( '#loadlink > p > a' )
                     const thisURL = encodeURIComponent( window.location.href )
-                    link?.setAttribute( 'href', 'http://localhost:2999/instructor.html?load=' + thisURL )
+                    link?.setAttribute( 'href', 'http://localhost:2999/student.html?load=' + thisURL )
                 </script>
             </div>
 
@@ -510,12 +510,31 @@
 </div>
 <hr>
 <ul>
-<li>Similarly, we can add a simple CAS tool to Lurch to check basic algebraic identities (equations only for now).&nbsp;</li>
-<li>Arithmetic in&nbsp;<span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expositorymath&quot;" data-metadata_latex="&quot;\\mathbb{N} &quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__bb">N</span></span></span></span></span>, <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expositorymath&quot;" data-metadata_latex="&quot;\\mathbb{Z} &quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__bb">Z</span></span></span></span></span>, or <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expositorymath&quot;" data-metadata_latex="&quot;\\mathbb{Q}&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__bb">Q</span></span></span></span></span> is available in a Lurch document only if you have a Rule environment in your document or its context like the following.&nbsp; It's usually in the context.&nbsp; (see Other Useful Contexts on the <a href="https://kenmonks.github.io/299-site" target="_blank" rel="noopener">299-site welcome page</a> )</li>
-<li>As with substitution, we explicitly cite 'by arithmetic' following an expression we want to justify using this rule.</li>
+<li>Similarly, we can add a simple CAS tool to Lurch to check basic algebraic identities (equations only, for now).&nbsp;</li>
+<li>The Algebra tool&nbsp;is available in a Lurch document only if you have a Rule environment in your document or its context like the following.&nbsp; It's usually in the context.&nbsp; (see Other Useful Contexts on the <a href="https://kenmonks.github.io/299-site" target="_blank" rel="noopener">299-site welcome page</a> )</li>
 <li>As with arithmetic, we explicitly cite 'by algebra' following an expression we want to justify using this rule.</li>
 </ul>
-<h2>&nbsp;10. Alpha Equivalence</h2>
+<div class="lurch-atom" data-metadata_type="&quot;rule&quot;" data-shell_title="Rule:">
+<p><strong>Algebra Rule:</strong> &nbsp;<span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;AlgebraRule&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__text">AlgebraRule</span></span></span></span></span></p>
+</div>
+<ul>
+<li>This rule is not guaranteed to be robust in the sense that the user may be able to exploit aspects of the CAS to derive contradictions, e.g., it says that this is valid</li>
+</ul>
+<p style="text-align: center;"><span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;z/z=1&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mfrac"><span class="ML__vlist-t ML__vlist-t2"><span class="ML__vlist-r"><span class="ML__vlist" style="height: 0.94em;"><span class="ML__center" style="top: -2.31em;"><span style="height: 0.44em; display: inline-block;"><span class="ML__mathit" style="margin-right: 0.05em;">z</span></span></span><span class="ML__center" style="top: -3.5em;"><span style="height: 0.44em; display: inline-block;"><span class="ML__mathit" style="margin-right: 0.05em;">z</span></span></span></span><span class="ML__vlist-s"></span></span></span></span><span class="ML__cmr">=</span><span class="ML__cmr">1</span></span></span></span></span> <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;by algebra&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__text">by algebra</span></span></span></span></span></p>
+<p style="padding-left: 40px;">&nbsp;without checking that <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expositorymath&quot;" data-metadata_latex="&quot;z&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mathit" style="margin-right: 0.05em;">z</span></span></span></span></span> is nonzero.</p>
+<hr>
+<p><span style="color: rgb(236, 240, 241); background-color: rgb(126, 140, 141);"><strong>&nbsp;Example:&nbsp;</strong></span></p>
+<p>Suppose all variables represent real numbers.&nbsp; Then we can prove the Theorem in the previous Example with a shorter proof if we are allowed to use the Algebra Rule.</p>
+<div class="lurch-atom" data-metadata_type="&quot;proof&quot;" data-shell_title="Proof:">
+<p><strong>Proof:</strong></p>
+<p><span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;Assume m is even, n is even&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__text">Assume </span><span class="ML__mathit">m</span><span class="ML__text"> is even and </span><span class="ML__mathit">n</span><span class="ML__text"> is even</span></span></span></span></span>.&nbsp; Then <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;2|m&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__cmr">2</span><span class="ML__cmr">∣</span><span class="ML__mathit">m</span></span></span></span></span> and <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;2|n&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__cmr">2</span><span class="ML__cmr">∣</span><span class="ML__mathit">n</span></span></span></span></span>. So <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;m=2*k for some k&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mathit">m</span><span class="ML__cmr">=</span><span class="ML__cmr">2</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.04em;">k</span><span class="ML__text"> for some </span><span class="ML__mathit" style="margin-right: 0.04em;">k</span></span></span></span></span> and <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;n=2*j for some j&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mathit">n</span><span class="ML__cmr">=</span><span class="ML__cmr">2</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.06em;">j</span><span class="ML__text"> for some </span><span class="ML__mathit" style="margin-right: 0.06em;">j</span></span></span></span></span>. Thus,&nbsp;</p>
+<p style="text-align: center;"><span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;m*n = (2*k)*n\n    = (2*k)*(2*j)\n    =  4*(k*j)&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mtable"><span class="col-align-r"><span class="ML__vlist-t ML__vlist-t2"><span class="ML__vlist-r"><span class="ML__vlist" style="height: 2.36em;"><span style="top: -4.51em;"><span style="height: 1.5em; display: inline-block;"><span class="ML__mathit">m</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit">n</span></span></span></span><span class="ML__vlist-s"></span></span></span></span><span class="col-align-l"><span class="ML__vlist-t ML__vlist-t2"><span class="ML__vlist-r"><span class="ML__vlist" style="height: 2.36em;"><span style="top: -4.51em;"><span style="height: 1.5em; display: inline-block;"><span class="ML__cmr">=</span><span class="ML__left-right" style="margin-top: 0em; height: 0.69444em;"><span class="ML__small-delim ML__open">(</span><span class="ML__cmr">2</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.04em;">k</span><span class="ML__small-delim ML__close">)</span></span><span class="ML__cmr">&sdot;</span><span class="ML__mathit">n</span></span></span><span style="top: -3.01em;"><span style="height: 1.5em; display: inline-block;"><span class="ML__cmr">=</span><span class="ML__left-right" style="margin-top: 0em; height: 0.69444em;"><span class="ML__small-delim ML__open">(</span><span class="ML__cmr">2</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.04em;">k</span><span class="ML__small-delim ML__close">)</span></span><span class="ML__cmr">&sdot;</span><span class="ML__left-right" style="margin-top: -0.19444em; height: 0.85396em;"><span class="ML__small-delim ML__open">(</span><span class="ML__cmr">2</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.06em;">j</span><span class="ML__small-delim ML__close">)</span></span></span></span><span style="top: -1.51em;"><span style="height: 1.2em; display: inline-block;"><span class="ML__cmr">=</span><span class="ML__cmr">4</span><span class="ML__cmr">&sdot;</span><span class="ML__left-right" style="margin-top: -0.19444em; height: 0.8888799999999999em;"><span class="ML__small-delim ML__open">(</span><span class="ML__mathit" style="margin-right: 0.04em;">k</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.06em;">j</span><span class="ML__small-delim ML__close">)</span></span></span></span></span><span class="ML__vlist-s"></span></span></span></span></span></span></span></span></span></p>
+<p>&nbsp;</p>
+<p>since&nbsp;<span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;(2*k)*(2*j)=4*(k*j)&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__left-right" style="margin-top: 0em; height: 0.69444em;"><span class="ML__small-delim ML__open">(</span><span class="ML__cmr">2</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.04em;">k</span><span class="ML__small-delim ML__close">)</span></span><span class="ML__cmr">&sdot;</span><span class="ML__left-right" style="margin-top: -0.19444em; height: 0.85396em;"><span class="ML__small-delim ML__open">(</span><span class="ML__cmr">2</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.06em;">j</span><span class="ML__small-delim ML__close">)</span></span><span class="ML__cmr">=</span><span class="ML__cmr">4</span><span class="ML__cmr">&sdot;</span><span class="ML__left-right" style="margin-top: -0.19444em; height: 0.8888799999999999em;"><span class="ML__small-delim ML__open">(</span><span class="ML__mathit" style="margin-right: 0.04em;">k</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.06em;">j</span><span class="ML__small-delim ML__close">)</span></span></span></span></span></span> <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;by algebra&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__text">by algebra</span></span></span></span></span>. So <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;4|m*n&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__cmr">4</span><span class="ML__cmr">∣</span><span class="ML__mathit">m</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit">n</span></span></span></span></span>.&nbsp;</p>
+<p><span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expositorymath&quot;" data-metadata_latex="&quot;\\square&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__ams">□</span></span></span></span></span></p>
+</div>
+<hr>
+<h2>10. Alpha Equivalence</h2>
 <ul>
 <li>Lurch does have <em>binding expressions</em> of the form <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;x.Q(x)&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mathit">x</span><span class="ML__cmr">.</span><span class="ML__mathit">Q</span><span class="ML__left-right" style="margin-top: 0em; height: 0.43056em;"><span class="ML__small-delim ML__open">(</span><span class="ML__mathit">x</span><span class="ML__small-delim ML__close">)</span></span></span></span></span></span> where <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expositorymath&quot;" data-metadata_latex="&quot;x&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mathit">x</span></span></span></span></span> is&nbsp;<em>bound</em> to the expression itself.&nbsp;</li>
 <li>Alpha-equivalent expressions are treated as the same thing for validation.</li>

diff --git a/help/cicm/cicm.lurch b/help/cicm/cicm.lurch
@@ -4,7 +4,7 @@
                 <script language="javascript">
                     const link = document.querySelector( '#loadlink > p > a' )
                     const thisURL = encodeURIComponent( window.location.href )
-                    link?.setAttribute( 'href', 'http://localhost:2999/instructor.html?load=' + thisURL )
+                    link?.setAttribute( 'href', 'http://localhost:2999/student.html?load=' + thisURL )
                 </script>
             </div>
 
@@ -489,11 +489,27 @@
 <hr>
 <ul>
 <li>Similarly, we can add a simple CAS tool to Lurch to check basic algebraic identities (equations only for now).&nbsp;</li>
-<li>Arithmetic in&nbsp;<span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expositorymath&quot;" data-metadata_latex="&quot;\\mathbb{N} &quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__bb">N</span></span></span></span></span>, <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expositorymath&quot;" data-metadata_latex="&quot;\\mathbb{Z} &quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__bb">Z</span></span></span></span></span>, or <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expositorymath&quot;" data-metadata_latex="&quot;\\mathbb{Q}&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__bb">Q</span></span></span></span></span> is available in a Lurch document only if you have a Rule environment in your document or its context like the following.&nbsp; It's usually in the context.&nbsp; (see Other Useful Contexts on the <a href="https://kenmonks.github.io/299-site" target="_blank" rel="noopener">299-site welcome page</a> )</li>
-<li>As with substitution, we explicitly cite 'by arithmetic' following an expression we want to justify using this rule.</li>
+<li>The Algebra tool&nbsp;is available in a Lurch document only if you have a Rule environment in your document or its context like the following.&nbsp; It's usually in the context.&nbsp; (see Other Useful Contexts on the <a href="https://kenmonks.github.io/299-site" target="_blank" rel="noopener">299-site welcome page</a> )</li>
 <li>As with arithmetic, we explicitly cite 'by algebra' following an expression we want to justify using this rule.</li>
 </ul>
-<h2>&nbsp;10. Alpha Equivalence</h2>
+<div class="lurch-atom" data-metadata_type="&quot;rule&quot;" data-shell_title="Rule:">
+<p><strong>Algebra Rule:</strong> &nbsp;<span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;AlgebraRule&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__text">AlgebraRule</span></span></span></span></span></p>
+</div>
+<ul>
+<li>This rule is not guaranteed to be robust in the sense that the user may be able to exploit aspects of the CAS to derive contradictions, e.g., it says that this is valid</li>
+</ul>
+<p style="text-align: center;"><span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;z/z=1&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mfrac"><span class="ML__vlist-t ML__vlist-t2"><span class="ML__vlist-r"><span class="ML__vlist" style="height: 0.94em;"><span class="ML__center" style="top: -2.31em;"><span style="height: 0.44em; display: inline-block;"><span class="ML__mathit" style="margin-right: 0.05em;">z</span></span></span><span class="ML__center" style="top: -3.5em;"><span style="height: 0.44em; display: inline-block;"><span class="ML__mathit" style="margin-right: 0.05em;">z</span></span></span></span><span class="ML__vlist-s"></span></span></span></span><span class="ML__cmr">=</span><span class="ML__cmr">1</span></span></span></span></span> <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;by algebra&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__text">by algebra</span></span></span></span></span></p>
+<p style="padding-left: 40px;">&nbsp;without checking that <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expositorymath&quot;" data-metadata_latex="&quot;z&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mathit" style="margin-right: 0.05em;">z</span></span></span></span></span> is nonzero.</p>
+<hr>
+<p><span style="color: rgb(236, 240, 241); background-color: rgb(126, 140, 141);"><strong>&nbsp;Example:&nbsp;</strong></span></p>
+<p>Suppose all variables represent real numbers.&nbsp; Then we can prove the Theorem in the previous Example with a shorter proof if we are allowed to use the Algebra Rule.</p>
+<div class="lurch-atom" data-metadata_type="&quot;proof&quot;" data-shell_title="Proof:">
+<p><strong>Proof:</strong></p>
+<p>&nbsp;</p>
+<p><span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expositorymath&quot;" data-metadata_latex="&quot;\\square&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__ams">□</span></span></span></span></span></p>
+</div>
+<hr>
+<h2>10. Alpha Equivalence</h2>
 <ul>
 <li>Lurch does have <em>binding expressions</em> of the form <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;x.Q(x)&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mathit">x</span><span class="ML__cmr">.</span><span class="ML__mathit">Q</span><span class="ML__left-right" style="margin-top: 0em; height: 0.43056em;"><span class="ML__small-delim ML__open">(</span><span class="ML__mathit">x</span><span class="ML__small-delim ML__close">)</span></span></span></span></span></span> where <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expositorymath&quot;" data-metadata_latex="&quot;x&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mathit">x</span></span></span></span></span> is&nbsp;<em>bound</em> to the expression itself.&nbsp;</li>
 <li>Alpha-equivalent expressions are treated as the same thing for validation.</li>