One line proof?

Stream: new members

[Martin C. Martin]

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]

This one also fails:

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

[Martin C. Martin]

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

[Johan Commelin]

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

[Kyle Miller]

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]

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]

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]

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.)