Skip to content

Commit

Permalink
Update Tue May 28 13:50:41 BST 2024
Browse files Browse the repository at this point in the history
  • Loading branch information
hrmacbeth committed May 28, 2024
1 parent 8bac760 commit cc55e52
Show file tree
Hide file tree
Showing 29 changed files with 1,640 additions and 14,377 deletions.
2 changes: 1 addition & 1 deletion .buildinfo
Original file line number Diff line number Diff line change
@@ -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: c5e3947f188c725080936ed2a1d1817e
config: 8d0cd22182f16ceb0046adb6c9422902
tags: 645f666f9bcd5a90fca523b33c5a78b7
196 changes: 99 additions & 97 deletions 01_Basics_of_Polyrith.html

Large diffs are not rendered by default.

302 changes: 165 additions & 137 deletions 02_Using_Polyrith.html

Large diffs are not rendered by default.

267 changes: 153 additions & 114 deletions 03_Nonsingularity_of_Curves.html

Large diffs are not rendered by default.

297 changes: 149 additions & 148 deletions 04_Combining_Tactics.html

Large diffs are not rendered by default.

6 changes: 3 additions & 3 deletions _sources/01_Basics_of_Polyrith.rst.txt
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,6 @@ Lean files. This will let you see the goal state of the Lean code and do the ex
Head over to the tutorial's GitHub repository, https://github.com/hrmacbeth/computations_in_lean,
to download the repository to your own computer or to open it in the cloud on Gitpod.

.. include:: 01_Basics_of_Polyrith/02_linear_combination.inc
.. include:: 01_Basics_of_Polyrith/03_nonlinear_examples.inc
.. include:: 01_Basics_of_Polyrith/04_polyrith.inc
.. include:: 01_Basics_of_Polyrith/02LinearCombination.inc
.. include:: 01_Basics_of_Polyrith/03NonlinearExamples.inc
.. include:: 01_Basics_of_Polyrith/04Polyrith.inc
6 changes: 3 additions & 3 deletions _sources/02_Using_Polyrith.rst.txt
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,6 @@ The focus in this section is on making sure that ``polyrith`` has all the hypoth
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
.. include:: 02_Using_Polyrith/01Chebyshev.inc
.. include:: 02_Using_Polyrith/02IsometryPlane.inc
.. include:: 02_Using_Polyrith/03DoubleCover.inc
4 changes: 2 additions & 2 deletions _sources/03_Nonsingularity_of_Curves.rst.txt
Original file line number Diff line number Diff line change
Expand Up @@ -3,5 +3,5 @@
Nonsingularity of algebraic curves
==================================

.. include:: 03_Nonsingularity_of_Curves/01_powers_case_splits.inc
.. include:: 03_Nonsingularity_of_Curves/02_projective_curves.inc
.. include:: 03_Nonsingularity_of_Curves/01PowersCaseSplits.inc
.. include:: 03_Nonsingularity_of_Curves/02ProjectiveCurves.inc
21 changes: 7 additions & 14 deletions _sources/04_Combining_Tactics.rst.txt
Original file line number Diff line number Diff line change
Expand Up @@ -3,19 +3,12 @@
Combining tactics
=================

In this last section we cover examples where several tactics need to be combined to complete a
computation.
In this last section we cover examples involving division.
The key tactic here is called ``field_simp``:
it clears denominators of fractions,
which gets us back to a setting in which ``ring`` or ``polyrith`` can be applied.

We will start with a discussion of the tactic ``field_simp``, which is used in working with
fractions; it clears denominators so that ``ring`` or ``polyrith`` can be applied.

Later we will give two extended examples in which ``polyrith`` and ``field_simp`` are combined as
needed with ``norm_cast`` (and variants), to deal with casts among different number systems
(:math:`\mathbb{N}`, :math:`\mathbb{Z}`, :math:`\mathbb{Q}`, :math:`\mathbb{R}`,
:math:`\mathbb{C}`) and with ``(n)linarith`` (to prove inequalities). But we will not give a
detailed description of these other tactics.


.. include:: 04_Combining_Tactics/01_field_simp.inc
.. include:: 04_Combining_Tactics/02_sphere.inc
.. include:: 04_Combining_Tactics/03_binomial.inc
.. include:: 04_Combining_Tactics/01FieldSimp.inc
.. include:: 04_Combining_Tactics/02Sphere.inc
.. include:: 04_Combining_Tactics/03Binomial.inc
28 changes: 18 additions & 10 deletions _sources/index.rst.txt
Original file line number Diff line number Diff line change
Expand Up @@ -4,26 +4,33 @@ Algebraic computations in Lean
==============================

This is a tutorial on doing proofs with a computational flavour using the
`mathlib <https://github.com/leanprover-community/mathlib>`_ library for the
`Lean 3 <https://leanprover.github.io/>`_ proof assistant.
`Mathlib <https://github.com/leanprover-community/mathlib4>`_ library for the
`Lean <https://leanprover.github.io/>`_ proof assistant.

The phrase "computational flavour" might need some explanation. These are not heavy computations
that require two hours running Mathematica, but simply the kind of mildly-painful calculation that
might take a couple of paragraphs on paper.

Currently the tutorial focuses on the brand new tactic ``polyrith`` and on ``field_simp``. There
are several other powerful tactics which are commonly needed for "computational" proofs, notably
``norm_num``, ``norm_cast`` (and variants), and ``(n)linarith``. These other tactics are discussed
in context as the need arises, but this tutorial might eventually be extended to cover them too.
The tutorial focuses on the Gröbner basis tactic ``polyrith``
and on the division-cancelling tactic ``field_simp``.
There are several other powerful tactics which are commonly needed for "computational" proofs,
notably ``norm_num``, ``norm_cast`` (and variants), ``(n)linarith`` and ``gcongr``.
These other tactics are discussed in context as the need arises.

This is an intermediate-level tutorial, requiring familiarity with the syntax of Lean as covered in
approximately the first two chapters of `Mathematics in Lean
<https://leanprover-community.github.io/mathematics_in_lean/>`_. But the focus of the exercises and
presentation is on the computations, so don't worry about understanding every detail of the syntax
if you can pick up the general idea.

This tutorial is new (July 2022) and feedback is very welcome. If you try this tutorial, come to
the Lean chat room on `Zulip <https://leanprover.zulipchat.com/>`_ and say hello!
This tutorial was originally written in Lean 3 in July 2022 when ``polyrith`` first appeared.
A video of a talk at `ICERM <https://icerm.brown.edu/>`_ following that version of the tutorial
is available in `ICERM's video database <https://icerm.brown.edu/video_archive/?play=2896>`_.
The update to Lean 4 was posted in May 2024.

Feedback is very welcome.
Email me (`Heather Macbeth <https://faculty.fordham.edu/hmacbeth1/>`_),
or come to the Lean chat room on `Zulip <https://leanprover.zulipchat.com/>`_ and say hello!

.. toctree::
:numbered:
Expand All @@ -34,7 +41,8 @@ the Lean chat room on `Zulip <https://leanprover.zulipchat.com/>`_ and say hello
03_Nonsingularity_of_Curves
04_Combining_Tactics

**Acknowledgements:** I have raided the mathlib contributions of a number of people for examples in
**Acknowledgements:** I have raided the Mathlib contributions of a number of people for examples in
this tutorial. Thank you to Johan Commelin, Julian Külshammer and François
Sunatori! And particular thanks to Jeremy Avigad, for sharing the Sphinx template for the tutorial,
Sunatori! And particular thanks to Jeremy Avigad, for sharing the Sphinx template for the tutorial;
Marc Masdeu and Patrick Massot, for work on the bump to Lean 4;
and Rob Lewis, for many conversations about automation in Lean.
123 changes: 123 additions & 0 deletions _static/_sphinx_javascript_frameworks_compat.js
Original file line number Diff line number Diff line change
@@ -0,0 +1,123 @@
/* Compatability shim for jQuery and underscores.js.
*
* Copyright Sphinx contributors
* Released under the two clause BSD licence
*/

/**
* small helper function to urldecode strings
*
* See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/decodeURIComponent#Decoding_query_parameters_from_a_URL
*/
jQuery.urldecode = function(x) {
if (!x) {
return x
}
return decodeURIComponent(x.replace(/\+/g, ' '));
};

/**
* small helper function to urlencode strings
*/
jQuery.urlencode = encodeURIComponent;

/**
* This function returns the parsed url parameters of the
* current request. Multiple values per key are supported,
* it will always return arrays of strings for the value parts.
*/
jQuery.getQueryParameters = function(s) {
if (typeof s === 'undefined')
s = document.location.search;
var parts = s.substr(s.indexOf('?') + 1).split('&');
var result = {};
for (var i = 0; i < parts.length; i++) {
var tmp = parts[i].split('=', 2);
var key = jQuery.urldecode(tmp[0]);
var value = jQuery.urldecode(tmp[1]);
if (key in result)
result[key].push(value);
else
result[key] = [value];
}
return result;
};

/**
* highlight a given string on a jquery object by wrapping it in
* span elements with the given class name.
*/
jQuery.fn.highlightText = function(text, className) {
function highlight(node, addItems) {
if (node.nodeType === 3) {
var val = node.nodeValue;
var pos = val.toLowerCase().indexOf(text);
if (pos >= 0 &&
!jQuery(node.parentNode).hasClass(className) &&
!jQuery(node.parentNode).hasClass("nohighlight")) {
var span;
var isInSVG = jQuery(node).closest("body, svg, foreignObject").is("svg");
if (isInSVG) {
span = document.createElementNS("http://www.w3.org/2000/svg", "tspan");
} else {
span = document.createElement("span");
span.className = className;
}
span.appendChild(document.createTextNode(val.substr(pos, text.length)));
node.parentNode.insertBefore(span, node.parentNode.insertBefore(
document.createTextNode(val.substr(pos + text.length)),
node.nextSibling));
node.nodeValue = val.substr(0, pos);
if (isInSVG) {
var rect = document.createElementNS("http://www.w3.org/2000/svg", "rect");
var bbox = node.parentElement.getBBox();
rect.x.baseVal.value = bbox.x;
rect.y.baseVal.value = bbox.y;
rect.width.baseVal.value = bbox.width;
rect.height.baseVal.value = bbox.height;
rect.setAttribute('class', className);
addItems.push({
"parent": node.parentNode,
"target": rect});
}
}
}
else if (!jQuery(node).is("button, select, textarea")) {
jQuery.each(node.childNodes, function() {
highlight(this, addItems);
});
}
}
var addItems = [];
var result = this.each(function() {
highlight(this, addItems);
});
for (var i = 0; i < addItems.length; ++i) {
jQuery(addItems[i].parent).before(addItems[i].target);
}
return result;
};

/*
* backward compatibility for jQuery.browser
* This will be supported until firefox bug is fixed.
*/
if (!jQuery.browser) {
jQuery.uaMatch = function(ua) {
ua = ua.toLowerCase();

var match = /(chrome)[ \/]([\w.]+)/.exec(ua) ||
/(webkit)[ \/]([\w.]+)/.exec(ua) ||
/(opera)(?:.*version|)[ \/]([\w.]+)/.exec(ua) ||
/(msie) ([\w.]+)/.exec(ua) ||
ua.indexOf("compatible") < 0 && /(mozilla)(?:.*? rv:([\w.]+)|)/.exec(ua) ||
[];

return {
browser: match[ 1 ] || "",
version: match[ 2 ] || "0"
};
};
jQuery.browser = {};
jQuery.browser[jQuery.uaMatch(navigator.userAgent).browser] = true;
}
Loading

0 comments on commit cc55e52

Please sign in to comment.