31:T2fe7,numComps = { const examples = [ String.raw`1 + 1 = 2`, String.raw`7 - 4 = 3`, String.raw`-2 * 7 = \frac{-28}{2}`, String.raw`\frac{1}{2} = 0.5`, String.raw`38 \bmod 12 = 2`, String.raw`5 < 6`, String.raw`10007 is prime` ]; const steps = [ { value: "import tactic.norm_num\nimport algebra.group_power\nimport data.nat.prime\n\nexample : 1 + 1 = 2 := by norm_num\nexample : 7 - 4 = 3 := by norm_num\nexample {f : ℕ → ℕ} : f(7 - 4) = f(3) := by norm_num\nexample : (-2 : ℤ) * 7 = -28 / 2 := by norm_num\nexample : (1 : ℚ) / 2 = 0.5 := by norm_num\nexample : 1 / 2 = 0 := by norm_num\nexample : (2 : ℤ) - 4 = -2 := by norm_num\nexample : 2 - 4 = 0 := by norm_num\nexample : 38 % 12 = 2 := by norm_num\nexample : 5 < 6 := by norm_num\nexample : nat.prime 10007 := by norm_num\n", desc: mdtex`Import the mighty \`norm_num\``, marks: [ { from: { line: 0, ch: 0 }, to: { line: 2, ch: 9007199254740991 } } ], cursorPos: { line: 2, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport algebra.group_power\nimport data.nat.prime\n\nexample : 1 + 1 = 2 := by norm_num\nexample : 7 - 4 = 3 := by norm_num\nexample {f : ℕ → ℕ} : f(7 - 4) = f(3) := by norm_num\nexample : (-2 : ℤ) * 7 = -28 / 2 := by norm_num\nexample : (1 : ℚ) / 2 = 0.5 := by norm_num\nexample : 1 / 2 = 0 := by norm_num\nexample : (2 : ℤ) - 4 = -2 := by norm_num\nexample : 2 - 4 = 0 := by norm_num\nexample : 38 % 12 = 2 := by norm_num\nexample : 5 < 6 := by norm_num\nexample : nat.prime 10007 := by norm_num\n", desc: mdtex`${exmpl()} ${tex`${examples[0]}`}
\nNothing special so far. By default, Lean assumes that numerals should be interpreted as\n[natural numbers](https://en.wikipedia.org/wiki/Natural_number) $\mathbb{N}$.\nAs promised, the proof is simple.`, marks: [ { from: { line: 4, ch: 0 }, to: { line: 4, ch: 9007199254740991 } } ], cursorPos: { line: 4, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport algebra.group_power\nimport data.nat.prime\n\nexample : 1 + 1 = 2 := by norm_num\nexample : 7 - 4 = 3 := by norm_num\nexample {f : ℕ → ℕ} : f(7 - 4) = f(3) := by norm_num\nexample : (-2 : ℤ) * 7 = -28 / 2 := by norm_num\nexample : (1 : ℚ) / 2 = 0.5 := by norm_num\nexample : 1 / 2 = 0 := by norm_num\nexample : (2 : ℤ) - 4 = -2 := by norm_num\nexample : 2 - 4 = 0 := by norm_num\nexample : 38 % 12 = 2 := by norm_num\nexample : 5 < 6 := by norm_num\nexample : nat.prime 10007 := by norm_num\n", desc: mdtex`${exmpl()} ${tex`${examples[1]}`}
\nAgain, nothing special so far.`, marks: [ { from: { line: 5, ch: 0 }, to: { line: 5, ch: 9007199254740991 } } ], cursorPos: { line: 5, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport algebra.group_power\nimport data.nat.prime\n\nexample : 1 + 1 = 2 := by norm_num\nexample : 7 - 4 = 3 := by norm_num\nexample {f : ℕ → ℕ} : f(7 - 4) = f(3) := by norm_num\nexample : (-2 : ℤ) * 7 = -28 / 2 := by norm_num\nexample : (1 : ℚ) / 2 = 0.5 := by norm_num\nexample : 1 / 2 = 0 := by norm_num\nexample : (2 : ℤ) - 4 = -2 := by norm_num\nexample : 2 - 4 = 0 := by norm_num\nexample : 38 % 12 = 2 := by norm_num\nexample : 5 < 6 := by norm_num\nexample : nat.prime 10007 := by norm_num\n", desc: mdtex`Note that tactics can also rewrite subexpressions.`, marks: [ { from: { line: 6, ch: 0 }, to: { line: 6, ch: 9007199254740991 } } ], cursorPos: { line: 6, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport algebra.group_power\nimport data.nat.prime\n\nexample : 1 + 1 = 2 := by norm_num\nexample : 7 - 4 = 3 := by norm_num\nexample {f : ℕ → ℕ} : f(7 - 4) = f(3) := by norm_num\nexample : (-2 : ℤ) * 7 = -28 / 2 := by norm_num\nexample : (1 : ℚ) / 2 = 0.5 := by norm_num\nexample : 1 / 2 = 0 := by norm_num\nexample : (2 : ℤ) - 4 = -2 := by norm_num\nexample : 2 - 4 = 0 := by norm_num\nexample : 38 % 12 = 2 := by norm_num\nexample : 5 < 6 := by norm_num\nexample : nat.prime 10007 := by norm_num\n", desc: mdtex`${exmpl()} ${tex`${examples[2]}`}
\nNote that $-2$ is not a natural number. We hence need to tell Lean that we want the numeral to be\ninterpreted as an [integer](https://en.wikipedia.org/wiki/Integer) $\mathbb{Z}$.\nThis can be done using a type annotation \`( : )\`.`, marks: [ { from: { line: 7, ch: 0 }, to: { line: 7, ch: 9007199254740991 } } ], cursorPos: { line: 7, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport algebra.group_power\nimport data.nat.prime\n\nexample : 1 + 1 = 2 := by norm_num\nexample : 7 - 4 = 3 := by norm_num\nexample {f : ℕ → ℕ} : f(7 - 4) = f(3) := by norm_num\nexample : (-2 : ℤ) * 7 = -28 / 2 := by norm_num\nexample : (1 : ℚ) / 2 = 0.5 := by norm_num\nexample : 1 / 2 = 0 := by norm_num\nexample : (2 : ℤ) - 4 = -2 := by norm_num\nexample : 2 - 4 = 0 := by norm_num\nexample : 38 % 12 = 2 := by norm_num\nexample : 5 < 6 := by norm_num\nexample : nat.prime 10007 := by norm_num\n", desc: mdtex`${exmpl()} ${tex`${examples[3]}`}
\nAgain, we need to be precise and tell Lean that we want to work with\n[rational numbers](https://en.wikipedia.org/wiki/Rational_number) $\mathbb{Q}$.\nCompare this with the next line.`, marks: [ { from: { line: 8, ch: 0 }, to: { line: 8, ch: 9007199254740991 } } ], cursorPos: { line: 8, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport algebra.group_power\nimport data.nat.prime\n\nexample : 1 + 1 = 2 := by norm_num\nexample : 7 - 4 = 3 := by norm_num\nexample {f : ℕ → ℕ} : f(7 - 4) = f(3) := by norm_num\nexample : (-2 : ℤ) * 7 = -28 / 2 := by norm_num\nexample : (1 : ℚ) / 2 = 0.5 := by norm_num\nexample : 1 / 2 = 0 := by norm_num\nexample : (2 : ℤ) - 4 = -2 := by norm_num\nexample : 2 - 4 = 0 := by norm_num\nexample : 38 % 12 = 2 := by norm_num\nexample : 5 < 6 := by norm_num\nexample : nat.prime 10007 := by norm_num\n", desc: mdtex`If we do not specify a type, 1 will be interpreted as a natural number and the division will be\nperformed in $\mathbb{N}$, where $\frac{1}{2}=\left\lfloor\frac{1}{2}\right\rfloor=0$.`, marks: [ { from: { line: 9, ch: 0 }, to: { line: 9, ch: 9007199254740991 } } ], cursorPos: { line: 9, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport algebra.group_power\nimport data.nat.prime\n\nexample : 1 + 1 = 2 := by norm_num\nexample : 7 - 4 = 3 := by norm_num\nexample {f : ℕ → ℕ} : f(7 - 4) = f(3) := by norm_num\nexample : (-2 : ℤ) * 7 = -28 / 2 := by norm_num\nexample : (1 : ℚ) / 2 = 0.5 := by norm_num\nexample : 1 / 2 = 0 := by norm_num\nexample : (2 : ℤ) - 4 = -2 := by norm_num\nexample : 2 - 4 = 0 := by norm_num\nexample : 38 % 12 = 2 := by norm_num\nexample : 5 < 6 := by norm_num\nexample : nat.prime 10007 := by norm_num\n", desc: mdtex`${exmpl()} $2 - 4 = -2$ when interpreted in $\mathbb{Z}$.`, marks: [ { from: { line: 10, ch: 0 }, to: { line: 10, ch: 9007199254740991 } } ], cursorPos: { line: 10, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport algebra.group_power\nimport data.nat.prime\n\nexample : 1 + 1 = 2 := by norm_num\nexample : 7 - 4 = 3 := by norm_num\nexample {f : ℕ → ℕ} : f(7 - 4) = f(3) := by norm_num\nexample : (-2 : ℤ) * 7 = -28 / 2 := by norm_num\nexample : (1 : ℚ) / 2 = 0.5 := by norm_num\nexample : 1 / 2 = 0 := by norm_num\nexample : (2 : ℤ) - 4 = -2 := by norm_num\nexample : 2 - 4 = 0 := by norm_num\nexample : 38 % 12 = 2 := by norm_num\nexample : 5 < 6 := by norm_num\nexample : nat.prime 10007 := by norm_num\n", desc: mdtex`However, $-2\notin\mathbb{N}$. Subtraction in $\mathbb{N}$ is\n[truncated](https://en.wikipedia.org/wiki/Monus#Natural_numbers) below by 0:\n$$sub(n,m)\coloneqq \max(0,n-m)$$\nHence, $2-4=0$ when interpreted in $\mathbb{N}$.`, marks: [ { from: { line: 11, ch: 0 }, to: { line: 11, ch: 9007199254740991 } } ], cursorPos: { line: 11, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport algebra.group_power\nimport data.nat.prime\n\nexample : 1 + 1 = 2 := by norm_num\nexample : 7 - 4 = 3 := by norm_num\nexample {f : ℕ → ℕ} : f(7 - 4) = f(3) := by norm_num\nexample : (-2 : ℤ) * 7 = -28 / 2 := by norm_num\nexample : (1 : ℚ) / 2 = 0.5 := by norm_num\nexample : 1 / 2 = 0 := by norm_num\nexample : (2 : ℤ) - 4 = -2 := by norm_num\nexample : 2 - 4 = 0 := by norm_num\nexample : 38 % 12 = 2 := by norm_num\nexample : 5 < 6 := by norm_num\nexample : nat.prime 10007 := by norm_num\n", desc: mdtex`${exmpl()} ${tex`${examples[4]}`}
\nModulo computations are no issue.`, marks: [ { from: { line: 12, ch: 0 }, to: { line: 12, ch: 9007199254740991 } } ], cursorPos: { line: 12, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport algebra.group_power\nimport data.nat.prime\n\nexample : 1 + 1 = 2 := by norm_num\nexample : 7 - 4 = 3 := by norm_num\nexample {f : ℕ → ℕ} : f(7 - 4) = f(3) := by norm_num\nexample : (-2 : ℤ) * 7 = -28 / 2 := by norm_num\nexample : (1 : ℚ) / 2 = 0.5 := by norm_num\nexample : 1 / 2 = 0 := by norm_num\nexample : (2 : ℤ) - 4 = -2 := by norm_num\nexample : 2 - 4 = 0 := by norm_num\nexample : 38 % 12 = 2 := by norm_num\nexample : 5 < 6 := by norm_num\nexample : nat.prime 10007 := by norm_num\n", desc: mdtex`${exmpl()} ${tex`${examples[5]}`}
\nNeither are inequalities.`, marks: [ { from: { line: 13, ch: 0 }, to: { line: 13, ch: 9007199254740991 } } ], cursorPos: { line: 13, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport algebra.group_power\nimport data.nat.prime\n\nexample : 1 + 1 = 2 := by norm_num\nexample : 7 - 4 = 3 := by norm_num\nexample {f : ℕ → ℕ} : f(7 - 4) = f(3) := by norm_num\nexample : (-2 : ℤ) * 7 = -28 / 2 := by norm_num\nexample : (1 : ℚ) / 2 = 0.5 := by norm_num\nexample : 1 / 2 = 0 := by norm_num\nexample : (2 : ℤ) - 4 = -2 := by norm_num\nexample : 2 - 4 = 0 := by norm_num\nexample : 38 % 12 = 2 := by norm_num\nexample : 5 < 6 := by norm_num\nexample : nat.prime 10007 := by norm_num\n", desc: mdtex`${exmpl()} ${ examples[6] }
\nWe can even prove the primality of numbers.`, marks: [ { from: { line: 14, ch: 0 }, to: { line: 15, ch: 9007199254740991 } } ], cursorPos: { line: 15, ch: 9007199254740991 } } ]; return { examples, steps }; }32:T3466,numFieldComps = { const steps = [ { value: "import tactic.norm_num\nimport data.real.basic\nvariable {α : Type*}\nvariable [field α]\n\nexample : (1 : α) - 2 = -1 := by norm_num\nexample : (3 : ℝ) * (2 / 3) = 2 := by norm_num\nexample : (3 : α) * (2 / 3) = 2 := by norm_num -- fails\nexample {β : Type*} [linear_ordered_field β] : (3 : β) * (2 / 3) = 2 := by norm_num\nexample {r : ℝ} : 0 * (r + 3) + r = r := by norm_num\nexample : (1 : α) / 3 = 3⁻¹ := by norm_num\nexample {a : α} : 1 / a = a⁻¹ := by norm_num\nexample : (-2 : α)^10 = 1024 := by norm_num\nexample {a : α} : (-a : α)^10 = a^10 := by norm_num\n", desc: mdtex`Import the mighty \`norm_num\`.`, marks: [ { from: { line: 0, ch: 0 }, to: { line: 0, ch: 9007199254740991 } } ], cursorPos: { line: 0, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport data.real.basic\nvariable {α : Type*}\nvariable [field α]\n\nexample : (1 : α) - 2 = -1 := by norm_num\nexample : (3 : ℝ) * (2 / 3) = 2 := by norm_num\nexample : (3 : α) * (2 / 3) = 2 := by norm_num -- fails\nexample {β : Type*} [linear_ordered_field β] : (3 : β) * (2 / 3) = 2 := by norm_num\nexample {r : ℝ} : 0 * (r + 3) + r = r := by norm_num\nexample : (1 : α) / 3 = 3⁻¹ := by norm_num\nexample {a : α} : 1 / a = a⁻¹ := by norm_num\nexample : (-2 : α)^10 = 1024 := by norm_num\nexample {a : α} : (-a : α)^10 = a^10 := by norm_num\n", desc: mdtex`Import the real numbers $\mathbb{R}$.`, marks: [ { from: { line: 1, ch: 0 }, to: { line: 1, ch: 9007199254740991 } } ], cursorPos: { line: 1, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport data.real.basic\nvariable {α : Type*}\nvariable [field α]\n\nexample : (1 : α) - 2 = -1 := by norm_num\nexample : (3 : ℝ) * (2 / 3) = 2 := by norm_num\nexample : (3 : α) * (2 / 3) = 2 := by norm_num -- fails\nexample {β : Type*} [linear_ordered_field β] : (3 : β) * (2 / 3) = 2 := by norm_num\nexample {r : ℝ} : 0 * (r + 3) + r = r := by norm_num\nexample : (1 : α) / 3 = 3⁻¹ := by norm_num\nexample {a : α} : 1 / a = a⁻¹ := by norm_num\nexample : (-2 : α)^10 = 1024 := by norm_num\nexample {a : α} : (-a : α)^10 = a^10 := by norm_num\n", desc: mdtex`Fix a carrier $\alpha$. For now, you might just think of a ${leanHL`Type`} as a set.
\n${question( mdtex`What's up with the curly brackets $\{\}$?`, mdtex`Curly brackets denote an implicit\nparameter. Implicit parameters do not have to be explicitly specified when instantiating a theorem.\nSee TODO for further details.` )}`, marks: [ { from: { line: 2, ch: 0 }, to: { line: 2, ch: 9007199254740991 } } ], cursorPos: { line: 2, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport data.real.basic\nvariable {α : Type*}\nvariable [field α]\n\nexample : (1 : α) - 2 = -1 := by norm_num\nexample : (3 : ℝ) * (2 / 3) = 2 := by norm_num\nexample : (3 : α) * (2 / 3) = 2 := by norm_num -- fails\nexample {β : Type*} [linear_ordered_field β] : (3 : β) * (2 / 3) = 2 := by norm_num\nexample {r : ℝ} : 0 * (r + 3) + r = r := by norm_num\nexample : (1 : α) / 3 = 3⁻¹ := by norm_num\nexample {a : α} : 1 / a = a⁻¹ := by norm_num\nexample : (-2 : α)^10 = 1024 := by norm_num\nexample {a : α} : (-a : α)^10 = a^10 := by norm_num\n", desc: mdtex`Fix a field over ${tex`{\alpha}`}.\n${question( mdtex`What's up with the square brackets []?`, inlinemd`Square brackets denote an\nimplicit parameter for instances that should automatically be inferred. See TODO for further details.` )}`, marks: [ { from: { line: 3, ch: 0 }, to: { line: 4, ch: 9007199254740991 } } ], cursorPos: { line: 4, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport data.real.basic\nvariable {α : Type*}\nvariable [field α]\n\nexample : (1 : α) - 2 = -1 := by norm_num\nexample : (3 : ℝ) * (2 / 3) = 2 := by norm_num\nexample : (3 : α) * (2 / 3) = 2 := by norm_num -- fails\nexample {β : Type*} [linear_ordered_field β] : (3 : β) * (2 / 3) = 2 := by norm_num\nexample {r : ℝ} : 0 * (r + 3) + r = r := by norm_num\nexample : (1 : α) / 3 = 3⁻¹ := by norm_num\nexample {a : α} : 1 / a = a⁻¹ := by norm_num\nexample : (-2 : α)^10 = 1024 := by norm_num\nexample {a : α} : (-a : α)^10 = a^10 := by norm_num\n", desc: mdtex`Again, subtraction is no issue.`, marks: [ { from: { line: 5, ch: 0 }, to: { line: 5, ch: 9007199254740991 } } ], cursorPos: { line: 5, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport data.real.basic\nvariable {α : Type*}\nvariable [field α]\n\nexample : (1 : α) - 2 = -1 := by norm_num\nexample : (3 : ℝ) * (2 / 3) = 2 := by norm_num\nexample : (3 : α) * (2 / 3) = 2 := by norm_num -- fails\nexample {β : Type*} [linear_ordered_field β] : (3 : β) * (2 / 3) = 2 := by norm_num\nexample {r : ℝ} : 0 * (r + 3) + r = r := by norm_num\nexample : (1 : α) / 3 = 3⁻¹ := by norm_num\nexample {a : α} : 1 / a = a⁻¹ := by norm_num\nexample : (-2 : α)^10 = 1024 := by norm_num\nexample {a : α} : (-a : α)^10 = a^10 := by norm_num\n", desc: mdtex`Multiplication and division in $\mathbb{R}$ works.`, marks: [ { from: { line: 6, ch: 0 }, to: { line: 6, ch: 9007199254740991 } } ], cursorPos: { line: 6, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport data.real.basic\nvariable {α : Type*}\nvariable [field α]\n\nexample : (1 : α) - 2 = -1 := by norm_num\nexample : (3 : ℝ) * (2 / 3) = 2 := by norm_num\nexample : (3 : α) * (2 / 3) = 2 := by norm_num -- fails\nexample {β : Type*} [linear_ordered_field β] : (3 : β) * (2 / 3) = 2 := by norm_num\nexample {r : ℝ} : 0 * (r + 3) + r = r := by norm_num\nexample : (1 : α) / 3 = 3⁻¹ := by norm_num\nexample {a : α} : 1 / a = a⁻¹ := by norm_num\nexample : (-2 : α)^10 = 1024 := by norm_num\nexample {a : α} : (-a : α)^10 = a^10 := by norm_num\n", desc: mdtex`However, nobody is perfect, and so \`norm_num\` fails for the more general statement over an\nabstract field.`, marks: [ { from: { line: 7, ch: 0 }, to: { line: 7, ch: 9007199254740991 } } ], cursorPos: { line: 7, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport data.real.basic\nvariable {α : Type*}\nvariable [field α]\n\nexample : (1 : α) - 2 = -1 := by norm_num\nexample : (3 : ℝ) * (2 / 3) = 2 := by norm_num\nexample : (3 : α) * (2 / 3) = 2 := by norm_num -- fails\nexample {β : Type*} [linear_ordered_field β] : (3 : β) * (2 / 3) = 2 := by norm_num\nexample {r : ℝ} : 0 * (r + 3) + r = r := by norm_num\nexample : (1 : α) / 3 = 3⁻¹ := by norm_num\nexample {a : α} : 1 / a = a⁻¹ := by norm_num\nexample : (-2 : α)^10 = 1024 := by norm_num\nexample {a : α} : (-a : α)^10 = a^10 := by norm_num\n", desc: mdtex`Interestingly enough, \`norm_num\` succeeds for the same example on ordered fields.`, marks: [ { from: { line: 8, ch: 0 }, to: { line: 8, ch: 9007199254740991 } } ], cursorPos: { line: 8, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport data.real.basic\nvariable {α : Type*}\nvariable [field α]\n\nexample : (1 : α) - 2 = -1 := by norm_num\nexample : (3 : ℝ) * (2 / 3) = 2 := by norm_num\nexample : (3 : α) * (2 / 3) = 2 := by norm_num -- fails\nexample {β : Type*} [linear_ordered_field β] : (3 : β) * (2 / 3) = 2 := by norm_num\nexample {r : ℝ} : 0 * (r + 3) + r = r := by norm_num\nexample : (1 : α) / 3 = 3⁻¹ := by norm_num\nexample {a : α} : 1 / a = a⁻¹ := by norm_num\nexample : (-2 : α)^10 = 1024 := by norm_num\nexample {a : α} : (-a : α)^10 = a^10 := by norm_num\n", desc: mdtex`\`norm_num\` can even solve some statements containing variables as long as they are not directly\ninvolved in the computation or can be manipulated by basic laws. In this case $0*(r+3)+3=0+r=r$.`, marks: [ { from: { line: 9, ch: 0 }, to: { line: 9, ch: 9007199254740991 } } ], cursorPos: { line: 9, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport data.real.basic\nvariable {α : Type*}\nvariable [field α]\n\nexample : (1 : α) - 2 = -1 := by norm_num\nexample : (3 : ℝ) * (2 / 3) = 2 := by norm_num\nexample : (3 : α) * (2 / 3) = 2 := by norm_num -- fails\nexample {β : Type*} [linear_ordered_field β] : (3 : β) * (2 / 3) = 2 := by norm_num\nexample {r : ℝ} : 0 * (r + 3) + r = r := by norm_num\nexample : (1 : α) / 3 = 3⁻¹ := by norm_num\nexample {a : α} : 1 / a = a⁻¹ := by norm_num\nexample : (-2 : α)^10 = 1024 := by norm_num\nexample {a : α} : (-a : α)^10 = a^10 := by norm_num\n", desc: mdtex`The multiplicative inverse of 3 is $\frac{1}{3}$.`, marks: [ { from: { line: 10, ch: 0 }, to: { line: 10, ch: 9007199254740991 } } ], cursorPos: { line: 10, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport data.real.basic\nvariable {α : Type*}\nvariable [field α]\n\nexample : (1 : α) - 2 = -1 := by norm_num\nexample : (3 : ℝ) * (2 / 3) = 2 := by norm_num\nexample : (3 : α) * (2 / 3) = 2 := by norm_num -- fails\nexample {β : Type*} [linear_ordered_field β] : (3 : β) * (2 / 3) = 2 := by norm_num\nexample {r : ℝ} : 0 * (r + 3) + r = r := by norm_num\nexample : (1 : α) / 3 = 3⁻¹ := by norm_num\nexample {a : α} : 1 / a = a⁻¹ := by norm_num\nexample : (-2 : α)^10 = 1024 := by norm_num\nexample {a : α} : (-a : α)^10 = a^10 := by norm_num\n", desc: mdtex`More abstractly: $\frac{1}{a}=a^{-1}$.`, marks: [ { from: { line: 11, ch: 0 }, to: { line: 11, ch: 9007199254740991 } } ], cursorPos: { line: 11, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport data.real.basic\nvariable {α : Type*}\nvariable [field α]\n\nexample : (1 : α) - 2 = -1 := by norm_num\nexample : (3 : ℝ) * (2 / 3) = 2 := by norm_num\nexample : (3 : α) * (2 / 3) = 2 := by norm_num -- fails\nexample {β : Type*} [linear_ordered_field β] : (3 : β) * (2 / 3) = 2 := by norm_num\nexample {r : ℝ} : 0 * (r + 3) + r = r := by norm_num\nexample : (1 : α) / 3 = 3⁻¹ := by norm_num\nexample {a : α} : 1 / a = a⁻¹ := by norm_num\nexample : (-2 : α)^10 = 1024 := by norm_num\nexample {a : α} : (-a : α)^10 = a^10 := by norm_num\n", desc: mdtex`Also exponentiation causes no trouble: $(-2)^{10}=1024$ holds in any field.`, marks: [ { from: { line: 12, ch: 0 }, to: { line: 12, ch: 9007199254740991 } } ], cursorPos: { line: 12, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nimport data.real.basic\nvariable {α : Type*}\nvariable [field α]\n\nexample : (1 : α) - 2 = -1 := by norm_num\nexample : (3 : ℝ) * (2 / 3) = 2 := by norm_num\nexample : (3 : α) * (2 / 3) = 2 := by norm_num -- fails\nexample {β : Type*} [linear_ordered_field β] : (3 : β) * (2 / 3) = 2 := by norm_num\nexample {r : ℝ} : 0 * (r + 3) + r = r := by norm_num\nexample : (1 : α) / 3 = 3⁻¹ := by norm_num\nexample {a : α} : 1 / a = a⁻¹ := by norm_num\nexample : (-2 : α)^10 = 1024 := by norm_num\nexample {a : α} : (-a : α)^10 = a^10 := by norm_num\n", desc: mdtex`Again, more abstractly: $(-a)^{10}=a^{10}$ holds in any field since\n$$(-a)^{10}=(-1)^{10}a^{10}=1*a^{10}=a^{10}.$$`, marks: [ { from: { line: 13, ch: 0 }, to: { line: 14, ch: 9007199254740991 } } ], cursorPos: { line: 14, ch: 9007199254740991 } } ]; return { steps }; }33:T1a99,numIneqComps = { const steps = [ { value: "import tactic.norm_num\nvariables {α : Type*} [linear_ordered_field α]\n\nexample {a : α} : a^2 ≤ (-a)^2 +1 := by norm_num\nexample {a : α} : a - 1 ≤ a := by norm_num\nexample {n : ℕ} : n - 1 ≤ n := by norm_num -- fails\nexample {n m : ℕ} : n ≤ n + m := by norm_num\nexample {a b : α} : a ≤ a + b := by norm_num -- fails\nexample {a b : α} (b_nonneg : 0 ≤ b) : a ≤ a + b := by { norm_num, assumption }\n", desc: mdtex`Import \`norm_num\`.`, marks: [ { from: { line: 0, ch: 0 }, to: { line: 0, ch: 9007199254740991 } } ], cursorPos: { line: 0, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nvariables {α : Type*} [linear_ordered_field α]\n\nexample {a : α} : a^2 ≤ (-a)^2 +1 := by norm_num\nexample {a : α} : a - 1 ≤ a := by norm_num\nexample {n : ℕ} : n - 1 ≤ n := by norm_num -- fails\nexample {n m : ℕ} : n ≤ n + m := by norm_num\nexample {a b : α} : a ≤ a + b := by norm_num -- fails\nexample {a b : α} (b_nonneg : 0 ≤ b) : a ≤ a + b := by { norm_num, assumption }\n", desc: mdtex`Fix a carrier $\alpha$ and an [ordered field](https://en.wikipedia.org/wiki/Ordered_field) over ${tex`{\alpha}`}.`, marks: [ { from: { line: 1, ch: 0 }, to: { line: 2, ch: 9007199254740991 } } ], cursorPos: { line: 2, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nvariables {α : Type*} [linear_ordered_field α]\n\nexample {a : α} : a^2 ≤ (-a)^2 +1 := by norm_num\nexample {a : α} : a - 1 ≤ a := by norm_num\nexample {n : ℕ} : n - 1 ≤ n := by norm_num -- fails\nexample {n m : ℕ} : n ≤ n + m := by norm_num\nexample {a b : α} : a ≤ a + b := by norm_num -- fails\nexample {a b : α} (b_nonneg : 0 ≤ b) : a ≤ a + b := by { norm_num, assumption }\n", desc: mdtex`We can solve some simple inequalities: $a^2\leq a^2+1 = (-a)^2+1$ in any ordered field.`, marks: [ { from: { line: 3, ch: 0 }, to: { line: 3, ch: 9007199254740991 } } ], cursorPos: { line: 3, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nvariables {α : Type*} [linear_ordered_field α]\n\nexample {a : α} : a^2 ≤ (-a)^2 +1 := by norm_num\nexample {a : α} : a - 1 ≤ a := by norm_num\nexample {n : ℕ} : n - 1 ≤ n := by norm_num -- fails\nexample {n m : ℕ} : n ≤ n + m := by norm_num\nexample {a b : α} : a ≤ a + b := by norm_num -- fails\nexample {a b : α} (b_nonneg : 0 ≤ b) : a ≤ a + b := by { norm_num, assumption }\n", desc: mdtex`${exmpl()} $a-1\leq a$.
Again, no issue for \`norm_num\`.`, marks: [ { from: { line: 4, ch: 0 }, to: { line: 4, ch: 9007199254740991 } } ], cursorPos: { line: 4, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nvariables {α : Type*} [linear_ordered_field α]\n\nexample {a : α} : a^2 ≤ (-a)^2 +1 := by norm_num\nexample {a : α} : a - 1 ≤ a := by norm_num\nexample {n : ℕ} : n - 1 ≤ n := by norm_num -- fails\nexample {n m : ℕ} : n ≤ n + m := by norm_num\nexample {a b : α} : a ≤ a + b := by norm_num -- fails\nexample {a b : α} (b_nonneg : 0 ≤ b) : a ≤ a + b := by { norm_num, assumption }\n", desc: mdtex`However, due to truncated subtraction, \`norm_num\` sometimes cannot solve seemingly simple goals involving subtraction in $\mathbb{N}$.`, marks: [ { from: { line: 5, ch: 0 }, to: { line: 5, ch: 9007199254740991 } } ], cursorPos: { line: 5, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nvariables {α : Type*} [linear_ordered_field α]\n\nexample {a : α} : a^2 ≤ (-a)^2 +1 := by norm_num\nexample {a : α} : a - 1 ≤ a := by norm_num\nexample {n : ℕ} : n - 1 ≤ n := by norm_num -- fails\nexample {n m : ℕ} : n ≤ n + m := by norm_num\nexample {a b : α} : a ≤ a + b := by norm_num -- fails\nexample {a b : α} (b_nonneg : 0 ≤ b) : a ≤ a + b := by { norm_num, assumption }\n", desc: mdtex`Since $0\leq m$ for any $m\in\mathbb{N}$, we have $n\leq n+m$.`, marks: [ { from: { line: 6, ch: 0 }, to: { line: 6, ch: 9007199254740991 } } ], cursorPos: { line: 6, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nvariables {α : Type*} [linear_ordered_field α]\n\nexample {a : α} : a^2 ≤ (-a)^2 +1 := by norm_num\nexample {a : α} : a - 1 ≤ a := by norm_num\nexample {n : ℕ} : n - 1 ≤ n := by norm_num -- fails\nexample {n m : ℕ} : n ≤ n + m := by norm_num\nexample {a b : α} : a ≤ a + b := by norm_num -- fails\nexample {a b : α} (b_nonneg : 0 ≤ b) : a ≤ a + b := by { norm_num, assumption }\n", desc: mdtex`However, in general, this is not the case. Thus, \`norm_num\` leaves us with an unsolved goal $0\leq b$.`, marks: [ { from: { line: 7, ch: 0 }, to: { line: 7, ch: 9007199254740991 } } ], cursorPos: { line: 7, ch: 9007199254740991 } }, { value: "import tactic.norm_num\nvariables {α : Type*} [linear_ordered_field α]\n\nexample {a : α} : a^2 ≤ (-a)^2 +1 := by norm_num\nexample {a : α} : a - 1 ≤ a := by norm_num\nexample {n : ℕ} : n - 1 ≤ n := by norm_num -- fails\nexample {n m : ℕ} : n ≤ n + m := by norm_num\nexample {a b : α} : a ≤ a + b := by norm_num -- fails\nexample {a b : α} (b_nonneg : 0 ≤ b) : a ≤ a + b := by { norm_num, assumption }\n", desc: mdtex`If we assume that $0\leq b$, we can prove the statement: first apply \`norm_num\` and then close the goal with our assumption.`, marks: [ { from: { line: 8, ch: 0 }, to: { line: 9, ch: 9007199254740991 } } ], cursorPos: { line: 9, ch: 9007199254740991 } } ]; return { steps }; }34:T181c,commSemiring = { const steps = [ { value: "import tactic.ring\nvariables {α : Type*} [comm_semiring α]\nvariables {a b : α}\n\ntheorem binomial_formula : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring\nexample {f : α → α} : f((a + b)^2) = f(a^2 + 2*a*b + b^2) := by ring\nexample : a*b + 0*a^0 + b*a = 2*a*b := by ring\nexample : (a*b)^8 = a^8 * b^8 := by ring\nexample {n : ℕ} : (a*b)^n = a^n * b^n := by ring -- fails\n", desc: mdtex`Again, first import the tactic.`, marks: [ { from: { line: 0, ch: 0 }, to: { line: 0, ch: 9007199254740991 } } ], cursorPos: { line: 0, ch: 9007199254740991 } }, { value: "import tactic.ring\nvariables {α : Type*} [comm_semiring α]\nvariables {a b : α}\n\ntheorem binomial_formula : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring\nexample {f : α → α} : f((a + b)^2) = f(a^2 + 2*a*b + b^2) := by ring\nexample : a*b + 0*a^0 + b*a = 2*a*b := by ring\nexample : (a*b)^8 = a^8 * b^8 := by ring\nexample {n : ℕ} : (a*b)^n = a^n * b^n := by ring -- fails\n", desc: mdtex`Fix a carrier $\alpha$ and a commutative semiring over $\alpha$.`, marks: [ { from: { line: 1, ch: 0 }, to: { line: 1, ch: 9007199254740991 } } ], cursorPos: { line: 1, ch: 9007199254740991 } }, { value: "import tactic.ring\nvariables {α : Type*} [comm_semiring α]\nvariables {a b : α}\n\ntheorem binomial_formula : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring\nexample {f : α → α} : f((a + b)^2) = f(a^2 + 2*a*b + b^2) := by ring\nexample : a*b + 0*a^0 + b*a = 2*a*b := by ring\nexample : (a*b)^8 = a^8 * b^8 := by ring\nexample {n : ℕ} : (a*b)^n = a^n * b^n := by ring -- fails\n", desc: mdtex`Let $a,b$ be two elements in $\alpha$.`, marks: [ { from: { line: 2, ch: 0 }, to: { line: 3, ch: 9007199254740991 } } ], cursorPos: { line: 3, ch: 9007199254740991 } }, { value: "import tactic.ring\nvariables {α : Type*} [comm_semiring α]\nvariables {a b : α}\n\ntheorem binomial_formula : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring\nexample {f : α → α} : f((a + b)^2) = f(a^2 + 2*a*b + b^2) := by ring\nexample : a*b + 0*a^0 + b*a = 2*a*b := by ring\nexample : (a*b)^8 = a^8 * b^8 := by ring\nexample {n : ℕ} : (a*b)^n = a^n * b^n := by ring -- fails\n", desc: mdtex`${thm('Bionomial Formula')} $(a+b)^2=a^2+2ab+b^2$.`, marks: [ { from: { line: 4, ch: 0 }, to: { line: 4, ch: 9007199254740991 } } ], cursorPos: { line: 4, ch: 9007199254740991 } }, { value: "import tactic.ring\nvariables {α : Type*} [comm_semiring α]\nvariables {a b : α}\n\ntheorem binomial_formula : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring\nexample {f : α → α} : f((a + b)^2) = f(a^2 + 2*a*b + b^2) := by ring\nexample : a*b + 0*a^0 + b*a = 2*a*b := by ring\nexample : (a*b)^8 = a^8 * b^8 := by ring\nexample {n : ℕ} : (a*b)^n = a^n * b^n := by ring -- fails\n", desc: mdtex`Again, remember that tactics can also rewrite subexpressions.`, marks: [ { from: { line: 5, ch: 0 }, to: { line: 5, ch: 9007199254740991 } } ], cursorPos: { line: 5, ch: 9007199254740991 } }, { value: "import tactic.ring\nvariables {α : Type*} [comm_semiring α]\nvariables {a b : α}\n\ntheorem binomial_formula : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring\nexample {f : α → α} : f((a + b)^2) = f(a^2 + 2*a*b + b^2) := by ring\nexample : a*b + 0*a^0 + b*a = 2*a*b := by ring\nexample : (a*b)^8 = a^8 * b^8 := by ring\nexample {n : ℕ} : (a*b)^n = a^n * b^n := by ring -- fails\n", desc: mdtex`${exmpl()} $ab + 0a^0+ba = 2ab$.`, marks: [ { from: { line: 6, ch: 0 }, to: { line: 6, ch: 9007199254740991 } } ], cursorPos: { line: 6, ch: 9007199254740991 } }, { value: "import tactic.ring\nvariables {α : Type*} [comm_semiring α]\nvariables {a b : α}\n\ntheorem binomial_formula : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring\nexample {f : α → α} : f((a + b)^2) = f(a^2 + 2*a*b + b^2) := by ring\nexample : a*b + 0*a^0 + b*a = 2*a*b := by ring\nexample : (a*b)^8 = a^8 * b^8 := by ring\nexample {n : ℕ} : (a*b)^n = a^n * b^n := by ring -- fails\n", desc: mdtex`${exmpl()} $(ab)^8 = a^8b^8$.
\nExponentiation with a fixed number is no issue.`, marks: [ { from: { line: 7, ch: 0 }, to: { line: 7, ch: 9007199254740991 } } ], cursorPos: { line: 7, ch: 9007199254740991 } }, { value: "import tactic.ring\nvariables {α : Type*} [comm_semiring α]\nvariables {a b : α}\n\ntheorem binomial_formula : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring\nexample {f : α → α} : f((a + b)^2) = f(a^2 + 2*a*b + b^2) := by ring\nexample : a*b + 0*a^0 + b*a = 2*a*b := by ring\nexample : (a*b)^8 = a^8 * b^8 := by ring\nexample {n : ℕ} : (a*b)^n = a^n * b^n := by ring -- fails\n", desc: mdtex`However, \`ring\` is not clever enough to prove the general law $(ab)^n = a^nb^n$.`, marks: [ { from: { line: 8, ch: 0 }, to: { line: 9, ch: 9007199254740991 } } ], cursorPos: { line: 9, ch: 9007199254740991 } } ]; return { steps }; }35:T1460,commRing = { const steps = [ { value: "import tactic.ring\nvariables {α : Type*} [comm_ring α] {a b c : α}\n\nexample : (a + b)*(a - b) = a^2 - b^2 := by ring\nexample : a - (b + 2*a) = -a - b := by ring\nexample : a^6 = (a^2)^3 := by ring\nexample : a^(2 * 3) = (a^2)^3 := by ring -- fails\nexample {β : Type*} [ring β] {x : β} : x = x := by ring -- fails\n", desc: mdtex`Again, first import the tactic.`, marks: [ { from: { line: 0, ch: 0 }, to: { line: 0, ch: 9007199254740991 } } ], cursorPos: { line: 0, ch: 9007199254740991 } }, { value: "import tactic.ring\nvariables {α : Type*} [comm_ring α] {a b c : α}\n\nexample : (a + b)*(a - b) = a^2 - b^2 := by ring\nexample : a - (b + 2*a) = -a - b := by ring\nexample : a^6 = (a^2)^3 := by ring\nexample : a^(2 * 3) = (a^2)^3 := by ring -- fails\nexample {β : Type*} [ring β] {x : β} : x = x := by ring -- fails\n", desc: mdtex`Fix a carrier $\alpha$, a commutative ring over $\alpha$, and let $a,b,c$ be elements in $\alpha$.`, marks: [ { from: { line: 1, ch: 0 }, to: { line: 2, ch: 9007199254740991 } } ], cursorPos: { line: 2, ch: 9007199254740991 } }, { value: "import tactic.ring\nvariables {α : Type*} [comm_ring α] {a b c : α}\n\nexample : (a + b)*(a - b) = a^2 - b^2 := by ring\nexample : a - (b + 2*a) = -a - b := by ring\nexample : a^6 = (a^2)^3 := by ring\nexample : a^(2 * 3) = (a^2)^3 := by ring -- fails\nexample {β : Type*} [ring β] {x : β} : x = x := by ring -- fails\n", desc: mdtex`${exmpl()} $(a+b)(a-b)=a^2-b^2$.
Since we now have a commutative ring, we can also use subtraction.`, marks: [ { from: { line: 3, ch: 0 }, to: { line: 3, ch: 9007199254740991 } } ], cursorPos: { line: 3, ch: 9007199254740991 } }, { value: "import tactic.ring\nvariables {α : Type*} [comm_ring α] {a b c : α}\n\nexample : (a + b)*(a - b) = a^2 - b^2 := by ring\nexample : a - (b + 2*a) = -a - b := by ring\nexample : a^6 = (a^2)^3 := by ring\nexample : a^(2 * 3) = (a^2)^3 := by ring -- fails\nexample {β : Type*} [ring β] {x : β} : x = x := by ring -- fails\n", desc: mdtex`${exmpl()} $a-(b + 2a)=-a-b$.`, marks: [ { from: { line: 4, ch: 0 }, to: { line: 4, ch: 9007199254740991 } } ], cursorPos: { line: 4, ch: 9007199254740991 } }, { value: "import tactic.ring\nvariables {α : Type*} [comm_ring α] {a b c : α}\n\nexample : (a + b)*(a - b) = a^2 - b^2 := by ring\nexample : a - (b + 2*a) = -a - b := by ring\nexample : a^6 = (a^2)^3 := by ring\nexample : a^(2 * 3) = (a^2)^3 := by ring -- fails\nexample {β : Type*} [ring β] {x : β} : x = x := by ring -- fails\n", desc: mdtex`${exmpl()} $a^6=(a^2)^3$.
On first glance, exponentiation works fine.`, marks: [ { from: { line: 5, ch: 0 }, to: { line: 5, ch: 9007199254740991 } } ], cursorPos: { line: 5, ch: 9007199254740991 } }, { value: "import tactic.ring\nvariables {α : Type*} [comm_ring α] {a b c : α}\n\nexample : (a + b)*(a - b) = a^2 - b^2 := by ring\nexample : a - (b + 2*a) = -a - b := by ring\nexample : a^6 = (a^2)^3 := by ring\nexample : a^(2 * 3) = (a^2)^3 := by ring -- fails\nexample {β : Type*} [ring β] {x : β} : x = x := by ring -- fails\n", desc: mdtex`${exmpl()} $a^{2 * 3}=(a^2)^3$.
However, changing the example slighly makes \`ring\` fail because TODO.`, marks: [ { from: { line: 6, ch: 0 }, to: { line: 6, ch: 9007199254740991 } } ], cursorPos: { line: 6, ch: 9007199254740991 } }, { value: "import tactic.ring\nvariables {α : Type*} [comm_ring α] {a b c : α}\n\nexample : (a + b)*(a - b) = a^2 - b^2 := by ring\nexample : a - (b + 2*a) = -a - b := by ring\nexample : a^6 = (a^2)^3 := by ring\nexample : a^(2 * 3) = (a^2)^3 := by ring -- fails\nexample {β : Type*} [ring β] {x : β} : x = x := by ring -- fails\n", desc: mdtex`Keep in mind that \`ring\` requires an instance of a commutative semiring even if multiplication is not involved when proving a theorem; in fact, \`ring\` will always fail on non-commutative ring instances.`, marks: [ { from: { line: 7, ch: 0 }, to: { line: 8, ch: 9007199254740991 } } ], cursorPos: { line: 8, ch: 9007199254740991 } } ]; return {steps}; }36:T3141,abel = { const steps = [ { value: "import tactic.abel\nvariables {α : Type*} {a b : α}\n\nexample [add_comm_monoid α] : a + (b + (0 + a)) = a + a + b := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by norm_num\n\nexample [add_comm_monoid α] : 2•a = a + a := by abel\nexample [add_comm_monoid α] : 2•a = a + a := by norm_num -- fails\nexample [add_comm_monoid α] : (2^3 - 5)•a = a + a + a := by abel\nexample [add_comm_monoid α] : 1•a + a = a + a := by abel\nexample [add_comm_group α] : 1•a + a = a + a := by abel -- fails, but works with {abel, abel}\nexample [add_comm_group α] : 2•a - a = a := by repeat {abel} -- fails also with repeat {abel}\n", desc: mdtex`First import the tactic.`, marks: [ { from: { line: 0, ch: 0 }, to: { line: 0, ch: 9007199254740991 } } ], cursorPos: { line: 0, ch: 9007199254740991 } }, { value: "import tactic.abel\nvariables {α : Type*} {a b : α}\n\nexample [add_comm_monoid α] : a + (b + (0 + a)) = a + a + b := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by norm_num\n\nexample [add_comm_monoid α] : 2•a = a + a := by abel\nexample [add_comm_monoid α] : 2•a = a + a := by norm_num -- fails\nexample [add_comm_monoid α] : (2^3 - 5)•a = a + a + a := by abel\nexample [add_comm_monoid α] : 1•a + a = a + a := by abel\nexample [add_comm_group α] : 1•a + a = a + a := by abel -- fails, but works with {abel, abel}\nexample [add_comm_group α] : 2•a - a = a := by repeat {abel} -- fails also with repeat {abel}\n", desc: mdtex`Fix a carrier $\alpha$ and let $a,b$ be elements in $\alpha$.`, marks: [ { from: { line: 1, ch: 0 }, to: { line: 2, ch: 9007199254740991 } } ], cursorPos: { line: 2, ch: 9007199254740991 } }, { value: "import tactic.abel\nvariables {α : Type*} {a b : α}\n\nexample [add_comm_monoid α] : a + (b + (0 + a)) = a + a + b := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by norm_num\n\nexample [add_comm_monoid α] : 2•a = a + a := by abel\nexample [add_comm_monoid α] : 2•a = a + a := by norm_num -- fails\nexample [add_comm_monoid α] : (2^3 - 5)•a = a + a + a := by abel\nexample [add_comm_monoid α] : 1•a + a = a + a := by abel\nexample [add_comm_group α] : 1•a + a = a + a := by abel -- fails, but works with {abel, abel}\nexample [add_comm_group α] : 2•a - a = a := by repeat {abel} -- fails also with repeat {abel}\n", desc: mdtex`${exmpl()} $a+(b+(0+a)) = a+a+b$ in any commutative monoid.`, marks: [ { from: { line: 3, ch: 0 }, to: { line: 3, ch: 9007199254740991 } } ], cursorPos: { line: 3, ch: 9007199254740991 } }, { value: "import tactic.abel\nvariables {α : Type*} {a b : α}\n\nexample [add_comm_monoid α] : a + (b + (0 + a)) = a + a + b := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by norm_num\n\nexample [add_comm_monoid α] : 2•a = a + a := by abel\nexample [add_comm_monoid α] : 2•a = a + a := by norm_num -- fails\nexample [add_comm_monoid α] : (2^3 - 5)•a = a + a + a := by abel\nexample [add_comm_monoid α] : 1•a + a = a + a := by abel\nexample [add_comm_group α] : 1•a + a = a + a := by abel -- fails, but works with {abel, abel}\nexample [add_comm_group α] : 2•a - a = a := by repeat {abel} -- fails also with repeat {abel}\n", desc: mdtex`${exmpl()} $a+b-\bigl((b+a)+a\bigr)=-a$ in any commutative group.`, marks: [ { from: { line: 4, ch: 0 }, to: { line: 4, ch: 9007199254740991 } } ], cursorPos: { line: 4, ch: 9007199254740991 } }, { value: "import tactic.abel\nvariables {α : Type*} {a b : α}\n\nexample [add_comm_monoid α] : a + (b + (0 + a)) = a + a + b := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by norm_num\n\nexample [add_comm_monoid α] : 2•a = a + a := by abel\nexample [add_comm_monoid α] : 2•a = a + a := by norm_num -- fails\nexample [add_comm_monoid α] : (2^3 - 5)•a = a + a + a := by abel\nexample [add_comm_monoid α] : 1•a + a = a + a := by abel\nexample [add_comm_group α] : 1•a + a = a + a := by abel -- fails, but works with {abel, abel}\nexample [add_comm_group α] : 2•a - a = a := by repeat {abel} -- fails also with repeat {abel}\n", desc: mdtex`Note that the previous two examples could also be solved by \`norm_num\`.`, marks: [ { from: { line: 5, ch: 0 }, to: { line: 6, ch: 9007199254740991 } } ], cursorPos: { line: 6, ch: 9007199254740991 } }, { value: "import tactic.abel\nvariables {α : Type*} {a b : α}\n\nexample [add_comm_monoid α] : a + (b + (0 + a)) = a + a + b := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by norm_num\n\nexample [add_comm_monoid α] : 2•a = a + a := by abel\nexample [add_comm_monoid α] : 2•a = a + a := by norm_num -- fails\nexample [add_comm_monoid α] : (2^3 - 5)•a = a + a + a := by abel\nexample [add_comm_monoid α] : 1•a + a = a + a := by abel\nexample [add_comm_group α] : 1•a + a = a + a := by abel -- fails, but works with {abel, abel}\nexample [add_comm_group α] : 2•a - a = a := by repeat {abel} -- fails also with repeat {abel}\n", desc: mdtex`${exmpl()} $2a$ is just $a+a$ by definition – no issue for \`abel\`.`, marks: [ { from: { line: 7, ch: 0 }, to: { line: 7, ch: 9007199254740991 } } ], cursorPos: { line: 7, ch: 9007199254740991 } }, { value: "import tactic.abel\nvariables {α : Type*} {a b : α}\n\nexample [add_comm_monoid α] : a + (b + (0 + a)) = a + a + b := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by norm_num\n\nexample [add_comm_monoid α] : 2•a = a + a := by abel\nexample [add_comm_monoid α] : 2•a = a + a := by norm_num -- fails\nexample [add_comm_monoid α] : (2^3 - 5)•a = a + a + a := by abel\nexample [add_comm_monoid α] : 1•a + a = a + a := by abel\nexample [add_comm_group α] : 1•a + a = a + a := by abel -- fails, but works with {abel, abel}\nexample [add_comm_group α] : 2•a - a = a := by repeat {abel} -- fails also with repeat {abel}\n", desc: mdtex`\`norm_num\`, on the other hand, cannot deal with powers in commutative monoids.`, marks: [ { from: { line: 8, ch: 0 }, to: { line: 8, ch: 9007199254740991 } } ], cursorPos: { line: 8, ch: 9007199254740991 } }, { value: "import tactic.abel\nvariables {α : Type*} {a b : α}\n\nexample [add_comm_monoid α] : a + (b + (0 + a)) = a + a + b := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by norm_num\n\nexample [add_comm_monoid α] : 2•a = a + a := by abel\nexample [add_comm_monoid α] : 2•a = a + a := by norm_num -- fails\nexample [add_comm_monoid α] : (2^3 - 5)•a = a + a + a := by abel\nexample [add_comm_monoid α] : 1•a + a = a + a := by abel\nexample [add_comm_group α] : 1•a + a = a + a := by abel -- fails, but works with {abel, abel}\nexample [add_comm_group α] : 2•a - a = a := by repeat {abel} -- fails also with repeat {abel}\n", desc: mdtex`${exmpl()} $(2^3-5)a=a+a+a$ in any commutative monoid.
\n\`abel\` even normalises subterms using \`norm_num\` to solve examples like this.`, marks: [ { from: { line: 9, ch: 0 }, to: { line: 9, ch: 9007199254740991 } } ], cursorPos: { line: 9, ch: 9007199254740991 } }, { value: "import tactic.abel\nvariables {α : Type*} {a b : α}\n\nexample [add_comm_monoid α] : a + (b + (0 + a)) = a + a + b := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by norm_num\n\nexample [add_comm_monoid α] : 2•a = a + a := by abel\nexample [add_comm_monoid α] : 2•a = a + a := by norm_num -- fails\nexample [add_comm_monoid α] : (2^3 - 5)•a = a + a + a := by abel\nexample [add_comm_monoid α] : 1•a + a = a + a := by abel\nexample [add_comm_group α] : 1•a + a = a + a := by abel -- fails, but works with {abel, abel}\nexample [add_comm_group α] : 2•a - a = a := by repeat {abel} -- fails also with repeat {abel}\n", desc: mdtex`${exmpl()} $1a+a=2a$ in any commutative monoid.
\nIt can also solve equations involving both powers and addition in monoids...`, marks: [ { from: { line: 10, ch: 0 }, to: { line: 10, ch: 9007199254740991 } } ], cursorPos: { line: 10, ch: 9007199254740991 } }, { value: "import tactic.abel\nvariables {α : Type*} {a b : α}\n\nexample [add_comm_monoid α] : a + (b + (0 + a)) = a + a + b := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by norm_num\n\nexample [add_comm_monoid α] : 2•a = a + a := by abel\nexample [add_comm_monoid α] : 2•a = a + a := by norm_num -- fails\nexample [add_comm_monoid α] : (2^3 - 5)•a = a + a + a := by abel\nexample [add_comm_monoid α] : 1•a + a = a + a := by abel\nexample [add_comm_group α] : 1•a + a = a + a := by abel -- fails, but works with {abel, abel}\nexample [add_comm_group α] : 2•a - a = a := by repeat {abel} -- fails also with repeat {abel}\n", desc: mdtex`however, at the time writing, \`abel\` seems to have issues with powers in groups,\nand so the previous example fails for additive groups.`, marks: [ { from: { line: 11, ch: 0 }, to: { line: 11, ch: 9007199254740991 } } ], cursorPos: { line: 11, ch: 9007199254740991 } }, { value: "import tactic.abel\nvariables {α : Type*} {a b : α}\n\nexample [add_comm_monoid α] : a + (b + (0 + a)) = a + a + b := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel\nexample [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by norm_num\n\nexample [add_comm_monoid α] : 2•a = a + a := by abel\nexample [add_comm_monoid α] : 2•a = a + a := by norm_num -- fails\nexample [add_comm_monoid α] : (2^3 - 5)•a = a + a + a := by abel\nexample [add_comm_monoid α] : 1•a + a = a + a := by abel\nexample [add_comm_group α] : 1•a + a = a + a := by abel -- fails, but works with {abel, abel}\nexample [add_comm_group α] : 2•a - a = a := by repeat {abel} -- fails also with repeat {abel}\n", desc: mdtex`Combining powers with subtraction makes matters even worse.`, marks: [ { from: { line: 12, ch: 0 }, to: { line: 13, ch: 9007199254740991 } } ], cursorPos: { line: 13, ch: 9007199254740991 } } ]; return { steps }; }37:T1c26,ac_refl = { const steps = [ { value: "import algebra.ring\nvariables {α : Type*} {a b : α}\n\nexample [comm_ring α] : b+a+b = a+(b+b) := by ac_refl -- also works with `ring` and `abel`\nexample [comm_ring α] : b*a*b = a*(b*b) := by ac_refl -- also works with `ring` but not `abel`\nexample [add_comm_monoid α] : b+a+b = a+(b+b) := by ac_refl -- also works with `abel`\nexample [comm_monoid α] : b*a*b = a*(b*b) := by ac_refl -- does not work with `abel`\nexample [add_comm_semigroup α] : b+a+b = a+(b+b) := by ac_refl -- does not work with `abel`\nexample [semigroup α] : a*b*b = a*(b*b) := by ac_refl -- fails\n", desc: mdtex`Fix a carrier $\alpha$ and let $a,b$ be elements in $\alpha$.
\nWe will show that $baa=a(bb)$ for gradually less restrictive, algebraic structures.`, marks: [ { from: { line: 1, ch: 0 }, to: { line: 2, ch: 9007199254740991 } } ], cursorPos: { line: 2, ch: 9007199254740991 } }, { value: "import algebra.ring\nvariables {α : Type*} {a b : α}\n\nexample [comm_ring α] : b+a+b = a+(b+b) := by ac_refl -- also works with `ring` and `abel`\nexample [comm_ring α] : b*a*b = a*(b*b) := by ac_refl -- also works with `ring` but not `abel`\nexample [add_comm_monoid α] : b+a+b = a+(b+b) := by ac_refl -- also works with `abel`\nexample [comm_monoid α] : b*a*b = a*(b*b) := by ac_refl -- does not work with `abel`\nexample [add_comm_semigroup α] : b+a+b = a+(b+b) := by ac_refl -- does not work with `abel`\nexample [semigroup α] : a*b*b = a*(b*b) := by ac_refl -- fails\n", desc: mdtex`${exmpl()} $b+a+a=a+(b+b)$ in any commutative ring.`, marks: [ { from: { line: 3, ch: 0 }, to: { line: 3, ch: 9007199254740991 } } ], cursorPos: { line: 3, ch: 9007199254740991 } }, { value: "import algebra.ring\nvariables {α : Type*} {a b : α}\n\nexample [comm_ring α] : b+a+b = a+(b+b) := by ac_refl -- also works with `ring` and `abel`\nexample [comm_ring α] : b*a*b = a*(b*b) := by ac_refl -- also works with `ring` but not `abel`\nexample [add_comm_monoid α] : b+a+b = a+(b+b) := by ac_refl -- also works with `abel`\nexample [comm_monoid α] : b*a*b = a*(b*b) := by ac_refl -- does not work with `abel`\nexample [add_comm_semigroup α] : b+a+b = a+(b+b) := by ac_refl -- does not work with `abel`\nexample [semigroup α] : a*b*b = a*(b*b) := by ac_refl -- fails\n", desc: mdtex`${exmpl()} $baa=a(bb)$ in any commutative ring.
\nNote that \`abel\` would fail since it requires and additive structure.`, marks: [ { from: { line: 4, ch: 0 }, to: { line: 4, ch: 9007199254740991 } } ], cursorPos: { line: 4, ch: 9007199254740991 } }, { value: "import algebra.ring\nvariables {α : Type*} {a b : α}\n\nexample [comm_ring α] : b+a+b = a+(b+b) := by ac_refl -- also works with `ring` and `abel`\nexample [comm_ring α] : b*a*b = a*(b*b) := by ac_refl -- also works with `ring` but not `abel`\nexample [add_comm_monoid α] : b+a+b = a+(b+b) := by ac_refl -- also works with `abel`\nexample [comm_monoid α] : b*a*b = a*(b*b) := by ac_refl -- does not work with `abel`\nexample [add_comm_semigroup α] : b+a+b = a+(b+b) := by ac_refl -- does not work with `abel`\nexample [semigroup α] : a*b*b = a*(b*b) := by ac_refl -- fails\n", desc: mdtex`${exmpl()} $b+a+a=a+(b+b)$ in any (additive) commutative monoid.`, marks: [ { from: { line: 5, ch: 0 }, to: { line: 5, ch: 9007199254740991 } } ], cursorPos: { line: 5, ch: 9007199254740991 } }, { value: "import algebra.ring\nvariables {α : Type*} {a b : α}\n\nexample [comm_ring α] : b+a+b = a+(b+b) := by ac_refl -- also works with `ring` and `abel`\nexample [comm_ring α] : b*a*b = a*(b*b) := by ac_refl -- also works with `ring` but not `abel`\nexample [add_comm_monoid α] : b+a+b = a+(b+b) := by ac_refl -- also works with `abel`\nexample [comm_monoid α] : b*a*b = a*(b*b) := by ac_refl -- does not work with `abel`\nexample [add_comm_semigroup α] : b+a+b = a+(b+b) := by ac_refl -- does not work with `abel`\nexample [semigroup α] : a*b*b = a*(b*b) := by ac_refl -- fails\n", desc: mdtex`${exmpl()} $baa=a(bb)$ in any (multiplicative) commutative monoid.
\nAgain, \`abel\` would fail since it requires and additive structure.`, marks: [ { from: { line: 6, ch: 0 }, to: { line: 6, ch: 9007199254740991 } } ], cursorPos: { line: 6, ch: 9007199254740991 } }, { value: "import algebra.ring\nvariables {α : Type*} {a b : α}\n\nexample [comm_ring α] : b+a+b = a+(b+b) := by ac_refl -- also works with `ring` and `abel`\nexample [comm_ring α] : b*a*b = a*(b*b) := by ac_refl -- also works with `ring` but not `abel`\nexample [add_comm_monoid α] : b+a+b = a+(b+b) := by ac_refl -- also works with `abel`\nexample [comm_monoid α] : b*a*b = a*(b*b) := by ac_refl -- does not work with `abel`\nexample [add_comm_semigroup α] : b+a+b = a+(b+b) := by ac_refl -- does not work with `abel`\nexample [semigroup α] : a*b*b = a*(b*b) := by ac_refl -- fails\n", desc: mdtex`${exmpl()} $b+a+a=a+(b+b)$ in any (additive) commutative semigroup.
\nIn this case, \`abel\` would fail since it requires a monoid.`, marks: [ { from: { line: 7, ch: 0 }, to: { line: 7, ch: 9007199254740991 } } ], cursorPos: { line: 7, ch: 9007199254740991 } }, { value: "import algebra.ring\nvariables {α : Type*} {a b : α}\n\nexample [comm_ring α] : b+a+b = a+(b+b) := by ac_refl -- also works with `ring` and `abel`\nexample [comm_ring α] : b*a*b = a*(b*b) := by ac_refl -- also works with `ring` but not `abel`\nexample [add_comm_monoid α] : b+a+b = a+(b+b) := by ac_refl -- also works with `abel`\nexample [comm_monoid α] : b*a*b = a*(b*b) := by ac_refl -- does not work with `abel`\nexample [add_comm_semigroup α] : b+a+b = a+(b+b) := by ac_refl -- does not work with `abel`\nexample [semigroup α] : a*b*b = a*(b*b) := by ac_refl -- fails\n", desc: mdtex`${exmpl()} $abb=a(bb)$ in any commutative semigroup.
\nOnce we drop commutativity, however, also \`ac_refl\` fails.`, marks: [ { from: { line: 8, ch: 0 }, to: { line: 9, ch: 9007199254740991 } } ], cursorPos: { line: 9, ch: 9007199254740991 } } ]; return { steps }; }38:T44c,chained = { const proofEq = [ { mathsEntry: mdtex`Import the ring tactic.`, leanEntry: "import tactic.ring\n" }, { mathsEntry: mdtex`${exmpl()} $\bigl((-n)^3m-(n-n^3)m\bigr)^2=n^2m^2$.`, leanEntry: "example {n m : ℤ} : ((-n)^3*m - (n - n^3)*m)^2 = n^2 * m^2 :=" }, { mathsEntry: mdtex`We have $\bigl((-n)^3m-(n-n^3)m\bigr)^2=(-n^3m-nm+n^3m)^2$`, leanEntry: "calc ((-n)^3*m - (n - n^3)*m)^2 = (-(n^3)*m - n*m + n^3*m)^2 : by ring" }, { mathsEntry: mdtex`$=(-nm)^2$`, leanEntry: "... = (-n*m)^2 : by ring" }, { mathsEntry: mdtex`$=n^2m^2$.`, leanEntry: "... = n^2 * m^2 : by ring" } ]; const proofMixed = String.raw`import tactic.norm_num example {k m n p : ℕ} (k_le_m : k ≤ m) (m_pow_p_eq_n_pow_p : m^p = n^p) : k^p < n^p + 1 := calc k^p ≤ m^p : nat.pow_le_pow_of_le_left k_le_m p -- change to "by exact nat.pow_le_pow_of_le_left k_le_m p" to see the proof state ... = n^p : m_pow_p_eq_n_pow_p ... < n^p +1 : by norm_num`; return { proofEq, proofMixed }; }39:T8ef,caseExample = { const proof = [ { mathsEntry: mdtex`Import the ring tactic.`, leanEntry: "import tactic.ring\n" }, { mathsEntry: mdtex`${lem()} Let $R,S$ be commutative rings, $\varphi: R\rightarrow S$ be a ring homomorphism,\n$n\in\mathbb{N}$, and $r\in R$.\nThen $\varphi(nr)=n\varphi(r)$.`, leanEntry: "lemma hom_mul_eq_mul_hom {R : Type*} [comm_ring R] {S : Type*} [comm_ring S]\n{φ : R →+* S} {n : ℕ} {r : R} : φ(n*r) = n * φ(r) :=\nbegin" }, { mathsEntry: mdtex`We prove the claim by induction on $n$.`, leanEntry: "induction n with n' IH," }, { mathsEntry: mdtex`First the base case:`, leanEntry: "case nat.zero {", proof: [ { mathsEntry: mdtex`We have $\varphi(0*r)=\varphi(0)$`, leanEntry: "calc φ(0*r) = φ(0) : by norm_num" }, { mathsEntry: mdtex`$=0$ ${justification( mdtex`$\varphi$ is a homomorphism` )}`, leanEntry: "... = 0 : φ.map_zero" }, { mathsEntry: mdtex`$=0*\varphi(r)$.`, leanEntry: "... = 0 * φ(r) : by norm_num }," } ] }, { mathsEntry: mdtex`Inductive step: Assume the claim holds for n'.`, leanEntry: "case nat.succ {", proof: [ { mathsEntry: mdtex`We have $\varphi((n'+1)*r)=\varphi(n'r+r)$`, leanEntry: "calc φ((n' + 1)*r) = φ(n'*r + r) : by { ring, rw mul_comm } -- why is ring not solving this?" }, { mathsEntry: mdtex`$=\varphi(n'r)+\varphi(r)$ ${justification( mdtex`$\varphi$ is a homomorphism` )}`, leanEntry: "... = φ(n'*r) + φ(r) : φ.map_add (n'*r) r -- or just φ.map_add _ _" }, { mathsEntry: mdtex`$=n'\varphi(r)+\varphi(r)$ ${justification( 'inductive hypothesis' )}`, leanEntry: "... = n'*φ(r) + φ(r) : by rw IH" }, { mathsEntry: mdtex`$=(n' + 1)\varphi(r)$`, leanEntry: "... = (n' + 1) * φ(r) : by ring }" } ] }, { mathsEntry: mdtex`This finishes the proof. ${qed()}`, leanEntry: "end" } ]; return { proof }; }3a:[] 2f:{"title":"🖥️ Computations in Lean (proof of concept for Lean tutorials; incomplete tutorial)","cells":[{"id":0,"value":"md`\n# 🖥️ Computations in Lean (proof of concept for Lean tutorials; incomplete tutorial)`","pinned":false,"hidden":false,"mode":"ojs"},{"id":995,"value":"md`When doing mathematics, one often has to solve routine computations like`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1010,"value":"responsive_katex(\n invalidation,\n tex.block`\\begin{aligned}\n 1+1&=2,&-2*7&=\\frac{-28}{2},\\\\\n (n+m)^2&=n^2+2nm+m^2,\\qquad&n^2&\\leq (-n)^2+1,\n\\end{aligned}`\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":1004,"value":"md`and so on.\nThough these statements seem obvious to us, they are not so obvious if they have to be formally proven, going all the way back to the axioms of our choice.\nLuckily, just like us, [Lean](https://leanprover.github.io/) has little problems verifying these statements.\nIn this tutorial, we show you how to deal with numerical and symbolic computations in Lean, that is we show you how translate a proof like this`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1020,"value":"md`> **Proof.** The proof follows by a simple computation.${qed()}`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1024,"value":"md`to a formal proof in Lean. We guarantee: it surely will not take you 379 pages to prove ${tex`1 + 1 = 2`} as it once did [Alfred Whitehead](https://en.wikipedia.org/wiki/Alfred_North_Whitehead) and [Bertrand Russell](https://en.wikipedia.org/wiki/Bertrand_Russell) in [Principia Mathematica](https://en.wikipedia.org/wiki/Principia_Mathematica).`","pinned":false,"hidden":false,"mode":"ojs"},{"id":531,"value":"md`## 🧮 Numerical Computations`","pinned":false,"hidden":false,"mode":"ojs"},{"id":518,"value":"md`[Numerical](https://en.wikipedia.org/wiki/Numeral_system) computations are one – if not the most – basic mathematical skill everyone is being taught in school:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":22,"value":"responsive_katex(invalidation,\ntex.block`${numComps.examples[0]},\\quad ${numComps.examples[1]},\\quad ${numComps.examples[2]},\\quad ${numComps.examples[5]},`\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":24,"value":"md`Formally proving these statements, however, requires tedious derivations from a given set of axioms.\nWhen doing mathematics, we do not want to get lost in details but want to explore and verify new, exciting theories.\nThe first step to avoid the formalism hell of numerical computations is to ${leanHL`import`} Lean's tactic called \\`norm_num\\`:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1682,"value":"leanEditor(\n {\n className: CSS_CLASSES.NO_EDITOR_BUTTONS,\n header: html``,\n height: 'auto',\n readOnly: true,\n value: 'import tactic.norm_num',\n infoView: numCompView.infoView\n },\n invalidation\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":236,"value":"md`The tactic **norm_num** tries to normalise numerical expressions including ${tex`+,\\,-,\\,*,\\,/,\\allowbreak\\,^\\wedge,\\,\\mathrm{mod},\\,\\lt,\\,\\neq,`} and more.\nMore precisely, it [rewrites](https://en.wikipedia.org/wiki/Rewriting) a given numerical expression into a certain [normal form](https://en.wikipedia.org/wiki/Normal_form_(abstract_rewriting%29) and checks whether the resulting statement can then easily be verified by basic laws, such as reflexivity of equality (${tex`\\forall x, x=x`}).\nIn fact, \\`norm_num\\` even knows how to prove primality of numbers and solve some computations containing variables.\n${question(\n inlinemd`When does \\`norm_num\\` know how to solve statements containing variables?`,\n mdtex`As long as variables are not directly involved in normalising the expression or can be manipulated by simple rules, such as\n$$n-n=0,\\quad0*n=0,\\quad n-m\\leq n,\\quad \\forall n,m\\in\\mathbb{N}.$$\nCheck out the examples [below](#numFieldCompsView).
TODO: make this more precise`\n)}`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2056,"value":"md`Have a look at the following examples (click anywhere in the Lean editor to see the proof state in the info view):`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2067,"value":"viewof numCompView = leanEditor(\n {\n className: CSS_CLASSES.NO_RESET_BUTTON,\n header: html``,\n height: 'auto',\n fileName: 'num_comp.lean',\n footer: explanationFooter(numComps.steps, 1),\n readOnly: true\n },\n invalidation\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":909,"value":"md`We can even solve numerical computations more generally for abstract [fields](https://en.wikipedia.org/wiki/Field_(mathematics%29);\nthough, in general, \\`norm_num\\` is performing better when dealing with concrete structures like ${tex`\\mathbb{N},\\mathbb{Z}, \\mathbb{Q},\\mathbb{R},`} etc. Here are some more examples to give you a better understanding of what \\`norm_num\\` can and cannot do:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":916,"value":"leanEditor(\n {\n className: CSS_CLASSES.NO_RESET_BUTTON,\n footer: explanationFooter(numFieldComps.steps, 1),\n header: html``,\n fileName: 'num_field_comp.lean',\n height: 'auto',\n readOnly: true\n },\n invalidation\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":2148,"value":"md`Do not forget that \\`norm_num\\` also works for inequalities:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2160,"value":"leanEditor(\n {\n className: CSS_CLASSES.NO_RESET_BUTTON,\n footer: explanationFooter(numIneqComps.steps, 1),\n header: html``,\n fileName: 'num_ineq_comps.lean',\n height: '180px',\n readOnly: true\n },\n invalidation\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":508,"value":"md`### 🏀 Playground`","pinned":false,"hidden":false,"mode":"ojs"},{"id":484,"value":"html`Now it is your turn – explore the beauty of norm_num on your own!${leanEditor(\n {\n header: html``,\n value: `import tactic.norm_num data.real.basic\nvariables {α : Type*} [field α] {β : Type*} [linear_ordered_field β]\n-- This is your playground ⚽ Use variables in α for statements in fields\n-- and variables in β for variables in ordered fields.\n\n-- Fix the following examples\nexample : 0 ≠ 1 := by sorry\nexample {a : α} : 1 + a - 1 = a := by sorry\nexample : (-1 : β)^3 ≤ 0 := by sorry\n\n-- Try to verify your own examples!\n`\n },\n invalidation\n)}`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1814,"value":"html`\n

\"Abacus — An abacus – norm_num's grandfather.

`","pinned":false,"hidden":false,"mode":"ojs"},{"id":549,"value":"md`## 🔡 Computations With Variables`","pinned":false,"hidden":false,"mode":"ojs"},{"id":552,"value":"md`Though \\`norm_num\\` knows how to solve some computations containing variables,\nit will only be able to do so if the statements are mainly about manipulating involved numerals or follow by \nbasic laws such as ${tex`n - n = 0`} and ${tex`n \\leq n + 1`}.\nHowever, computations, as understood by mathematicians, go way beyond what can be done on an abacus.\nFor example, they include variables:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":732,"value":"responsive_katex(invalidation, \ntex.block`(n+m)^2=n^2+2nm+m^2,\\quad a - (b + 2a) = -a - b,\\dotso`) ","pinned":false,"hidden":false,"mode":"ojs"},{"id":1219,"value":"md`Note that we assumed commutativity of multiplication for the first example. In a general ring, the binomial formula does not hold.\nWe need to be careful about the assumptions we take and structures we talk about.\nDifferent structures obey different laws.\nLean thus also offers different tactics to deal with these computations, depending on the structure at hand.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":864,"value":"md`### 🌾 Fields`","pinned":false,"hidden":false,"mode":"ojs"},{"id":867,"value":"md`TODO: This tactic does not exist (yet).`","pinned":false,"hidden":false,"mode":"ojs"},{"id":777,"value":"commutative_rings = md`### 💍 Commutative Rings`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1252,"value":"md`The next tactic, called **ring**, allows us, perhaps surprisingly, not to verify statements about [rings](https://en.wikipedia.org/wiki/Ring_(algebra%29), but about commutative [semirings](https://en.wikipedia.org/wiki/Semiring).\nThis means that \\`ring\\` does work, for example, on ${tex`\\mathbb{N}`} but not on a general non-commutative ring, such as ${tex`\\mathbb{ℝ}^{n\\times n}`}.\nLet us import the tactic and have a look at some examples for commutative semirings:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":758,"value":"leanEditor(\n {\n className: CSS_CLASSES.NO_RESET_BUTTON,\n footer: explanationFooter(commSemiring.steps),\n header: html``,\n height: '170px',\n fileName: 'comm_semi_ring.lean',\n readOnly: true\n },\n invalidation\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":1937,"value":"md`In order to verify statements involving subtraction and negation, we need to assume the existence of a commutative ring:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1943,"value":"leanEditor(\n {\n className: CSS_CLASSES.NO_RESET_BUTTON,\n footer: explanationFooter(commRing.steps, 1),\n header: html``,\n height: '170px',\n fileName: 'comm_ring.lean',\n readOnly: true\n },\n invalidation\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":1367,"value":"md`### 🔁 Commutative Groups, Monoids, and Semigroups`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1371,"value":"md`We now consider even simpler commutative structures, in particular, commutative [groups](https://en.wikipedia.org/wiki/Abelian_group), [monoids](https://en.wikipedia.org/wiki/Monoid), and [semigroups](https://en.wikipedia.org/wiki/Semigroup).\nThere are two tactics to deal with computational problems in these structures: \\`abel\\` and \\`ac_refl\\`.\nWhile the former focuses on proving equalities in commutative groups and monoids,\nthe latter specialises in proving equalities of terms up to commutative and associativity of their binary operator.\n\nFirst check out the following examples for \\`abel\\`:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2142,"value":"leanEditor(\n {\n className: CSS_CLASSES.NO_RESET_BUTTON,\n footer: explanationFooter(abel.steps),\n header: html``,\n height: '305px',\n fileName: 'abel.lean',\n readOnly: true\n },\n invalidation\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":2600,"value":"md`Now, in contrast, check out the following examples for \\`ac_refl\\`.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2580,"value":"leanEditor(\n {\n className: CSS_CLASSES.NO_RESET_BUTTON,\n footer: explanationFooter(ac_refl.steps),\n header: html``,\n height: '250px',\n fileName: 'ac_refl.lean',\n readOnly: true\n },\n invalidation\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":1449,"value":"md`## 🎁 Decidable Propositions`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1452,"value":"md`Something about \\`dec_trivial\\` – what are good examples for something that cannot be done with the previous tatics but with \\`dec_trivial\\`?`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2194,"value":"md`## ⛓️ Chained Computations`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2203,"value":"md`So far, we were able to solve all of our computational problems with a single tactic invocation.\nSometimes, however, we have to approach our goal step by step, using multiple intermediate rewrite steps, or we\nwant to provide the reader with an intermediate goal for a better understanding of the proof.\nCompare, for example, the following two computations for ${tex`n,m\\in\\mathbb{Z}`}:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2254,"value":"responsive_katex(\n invalidation,\n tex.block`\n\\bigl((-n)^3m-(n-n^3)m\\bigr)^2=n^2m^2\\\\\n\\text{vs}\\\\\n\\bigl((-n)^3m-(n-n^3)m\\bigr)^2=(-n^3m-nm+n^3m)^2=(-nm)^2=n^2m^2\n`\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":2249,"value":"md`Luckily, Lean provides a neat way to perform chained computations:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2396,"value":"viewof chainedProofView = proofView({\n proof: chained.proofEq,\n invalidation,\n startIndex: 1\n})","pinned":false,"hidden":false,"mode":"ojs"},{"id":2443,"value":"question(\n mdtex`**Gotcha:** Why did we translate $-n^3$ to \"${leanHL`-(n^3)`}\" and not \"${leanHL`-n^3`}\"?`,\n inlinemd`The negation operator \"${leanHL`-`}\" has a greater \n[precedence](https://en.wikipedia.org/wiki/Order_of_operations) than the power operator\n\"${leanHL`^`}\". For example, ${leanHL`-(1^2)=-(1*1)=-1`} and ${leanHL`-1^2=(-1)*(-1)=1`}.\n${leanEditor(\n {\n className: CSS_CLASSES.NO_EDITOR_BUTTONS,\n header: html``,\n value: String.raw`import algebra.group_power\n\n#eval -((1 : int)^2)\n#eval -(1 : int)^2`,\n height: 'auto',\n readOnly: true\n },\n invalidation\n)}`\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":2477,"value":"md`Note that ${leanHL`calc`} does not only work for a chain of equalities, but also for chains including ${tex`\\leq, <, \\iff,\\implies,`} etc. Have a look at the following example – and feel free to play around with it!`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2493,"value":"leanEditor(\n {\n header: html``,\n height: '180px',\n value: chained.proofMixed\n },\n invalidation\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":2311,"value":"md`## ⚔️ Case Example - Putting It All Together`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2310,"value":"md`If you followed our adventurous tutorial series, you already know how to\n1. write definitions,\n2. apply, rewrite, and simplify theorems, and\n3. solve computational problems in Lean.\n\nLet us combine all of our hitherto acquired skills to solve the final quest of this notebook:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2220,"value":"proofView({ proof: caseExample.proof, invalidation, startIndex: 1 })","pinned":false,"hidden":false,"mode":"ojs"},{"id":848,"value":"md`## 🙋 Quiz`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2511,"value":"md`Now it's your turn! Use the right tactics to solve all problems below and collect your Lean computations medal 🥇${tex`\\neq`}🥈.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":851,"value":"{\n const editor = leanEditor(\n {\n header: html``,\n height: '330px',\n value: quiz.value\n },\n invalidation\n );\n quizMarks(editor);\n return editor;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":2611,"value":"// md`🏆 Finally, collect your trophy and prove the following theorem:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2620,"value":"//md`${thm()} TODO`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2623,"value":"//leanEditor({ value: '--The theorem to prove', header: html`` }, invalidation)","pinned":true,"hidden":false,"mode":"ojs"},{"id":1950,"value":"md`## 🤓 Continue Reading`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1953,"value":"md`TODO: Links to other tutorials`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1637,"value":"md`## Acknowledgments`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1640,"value":"md`This work was created as part of the [Lean Forward Project](https://lean-forward.github.io/).`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2462,"value":"md`## 📓 Help Us Creating Great Tutorials`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2469,"value":"md`If you are keen on helping us to create great Lean tutorials to boost the interactive theorem proving community,\ncontact Kevin Kappelmann.\n\nYou can check out the code of the notebook by opening the cells on the left sidebar of the page.\nAll side by side proofs were created using the [Lean proof view designer template](/@kappelmann/proof-view-designer-template) and all step by step explanations using the [Lean step designer template](/@kappelmann/steps-designer-template).`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1643,"value":"LICENSE = md`## License:\n\nCopyright 2019 @ [Kevin Kappelmann](https://kappelmann.me)\n\nLicensed under the Apache License, Version 2.0 (the \"License\");\nyou may not use this file except in compliance with the License.\nYou may obtain a copy of the License at [http://www.apache.org/licenses/LICENSE-2.0](http://www.apache.org/licenses/LICENSE-2.0).\n\nUnless required by applicable law or agreed to in writing, software\ndistributed under the License is distributed on an \"AS IS\" BASIS,\nWITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.\nSee the License for the specific language governing permissions and\nlimitations under the License.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":95,"value":"md`## Appendix`","pinned":false,"hidden":false,"mode":"ojs"},{"id":133,"value":"md`### Variables`","pinned":false,"hidden":false,"mode":"ojs"},{"id":708,"value":"$31","pinned":false,"hidden":false,"mode":"ojs"},{"id":955,"value":"$32","pinned":false,"hidden":false,"mode":"ojs"},{"id":2156,"value":"$33","pinned":false,"hidden":false,"mode":"ojs"},{"id":1821,"value":"$34","pinned":false,"hidden":false,"mode":"ojs"},{"id":1935,"value":"$35","pinned":false,"hidden":false,"mode":"ojs"},{"id":2138,"value":"$36","pinned":false,"hidden":false,"mode":"ojs"},{"id":2576,"value":"$37","pinned":false,"hidden":false,"mode":"ojs"},{"id":2391,"value":"$38","pinned":false,"hidden":false,"mode":"ojs"},{"id":2214,"value":"$39","pinned":false,"hidden":false,"mode":"ojs"},{"id":2536,"value":"quiz = {\n const value = String.raw`import tactic.norm_num tactic.ring tactic.abel\nvariable {α : Type*}\n\n-- norm_num, field, ring, abel, ac_refl, or something different?\n-- Use the right tactics to fill in the sorry placeholders.\n\nexample : 1 ≠ 2 := by sorry\nexample {n m : ℤ} : n * (m - n) = -n * n + n * m := by sorry\nexample {z : ℤ} : 2 * z / 2 = z := by sorry\nexample [comm_semigroup α] {f : α → α} {a b c : α} :\n f((a*(b*(b*c*a)))*c) = f(a*a*b*b*c*c) := by sorry\nexample [add_comm_group α] {a b c : α} :\n -b - -(-(-a)) = a - b := by sorry\nexample [add_comm_monoid α] {a : α} :\n 3•a = 1•a + a + 1•a := by sorry\nexample [field α] {a b : α} {φ : α →+* α} :\n φ(a^2 * a⁻¹ * (b + (-b))) = φ(0) := by sorry`;\n return { value };\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":136,"value":"md`### Imports`","pinned":false,"hidden":false,"mode":"ojs"},{"id":92,"value":"import {LEAN_LIBS, CSS_CLASSES} from '@kappelmann/lean-configuration'","pinned":false,"hidden":false,"mode":"ojs"},{"id":1860,"value":"leanLibName = LEAN_LIBS.MATHLIB // we are using mathlib in this file","pinned":false,"hidden":false,"mode":"ojs"},{"id":1401,"value":"import {\n leanEditor,\n leanHL,\n explanationFooter,\n info,\n justification,\n question,\n exmpl,\n lem,\n thm,\n qed,\n proofView,\n proofCreatorFooter,\n quizMarks,\n mdtex,\n inlinemd,\n responsive_katex\n} with { leanLibName } from '@kappelmann/lean-utility-functions'","pinned":false,"hidden":false,"mode":"ojs"}],"files":"$W3a","stdlib":"1","titling":"auto"}