Which rule to use for arithmetic calculations in calc mode?

Stream: new members

[Yufan Lou]

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.

[Kenny Lau]

by rw add_assoc

[Mario Carneiro]

rfl

[Mario Carneiro]

norm_num is the correct answer though

[Yufan Lou]

norm_num is unknown identifier tho

[Yufan Lou]

I am using the online version

[Abhimanyu Pallavi Sudhir]

norm_num is unknown identifier tho

Just import tactic.norm_num

[Mario Carneiro]

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

[Yufan Lou]

import went through

[Yufan Lou]

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

[Yufan Lou]

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

[Mario Carneiro]

You have to reassociate first

[Kenny Lau]

norm_num is the correct answer though

I would prefer rfl over norm_num

[Mario Carneiro]

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

[Mario Carneiro]

rfl works in small cases, especially on nat

[Yufan Lou]

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

[Mario Carneiro]

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

[Kenny Lau]

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

it just means they are not definitionally equal

[Yufan Lou]

oh for my case I only work with int and nat

[Yufan Lou]

no need for real here

[Mario Carneiro]

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

[Kenny Lau]

sure

[Mario Carneiro]

but for numbers less than 10 you should be fine

[Yufan Lou]

cuz rfl does induction?

[Mario Carneiro]

It calculates both sides to a normal form in unary

[Mario Carneiro]

so it's exponentially slower than norm_num in large cases

[Yufan Lou]

gotcha

[Yufan Lou]

You have to reassociate first

this kinda beats the purpose of replacing rw add_assoc tho

[Mario Carneiro]

that's true

[Mario Carneiro]

ring will actually solve the whole goal in this case

[Yufan Lou]

... = 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]

you can do mul_comm 2

[Mario Carneiro]

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

[Yufan Lou]

gotcha

[Mario Carneiro]

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

[Kenny Lau]

import data.real.basic tactic.norm_num

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

#print test

theorem test1 : (3:ℝ) + 5 = 8 :=
by rw [norm_num.bit1_add_bit1, norm_num.one_add_bit0,
norm_num.add1_bit1, norm_num.add1_one]

#print test1

theorem test2 : (3:ℝ) + 5 = 8 :=
calc  (3:ℝ) + 5
    = bit0 (norm_num.add1 ((1:ℝ) + 2)) : norm_num.bit1_add_bit1 _ _
... = bit0 (norm_num.add1 (bit1 (1:ℝ))) : congr_arg _ (congr_arg _ (norm_num.one_add_bit0 _))
... = bit0 (bit0 (norm_num.add1 (1:ℝ))) : congr_arg _ (norm_num.add1_bit1 _)
... = 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)
              (norm_num.bit1_add_bit1_helper 1 2 3 4 (norm_num.one_add_bit0 1)
                 (norm_num.add1_bit1_helper 1 2 norm_num.add1_one)))
           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 (norm_num.add1 3) = 8)) (norm_num.add1_bit1 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
  (eq.trans (eq.trans (norm_num.bit1_add_bit1 1 2) (congr_arg bit0 (congr_arg norm_num.add1 (norm_num.one_add_bit0 1))))
     (congr_arg bit0 (norm_num.add1_bit1 1)))
  (congr_arg bit0 (congr_arg bit0 norm_num.add1_one))

[Kenny Lau]

@Mario Carneiro Can Lean be better at golfing?

[Kenny Lau]

or is that actually pointless?

[Mario Carneiro]

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

[Kenny Lau]

I see

[Yufan Lou]

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

[Mario Carneiro]

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

[Yufan Lou]

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

[Yufan Lou]

rfl is less powerful than I thought

[Yufan Lou]

or is it just in calc mode

[Mario Carneiro]

that's surprising

[Mario Carneiro]

this works for me in the web editor:

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

[Mario Carneiro]

do you have a MWE with your unrflable proof?

[Yufan Lou]

Maybe I had a typo... a minute

[Yufan Lou]

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]

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

[Yufan Lou]

same as norm_num

[Kenny Lau]

rfl works iff the two expressions are definitionally equal

[Kenny Lau]

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

[Kenny Lau]

that's unfolding definition of natural number multiplication

[Yufan Lou]

it doesn't work tho

[Yufan Lou]

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]

rfl is a term not a tactic

[Mario Carneiro]

so there is no by

[Mario Carneiro]

also by rw rfl is always redundant (does nothing)

[Yufan Lou]

ah i see

[Yufan Lou]

didn't think to replace by as well

[Yufan Lou]

works now

[Mario Carneiro]

there is a tactic version, called refl

[Mario Carneiro]

so by refl and rfl are usually interchangeable

[Yufan Lou]

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

[Yufan Lou]

thx y'all

[Mario Carneiro]

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

[Yufan Lou]

I know, writing out just for demonstration

[Mario Carneiro]

right

[Yufan Lou]

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

[Mario Carneiro]

what are the definitions?

[Mario Carneiro]

MWE please

[Yufan Lou]

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]

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

[Mario Carneiro]

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

[Yufan Lou]

cool

[Yufan Lou]

what does | do and why _ following it?

[Mario Carneiro]

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

[Mario Carneiro]

the _ is the n from the statement

[Yufan Lou]

ahh pattern matching thx

[Mario Carneiro]

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

[Yufan Lou]

using rfl in pattern matching is pretty eye opening

[Yufan Lou]

Could you explain the pattern matching more thoroughly?

[Yufan Lou]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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