Lean exercises on your machine

Three theorems of constant acceleration and of an impulse between two particles, given as Lean 4 stubs to complete locally, with hints, and with the solutions that CI compiles, read from the repository.

Course

Classical mechanics, lesson 27 of 28

Methods

Formal proofs

Difficulty

Intermediate, level 2 of 3

What you’ll learn

Complete a Lean 4 stub on your own machine and check it with the pinned toolchain
Prove an identity of constant acceleration and a momentum balance by substitution and algebra
Say why the site shows a stub as not verified and a solution as checked

Prerequisites

Proving what the simulation showed.

Before you begin

Logic: reading a statement that says if these hypotheses hold, then this conclusion holds
Algebra: expanding and factorising polynomials in several variables

Related

none

Previous

What symplectic Euler conserves

Next

The chirp law, proved

With scripts, this page keeps a record in your browser of whether you completed the lesson. Nothing is stored without them.

With scripts, this place suggests what to do next, with the reason, from the progress saved in your browser. Without them, follow the learning path.

The first Lean lesson showed finished proofs. Reading a proof is not writing one: the tactics only make sense once you have been stuck with a goal that will not close. This lesson gives you three theorems to prove yourself, in the same Lean project that checks the proofs of the other lessons.

The site does not run Lean for you, and there is no editor on this page. You work in a clone of the repository, with the pinned toolchain, and the compiler tells you whether a proof is finished. What the site adds is the statement, a sequence of hints that you open one at a time, and a solution that CI compiles on every change.

Assumptions

The model is that of the kinematics lesson. Position and velocity at time $t$ are the two formulas of constant acceleration, taken as the hypotheses hx and hv. Nothing is assumed about a program.
A non-zero acceleration where the statement divides by it. The hypothesis ha : a ≠ 0 is part of the statement: with $a = 0$ the speed does not change and the distance cannot be recovered from it.
Non-zero masses in the impulse exercise. hm₁ and hm₂ let the impulse $J$ be turned into a change of velocity, $J / m$ .
Real numbers, not floating-point numbers. As in the other Lean lessons.

How an exercise works

Each exercise is a file of the repository, lean/Exercises/<Name>.lean. It states one or more theorems and ends each proof with sorry, Lean’s word for “proof missing”. Lean accepts the file and warns, for every sorry: the theorem is stated and nothing is proved. You replace the sorry with tactics until the warning is gone.

The stubs are not in the library that the other lessons display. The library may not contain sorry, and the check that guarantees it (./scripts/check-lean.sh) would fail on a stub. The stubs therefore live in lean/Exercises/, outside the library, and the check treats them in a different way. For each stub it requires a module of the library, in lean/PhysicsByConstruction/Exercises/, with the same name and the same theorem statements, and a proof without sorry that it compiles and audits like every other proof. A stub without a solution, or with a statement that differs from its solution’s, fails the check (the decision record on exercise stubs is ADR 011).

So on this page a stub is shown in a box marked not verified, because it proves nothing, and a solution is shown like any proof of the project, read from the file that was compiled.

To work on an exercise, open the lean/ directory of your clone in an editor with Lean support, edit the file, and check it:

Not verified. The build of this site did not run or check the material in this box.

$ cd lean
$ lake env lean Exercises/ConstantAcceleration.lean

The exercises

Compiled with Lean 4.34.1 and Mathlib v4.34.1: ./scripts/check-lean.sh found no sorry and no axiom declared by the project before this page was built.

Commit 6417e2ff90258bd2d2ba21d217eb7666fd24f680 of the repository.

What was checked, and where to read the proofs

./scripts/check-lean.sh ran lake build on every module of the project and found no sorry and no axiom declared by the project before this page was built. CI runs the same check on every pull request and on main.

Lean 4.34.1, from the toolchain pinned in lean/lean-toolchain.
Mathlib v4.34.1, revision d13f23b723.
lean/PhysicsByConstruction/Exercises/ConstantAcceleration.lean, or open it in the Lean web editor
lean/PhysicsByConstruction/Exercises/Impulse.lean, or open it in the Lean web editor

The file in the repository at that commit and the result of the CI run are authoritative. The Lean web editor is a convenience: it runs its own version of Mathlib, which can differ from the one above, so a proof that compiled here may report an error there.

The box above states what compiled the solutions. The stubs shown in the exercises below are the files lean/Exercises/ConstantAcceleration.lean and lean/Exercises/Impulse.lean, which the same check compiled with nothing but their sorry warnings.

Worked examples

A theorem covers every choice of the numbers, and a run covers a few. Before you prove a statement, it is worth seeing what it says about one choice. The cell evaluates both sides of the first two statements for a particle thrown up at 20 m/s and slowed by gravity, and the momentum balance for two carts.

a, v0, x0, t = -9.81, 20.0, 0.0, 1.5  # m/s^2, m/s, m, s

src/pbc/mechanics/experiments/lean_exercises_on_your_machine.py, line 20, read from the repository when this page was built.

def both_sides():
    """Both sides of the three statements, for a throw and for an impulse."""
    x = x0 + v0 * t + a * t**2 / 2
    v = v0 + a * t
    print(f"x - x0                 = {x - x0:.4f} m")
    print(f"(v^2 - v0^2) / (2 a)   = {(v**2 - v0**2) / (2 * a):.4f} m")
    print(f"t                      = {t:.4f} s")
    print(f"(v - v0) / a           = {(v - v0) / a:.4f} s")

    m1, m2, u1, u2, J = 0.5, 1.5, 2.0, -1.0, 0.8  # kg, kg, m/s, m/s, N s
    w1, w2 = u1 - J / m1, u2 + J / m2
    print(f"momentum before        = {m1 * u1 + m2 * u2:.4f} kg m/s")
    print(f"momentum after         = {m1 * w1 + m2 * w2:.4f} kg m/s")

src/pbc/mechanics/experiments/lean_exercises_on_your_machine.py, lines 24 to 36, read from the repository when this page was built.

x - x0                 = 18.9637 m
(v^2 - v0^2) / (2 a)   = 18.9638 m
t                      = 1.5000 s
(v - v0) / a           = 1.5000 s
momentum before        = -0.5000 kg m/s
momentum after         = -0.5000 kg m/s

def draw_two_sides() -> Figure:
    """The two sides of the first statement over three seconds."""
    times = np.linspace(0.0, 3.0, 61)
    distance = v0 * times + a * times**2 / 2
    speed = v0 + a * times
    fig, ax = plt.subplots(figsize=(6.4, 3.4))
    ax.plot(times, distance, color="#00429d", linewidth=3, label="x - x0")
    ax.plot(
        times,
        (speed**2 - v0**2) / (2 * a),
        color="white",
        linestyle="--",
        linewidth=1.2,
        label="(v^2 - v0^2) / (2 a)",
    )
    ax.set_xlabel("time (s)")
    ax.set_ylabel("distance (m)")
    ax.legend(loc="lower center")
    return fig

src/pbc/mechanics/experiments/lean_exercises_on_your_machine.py, lines 39 to 57, read from the repository when this page was built.

Plot of distance in metres against time in seconds from 0 to 3. A thick blue solid curve of the distance covered rises, bends over near 2 seconds and falls. A white dashed curve of the change of the squared speed divided by 2a lies exactly on it, so the two cannot be told apart. — Figure 1: simulated Both sides of the first statement, the distance covered and the change of the squared speed divided by 2a, against time for the thrown particle.

The two sides agree to the digits shown. That is an instance of each statement, not a proof of it: the proof is what you write in Lean.

Limits

The site cannot check your proof. There is no Lean in the page. The compiler on your machine is the judge; a proof that compiles there, with the toolchain pinned in lean/lean-toolchain, is complete.
Not graded and not recorded. Nothing you do is sent anywhere or stored by the site.
The solutions are public. They are in the repository. The hints are a courtesy for a reader who wants to find the proof alone.
Statements, not physics. A theorem here says what follows from the hypotheses; whether a real motion has constant acceleration is a question for measurement.

Self-check. Why is ha : a ≠ 0 a hypothesis of displacement_from_speeds and not something the proof can derive?

With scripts, you can record in this browser that you answered this question.

Solution to the self-check

Because the statement is false without it. With $a = 0$ the speed never changes, so $v^2 - v_0^2 = 0$ for every distance, and in Lean division by zero is zero, so the right-hand side is zero while $x - x_0 = v_0 t$ is not. A hypothesis is the place where the theorem says what it needs.

Exercises

Exercise 1. The distance from the speeds. Prove that, with constant acceleration, the distance covered is the change of the squared speed divided by $2a$ .

Not verified. The build of this site did not run or check the material in this box.

/-- With a non-zero constant acceleration `a`, the distance covered is the
change of the squared speed divided by `2 a`. -/
theorem displacement_from_speeds
    (x₀ v₀ a t x v : ℝ) (ha : a ≠ 0)
    (hx : x = x₀ + v₀ * t + a * t ^ 2 / 2)
    (hv : v = v₀ + a * t) :
    x - x₀ = (v ^ 2 - v₀ ^ 2) / (2 * a) := by
  sorry

The stub lean/Exercises/ConstantAcceleration.lean contains sorry: it states the exercise and proves nothing. You complete it on your machine; the site does not run Lean for you.

Hint 1 of 3 for exercise 1

The two hypotheses give $x$ and $v$ as expressions. Remove the variables x and v first.

Hint 2 of 3 for exercise 1

The subst tactic does that, for both hypotheses at once.

Hint 3 of 3 for exercise 1

The goal now has a division by $2a$ . The tactic field_simp clears it, using ha, and ring closes the remaining identity of polynomials.

Solution to exercise 1

/-- With a non-zero constant acceleration `a`, the distance covered is the
change of the squared speed divided by `2 a`. -/
theorem displacement_from_speeds
    (x₀ v₀ a t x v : ℝ) (ha : a ≠ 0)
    (hx : x = x₀ + v₀ * t + a * t ^ 2 / 2)
    (hv : v = v₀ + a * t) :
    x - x₀ = (v ^ 2 - v₀ ^ 2) / (2 * a) := by
  subst hx hv
  field_simp
  ring

lean/PhysicsByConstruction/Exercises/ConstantAcceleration.lean, lines 18 to 27, read from the repository when this page was built.

After the substitution both sides are rational expressions in the same variables; field_simp multiplies out the denominator and ring checks the identity.

Exercise 2. The time from the speeds. Prove that the time taken is the change of speed divided by the acceleration.

Not verified. The build of this site did not run or check the material in this box.

/-- With a non-zero constant acceleration `a`, the time taken is the change
of speed divided by `a`. -/
theorem time_from_speeds
    (v₀ a t v : ℝ) (ha : a ≠ 0)
    (hv : v = v₀ + a * t) :
    t = (v - v₀) / a := by
  sorry

The stub lean/Exercises/ConstantAcceleration.lean contains sorry: it states the exercise and proves nothing. You complete it on your machine; the site does not run Lean for you.

Hint 1 of 2 for exercise 2

Only one hypothesis is needed, and it is the one about v.

Hint 2 of 2 for exercise 2

The same three tactics as in the first exercise work: substitute, clear the division, and close with ring.

Solution to exercise 2

/-- With a non-zero constant acceleration `a`, the time taken is the change
of speed divided by `a`. -/
theorem time_from_speeds
    (v₀ a t v : ℝ) (ha : a ≠ 0)
    (hv : v = v₀ + a * t) :
    t = (v - v₀) / a := by
  subst hv
  field_simp
  ring

lean/PhysicsByConstruction/Exercises/ConstantAcceleration.lean, lines 31 to 39, read from the repository when this page was built.

Exercise 3. Momentum under an impulse. Two particles on a line exchange an impulse: the first loses $J$ , the second gains it. Prove that the total momentum is the same before and after.

Not verified. The build of this site did not run or check the material in this box.

/-- Two particles on a line exchange an impulse `J`: the first loses it, the
second gains it. Their total momentum is the same before and after. -/
theorem impulse_momentum
    (m₁ m₂ v₁ v₂ v₁' v₂' J : ℝ) (hm₁ : m₁ ≠ 0) (hm₂ : m₂ ≠ 0)
    (h₁ : v₁' = v₁ - J / m₁)
    (h₂ : v₂' = v₂ + J / m₂) :
    m₁ * v₁' + m₂ * v₂' = m₁ * v₁ + m₂ * v₂ := by
  sorry

The stub lean/Exercises/Impulse.lean contains sorry: it states the exercise and proves nothing. You complete it on your machine; the site does not run Lean for you.

Hint 1 of 2 for exercise 3

The hypotheses h₁ and h₂ define the new velocities. Substitute them.

Hint 2 of 2 for exercise 3

The goal now contains each mass times the impulse divided by that same mass. They cancel only because the masses are not zero: that is what hm₁ and hm₂ are for, and what field_simp uses.

Solution to exercise 3

/-- Two particles on a line exchange an impulse `J`: the first loses it, the
second gains it. Their total momentum is the same before and after. -/
theorem impulse_momentum
    (m₁ m₂ v₁ v₂ v₁' v₂' J : ℝ) (hm₁ : m₁ ≠ 0) (hm₂ : m₂ ≠ 0)
    (h₁ : v₁' = v₁ - J / m₁)
    (h₂ : v₂' = v₂ + J / m₂) :
    m₁ * v₁' + m₂ * v₂' = m₁ * v₁ + m₂ * v₂ := by
  subst h₁ h₂
  field_simp
  ring

lean/PhysicsByConstruction/Exercises/Impulse.lean, lines 15 to 24, read from the repository when this page was built.

Compare with the collision lesson, which proves the same conservation for a rule with a direction and a sum over axes; here the impulse is given, and the proof is the cancellation alone.

Check this proof

This page was built from commit 6417e2ff90258bd2d2ba21d217eb7666fd24f680 of the repository.

In a clone at that commit, with the pinned Lean toolchain, this command in lean/ checks the proofs of this page:

lake build PhysicsByConstruction.Exercises.ConstantAcceleration PhysicsByConstruction.Exercises.Impulse

Files, tests, and every command

The files behind it:

site/lessons/lean/04-lean-exercises-on-your-machine/index.qmd: this page, with every code cell.
lean/Exercises/ConstantAcceleration.lean: a Lean file the page shows.
lean/Exercises/Impulse.lean: a Lean file the page shows.
lean/PhysicsByConstruction/Exercises/ConstantAcceleration.lean: a Lean file the page shows.
lean/PhysicsByConstruction/Exercises/Impulse.lean: a Lean file the page shows.
src/pbc/mechanics/experiments/lean_exercises_on_your_machine.py: code the experiment runs.
src/pbc/experiment.py: code the experiment runs.
tests/unit/test_lean_exercises.py: tests of that code.
tests/unit/test_lean_exercises_on_your_machine_experiment.py: tests of that code.

With Git and uv, and elan for the proofs, installed (see the setup page), run:

git clone https://github.com/taspinar/physics-by-construction.git
cd physics-by-construction
git checkout 6417e2ff90258bd2d2ba21d217eb7666fd24f680
uv sync --locked --no-dev
uv run --locked --no-dev python -m pbc.mechanics.experiments.lean_exercises_on_your_machine results
cd lean
lake exe cache get
lake build PhysicsByConstruction.Exercises.ConstantAcceleration PhysicsByConstruction.Exercises.Impulse

The experiment writes every figure of this page into results/, as <label>.png, and every number and table of the page, as the page shows it, into results/results.json. Its numbers match this page to the digits shown, and its figure files are the ones the page shows; digits beyond those can differ between machines, because floating-point libraries differ. Change the code of the experiment and run it again to see what changes.

lake build compiles the proofs of this page with the Lean toolchain that elan installs; the first run fetches the Mathlib build cache, which is large. The setup page says how to install elan.