Failure to halve an odd number

Stream: maths

[Nicholas McConnell]

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]

There are lots of ways to do this.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

omg a black out? are you okay?

[Kevin Buzzard]

They're back on now, just a random glitch

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

Thanks Kevin. Now I am learning more about Lean :

[Kevin Buzzard]

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]

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

[Matt Earnshaw]

how does one perform the search trick in emacs?

[Bryan Gin-ge Chen]

Maybe C-c C-d?

[Reid Barton]

M-. I think

[Reid Barton]

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

[Matt Earnshaw]

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]

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]

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]

I also have something about company-lean

[Reid Barton]

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

[Reid Barton]

This is all written down somewhere obvious

[Matt Earnshaw]

thanks both

[Matt Earnshaw]

helm-lean works nicely