Zulip Chat Archive

Stream: maths

Topic: Failure to halve an odd number


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 24 2020 at 23:13):

There are lots of ways to do this.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 24 2020 at 23:14):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yufan Lou (Feb 25 2020 at 02:59):

omg a black out? are you okay?

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 07:10):

They're back on now, just a random glitch

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Nicholas McConnell (Feb 26 2020 at 14:26):

Thanks Kevin. Now I am learning more about Lean :

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Matt Earnshaw (Mar 03 2020 at 17:18):

how does one perform the search trick in emacs?

view this post on Zulip Bryan Gin-ge Chen (Mar 03 2020 at 17:21):

Maybe C-c C-d?

view this post on Zulip Reid Barton (Mar 03 2020 at 17:22):

M-. I think

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Reid Barton (Mar 03 2020 at 17:27):

I also have something about company-lean

view this post on Zulip Reid Barton (Mar 03 2020 at 17:28):

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

view this post on Zulip Reid Barton (Mar 03 2020 at 17:28):

This is all written down somewhere obvious

view this post on Zulip Matt Earnshaw (Mar 03 2020 at 17:33):

thanks both

view this post on Zulip Matt Earnshaw (Mar 03 2020 at 17:38):

helm-lean works nicely


Last updated: May 12 2021 at 07:17 UTC