λleanlab

Proofs

have, rw, and calc

Name intermediate facts and justify each step of an equality.

Open Calculations.lean in editor
example (a b c : Nat) (hab : a = b) (hbc : b = c) :
    a + 1 = c + 1 := by
  have hac : a = c := by
    calc
      a = b := hab
      _ = c := hbc
  rw [hac]

-- rw [← h] uses an equality from right to left.
example (a b : Nat) (h : a = b) : b + 0 = a := by
  rw [← h]
  rfl

Explanation

have hac : a = c := by

Creates a local fact with its own proof. Later proof steps can refer to hac.

calc · _

Chains justified relations. The underscore in the next line stands for the previous right-hand side.

rw [← h]

Rewrites using h in the reverse direction. This ← has a different role from extracting a result in a do block.

Expected output

Reference only. Run the file to check its actual result.

File checked successfully.

Exercise

Change + 1 to + 2 in the first statement. The same proof should still work.

Related examples