## Stream: new members

### Topic: Which rule to use for arithmetic calculations in calc mode?

#### Yufan Lou (Oct 11 2018 at 22:59):

I am trying to prove for any odd number n, 3n + 5 is even as a practice. In the calc steps I have:
3 * n + 5 = ...
... = 3 * 2 * k + 3 + 5 : by rw mul_assoc
... = 3 * 2 * k + 8 : by ?

What do I need to put in place of the question mark? I wrote the proof this way so as to closely track how I would write it manually, in hope I may introduce this to my classmates as a tool, so I don’t need to simplify it further.

#### Mario Carneiro (Oct 11 2018 at 23:02):

rfl

#### Mario Carneiro (Oct 11 2018 at 23:02):

norm_num is the correct answer though

#### Yufan Lou (Oct 11 2018 at 23:09):

norm_num is unknown identifier tho

#### Yufan Lou (Oct 11 2018 at 23:09):

I am using the online version

#### Abhimanyu Pallavi Sudhir (Oct 11 2018 at 23:10):

norm_num is unknown identifier tho

Just import tactic.norm_num

#### Mario Carneiro (Oct 11 2018 at 23:12):

I'm not sure if the online version has tactic.norm_num, it's got a quite old version of mathlib

#### Yufan Lou (Oct 11 2018 at 23:12):

import went through

#### Yufan Lou (Oct 11 2018 at 23:13):

curiously it still doesn't work. rw add_assoc works btw

#### Yufan Lou (Oct 11 2018 at 23:14):

Given by norm_num: ⊢ 3 + (5 + 6 * k) = 8 + 6 * k

#### Mario Carneiro (Oct 11 2018 at 23:14):

You have to reassociate first

#### Kenny Lau (Oct 11 2018 at 23:14):

norm_num is the correct answer though

I would prefer rfl over norm_num

#### Mario Carneiro (Oct 11 2018 at 23:15):

norm_num will evaluate closed term expressions but they have to all be gathered together

#### Mario Carneiro (Oct 11 2018 at 23:15):

rfl works in small cases, especially on nat

#### Yufan Lou (Oct 11 2018 at 23:15):

Problem I have with rfl is that the error is not helpful at all

#### Mario Carneiro (Oct 11 2018 at 23:16):

But stuff like 3 + 5 = 8 on real needs norm_num

#### Kenny Lau (Oct 11 2018 at 23:16):

Problem I have with rfl is that the error is not helpful at all

it just means they are not definitionally equal

#### Yufan Lou (Oct 11 2018 at 23:16):

oh for my case I only work with int and nat

#### Yufan Lou (Oct 11 2018 at 23:16):

no need for real here

#### Mario Carneiro (Oct 11 2018 at 23:17):

Also stuff like 100 * 35 = 3500 should not be done by rfl

sure

#### Mario Carneiro (Oct 11 2018 at 23:17):

but for numbers less than 10 you should be fine

#### Yufan Lou (Oct 11 2018 at 23:18):

cuz rfl does induction?

#### Mario Carneiro (Oct 11 2018 at 23:18):

It calculates both sides to a normal form in unary

#### Mario Carneiro (Oct 11 2018 at 23:19):

so it's exponentially slower than norm_num in large cases

gotcha

#### Yufan Lou (Oct 11 2018 at 23:25):

You have to reassociate first

this kinda beats the purpose of replacing rw add_assoc tho

that's true

#### Mario Carneiro (Oct 11 2018 at 23:26):

ring will actually solve the whole goal in this case

#### Yufan Lou (Oct 11 2018 at 23:26):

... = 3 * 2 * k + 8            : by rw add_assoc
... = 2 * 3 * k + 8            : by rw mul_comm


gives me ⊢ k * (3 * 2) + 8 = 2 * 3 * k + 8

#### Mario Carneiro (Oct 11 2018 at 23:26):

you can do mul_comm 2

#### Mario Carneiro (Oct 11 2018 at 23:27):

to give lean a bit of a hint of which mul to comm

gotcha

#### Mario Carneiro (Oct 11 2018 at 23:27):

that's one that norm_num can solve btw... or rfl

#### Kenny Lau (Oct 11 2018 at 23:28):

import data.real.basic tactic.norm_num

theorem test : (3:ℝ) + 5 = 8 :=
by norm_num

#print test

theorem test1 : (3:ℝ) + 5 = 8 :=

#print test1

theorem test2 : (3:ℝ) + 5 = 8 :=
calc  (3:ℝ) + 5
... = bit0 (norm_num.add1 (bit1 (1:ℝ))) : congr_arg _ (congr_arg _ (norm_num.one_add_bit0 _))
... = bit0 (bit0 (bit0 (1:ℝ))) : congr_arg _ (congr_arg _ norm_num.add1_one)

#print test2

theorem test : 3 + 5 = 8 :=
eq.mpr
(id
(eq.trans
((λ (a a_1 : ℝ) (e_1 : a = a_1) (a_2 a_3 : ℝ) (e_2 : a_2 = a_3), congr (congr_arg eq e_1) e_2) (3 + 5) 8
(norm_num.subst_into_sum 3 5 3 5 8 (eq.refl 3) (eq.refl 5)
8
8
(eq.refl 8))
(eq_true_intro (eq.refl 8))))
trivial

theorem test1 : 3 + 5 = 8 :=
eq.mpr (id (eq.rec (eq.refl (3 + 5 = 8)) (norm_num.bit1_add_bit1 1 2)))
(eq.mpr (id (eq.rec (eq.refl (bit0 (norm_num.add1 (1 + 2)) = 8)) (norm_num.one_add_bit0 1)))
(eq.mpr (id (eq.rec (eq.refl (bit0 (bit0 (norm_num.add1 1)) = 8)) norm_num.add1_one)) (eq.refl 8))))

theorem test2 : 3 + 5 = 8 :=
eq.trans


#### Kenny Lau (Oct 11 2018 at 23:28):

@Mario Carneiro Can Lean be better at golfing?

#### Kenny Lau (Oct 11 2018 at 23:28):

or is that actually pointless?

#### Mario Carneiro (Oct 11 2018 at 23:29):

Lean doesn't make it easy to golf proofs in tactics

I see

#### Yufan Lou (Oct 11 2018 at 23:29):

nevermind... the import seems successful but norm_num is not actually imported

#### Mario Carneiro (Oct 11 2018 at 23:30):

I would prefer that lean produced kind of short proofs (i.e. not obviously stupid things) but unfortunately dsimp ignores proof arguments

#### Yufan Lou (Oct 11 2018 at 23:32):

btw rfl didn't work on the replacement of rw mul_comm 2either

#### Yufan Lou (Oct 11 2018 at 23:32):

rfl is less powerful than I thought

#### Yufan Lou (Oct 11 2018 at 23:32):

or is it just in calc mode

#### Mario Carneiro (Oct 11 2018 at 23:32):

that's surprising

#### Mario Carneiro (Oct 11 2018 at 23:33):

this works for me in the web editor:

import tactic.norm_num
example : 3 + 5 = 8 := by norm_num


#### Mario Carneiro (Oct 11 2018 at 23:33):

do you have a MWE with your unrflable proof?

#### Yufan Lou (Oct 11 2018 at 23:36):

Maybe I had a typo... a minute

#### Yufan Lou (Oct 11 2018 at 23:40):

example {n : nat} (h1 : is_odd n) : is_even (n + 1) :=
exists.elim h1 (assume k, assume hw : n = 2 * k + 1,
exists.intro (k + 1)
(calc
n + 1 = 2 * k + 1 + 1 : by rw [hw]
... = 2 * k + 2     : by rw rfl
... = 2 * (k + 1)   : by rfl)


#### Yufan Lou (Oct 11 2018 at 23:42):

rfl doesn't work anytime I need to adjust association right

#### Yufan Lou (Oct 11 2018 at 23:42):

same as norm_num

#### Kenny Lau (Oct 11 2018 at 23:43):

rfl works iff the two expressions are definitionally equal

#### Kenny Lau (Oct 11 2018 at 23:43):

2*(n+1) for natural numbers is defined to be 2*n+2

#### Kenny Lau (Oct 11 2018 at 23:43):

that's unfolding definition of natural number multiplication

#### Yufan Lou (Oct 11 2018 at 23:45):

it doesn't work tho

#### Yufan Lou (Oct 11 2018 at 23:46):

example {n : nat} (h1 : is_odd n) : is_even (n + 1) :=
exists.elim h1 (assume k, assume hw : n = 2 * k + 1,
exists.intro (k + 1)
(calc
n + 1 = 2 * k + 1 + 1 : by rw [hw]
... = 2 * k + 2     : by rw add_assoc
... = 2 * k + 2 * 1 : by rw mul_one
... = 2 * (k + 1)   : by rw mul_add
))


without rfl this works, but I can't seem to replace any of them with rw rflor rfl

#### Mario Carneiro (Oct 11 2018 at 23:49):

rfl is a term not a tactic

#### Mario Carneiro (Oct 11 2018 at 23:49):

so there is no by

#### Mario Carneiro (Oct 11 2018 at 23:49):

also by rw rfl is always redundant (does nothing)

ah i see

#### Yufan Lou (Oct 11 2018 at 23:50):

didn't think to replace by as well

works now

#### Mario Carneiro (Oct 11 2018 at 23:50):

there is a tactic version, called refl

#### Mario Carneiro (Oct 11 2018 at 23:50):

so by refl and rfl are usually interchangeable

#### Yufan Lou (Oct 11 2018 at 23:52):

okay for simple calc proofs I can just put : rfl after each step nice

thx y'all

#### Mario Carneiro (Oct 11 2018 at 23:53):

actually a : rfl calc step can usually just be deleted entirely

#### Yufan Lou (Oct 11 2018 at 23:54):

I know, writing out just for demonstration

right

#### Yufan Lou (Oct 12 2018 at 00:02):

while we are at it is there a one-line proof of that theorem

#### Mario Carneiro (Oct 12 2018 at 00:04):

what are the definitions?

#### Yufan Lou (Oct 12 2018 at 00:04):

def is_even (a : nat) := ∃ b, a = 2 * b
def is_odd (a: nat) := ∃ b, a = 2 * b + 1
example {n : nat} (h1 : is_odd n) : is_even (n + 1)


#### Mario Carneiro (Oct 12 2018 at 00:05):

example : ∀ {n : nat}, is_odd n → is_even (n + 1)
| _ ⟨n, rfl⟩ := ⟨n+1, rfl⟩


#### Mario Carneiro (Oct 12 2018 at 00:06):

turns out the important part of the theorem is 2 * n + 1 + 1 = 2 * (n + 1) which is true by definition

cool

#### Yufan Lou (Oct 12 2018 at 00:07):

what does | do and why _ following it?

#### Mario Carneiro (Oct 12 2018 at 00:07):

I'm using the equation compiler to pattern match on the exists

#### Mario Carneiro (Oct 12 2018 at 00:08):

the _ is the n from the statement

#### Yufan Lou (Oct 12 2018 at 00:08):

ahh pattern matching thx

#### Mario Carneiro (Oct 12 2018 at 00:08):

but it is matched against 2*n+1 because I matched on the equality too

#### Yufan Lou (Oct 12 2018 at 00:10):

using rfl in pattern matching is pretty eye opening

#### Yufan Lou (Oct 12 2018 at 00:16):

Could you explain the pattern matching more thoroughly?

#### Yufan Lou (Oct 12 2018 at 00:16):

| _ ⟨n, rfl⟩ := ⟨n + 1, rfl⟩


#### Mario Carneiro (Oct 12 2018 at 00:28):

Since exists and eq are both inductive types, you can match on them, meaning you have to give a case for each constructor. Both only have one constructor, so there is only one case, where the exists is the Exists.mk function (which can also be written using the angle pair bracket) and the eq has the contstructor for equality which is rfl. If you put in both of those for the second argument, the first argument is forced to be (2*n+1) (Lean can figure this out, but if you want you can replace the _ with .(2*n+1), where the dot means that this argument's value is forced by later arguments.)

So in this case of the match, we have to prove the statement with n replaced with 2*n+1, that is, is_even (2 * n + 1 + 1). This is defeq to an exists, so I use the angle brackets to supply the witness, which is n+1, and the proof of equality, of type 2 * n + 1 + 1 = 2 * (n + 1), which as I said is true by reflexivity because both sides are defeq.

#### Mario Carneiro (Oct 12 2018 at 00:31):

the defeq chain looks like this btw:

2 * (n + 1)
= 2 * succ n
= 2 * n + 2
= 2 * n + succ 1
= succ (2 * n + 1)
= succ (succ (2 * n))

2 * n + 1 + 1
= succ (2 * n + 1)
= succ (succ (2 * n))


#### Kenny Lau (Oct 12 2018 at 00:32):

2 * (n + 1)
= 2 * (succ (n + 0))
= 2 * (succ n)
= 2 * n + 2
= ...


#### Mario Carneiro (Oct 12 2018 at 00:32):

I'll omit the steps that unfold the definition of +. :)

Last updated: May 12 2021 at 04:19 UTC