# Zulip Chat Archive

## 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
(λ k ih, by simp [ih, nat.add_assoc, nat.add_comm, nat.add_left_comm])
```

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
simp [mult, nat.add_assoc, nat.add_comm, nat.add_left_comm] at ih,
simp [mult, ih, nat.add_assoc, nat.add_comm, nat.add_left_comm],
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
(λ k ih, by simp! [ih, nat.add_assoc, nat.add_comm, nat.add_left_comm])
```

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

```
lemma they_are_equal (m n : nat) :
mult m n = nat.rec_on n 0 (λ n mult_m_n, mult_m_n + m) :=
by induction n; simp! [*]
```

(The equation compiler's encoding isn't definitionally equal.)

Last updated: Dec 20 2023 at 11:08 UTC