## Stream: new members

### Topic: One line proof?

#### Martin C. Martin (Jul 27 2022 at 13:56):

In TPiL chapter 7, they introduce calc proofs for zero_add, add_assoc and add_comm, then reduce each to a single line using simp.

I defined my own multiplication this way:

def mult (m n : nat) : nat :=
nat.rec_on n 0 (λ n mult_m_n, mult_m_n + m)


And can prove right distributivity this way:

local attribute [simp] nat.add_assoc nat.add_comm nat.add_left_comm

theorem distrib_right : mult (n + m) k = (mult n k) + mult m k :=
nat.rec_on k
(show mult (n + m) 0 = (mult n 0) + mult m 0, from rfl)
(assume k ih,
calc
mult (n + m) k.succ = (mult (n + m) k) + (n + m) : rfl
... = (mult n k) + (mult m k)  + (n + m) : by rw ih
... = (mult n k) + n + ((mult m k) + m) : by simp
... = (mult n k.succ) + mult m k.succ : rfl )


But when I try to reduce it to a single line, I just get "simp failed" with no details:

theorem distrib_right' : mult (n + m) k = (mult n k) + mult m k :=
nat.rec_on k
rfl


Can we get the single line version working? Also, how can I get more information when simp fails, to debug things like this?

#### Martin C. Martin (Jul 27 2022 at 14:12):

This one also fails:

theorem mul_one' : mult n 1 = n := by simp [nat.zero_add]


#### Martin C. Martin (Jul 27 2022 at 15:13):

It looks like I can't rely on simp to apply my definition of mult, as rfl does?

#### Johan Commelin (Jul 27 2022 at 15:15):

Yes, you'll certainly have to pass mult to simp.

#### Kyle Miller (Jul 27 2022 at 15:27):

You can also use the ! flag for simp (so use simp!) to do definition expansion for all definitions (edit: but that doesn't seem to work here)

#### Kyle Miller (Jul 27 2022 at 15:30):

One issue with distrib_right is that ih is not in the right form to be applied. Here's a rough fix:

theorem distrib_right' : mult (n + m) k = (mult n k) + mult m k :=
nat.rec_on k
rfl
(λ k ih, begin
end)


#### Kyle Miller (Jul 27 2022 at 15:32):

Generally in Lean you write recursive definitions using the so-called "equation compiler" rather than using recursors directly. That generates additional simplification lemmas that the ! flag has access to:

def mult (m : nat) : Π (n : nat), nat
| 0 := 0
| (n+1) := mult n + m

variables {n m k : nat}

theorem distrib_right' : mult (n + m) k = (mult n k) + mult m k :=
nat.rec_on k
rfl

lemma they_are_equal (m n : nat) :