How to do 1 + 1 = 2

Stream: new members

[jakub]

Within a larger proof, how can I convert 1 + 1 to 2?

[Edward van de Meent]

norm_num

[Edward van de Meent]

(likely)

[Edward van de Meent]

if this is not actual integers, it might be a bit more complicated.

[jakub]

Edward van de Meent said:

if this is not actual integers, it might be a bit more complicated.

Yeah it is integers. So do I have to introduce an intermediary theorem with the have statement?

[Edward van de Meent]

no, i think you can do without introducing this as a local lemma

[Edward van de Meent]

the norm_num tactic should be able to simplify the term in most hypotheses and goals, afaik

[Edward van de Meent]

it might take norm_num at some_hypothesis if it's not the goal you're simplifying though

[jakub]

It doesn't even appear to be working within a calc, unless I misunderstood the syntax...

calc
      n * (n + 1) / 2 + (n + 1) = (n^2 + n) / 2 + (n + 1) := by norm_num

[jakub]

I'm struggling to do general arithmetic in lean

[Yaël Dillies]

I don't see any 1 + 1 in your calc. Did you accidentally copy the wrong line?

[jakub]

Yaël Dillies said:

I don't see any 1 + 1 in your calc. Did you accidentally copy the wrong line?

Nono what I'm referring to here is this

the norm_num tactic should be able to simplify the term in most hypotheses and goals, afaik

I understand this as norm_num being able to multiply and add things, (a more complicated example than 1 + 1 = 2 in this case,) but perhaps it can only add?

[Eric Wieser]

The claim was "if 1 + 1 appears somewhere in your goal, norm_num will replace it with 2"

[Eric Wieser]

The issue with your example is that norm_num does calculations on numeric literals, and n is not a literal

[jakub]

Either way it doesn't work as intended
For some reason this use of norm_num does not affect the goal

example (n : ℕ) : ∑ i in range n, (i + 1) = n * (n+1)/2 := by
  induction n
  case zero =>
    rw [sum_range_zero]

    rw [Nat.zero_mul]
    rw [Nat.zero_div]
  case succ n ih =>
    rw [sum_range_succ]
    rw [ih]
    norm_num

While doing it this way works:

example (n : ℕ) : ∑ i in range n, (i + 1) = n * (n+1)/2 := by
  induction n
  case zero =>
    rw [sum_range_zero]
    rw [Nat.zero_mul]
    rw [Nat.zero_div]
  case succ n ih =>
    rw [sum_range_succ]
    rw [ih]
    have h₁ : n + 1 + 1 = n + 2 := by norm_num
    rw [h₁]

[Ruben Van de Velde]

I'd probably recommend that anyway. Though note that somehow you ended up with unexpected spaces (non-breaking ones?) in your code, so the button to run in the live viewer doesn't work

[jakub]

Ruben Van de Velde said:

I'd probably recommend that anyway. Though note that somehow you ended up with unexpected spaces (non-breaking ones?) in your code, so the button to run in the live viewer doesn't work

How can I perform even more simplifications incrementally like the expansion one above?

[Eric Wieser]

I agree the behavior above is surprising; here's a minimized example:

import Mathlib

open scoped Nat

example : (n + 1 + 1) = (n + 2) := by norm_num
example : (n + 1 + 1)! = (n + 2)! := by norm_num
example : (n + 1 + 1) / 2 = (n + 2) / 2 := by norm_num  -- fails

[Shreyas Srinivas]

Btw, while others figure out why norm_num fails, omega is surprisingly versatile (no non-linearities allowed though):

import Mathlib

open scoped Nat

example : (n + 1 + 1) = (n + 2) := by norm_num
example : (n + 1 + 1)! = (n + 2)! := by norm_num
example : (n + 1 + 1) / 2 = (n + 2) / 2 := by norm_num  -- fails
example : (n + 1 + 1) / 2 = (n + 2) / 2 := by omega  -- succeeds

[Shreyas Srinivas]

as is nlinarith sometimes when no subtraction stuff is involved:

import Mathlib

open scoped Nat

example : (n + 1 + 1)! = (n + 2)! := by nlinarith

[Heather Macbeth]

The point here is that it's not norm_num's core operation doing the work, it's simp:

example : (n + 1 + 1) = (n + 2) := by simp -- works
example : (n + 1 + 1)! = (n + 2)! := by simp -- works

example : (n + 1 + 1) = (n + 2) := by norm_num1 -- fails
example : (n + 1 + 1)! = (n + 2)! := by norm_num1 -- fails

[Eric Wieser]

Aha!

import Mathlib

open scoped Nat

example : (n + 1 + 1) = (n + 2) := by norm_num only
example : (n + 1 + 1)! = (n + 2)! := by norm_num only
example : (n + 1 + 1) / 2 = (n + 2) / 2 := by norm_num only -- works

[Eric Wieser]

So simp is getting in the way of norm_num here

[Edward van de Meent]

actually, it doesnt:

import Mathlib

open scoped Nat

example : (n + 1 + 1) = 0 := by
  norm_num only
  sorry
example : (n + 1 + 1)! = 0 := by
  norm_num
  sorry
example : (n + 1 + 1) / 2 = 0 := by
  norm_num only -- works
  sorry

check the goals at sorry; i think the trick is that norm_num only tries rfl

[Edward van de Meent]

it doesn't actually change n + 1 + 1 into n + 2

[Heather Macbeth]

Observe the result of

example : (n + 1 + 1) / 2 = (n + 2) / 2 := by simp?

Namely, there are two simp-lemmas here which send simp (and by extension norm_num) down the wrong path: Nat.ofNat_pos, Nat.add_div_right.

[Heather Macbeth]

This works:

attribute [-simp] Nat.ofNat_pos Nat.add_div_right

example : (n + 1 + 1) / 2 = (n + 2) / 2 := by simp

[Heather Macbeth]

As does

example : (n + 1 + 1) / 2 = (n + 2) / 2 := by simp only

[Heather Macbeth]

Anyway, in my opinion the "correct" way to solve all three problems is ring_nf:

example : (n + 1 + 1) = (n + 2) := by ring_nf
example : (n + 1 + 1)! = (n + 2)! := by ring_nf
example : (n + 1 + 1) / 2 = (n + 2) / 2 := by ring_nf

[Heather Macbeth]

This is robust to variants like

example : (1 + n + 1) = (n + 2) := by ring_nf
example : (1 + n + 1)! = (n + 2)! := by ring_nf
example : (1 + n + 1) / 2 = (n + 2) / 2 := by ring_nf

[Heather Macbeth]

And ring_nf subsumes norm_num1.

[jakub]

Why is doing arithmetic so complicated in Lean?

[Edward van de Meent]

because arithmetic notation is secretly complicated

[Riccardo Brasca]

Because formalized mathematics is intrinsically difficult. We are working hard to create tactics to help, and indeed you first example 1+1=2 is not difficult (norm_num can do it).
Note that we immediately asked "which 1 are you talking about?" Normally one can ignore the difference between the natural number 1 and the real number 1, but in Lean everything must be 100% precise, and this difference has to be taken into account.

[Edward van de Meent]

you just don't notice because you're smart enough to get used to it and notice patterns of what you can/can't do. but lean doesn't learn those unless you tell them.

[Edward van de Meent]

and writing a lemma for each of those possible computations is sort of impractical

[Riccardo Brasca]

Yes, the point is that we (humans beings) are quite clever, even if computers are faster than us.

[jakub]

So what would be the best way of proving
n * (n + 1) / 2 + (n + 1) = (n + 1) * (n + 1 + 1) / 2
where n belongs to Nat without making a mess

[Riccardo Brasca]

Well, that statement is a mess. This is because the last operation / 2 is not what you think it is.

[Riccardo Brasca]

My suggestion is to simply avoid division of natural numbers, so to prove something like

import Mathlib

example (n : ℕ) : (n : ℚ) * (n + 1) / 2 + (n + 1) = (n + 1) * (n + 1 + 1) / 2 := by
  sorry

[Riccardo Brasca]

And then

import Mathlib

example (n : ℕ) : (n : ℚ) * (n + 1) / 2 + (n + 1) = (n + 1) * (n + 1 + 1) / 2 := by
  field_simp
  ring

works

[jakub]

Riccardo Brasca said:

Well, that statement is a mess. This is because the last operation / 2 is not what you think it is.

And what would that be? Is it like integer division in C (result in Nat)?

[Riccardo Brasca]

Yes, it is truncated division, so 1/2 = 0.

[Riccardo Brasca]

Note that what you want is true, but this is because n(n+1) and (n+1)(n+1+1) are even, and this step cannot be avoided in the proof.

[jakub]

Riccardo Brasca said:

And then

import Mathlib

example (n : ℕ) : (n : ℚ) * (n + 1) / 2 + (n + 1) = (n + 1) * (n + 1 + 1) / 2 := by
  field_simp
  ring

works

Is there a way to do that in even more incremental steps, so that it's more readable? Like break up the field_simpinto multiple simplifications?

[Riccardo Brasca]

Well, you can of course write down a calc proof that does every step explicitly, but these two tactics are not designed to write down a more readable proof.

[Riccardo Brasca]

But the full proof will probably be quite noisy, for example you are dividing by something (in ℚ now), so you surely have to prove that this something (that is 2) is not zero. This is "obvious", but Lean will ask you a proof (norm_num can do it).

[jakub]

Riccardo Brasca said:

And then

import Mathlib

example (n : ℕ) : (n : ℚ) * (n + 1) / 2 + (n + 1) = (n + 1) * (n + 1 + 1) / 2 := by
  field_simp
  ring

works

How could I convert n to Q when this goal is the final step in a larger proof?

[Riccardo Brasca]

import Mathlib

example (n : ℕ) : n * (n + 1) / 2 + (n + 1) = (n + 1) * (n + 1 + 1) / 2 := by
  have h₁ : 2 ∣ (n : ℤ) * (n + 1) := by
    obtain ⟨k, hk⟩ := Nat.even_mul_succ_self n
    use k
    rw [← two_mul] at hk
    exact mod_cast hk
  have h₂ : 2 ∣ ((n : ℤ) + 1) * (n + 1 + 1) := by
    obtain ⟨k, hk⟩ := Nat.even_mul_succ_self (n+1)
    use k
    rw [← two_mul] at hk
    exact mod_cast hk
  qify [h₁, h₂]
  field_simp
  ring

[Riccardo Brasca]

this is a proof of your initial result. I use the qify tactic to move to ℚ, where the same as above works. But note that I have to prove by hand that 2 ∣ (n : ℤ) * (n + 1), otherwise qify is not smart enough to understand that (n*(n+1)/2 : ℚ) = (n:ℚ)*(n+1)/2.

[Riccardo Brasca]

This may look over complicated, but the point is that truncated division is not well behaved, so if you really want to use it you have to work a little harder.

[jakub]

Riccardo Brasca said:

this is a proof of your initial result. I use the qify tactic to move to ℚ, where the same as above works. But note that I have to prove by hand that 2 ∣ (n : ℤ) * (n + 1), otherwise qify is not smart enough to understand that (n*(n+1)/2 : ℚ) = (n:ℚ)*(n+1)/2.

Could you not instead say, "this is true for all n belongs to Q" and "N is a subset of Q" so therefore it holds for all N?

[Riccardo Brasca]

This is what the tactic does, but if a and b are natural numbers, it is not true that a/b (that is a natural number!) viewed as a rational number is the same as (a : ℚ)/(b : ℚ).

[Riccardo Brasca]

I mean, 1/2=0 in ℕ, but (1: ℚ)/(2:ℚ) = 0.5 ≠ 0

[jakub]

Yeah that's fair enough. Thanks for explaining.

[jakub]

@Riccardo Brasca I followed your suggestion to avoid integer division and tried making it divide properly by making the divisor a member of Q, however I don't understand why the following code doesn't work. (I have replaced Nat.zero_mul and Nat.zero_div with Rat.zero_mul and Rat.zero_div, respectively.)

example (n : ℕ) : ∑ i in range n, (i + 1) = n * (n+1)/(2: ℚ) := by
  induction n
  case zero =>
    rw [sum_range_zero]
    rw [Rat.zero_mul]  -- error
    rw [Rat.zero_div]
  case succ n ih =>
    sorry

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  0 * ?a
⊢ ↑0 = ↑0 * (↑0 + 1) / 2

[Riccardo Brasca]

I am with the phone and I cannot check, but try to make the very first n a rational. Lean will make everything else also a rational automatically

[jakub]

That appears to be giving me the same error.

[Riccardo Brasca]

You probably need the fact that the coercion of zero is zero, maybe it is coe_zero. Anyway simp will surely do it

[Kyle Miller]

(In case it helps here and elsewhere, set_option pp.numericTypes true causes Lean to print the types of numerals)

[Kyle Miller]

norm_cast is helpful for getting rid of casts too

[Kyle Miller]

I might expect norm_num to be able to prove this too

[Kevin Buzzard]

The error message says it all : there's no 0, there's only a ↑0.

[Kevin Buzzard]

Note that case zero => simp works. You noted above that formalization is hard, and indeed this is true. We have built tactics to do all the grunt work, and you're just noting that if you don't use these tactics then reasoning formally can be very tedious. If you use simp? you'll be able to see exactly which lemmas are being used.

[Kevin Buzzard]

import Mathlib

open Finset

example (n : ℕ) : ∑ i in range n, (i + 1) = n * (n+1)/(2: ℚ) := by
  induction n
  case zero => simp
  case succ n ih =>
    push_cast at * -- deals with all the up-arrow issues
    simp [ih, sum_range_succ] -- applies the inductive hypothesis
    ring -- does the remaining algebra

[Kevin Buzzard]

On the other hand, especially if you are just beginning to explore in this area and really want to see everything from first principles, then I think you would have a lot more fun doing an example which does not involve subtraction or division, because then you can stay purely within the realm of the natural numbers and you won't run into all these annoyances with coercions. For example you might enjoy playing with this example, where a first principles approach will be far less tedious:

import Mathlib

open Finset

example (n : ℕ) : ∑ i in range n, (2 * i + 1) = n * n := by
  induction n
  case zero =>
    sorry
  case succ n ih =>
    sorry

[Kevin Buzzard]

When I was in your situation in 2017, wanting to see how everything fitted together, not only was the subtraction/division annoyance still there, but we didn't have the tools to do everything automatically so the tedious approach was the only approach. It was at that time that I started realising that avoiding natural division made things much more fun.

[jakub]

Kevin Buzzard said:

On the other hand, especially if you are just beginning to explore in this area and really want to see everything from first principles, then I think you would have a lot more fun doing an example which does not involve subtraction or division, because then you can stay purely within the realm of the natural numbers and you won't run into all these annoyances with coercions. For example you might enjoy playing with this example, where a first principles approach will be far less tedious:

import Mathlib

open Finset

example (n : ℕ) : ∑ i in range n, (2 * i + 1) = n * n := by
  induction n
  case zero =>
    sorry
  case succ n ih =>
    sorry

I proved the theorem you suggested above :smile:
Do you know if you could point me to some resources that teach coercions in lean? I'm having trouble finding some but would love to understand how the proof of my original theorem with division and coercions functions

[jakub]

Of course this also applies to anyone else who might have resources covering coercions :smile:

[Yan Yablonovskiy]

jakub said:

Why is doing arithmetic so complicated in Lean?

As someone that is also new to it, i think it seems more that way because we might be used to 'programming' generally doing something like this easily.

But in the sense of a proof assistant, 'proving' 1+1 = 2 isn't the same as calculating it generally. So just from the way i've reconciled it -- is that when a calculator does 1+1=2 it carries very little actual logical information to what this even means.

For a proof context however, it comes with all sorts of implications tied to what '1' is and what it does in other contexts, how '+' might work in the most abstract setting , whether univalence is involved, how the new object '2' might 'relate' to 1 ( 2 > 1) etc.

In this way too, the ring tactic carries the least auxiliary information; it may be more flexible in some specialised contexts.

Just my 2 cents though, not sure if that is helpful.

[Kevin Buzzard]

I don't know what "teach coercions in lean" means. The thing you need to know are the norm_cast and push_cast tactics, and you can read their docstrings to see what they do. In a nutshell, the natural number 37 and the integer 37 and the rational number 37 and etc etc are all different objects in lean, and they're all related by maps which don't appear in the textbooks (ie they're invisible) but in lean they're all visible and all have the same notation which is up-arrow.

[Edward van de Meent]

even in textbooks, they aren't technically the same... the construction of 37 : Real in ZFC, for example, is a different set from 37 : Nat, 37 : Int or 37 : Rat.

[Edward van de Meent]

to the point that stuff like (37:Rat) ∈ (2074 : Real) is a true statement that makes sense in ZFC :vomit:

[Edward van de Meent]

(i like type theory, if you hadn't noticed)

[jakub]

Kevin Buzzard said:

I don't know what "teach coercions in lean" means. The thing you need to know are thenorm_cast and push_cast tactics, and you can read their docstrings to see what they do. In a nutshell, the natural number 37 and the integer 37 and the rational number 37 and etc etc are all different objects in lean, and they're all related by maps which don't appear in the textbooks (ie they're invisible) but in lean they're all visible and all have the same notation which is up-arrow.

If you're giving me the nutshell here, what I'm looking for is the nut :big_smile:
That's what I meant by "teaching coercions", i.e. I'm trying to find a resource that goes more into detail into how to work with coercions in lean. And I'm sure there's more to it than just norm_cast and push_cast.

[Luigi Massacci]

Edward van de Meent said:

to the point that stuff like (37:Rat) ∈ (2074 : Real) is a true statement that makes sense in ZFC :vomit:

wait, at the risk of derailing the conversation, while I agree that is a well formed statement in ZFC, I am rather skeptical that it is true (at least in the usual cauchy seq. encoding of reals and with kuratowski pairs)

[Niels Voss]

He might be talking about Dedekind cuts, in which a real number is identified with the set of rational numbers less than it.

[Luigi Massacci]

Ah, yes makese sense