Put a small file together
A structure, a function, a test and a theorem in one file you can take home.
In this course 7 / 8
A real Lean file mixes everything from the last two courses: data, functions, quick #eval tests, and theorems that say what callers can rely on. The #eval shows one example; the theorem covers every input it describes.
The Score structure and the award function are given above the editor. You will add one theorem and one #eval underneath them.
The theorem is about any score with five points, so it needs a score and a hypothesis: (s : Score) (h : s.points = 5). After unfold award the goal mentions s.points + 3, and rw [h] turns it into a calculation Lean finishes itself.
To keep working on your own computer: Download .lean saves the whole file, definitions and checks included. Install Lean with elan, open the file in VS Code with the Lean 4 extension, and you get the same goal view while you type. This Academy uses Lean 4.30.
Worked example
structure Account where
balance : Nat
def credit (a : Account) (amount : Nat) : Account :=
{ a with balance := a.balance + amount }
theorem credit_known (a : Account) (h : a.balance = 10) : (credit a 2).balance = 12 := by
unfold credit
rw [h]
#eval (credit { balance := 4 } 3).balance
At the start of the proof on line 7. Everything above ⊢ may be used; the line below it is what must be proved.
One structure, one function, one theorem and one test. Your exercise has the same parts for a score.
A Lean file combines data, functions, tests and theorems. Tests check examples; theorems cover every input they describe.
Prove award_from_five: a score with five points has eight after an award of three. Then add an #eval that prints the points after awarding 4 to a score of 7. The exercise is complete when Lean prints 11.
Suggested steps
- State
award_from_fivewith a score and a hypothesis - Unfold the update and rewrite the known points
- Evaluate awarding four points to a score of seven
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:These lines run underneath whatever you write. They are what decides the exercise, so your names and types have to match them.
example (s : Score) (h : s.points = 5) : (award s 3).points = 8 := award_from_five s h
Knowledge check
Answer without looking back, then check your reasoning.
correct