patricktree.me
forked from
danabra.mov/overreacted
my blog https://overreacted.io
meh
danabra.mov
+2
-2
public/the-math-is-haunted/index.md
+2
-2
public/the-math-is-haunted/index.md
···
174
174
175
175
The `rewrite` tactic is like a "find and replace" within your goal. If you have a proof that `a = b`, giving that proof to `rewrite` will rewrite your goal so that all `a` become `b` instead. Since `math_is_haunted` "proves" that `2 = 3`, `rewrite [math_is_haunted]` turns the goal from `⊢ 2 + 2 = 6` into `⊢ 3 + 3 = 6`.
176
176
177
-
(For the programmer-minded friends, this isn't some kind of string replacement. Some state-of-the-art pattern matching and type inference may be involved.)
178
-
179
177
And now that our goal is `⊢ 3 + 3 = 6`, our job is much easier. In fact, the `rfl` tactic alone will be enough to close *that* goal and thus complete the proof:
180
178
181
179
```lean {8}
···
188
186
rewrite [math_is_haunted]
189
187
rfl
190
188
```
189
+
190
+
(Here, `rfl` works but for a different reason than one might think. It doesn't try to calculate `3 + 3` per se. Rather, `rfl` unfolds the definitions on both sides before comparing them, and both `3 + 3` and `6`, as they get unfolded, eventually become something like `Nat.zero.succ.succ.succ.succ.succ.succ`. So this *is* actually a `something = something` situation, and therefore `rfl` can close `3 + 3 = 6`.)
191
191
192
192
The above example is checked with no errors, so we've proven `2 + 2 = 6`.
193
193