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 }; }