refer to R to prove things in N?

Stream: new members

[Abhimanyu Pallavi Sudhir]

I'm proving that there is no natural number such that 2n = 1. One way of doing this would be to point out that multiplication by a non-zero constant is injective, and that multiplication in R generalises multiplication in N, and since we already have 2*(1/2) = 1, this would imply n = 1/2, which is not a natural number.

[Kenny Lau]

and yet you asked us about why you need universes to prove fermat's last theorem :P

[Mario Carneiro]

they are both valid questions

[Abhimanyu Pallavi Sudhir]

My question is: Can this be formalised in Lean? How would you state "multiplication in R generalises multiplication in N"?

[Abhimanyu Pallavi Sudhir]

Ok, wait, you can state that pretty easily, but how would you use that?

[Kenny Lau]

nat.cast_mul, I guess

[Kenny Lau]

but you see

[Kenny Lau]

how would you prove that 1/2 is not a natural number?

[Mario Carneiro]

There are other ways to prove that theorem, but sure you can do it that way

[Abhimanyu Pallavi Sudhir]

@Kenny Lau 1/2 is not natural because 1/2 is between 0 and 1, but 1 is the successor of 0 and nothing can be between an element and its successor.

[Kenny Lau]

so you also want nat.cast_lt :P

[Kenny Lau]

can't omega solve this? @Mario Carneiro

[Kenny Lau]

example : ∀ n, 2*n ≠ 1 :=
λ n, nat.cases_on n dec_trivial $ λ n H,
nat.no_confusion $ nat.succ_inj H

[Kenny Lau]

example : ¬∃ n, 2*n = 1 :=
by simp only [eq_comm]; exact dec_trivial

[Kenny Lau]

example : ∀ n, 2*n ≠ 1 :=
λ n H, absurd (Exists.intro n H.symm) dec_trivial

[Mario Carneiro]

I think this is a faithful rendition of your proof:

example (n : ℕ) : 2 * n ≠ 1 :=
λ h, begin
  have : 2 * (n:ℝ) = 1, {simpa using congr_arg (coe : ℕ → ℝ) h},
  rw [mul_comm, ← div_eq_iff_mul_eq (two_ne_zero : (2:ℝ)≠0)] at this,
  have h0 : ((0:ℕ):ℝ) < (1 / 2 : ℝ), {simp, norm_num},
  have h1 : (1 / 2 : ℝ) < (1:ℕ), {simp, norm_num},
  rw [this, nat.cast_lt] at h0 h1,
  exact not_le_of_lt h1 h0
end

[Kenny Lau]

```lean

[Kenny Lau]

Also, who needs the reals, we only need Q

[Mario Carneiro]

I know

[Mario Carneiro]

but if I did that then I wouldn't be "referring to R to prove things in N"

[Kenny Lau]

that's mostly a comment to him

[Mario Carneiro]

If you use Q instead the two lemmas h0 and h1 can be proven by dec_trivial

[Mario Carneiro]

what's going on in your proof? I'm surprised that dec_trivial proves ¬∃ (n : ℕ), 1 = 2 * n

[Kenny Lau]

it's dvd in disguise :P

[Mario Carneiro]

oh whoa, didn't realize dvd was reducible

[Kenny Lau]

me neither

[Kenny Lau]

this is the residue of a longer proof

[Mario Carneiro]

to answer your question, yes omega can handle this

[Mario Carneiro]

I think linarith can too if you fiddle with the statement a bit

[Abhimanyu Pallavi Sudhir]

I think this is a faithful rendition of your proof:

example (n : ℕ) : 2 * n ≠ 1 :=
λ h, begin
  have : 2 * (n:ℝ) = 1, {simpa using congr_arg (coe : ℕ → ℝ) h},
  rw [mul_comm, ← div_eq_iff_mul_eq (two_ne_zero : (2:ℝ)≠0)] at this,
  have h0 : ((0:ℕ):ℝ) < (1 / 2 : ℝ), {simp, norm_num},
  have h1 : (1 / 2 : ℝ) < (1:ℕ), {simp, norm_num},
  rw [this, nat.cast_lt] at h0 h1,
  exact not_le_of_lt h1 h0
end

I'm trying to unpack that, but Lean says it fails to synthesise type class instance (I fixed one bracket).

[Mario Carneiro]

where is the error, and where did you fix a bracket?

[Mario Carneiro]

you need import data.real.basic tactic.norm_num in the header

[Abhimanyu Pallavi Sudhir]

Yeah, I've done that.

[Abhimanyu Pallavi Sudhir]

Wait, I put the wrong bracket. It works now.

[Mario Carneiro]

kenny, here is a marginally less obfuscatory (and shorter!) version of your proof:

example (n : ℕ) : 2*n ≠ 1 :=
λ h, (dec_trivial : ¬ 2 ∣ 1) ⟨n, h.symm⟩

[Kenny Lau]

import data.real.basic

example (n : ℕ) : 2 * n ≠ 1 :=
λ h, begin
  have h1 : 0 < 2 * n ∧ 2 * n < 2,
  { rw h,
    exact dec_trivial },
  rw [← @nat.cast_lt ℝ, ← @nat.cast_lt ℝ, nat.cast_mul] at h1,
  rw [nat.cast_zero, nat.cast_bit0, nat.cast_one] at h1,
  have h2 : 0 < (2:ℝ),
  { exact two_pos },
  have h3 : (2:ℝ) ≠ 0,
  { exact ne_of_gt h2 },
  rw [← div_lt_div_right h2, mul_div_cancel_left _ h3, and_comm] at h1,
  rw [← div_lt_div_right h2, mul_div_cancel_left _ h3, and_comm] at h1,
  rw [div_self h3, zero_div, ← nat.cast_zero, ← nat.cast_one] at h1,
  rw [nat.cast_lt, nat.cast_lt] at h1,
  cases h1 with h4 h5, clear h h2 h3,
  revert n h5,
  exact dec_trivial
end

[Kenny Lau]

is this a more faithful rendition?

[Kenny Lau]

(sorry, can't get nat.cast_div to work, guess it doesn't exist)

[Mario Carneiro]

lol, of course not

[Mario Carneiro]

it's not true... I'm not even sure what the statement would be

[Kenny Lau]

cast it to a char_zero decidable_division_ring or something like that

[Abhimanyu Pallavi Sudhir]

import data.real.basic

example (n : ℕ) : 2 * n ≠ 1 :=
λ h, begin
  have h1 : 0 < 2 * n ∧ 2 * n < 2,
  { rw h,
    exact dec_trivial },
  rw [← @nat.cast_lt ℝ, ← @nat.cast_lt ℝ, nat.cast_mul] at h1,
  rw [nat.cast_zero, nat.cast_bit0, nat.cast_one] at h1,
  have h2 : 0 < (2:ℝ),
  { exact two_pos },
  have h3 : (2:ℝ) ≠ 0,
  { exact ne_of_gt h2 },
  rw [← div_lt_div_right h2, mul_div_cancel_left _ h3, and_comm] at h1,
  rw [← div_lt_div_right h2, mul_div_cancel_left _ h3, and_comm] at h1,
  rw [div_self h3, zero_div, ← nat.cast_zero, ← nat.cast_one] at h1,
  rw [nat.cast_lt, nat.cast_lt] at h1,
  cases h1 with h4 h5, clear h h2 h3,
  revert n h5,
  exact dec_trivial
end

Ok, I'm lost here -- what exactly does nat.cast do?

[Abhimanyu Pallavi Sudhir]

And what are the up-arrow signs lean gives in the feedback?

[Kenny Lau]

it's the coercion function from nat to real

[Mario Carneiro]

the up arrows are nat.cast

[Kenny Lau]

n is a natural number and "up-arrow n" is a real number

[Abhimanyu Pallavi Sudhir]

Ah ok.

[Mario Carneiro]

and there are theorems saying ↑(n + m) = ↑n + ↑m and so on, that's nat.cast_add

[Mario Carneiro]

this is how you turn a whole equation from talking about naturals to talking about reals or vice versa

[Bryan Gin-ge Chen]

Coercions are discussed here in TPiL.

[Abhimanyu Pallavi Sudhir]

And nat.cast_lt means "n < m implies ↑n < ↑m"?

[Mario Carneiro]

it's an iff

[Mario Carneiro]

so you can turn a nat inequality into a real inequality or vice versa

[Abhimanyu Pallavi Sudhir]

I see. And perhaps a ridiculously elementary question, but what exactly are the @ signs? Why does nat.cast_mul not have them while the others do?

[Bryan Gin-ge Chen]

@function means that you have to provide the implicit arguments to function. Implicit arguments are those that lean tries to infer and are denoted by curly braces.

[Bryan Gin-ge Chen]

See this section of TPiL.

[Abhimanyu Pallavi Sudhir]

Oh ok, that makes sense. So e.g. if I was simplifying a calculational proof and had to simplify 1*x to x, then I could use @one_mul x if one_mul didn't work?

[Kenny Lau]

you would need way more arguments than x

[Kenny Lau]

it would be something like @one_mul \R _ x

[Abhimanyu Pallavi Sudhir]

What does the underscore do?

[Bryan Gin-ge Chen]

Yeah, I forgot to say you have to provide type class arguments as well (stuff in square brackets).

[Bryan Gin-ge Chen]

The underscore tells lean to try to infer that argument.

[Abhimanyu Pallavi Sudhir]

(deleted)

[Kenny Lau]

you know, there was a time when I tried to type something and decided that part of a sentence can be inferred from the previous part of the sentence, and subconsciously typed an underscore

[Abhimanyu Pallavi Sudhir]

Oh wait, do you mean the brackets in the definitions themselves?

[Kenny Lau]

if you do #check @one_mul then you can see all of the arguments required

[Mario Carneiro]

The reason nat.cast_lt got a @ and none of the others did is because at the beginning it's not clear what we are casting to. nat.cast actually works for a whole bunch of target types not just ℝ. Once the up arrows are introduced they carry enough information to figure out what type we are talking about

[Abhimanyu Pallavi Sudhir]

Ok, that makes sense. I also don't understand the bit0 stuff. Doesn't bit0 just double things? Why does it matter that the thing being casted is written as twice of something?

[Kenny Lau]

2 is just a notation. it really means bit0 1

[Kenny Lau]

try set_option pp.notations false

[Abhimanyu Pallavi Sudhir]

Yeah I get that, but if we were dealing with 1000 instead of 2, do we need to write a series of bit1's and bit0's there? What if we were dealing with a general natural number instead of 2?

[Kenny Lau]

simp will deal with it for you, I just don't really like using simp

[Kenny Lau]

change that to, I just really don't like using simp

[Abhimanyu Pallavi Sudhir]

You mean just "simp at h1"? Ok, yeah, that works.

[Mario Carneiro]

If we are dealing with a general natural number it is easier because it is just \u n

[Mario Carneiro]

The problem with \u 1000 vs 1000 is that the terms are completely different (the type of the expression is stored in all the subterms), and so we have to rewrite all the way through the term

[Mario Carneiro]

set_option pp.all true
#check (1000:ℤ)
-- @bit0.{0} int int.has_add
--   (@bit0.{0} int int.has_add
--      (@bit0.{0} int int.has_add
--         (@bit1.{0} int int.has_one int.has_add
--            (@bit0.{0} int int.has_add
--               (@bit1.{0} int int.has_one int.has_add
--                  (@bit1.{0} int int.has_one int.has_add
--                     (@bit1.{0} int int.has_one int.has_add
--                        (@bit1.{0} int int.has_one int.has_add (@has_one.one.{0} int int.has_one))))))))) :
--   int
#check ((1000:ℕ):ℤ)
-- @coe.{1 1} nat int (@coe_to_lift.{1 1} nat int (@coe_base.{1 1} nat int int.has_coe))
--   (@bit0.{0} nat nat.has_add
--      (@bit0.{0} nat nat.has_add
--         (@bit0.{0} nat nat.has_add
--            (@bit1.{0} nat nat.has_one nat.has_add
--               (@bit0.{0} nat nat.has_add
--                  (@bit1.{0} nat nat.has_one nat.has_add
--                     (@bit1.{0} nat nat.has_one nat.has_add
--                        (@bit1.{0} nat nat.has_one nat.has_add
--                           (@bit1.{0} nat nat.has_one nat.has_add (@has_one.one.{0} nat nat.has_one)))))))))) :
--   int

[Kenny Lau]

The thing is, simp is somewhat expensive, although not as expensive as norm_num

[Mario Carneiro]

is norm_num actually more expensive?

[Kenny Lau]

oops, I was thinking about ring

[Kenny Lau]

I was typing one thing and thinking about another thing

[Kenny Lau]

Anyway, I've been replacing simp with less expensive tactics from files in mathlib

[Abhimanyu Pallavi Sudhir]

Ok, I managed to work through and understand the proofs (at least the two longer ones -- will be a while before I can understand Kenny's two-line proofs). Thanks a lot! (that was my missing little lemma in proving p even if p^2 even).

[Mario Carneiro]

the two line proofs are easy: your theorem is by definition the same as "2 does not divide 1" and this is decidable (there is an instance in mathlib for it)

[Abhimanyu Pallavi Sudhir]

Why does expense/efficiency matter? You only need to run it once anyway.

[Abhimanyu Pallavi Sudhir]

the two line proofs are easy: your theorem is by definition the same as "2 does not divide 1" and this is decidable (there is an instance in mathlib for it)

Oh, ok. I just couldn't see through the notation.

[Mario Carneiro]

It doesn't matter too much, but once you start building up a huge library of maths the costs add up, and everyone who downloads mathlib will need to compile it, and mathlib itself changes on a daily basis and needs to be recompiled

[Mario Carneiro]

so it's not really a one time cost unless you view mathlib as fixed

[Mario Carneiro]

Most users can do so, but I can't since I'm a maintainer and neither can many contributors that jump between branches of mathlib

[Kevin Buzzard]

@Abhimanyu Pallavi Sudhir just to let you know that theorems like this (real 1/2 not the image of an integer), which are needed to do my problem sheets but which I would not expect a general undergraduate with 1 week's Lean experience to be able to do, are actually part of a small library I am writing which enables a generic UG to solve the problem sheet questions. See here https://github.com/ImperialCollegeLondon/M1F_example_sheets/tree/master/src/xenalib and in particular note the file called real_half_not_an_integer.lean. I am trying to do these messy parts for the students so they can just use them instead of running into walls.

[Abhimanyu Pallavi Sudhir]

@Kevin Buzzard Oh ok -- I wasn't really doing this for a problem sheet, though.

[Patrick Massot]

Kevin, why do you keep up arrows in statement? Is it meant to clarify the statement for human readers?

[Kevin Buzzard]

@Abhimanyu Pallavi Sudhir -- ha! I assumed you were working on Q7! @Patrick Massot you mean things like ¬ ∃ n : ℤ, (1/2 : ℚ) = ↑n? I guess so! I think the fact that Z is not a subset of Q is quite confusing for beginners. Maybe the arrow means "note: something a bit funny is going on here."

[Patrick Massot]

Yes, I meant that line. Lean wouldn't care if you wrote it without that up arrow

[Kevin Buzzard]

Right (although you'd see the arrow in the goal ;-) ).

[Patrick Massot]

You don't have to: set_option pp.coercions false :wink:

[Abhimanyu Pallavi Sudhir]

I managed to prove the statement in a "morally similar" way but without casting to R (or Q) -- it ends up being kinda long, see theorem one_not_even at https://github.com/abhimanyupallavisudhir/lean/blob/master/num_theo_theorems.lean

[Kenny Lau]

de_morgan is not_exists

[Kenny Lau]

all your by norm_num is rfl

[Kevin Buzzard]

We don't teach the first years complicated tactics like rfl

[Kevin Buzzard]

we stick to the simple ones like norm_num

[Kevin Buzzard]

they're a darn sight easier to learn

[Simon Hudon]

rfl is not necessarily faster than norm_num. The main idea of norm_num is actually to do things faster than than rfl and I think it worked out pretty well.

[Kenny Lau]

fair enough