# Zulip Chat Archive

## 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?

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

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

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

thanks both

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

helm-lean works nicely

Last updated: May 12 2021 at 07:17 UTC