Zulip Chat Archive

Stream: new members

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


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

view this post on Zulip Kenny Lau (Oct 11 2018 at 22:59):

by rw add_assoc

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:02):

rfl

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:02):

norm_num is the correct answer though

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:09):

norm_num is unknown identifier tho

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:09):

I am using the online version

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 11 2018 at 23:10):

norm_num is unknown identifier tho

Just import tactic.norm_num

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

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:12):

import went through

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:13):

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

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:14):

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

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:14):

You have to reassociate first

view this post on Zulip Kenny Lau (Oct 11 2018 at 23:14):

norm_num is the correct answer though

I would prefer rfl over norm_num

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:15):

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

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:15):

rfl works in small cases, especially on nat

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:15):

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

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:16):

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

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

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:16):

oh for my case I only work with int and nat

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:16):

no need for real here

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:17):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 23:17):

sure

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:17):

but for numbers less than 10 you should be fine

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:18):

cuz rfl does induction?

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:18):

It calculates both sides to a normal form in unary

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:19):

so it's exponentially slower than norm_num in large cases

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:19):

gotcha

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:25):

You have to reassociate first

this kinda beats the purpose of replacing rw add_assoc tho

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:26):

that's true

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:26):

ring will actually solve the whole goal in this case

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

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:26):

you can do mul_comm 2

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:27):

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

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:27):

gotcha

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:27):

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

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 23:28):

@Mario Carneiro Can Lean be better at golfing?

view this post on Zulip Kenny Lau (Oct 11 2018 at 23:28):

or is that actually pointless?

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:29):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 23:29):

I see

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:29):

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

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

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:32):

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

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:32):

rfl is less powerful than I thought

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:32):

or is it just in calc mode

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:32):

that's surprising

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

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:33):

do you have a MWE with your unrflable proof?

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:36):

Maybe I had a typo... a minute

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

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:42):

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

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:42):

same as norm_num

view this post on Zulip Kenny Lau (Oct 11 2018 at 23:43):

rfl works iff the two expressions are definitionally equal

view this post on Zulip Kenny Lau (Oct 11 2018 at 23:43):

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

view this post on Zulip Kenny Lau (Oct 11 2018 at 23:43):

that's unfolding definition of natural number multiplication

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:45):

it doesn't work tho

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

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:49):

rfl is a term not a tactic

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:49):

so there is no by

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:49):

also by rw rfl is always redundant (does nothing)

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:49):

ah i see

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:50):

didn't think to replace by as well

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:50):

works now

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:50):

there is a tactic version, called refl

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:50):

so by refl and rfl are usually interchangeable

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:52):

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

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:52):

thx y'all

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:53):

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

view this post on Zulip Yufan Lou (Oct 11 2018 at 23:54):

I know, writing out just for demonstration

view this post on Zulip Mario Carneiro (Oct 11 2018 at 23:54):

right

view this post on Zulip Yufan Lou (Oct 12 2018 at 00:02):

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

view this post on Zulip Mario Carneiro (Oct 12 2018 at 00:04):

what are the definitions?

view this post on Zulip Mario Carneiro (Oct 12 2018 at 00:04):

MWE please

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

view this post on Zulip Mario Carneiro (Oct 12 2018 at 00:05):

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

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

view this post on Zulip Yufan Lou (Oct 12 2018 at 00:06):

cool

view this post on Zulip Yufan Lou (Oct 12 2018 at 00:07):

what does | do and why _ following it?

view this post on Zulip Mario Carneiro (Oct 12 2018 at 00:07):

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

view this post on Zulip Mario Carneiro (Oct 12 2018 at 00:08):

the _ is the n from the statement

view this post on Zulip Yufan Lou (Oct 12 2018 at 00:08):

ahh pattern matching thx

view this post on Zulip Mario Carneiro (Oct 12 2018 at 00:08):

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

view this post on Zulip Yufan Lou (Oct 12 2018 at 00:10):

using rfl in pattern matching is pretty eye opening

view this post on Zulip Yufan Lou (Oct 12 2018 at 00:16):

Could you explain the pattern matching more thoroughly?

view this post on Zulip Yufan Lou (Oct 12 2018 at 00:16):

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

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

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

view this post on Zulip Kenny Lau (Oct 12 2018 at 00:32):

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

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