Stream: new members

Topic: How to use equation compiler

Viktoriya Malyasova (Mar 16 2020 at 18:39):

I have a proof of zero_mult theorem:
--theorem zero_mult (n : nat) : 0 * n = 0 :=
--nat.rec_on n
--(show 0 * 0 = 0, by refl)
--(assume n,
-- assume ih: 0 * n = 0,
-- show 0 * succ n = 0, from
-- calc
-- 0 * succ n = 0 * n: by refl
-- ... = 0 : by rw ih
--)
And I am trying to rewrite it using equation compiler:
theorem zero_mult (n : nat) : 0 * n = 0
| 0 := rfl
|(succ n) :=
calc
0 * succ n = 0 * n: by refl
... = 0 : by rw (zero_mult n)

Lean says:
function expected at
zero_mult
term has type
0 * n = 0
Why? How am I supposed to do this?

Wojciech Nawrocki (Mar 16 2020 at 18:47):

The equation compiler will only match arguments to the right of the colon (:), so to make it work your declaration should look like: theorem zero_mult : ∀ (n : nat), 0 * n = 0.

Wojciech Nawrocki (Mar 16 2020 at 18:48):

By the way, when posting Lean code here you can wrap it in three backticks on both sides to have it pretty-printed, like so (you can click "View source" on my message to see what I typed in):

theorem zero_mult : ∀ (n : nat), 0 * n = 0
| 0 := rfl
| (nat.succ n) :=
calc
0 * (nat.succ n) = 0 * n : by refl
...              = 0     : by rw (zero_mult n)


Viktoriya Malyasova (Mar 16 2020 at 22:07):

Thank you so much!!!

Last updated: May 11 2021 at 00:31 UTC