Summary

rfl proves goals of the form X = X.

In other words, the rfl tactic will close any goal of the form A = B if A and B are identical.

rfl is short for "reflexivity (of equality)".

Example:

If the goal looks like this:

x + 37 = x + 37

then rfl will close it. But if it looks like 0 + x = x then rfl won't work, because even though 0+x and x are always equal as numbers, they are not equal as terms. The only term which is identical to 0 + x is 0 + x.

Details

rfl is short for "reflexivity of equality".

Game Implementation

Note that our rfl is weaker than the version used in core Lean and mathlib, for pedagogical purposes; mathematicians do not distinguish between propositional and definitional equality because they think about definitions in a different way to type theorists (zero_add and add_zero are both "facts" as far as mathematicians are concerned, and who cares what the definition of addition is).

Summary

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

Variants

• rw [← h] (changes Ys to Xs; get the back arrow by typing \left or \l.)

• rw [h1, h2] (a sequence of rewrites)

• rw [h] at h2 (changes Xs to Ys in hypothesis h2)

• rw [h] at h1 h2 ⊢ (changes Xs to Ys in two hypotheses and the goal; get the ⊢ symbol with \|-.)

• repeat rw [add_zero] will keep changing ? + 0 to ? until there are no more matches for ? + 0.

• nth_rewrite 2 [h] will change only the second X in the goal to Y.

Example:

If you have the assumption h : x = y + y and your goal is

succ (x + 0) = succ (y + y)

then

rw [add_zero]

will change the goal into succ x = succ (y + y), and then

rw [h]

will change the goal into succ (y + y) = succ (y + y), which can be solved with rfl.

Example:

You can use rw to change a hypothesis as well. For example, if you have two hypotheses

h1 : x = y + 3
h2 : 2 * y = x

then rw [h1] at h2 will turn h2 into h2 : 2 * y = y + 3.

Common errors

• You need the square brackets. rw h is never correct.

• If h is not a proof of an equality (a statement of the form A = B), for example if h is a function or an implication, then rw is not the tactic you want to use. For example, rw [P = Q] is never correct: P = Q is the theorem statement, not the proof. If h : P = Q is the proof, then rw [h] will work.

Details

The rw tactic is a way to do "substituting in". There are two distinct situations where you can use this tactic.

1. Basic usage: if h : A = B is an assumption or the proof of a theorem, and if the goal contains one or more As, then rw [h] will change them all to Bs. The tactic will error if there are no As in the goal.

2. Advanced usage: Assumptions coming from theorem proofs often have missing pieces. For example add_zero is a proof that ? + 0 = ? because add_zero really is a function, and ? is the input. In this situation rw will look through the goal for any subterm of the form x + 0, and the moment it finds one it fixes ? to be x then changes all x + 0s to xs.

Exercise: think about why rw [add_zero] changes the term (0 + 0) + (x + 0) + (0 + 0) + (x + 0) to 0 + (x + 0) + 0 + (x + 0)

If you can't remember the name of the proof of an equality, look it up in the list of lemmas on the right.

Targeted usage

If your goal is b + c + a = b + (a + c) and you want to rewrite a + c to c + a, then rw [add_comm] will not work because Lean finds another addition first and swaps those inputs instead. Use rw [add_comm a c] to guarantee that Lean rewrites a + c to c + a. This works because add_comm is a proof that ?1 + ?2 = ?2 + ?1, add_comm a is a proof that a + ? = ? + a, and add_comm a c is a proof that a + c = c + a.

If h : X = Y then rw [h] will turn all Xs into Ys. If you only want to change the 37th occurrence of X to Y then do nth_rewrite 37 [h].

four_eq_succ_three is a proof of 4 = succ 3.

one_eq_succ_zero is a proof of 1 = succ 0.

three_eq_succ_two is a proof of 3 = succ 2.

two_eq_succ_one is a proof of 2 = succ 1.

ℕ is the natural numbers, just called "numbers" in this game. It's defined via two rules:

• 0 : ℕ (zero is a number)

• succ (n : ℕ) : ℕ (the successor of a number is a number)

Game Implementation

The game uses its own copy of the natural numbers, called MyNat with notation ℕ. It is distinct from the Lean natural numbers Nat, which should hopefully never leak into the natural number game.

add_zero a is a proof that a + 0 = a.

Summary

add_zero is really a function, which eats a number, and returns a proof of a theorem about that number. For example add_zero 37 is a proof that 37 + 0 = 37.

The rw tactic will accept rw [add_zero] and will try to figure out which number you omitted to input.

Details

A mathematician sometimes thinks of add_zero as "one thing", namely a proof of \forall n ∈ ℕ, n + 0 = n. This is just another way of saying that it's a function which can eat any number n and will return a proof that n + 0 = n.

Add a b, with notation a + b, is the usual sum of natural numbers. Internally it is defined via the following two hypotheses:

• add_zero a : a + 0 = a

• add_succ a b : a + succ b = succ (a + b)

Other theorems about naturals, such as zero_add a : 0 + a = a, are proved by induction using these two basic theorems.

add_succ a b is the proof of a + succ b = succ (a + b).