I found another way of proving zero_force_zero_acceleration

Stream: Lean for Scientists and Engineers 2024

[Arshak Parsa]

If m*a=0 then either m=0 or a=0. but we know that m ≠ 0 so a must be zero!

import Mathlib

theorem zero_force_zero_acceleration {F m a : ℝ }
  (h1 : F = m*a)
  (h2 : m > 0):
  F = 0 → a = 0 := by
  intro hF
  have  hma : m*a = 0 := by rw [← h1, hF]
  rw [mul_eq_zero] at hma
  have hm : (m ≠ 0) := by exact ne_of_gt h2
  simp [hm] at hma
  exact hma

[Rick de Wolf]

Nice proof!

[Simon Beaumont]

Great work! :+1:

[Tyler Josephson ⚛️]

Nice, clean solution! Thank you! I'll put this in the post-lecture file.

[Kevin Buzzard]

What do you make of this proof:

import Mathlib

theorem zero_force_zero_acceleration {F m a : ℝ }
  (h1 : F = m*a)
  (h2 : m > 0):
  F = 0 → a = 0 := by
  rintro rfl
  exact eq_zero_of_ne_zero_of_mul_left_eq_zero h2.ne' <| h1.symm

[Kevin Buzzard]

You do all the work with mul_eq_zero, which says that $xy=0$ implies $x=0$ or $y=0$. But then you have to do some logic to deduce what you want. The logically very similar, but even better-fitting (for this problem) docs#eq_zero_of_ne_zero_of_mul_left_eq_zero can close it more quickly. I found this lemma using exact? (I'm not some guru that knows the names of all the lemmas, I just know how to use the tools to find them).

Here's how I found the proof:

import Mathlib

theorem zero_force_zero_acceleration {F m a : ℝ }
  (h1 : F = m*a)
  (h2 : m > 0):
  F = 0 → a = 0 := by
  -- let F be 0
  rintro rfl
  -- the lemma in mathlib won't have m > 0, it'll have m ≠ 0, because that's more general
  have foo : m ≠ 0 := by exact?
  -- Now find the lemma in the library which solves the problem immediately
  exact?

I then did some golfy tidying up to make the answer look more impressive and hence make me look cleverer than I am.

[Arshak Parsa]

@Kevin Buzzard
We actually had a proof for this theorem, but I was looking for a more human readable one. You golfed the proof. Your proof is not human readable to me, but there is an advantage here : Your proof uses less heartbeats compared to my proof, which means there is a trade-off between human readability and performance. Nice efficient proof, good job :+1:.

[Kevin Buzzard]

Oh I see, I didn't see the context! Yeah, the more you golf, the worse it gets :-)

Here's how you might use eq_zero_of_ne_zero_of_mul_left_eq_zero in a comprehensible way:

import Mathlib

theorem zero_force_zero_acceleration {F m a : ℝ }
    (h1 : F = m*a)
    (h2 : m > 0) (hF : F = 0) : -- why state the theorem as `F = 0 → a = 0`? Save the user the
                                -- bother of having to type `intro` by putting all your
                                -- assumptions left of the colon.
    a = 0 := by
  -- Replace `F` by `0` everywhere
  subst hF -- this is more efficient than rewriting `hF` everywhere.
  -- The library function `eq_zero_of_ne_zero_of_mul_left_eq_zero` says that x ≠ 0 and xy=0
  -- implies y = 0. So let's apply this theorem and then pick up the pieces.
  apply eq_zero_of_ne_zero_of_mul_left_eq_zero
  · -- here we need to show m ≠ 0
    show m ≠ 0
    -- but m > 0 so our inequality tactic will prove this
    linarith
  · -- here we need to show `⊢ m * a = 0` but we know `h1 : 0 = m * a`
    exact h1.symm -- this is "dot notation"!

Dot notation (used in the last line) is a cool trick, h1 is a proof of an equality, and = is just notation for the actual Lean equality function, which is Eq. So h1.symm means Eq.symm h1, which is h1 but with the sides swapped.

[Arshak Parsa]

Update :
I ran these theorems on my laptop instead of lean4 web, and here is the result in heartbeats :
My proof : 645 heartbeats
Kevin's first proof : 432 heartbeats
Kevin's second proof (linarith) : 826

linarith is ruining everything.
if you replace linarith with exact ne_of_gt h2, then heartbeats decrease to 436, which means you can have both readability and performance at the same time :)

[Kim Morrison]

Until you get to 10000(0?) heartbeats, please don't count. Readability and maintainability matter much more than counts in 100s or 1000s.

[Arshak Parsa]

Interesting observation:
you can reduce the heartbeats by changing import Mathlib to :

import Mathlib.Data.Real.Basic
import Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Now Kevin's first prove uses 190 heartbeats .

[Kim Morrison]

This is a true, interesting, and sad observation. Unfortunately as you import more and more, typeclass inference problems become harder, and sometimes simp works harder (this is sometimes a bug in mathlib, introducing @[simp] lemmas that always fire). We are working on improving this!