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