Update Tue May 28 13:50:39 BST 2024

.docker/gitpod/Dockerfile

@@ -0,0 +1,37 @@
+# This is the Dockerfile for `leanprovercommunity/mathlib:gitpod`.
+
+# gitpod doesn't support multiple FROM statements, (or rather, you can't copy from one to another)
+# so we just install everything in one go
+FROM ubuntu:jammy
+
+USER root
+
+RUN apt-get update && apt-get install sudo git curl git bash-completion -y && apt-get clean
+
+RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
+    # passwordless sudo for users in the 'sudo' group
+    && sed -i.bkp -e 's/%sudo\s\+ALL=(ALL\(:ALL\)\?)\s\+ALL/%sudo ALL=NOPASSWD:ALL/g' /etc/sudoers
+USER gitpod
+WORKDIR /home/gitpod
+
+SHELL ["/bin/bash", "-c"]
+
+# gitpod bash prompt
+RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[00m\]\$(__git_ps1 \" (%s)\") $ '" ; } >> .bashrc
+
+# install elan
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+# install whichever toolchain mathlib is currently using
+RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/hrmacbeth/computations_in_lean/main/lean-toolchain)
+
+ENV PATH="/home/gitpod/.local/bin:/home/gitpod/.elan/bin:${PATH}"
+
+# fix the infoview when the container is used on gitpod:
+ENV VSCODE_API_VERSION="1.50.0"
+
+# ssh to github once to bypass the unknown fingerprint warning
+RUN ssh -o StrictHostKeyChecking=no github.com || true
+
+# run sudo once to suppress usage info
+RUN sudo echo finished

.gitignore

@@ -1,4 +1,5 @@
 /.vscode
 *.olean
 /_target
+/.lake/
 /leanpkg.path

PolyrithTutorial.lean

@@ -0,0 +1,11 @@
+import PolyrithTutorial.«01_Basics_of_Polyrith».«02LinearCombination»
+import PolyrithTutorial.«01_Basics_of_Polyrith».«03NonlinearExamples»
+import PolyrithTutorial.«01_Basics_of_Polyrith».«04Polyrith»
+import PolyrithTutorial.«02_Using_Polyrith».«01Chebyshev»
+import PolyrithTutorial.«02_Using_Polyrith».«02IsometryPlane»
+import PolyrithTutorial.«02_Using_Polyrith».«03DoubleCover»
+import PolyrithTutorial.«03_Nonsingularity_Of_Curves».«01PowersCaseSplits»
+import PolyrithTutorial.«03_Nonsingularity_Of_Curves».«02ProjectiveCurves»
+import PolyrithTutorial.«04_Combining_Tactics».«01FieldSimp»
+import PolyrithTutorial.«04_Combining_Tactics».«02Sphere»
+import PolyrithTutorial.«04_Combining_Tactics».«03Binomial»

PolyrithTutorial/01_Basics_of_Polyrith/02LinearCombination.lean

@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2022 Heather Macbeth. All rights reserved.
+Authors: Heather Macbeth
+-/
+import Mathlib.Data.Complex.Basic
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.LinearCombination
+
+
+/-! # Section 1.2: Basics of the linear_combination tactic
+
+This file should be worked through in parallel with the corresponding section of the tutorial:
+https://hrmacbeth.github.io/computations_in_lean/01_Basics_of_Polyrith.html#basics-of-the-linear-combination-tactic
+
+I recommend splitting your screen to display the code and the tutorial side by side! -/
+
+
+example {a b : ℂ} (h₁ : a - 5 * b = 4) (h₂ : b + 2 = 3) : a = 9 :=
+  calc
+    a = a - 5 * b + 5 * b := by ring
+    _ = 4 + 5 * b := by rw [h₁]
+    _ = -6 + 5 * (b + 2) := by ring
+    _ = -6 + 5 * 3 := by rw [h₂]
+    _ = 9 := by ring
+
+
+example {a b : ℝ} (h₁ : a - 5 * b = 4) (h₂ : b + 2 = 3) : a = 9 := by linarith
+
+
+example {a b : ℂ} (h₁ : a - 5 * b = 4) (h₂ : b + 2 = 3) : a = 9 := by
+  linear_combination h₁ + 5 * h₂
+
+
+example {m n : ℤ} (h : m - n = 0) : m = n := by linear_combination h
+
+
+example {K : Type*} [Field K] [CharZero K] {s : K} (hs : 3 * s + 1 = 4) : s = 1 := by
+  linear_combination 1 / 3 * hs
+
+
+example {p q : ℂ} (h₁ : p + 2 * q = 4) (h₂ : p - 2 * q = 2) : 2 * p = 6 := by
+  linear_combination h₁ + h₂
+
+
+/-! # Exercises -/
+
+
+example {x y : ℤ} (h₁ : 2 * x + y = 4) (h₂ : x + y = 1) : x = 3 := by
+  sorry
+
+example {r s : ℝ} (h₁ : r + 2 * s = -1) (h₂ : s = 3) : r = -7 := by
+  sorry
+
+example {c : ℚ} (h₁ : 4 * c + 1 = 3 * c - 2) : c = -3 := by
+  sorry
+
+example {x y : ℤ} (h₁ : x - 3 * y = 5) (h₂ : y = 3) : x = 14 := by
+  sorry
+
+example {x y : ℤ} (h₁ : 2 * x - y = 4) (h₂ : y - x + 1 = 2) : x = 5 := by
+  sorry
+
+example {x y : ℝ} (h₁ : x = 3) (h₂ : y = 4 * x - 3) : y = 9 := by
+  sorry
+
+example {a b c : ℝ} (h₁ : a + 2 * b + 3 * c = 7) (h₂ : b + 2 * c = 3) (h₃ : c = 1) :
+    a = 2 := by
+  sorry
+
+example {a b : ℝ} (h₁ : a + 2 * b = 4) (h₂ : a - b = 1) : a = 2 := by
+  sorry
+
+example {u v : ℚ} (h₁ : u + 2 * v = 4) (h₂ : u - 2 * v = 6) : u = 5 := by
+  sorry
+
+example {u v : ℚ} (h₁ : 4 * u + v = 3) (h₂ : v = 2) : u = 1 / 4 := by
+  sorry

src/01_Basics_of_Polyrith/03_nonlinear_examples.lean → PolyrithTutorial/01_Basics_of_Polyrith/03NonlinearExamples.lean

@@ -2,40 +2,45 @@
 Copyright (c) 2022 Heather Macbeth. All rights reserved.
 Authors: Heather Macbeth
 -/
-import data.complex.basic
-import tactic.polyrith
+import Mathlib.Data.Complex.Basic
+import Mathlib.Tactic.LinearCombination
 
 
-example {x y z w : ℂ} (h₁ : x * z = y ^ 2) (h₂ : y * w = z ^ 2) : z * (x * w - y * z) = 0 :=
-by linear_combination w * h₁ + y * h₂
+example {x y z w : ℂ} (h₁ : x * z = y ^ 2) (h₂ : y * w = z ^ 2) :
+    z * (x * w - y * z) = 0 := by
+  linear_combination w * h₁ + y * h₂
 
 
-example {a b : ℚ} (h : a = b) : a ^ 2 = b ^ 2 :=
-by linear_combination (a + b) * h
+example {a b : ℚ} (h : a = b) : a ^ 2 = b ^ 2 := by linear_combination (a + b) * h
 
 
-example {a b : ℚ} (h : a = b) : a ^ 3 = b ^ 3 :=
-by linear_combination (a ^ 2 + a * b + b ^ 2) * h
+example {a b : ℚ} (h : a = b) : a ^ 3 = b ^ 3 := by
+  linear_combination (a ^ 2 + a * b + b ^ 2) * h
 
-example (m n : ℤ) : (m ^ 2 - n ^ 2) ^ 2 + (2 * m * n) ^ 2 = (m ^ 2 + n ^ 2) ^ 2 :=
-by { linear_combination }
 
-example {x y : ℝ} (h₁ : x + 3 = 5) (h₂ : 2 * x - y * x = 0) : y = 2 :=
-sorry
+example (m n : ℤ) : (m ^ 2 - n ^ 2) ^ 2 + (2 * m * n) ^ 2 = (m ^ 2 + n ^ 2) ^ 2 := by
+  linear_combination
 
-example {x y : ℝ} (h₁ : x - y = 4) (h₂ : x * y = 1) : (x + y) ^ 2 = 20 :=
-sorry
+
+/-! # Exercises -/
+
+
+example {x y : ℝ} (h₁ : x + 3 = 5) (h₂ : 2 * x - y * x = 0) : y = 2 := by
+  sorry
+
+example {x y : ℝ} (h₁ : x - y = 4) (h₂ : x * y = 1) : (x + y) ^ 2 = 20 := by
+  sorry
 
 example {a b c d e f : ℤ} (h₁ : a * d = b * c) (h₂ : c * f = d * e) :
-  d * (a * f - b * e) = 0 :=
-sorry
+    d * (a * f - b * e) = 0 := by
+  sorry
 
-example {u v : ℝ} (h₁ : u + 1 = v) : u ^ 2 + 3 * u + 1 = v ^ 2 + v - 1 :=
-sorry
+example {u v : ℝ} (h₁ : u + 1 = v) : u ^ 2 + 3 * u + 1 = v ^ 2 + v - 1 := by
+  sorry
 
-example {z : ℝ} (h₁ : z ^ 2 + 1 = 0) : z ^ 4 + z ^ 3 + 2 * z ^ 2 + z + 3 = 2 :=
-sorry
+example {z : ℝ} (h₁ : z ^ 2 + 1 = 0) : z ^ 4 + z ^ 3 + 2 * z ^ 2 + z + 3 = 2 := by
+  sorry
 
 example {p q r : ℚ} (h₁ : p + q + r = 0) (h₂ : p * q + p * r + q * r = 2) :
-  p ^ 2 + q ^ 2 + r ^ 2 = -4 :=
-sorry
+    p ^ 2 + q ^ 2 + r ^ 2 = -4 := by
+  sorry

PolyrithTutorial/01_Basics_of_Polyrith/04Polyrith.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2022 Heather Macbeth. All rights reserved.
+Authors: Heather Macbeth
+-/
+import Mathlib.Data.Complex.Basic
+import Mathlib.Tactic.Polyrith
+
+
+example {a b : ℂ} (h₁ : a - 5 * b = 4) (h₂ : b + 2 = 3) : a = 9 := by polyrith
+
+example {m n : ℤ} (h : m - n = 0) : m = n := by polyrith
+
+example {K : Type*} [Field K] [CharZero K] {s : K} (hs : 3 * s + 1 = 4) : s = 1 := by
+  polyrith
+
+example {p q : ℂ} (h₁ : p + 2 * q = 4) (h₂ : p - 2 * q = 2) : 2 * p = 6 := by polyrith
+
+example {x y z w : ℂ} (h₁ : x * z = y ^ 2) (h₂ : y * w = z ^ 2) :
+    z * (x * w - y * z) = 0 := by
+  polyrith
+
+example {a b : ℚ} (h : a = b) : a ^ 2 = b ^ 2 := by polyrith
+
+example {a b : ℚ} (h : a = b) : a ^ 3 = b ^ 3 := by polyrith
+
+example (m n : ℤ) : (m ^ 2 - n ^ 2) ^ 2 + (2 * m * n) ^ 2 = (m ^ 2 + n ^ 2) ^ 2 := by
+  polyrith

PolyrithTutorial/01_Basics_of_Polyrith/solutions/Solutions02LinearCombination.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2022 Heather Macbeth. All rights reserved.
+Authors: Heather Macbeth
+-/
+import Mathlib.Data.Complex.Basic
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.LinearCombination
+
+
+/-! # Section 1.2: Basics of the linear_combination tactic
+
+This file should be worked through in parallel with the corresponding section of the tutorial:
+https://hrmacbeth.github.io/computations_in_lean/01_Basics_of_Polyrith.html#basics-of-the-linear-combination-tactic
+
+I recommend splitting your screen to display the code and the tutorial side by side! -/
+
+example {x y : ℤ} (h₁ : 2 * x + y = 4) (h₂ : x + y = 1) : x = 3 := by
+  linear_combination h₁ - h₂
+
+example {r s : ℝ} (h₁ : r + 2 * s = -1) (h₂ : s = 3) : r = -7 := by
+  linear_combination h₁ - 2 * h₂
+
+example {c : ℚ} (h₁ : 4 * c + 1 = 3 * c - 2) : c = -3 := by
+  linear_combination h₁
+
+example {x y : ℤ} (h₁ : x - 3 * y = 5) (h₂ : y = 3) : x = 14 := by
+  linear_combination h₁ + 3 * h₂
+
+example {x y : ℤ} (h₁ : 2 * x - y = 4) (h₂ : y - x + 1 = 2) : x = 5 := by
+  linear_combination h₁ + h₂
+
+example {x y : ℝ} (h₁ : x = 3) (h₂ : y = 4 * x - 3) : y = 9 := by
+  linear_combination 4 * h₁ + h₂
+
+example {a b c : ℝ} (h₁ : a + 2 * b + 3 * c = 7) (h₂ : b + 2 * c = 3) (h₃ : c = 1) :
+    a = 2 := by
+  linear_combination h₁ - 2 * h₂ + h₃
+
+example {a b : ℝ} (h₁ : a + 2 * b = 4) (h₂ : a - b = 1) : a = 2 := by
+  linear_combination 1 / 3 * h₁ + 2 / 3 * h₂
+
+example {u v : ℚ} (h₁ : u + 2 * v = 4) (h₂ : u - 2 * v = 6) : u = 5 := by
+  linear_combination 1 / 2 * h₁ + 1 / 2 * h₂
+
+example {u v : ℚ} (h₁ : 4 * u + v = 3) (h₂ : v = 2) : u = 1 / 4 := by
+  linear_combination 1 / 4 * h₁ - 1 / 4 * h₂

src/01_Basics_of_Polyrith/solutions/solutions_03_nonlinear_examples.lean → PolyrithTutorial/01_Basics_of_Polyrith/solutions/Solutions03NonlinearExamples.lean

@@ -2,27 +2,25 @@
 Copyright (c) 2022 Heather Macbeth. All rights reserved.
 Authors: Heather Macbeth
 -/
-import data.complex.basic
-import tactic.polyrith
+import Mathlib.Data.Complex.Basic
+import Mathlib.Tactic.LinearCombination
 
-example {x y : ℝ} (h₁ : x + 3 = 5) (h₂ : 2 * x - y * x = 0) : y = 2 :=
-by linear_combination (-1 / 2 * y + 1) * h₁ - 1 / 2 * h₂
+example {x y : ℝ} (h₁ : x + 3 = 5) (h₂ : 2 * x - y * x = 0) : y = 2 := by
+  linear_combination (-1 / 2 * y + 1) * h₁ - 1 / 2 * h₂
 
-example {x y : ℝ} (h₁ : x - y = 4) (h₂ : x * y = 1) : (x + y) ^ 2 = 20 :=
-by linear_combination (x - y + 4) * h₁ + 4 * h₂
+example {x y : ℝ} (h₁ : x - y = 4) (h₂ : x * y = 1) : (x + y) ^ 2 = 20 := by
+  linear_combination (x - y + 4) * h₁ + 4 * h₂
 
 example {a b c d e f : ℤ} (h₁ : a * d = b * c) (h₂ : c * f = d * e) :
-  d * (a * f - b * e) = 0 :=
-by linear_combination f * h₁ + b * h₂
+    d * (a * f - b * e) = 0 := by
+  linear_combination f * h₁ + b * h₂
 
-example {u v : ℝ} (h₁ : u + 1 = v) : u ^ 2 + 3 * u + 1 = v ^ 2 + v - 1 :=
-by linear_combination (u + v + 2) * h₁
+example {u v : ℝ} (h₁ : u + 1 = v) : u ^ 2 + 3 * u + 1 = v ^ 2 + v - 1 := by
+  linear_combination (u + v + 2) * h₁
 
-example {z : ℝ} (h₁ : z ^ 2 + 1 = 0) : z ^ 4 + z ^ 3 + 2 * z ^ 2 + z + 3 = 2 :=
-by linear_combination (z ^ 2 + z + 1) * h₁
+example {z : ℝ} (h₁ : z ^ 2 + 1 = 0) : z ^ 4 + z ^ 3 + 2 * z ^ 2 + z + 3 = 2 := by
+  linear_combination (z ^ 2 + z + 1) * h₁
 
 example {p q r : ℚ} (h₁ : p + q + r = 0) (h₂ : p * q + p * r + q * r = 2) :
-  p ^ 2 + q ^ 2 + r ^ 2 = -4 :=
-by linear_combination (p + q + r) * h₁ - 2 * h₂
-
-
+    p ^ 2 + q ^ 2 + r ^ 2 = -4 := by
+  linear_combination (p + q + r) * h₁ - 2 * h₂

src/01_Basics_of_Polyrith/solutions/solutions_04_polyrith.lean → PolyrithTutorial/01_Basics_of_Polyrith/solutions/Solutions04Polyrith.lean

@@ -2,6 +2,6 @@
 Copyright (c) 2022 Heather Macbeth. All rights reserved.
 Authors: Heather Macbeth
 -/
-import data.complex.basic
-import tactic.polyrith
+import Mathlib.Data.Complex.Basic
+import Mathlib.Tactic.Polyrith
 

PolyrithTutorial/02_Using_Polyrith/01Chebyshev.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2020 Johan Commelin. All rights reserved.
+Adapted from mathlib, released under Apache 2.0 license as described in that repository.
+Authors: Johan Commelin, Julian Kuelshammer, Heather Macbeth
+-/
+import Mathlib.Algebra.Polynomial.Basic
+import Mathlib.Tactic.Polyrith
+
+open Polynomial
+
+
+/-- The Chebyshev polynomials, defined recursively. -/
+noncomputable def T : ℕ → ℤ[X]
+  | 0 => 1
+  | 1 => X
+  | n + 2 => 2 * X * T (n + 1) - T n
+
+-- now record the three pieces of the recursive definition for easy access
+theorem T_zero : T 0 = 1 := rfl
+
+theorem T_one : T 1 = X := rfl
+
+theorem T_add_two (n : ℕ) : T (n + 2) = 2 * X * T (n + 1) - T n := by rw [T]
+
+
+/-- The product of two Chebyshev polynomials is the sum of two other Chebyshev polynomials. -/
+theorem mul_T : ∀ m : ℕ, ∀ k, 2 * T m * T (m + k) = T (2 * m + k) + T k
+  | 0 => by
+    intro k
+    ring_nf
+    have h := T_zero
+    polyrith
+  | 1 => by
+    intro k
+    have h₁ := T_add_two k
+    have h₂ := T_one
+    ring_nf at h₁ h₂ ⊢
+    polyrith
+  | m + 2 => by
+    intro k
+    have H₁ := mul_T (m - 5) (k * 37) -- not actually a relevant pair of input values!
+    have h₁ := T_add_two 7 -- not actually a relevant input value!
+    have h₂ := T_add_two (37 * k) -- not actually a relevant input value!
+    -- ... add more/different instantiations of `mul_T` and `T_add_two` here
+    ring_nf at H₁ h₁ h₂ ⊢
+    polyrith -- this will work once the right facts have been provided above