## Stream: maths

### Topic: Failure to halve an odd number

#### Nicholas McConnell (Feb 24 2020 at 23:04):

In Leanprover, what's the best way to show that ¬∃(x:ℤ),(2*x=1) ? For the sake of proving no number can be both odd and even.

#### Kevin Buzzard (Feb 24 2020 at 23:13):

There are lots of ways to do this.

#### Kevin Buzzard (Feb 24 2020 at 23:14):

Probably the easiest way is to learn how to use mathlib's library which deals with division and remainder

#### Kevin Buzzard (Feb 24 2020 at 23:14):

If they're equal then they'll have equal remainder when you divide by two

#### Kevin Buzzard (Feb 24 2020 at 23:15):

But a lemma in the library tells you that 2x has remainder 0 and another one shows 1 has remainder 1

#### Kevin Buzzard (Feb 24 2020 at 23:15):

You might want to browse through something like data.int.modeq but I need to sort out the fact that all the lights just went off in my house

#### Yufan Lou (Feb 25 2020 at 02:59):

omg a black out? are you okay?

#### Kevin Buzzard (Feb 25 2020 at 07:10):

They're back on now, just a random glitch

#### Kevin Buzzard (Feb 25 2020 at 22:06):

OK so as I was saying, this is not so hard if you use results in the library. In fact probably data.int.basic has everything you need. Assume such an x exists; then 2 * x = 1 and we want to prove a contradiction. But we can now use calc to prove that 1 = 1 % 2 = (2 * x) % 2 = 0 and that's the contradiction we seek. The reason 1 % 2 = 1 is mod_eq_of_lt, and the reason (2 * x) % 2 = 0 is mul_mod_right.

#### Nicholas McConnell (Feb 26 2020 at 05:15):

I tried various things, like

have h : (2*x) % 2 = 0 := mul_mod_right,
have h : (2*x) % 2 = 0 := data.int.basic.mul_mod_right,

and so on. But none of them worked

#### Kevin Buzzard (Feb 26 2020 at 07:06):

You need to import data.int.basic and then type #check mul_mod_right without hitting enter and then press ctrl-space to search

#### Kevin Buzzard (Feb 26 2020 at 07:10):

and then you find that there is int.mul_mod_right and nat.mul_mod_right. This is a really powerful way to search the library (especially when you get to the point where you can start guessing the names of lemmas).

#### Kevin Buzzard (Feb 26 2020 at 07:11):

Now your x is an integer so you want int.mul_mod_right so change #check mul_mod_right to #check int.mul_mod_right and you can see that this function wants explicit integers a and b as input, and then returns a proof that (a * b) % a = 0.

#### Kevin Buzzard (Feb 26 2020 at 07:12):

and we conclude that example (x : ℤ) : (2 * x) % 2 = 0 := int.mul_mod_right 2 x should work

#### Kevin Buzzard (Feb 26 2020 at 07:14):

and example (x : ℤ) : (2 * x) % 2 = 0 := int.mul_mod_right _ _ works too (making the elaborator do the work of guessing the inputs to the function) as does example (x : ℤ) : (2 * x) % 2 = 0 := by rw int.mul_mod_right (making the rw tactic do the work)

#### Nicholas McConnell (Feb 26 2020 at 14:26):

Thanks Kevin. Now I am learning more about Lean :

#### Kevin Buzzard (Feb 26 2020 at 16:10):

Did you get the ctrl-space thing to work? It's a really useful trick. I use it all the time. After a while you can start guessing what things are called -- you know you want (a * b) % a = 0 and immediately you guess the lemma is going to have mul_mod in its name, and already #check mul_mod and ctrl-space is giving you a list of things including the answer. @Johan Commelin knows another way of doing this involving Ctrl-P but I can never remember it.

#### Kevin Buzzard (Feb 26 2020 at 16:11):

Ctrl-P and then # mul_mod in the box at the top But this seems to produce far more output.

#### Matt Earnshaw (Mar 03 2020 at 17:18):

how does one perform the search trick in emacs?

Maybe C-c C-d?

#### Reid Barton (Mar 03 2020 at 17:22):

M-. I think

#### Reid Barton (Mar 03 2020 at 17:23):

(assuming Kevin is talking about what I think, and assuming I haven't customized the keybinding somehow)

#### Matt Earnshaw (Mar 03 2020 at 17:24):

M-. is lean-find-definition for me, which doesn't work just on mul_mod_right (it needs a fully qualified identifier). C-c C-d is undefined

#### Bryan Gin-ge Chen (Mar 03 2020 at 17:26):

For C-c C-d I was going off of this file, which seems to send a search command to the Lean server (this is what C-p # does in VS Code): https://github.com/leanprover/lean-mode/blob/master/helm-lean.el#L40 . But I don't actually use emacs, so I don't know.

#### Reid Barton (Mar 03 2020 at 17:27):

Sorry, I should have said M-n--these are all in physical memory for me. I have this:

(global-set-key (kbd "M-n") #'company-complete)


#### Reid Barton (Mar 03 2020 at 17:27):

I also have something about company-lean

#### Reid Barton (Mar 03 2020 at 17:28):

I think you need to M-x package-install that

#### Reid Barton (Mar 03 2020 at 17:28):

This is all written down somewhere obvious

thanks both

#### Matt Earnshaw (Mar 03 2020 at 17:38):

helm-lean works nicely

Last updated: May 12 2021 at 07:17 UTC