NNG4 Solutions

Website Hosted By Heinrich Heine University Düsseldorf

Assuming you have a basic understanding of Lean 4 — at least knowing what it is used for.

Tutorial World

Level 1. The rfl tactic

Introduce the first tactic called rfl, which proves all the theorems of the form X = X.

example (x q : Nat) : 37 * x + q = 37 * x + q := by
  rfl

About rfl:

• rfl is short for “reflexivity of equality”.
• For pedagogical purposes, our rfl is weaker than the standard version in Lean. Mathematicians don’t distinguish between propositional equality and definitional equality — to them, zero_add and add_zero are just “facts”, and who cares about how addition is defined.
• So in standard Lean, 2 + 2 = 4 can be provide by rfl because it’s a definitional equality. But in NNG4, 2 + 2 = 4 cannot be proved by rfl alone.

Level 2. the rw tactic

The proof is simply to substitute h into the goal, which can be done by rw [h]. After rewriting, the goal becomes 2 * (x + 7) = 2 * (x + 7).

example (x y : Nat) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by
  rw [h]
  rfl

About rw:

• If h is a proof of an equality X = Y, then rw [h] will change all Xs in the goal to Ys. It’s the way to “substitute in”.