greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

docs: more tauto docstring

Browse Source
This commit is contained in:
Kevin Buzzard
2025-02-15 16:52:55 +00:00
parent 88021db205
commit a59282f10b
1 changed files with 10 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

15
Game/Levels/AdvMultiplication/L03eq_succ_of_ne_zero.lean
View File

@@ -17,12 +17,12 @@ truth tables).
## Details ## Details
`tauto` *does not do magic*! It doesn't know *anything* about addition or multiplication, `tauto` *does not do magic*! It doesn't know *anything* about addition or multiplication,
it doesn't even know `add_zero`. It doesn't know anything about *numbers*. it doesn't even know `add_zero`. The only things that `tauto` knows about numbers
What `tauto` knows about is *logic*. I guess it does know one fact about numbers, it are firstly that `a = a` and secondly that `0 ≠ 1`, `0 ≠ 2`, `1 ≠ 2` and so on.
knows that `a = a`. And that's it. But if you have a hypothesis `x < 37` What `tauto`'s strength is, is *logic*. If you have a hypothesis `x < 37`
and another hypothesis `x < 37 → y = 42` and your goal is `y = 42` then `tauto` will and another hypothesis `x < 37 → y + z = 42` and your goal is `y + z = 42` then `tauto` will
solve this goal, because to solve that goal you don't need to know any facts solve this goal, because to solve that goal you don't need to know any facts
about numbers, all you need to know is the rules of logic. about inequalities or addition, all you need to know is the rules of logic.
## Example ## Example
@@ -46,6 +46,11 @@ If you have one hypothesis `h : a ≠ a` then `tauto` will solve the goal becaus
## Example ## Example
If you have a hypothesis `h : 0 = 1` then `tauto` will solve the goal, because
`tauto` knows `0 ≠ 1` and this is enough to prove `False`, which implies any goal.
## Example
If you have a hypothesis of the form `a = 0 → a * b = 0` and your goal is `a * b ≠ 0 → a ≠ 0`, then If you have a hypothesis of the form `a = 0 → a * b = 0` and your goal is `a * b ≠ 0 → a ≠ 0`, then
`tauto` will solve the goal, because the goal is logically equivalent to the hypothesis. `tauto` will solve the goal, because the goal is logically equivalent to the hypothesis.
If you switch the goal and hypothesis in this example, `tauto` would solve it too. If you switch the goal and hypothesis in this example, `tauto` would solve it too.