Lecture 1.2: Basics — Proofs

We now see how to prove statements about specifications, using basic Lean tactics

Demo

12_lecture.lean

Tactical proofs

A tactic operates on a proof goal and either solves it or creates new subgoals

Tactics are a backward (or bottom-up) proof mechanism: they start from the goal and break it down

Terminal (end-game) tactic invocation: by tactic

Multiple tactics in sequence: begin tactic1, ..., tacticN end

Tactic composition: tactic1 ; tactic2, where tactic2 is applied to all subgoals emerging from tactic1

Tactics are arbitrarily powerful, but they can be brittle

Structuring mechanisms

The { ... } combinator focuses on the first subgoal; the tactic inside must (fully) solve it

Lean also provides forward (or top-down) proof mechanisms such as have, which give the user more control on the shape of the subgoals

Syntax:

have name : proposition := proof

Often we put a _ placeholder for proposition, when it can be inferred from the proof

Backward proofs are often easier to write but harder to read; it is always easier to destruct than to construct things

Basic tactics

refl

Proves x = y, where the two sides are equal up to computation

Computation means unfolding of definitions, β-reduction (application of λ to an argument), projections, let, and more

CIC is a computational logic: logical formulas have computational content

ac_refl

Proves x = y, where the two sides are equal up to associativity and commutativity

This works for binary operations that are registered as associative and commutative, e.g. + on ℕ

cases term

Destructs a record into its fields

More generally, it destructs inductively defined types into their constructors

Instead, we can also use pattern matching in proofs

rw lemma

Applies a single equation as a left-to-right rewrite rule, once

To apply an equation right-to-left, prefix its name with ←

rw [lemma1, ..., lemmaN]

Synonym for rw lemma1, ..., rw lemmaN

simp

Applies a standard set of rewrite rules (the simp set) exhaustively

The set can be extended using the [simp] attribute

It is generally more powerful than rw because it can rewrite terms containing variables bound by λ, ∀, ∃, etc.

simp [lemma1, ..., lemmaN]

Same as above, except that the specified lemmas are temporarily added to the simp set

* (as a lemmaI) represents all local hypotheses

- in front of a lemma name temporarily removes the lemma from the simp set

intros var1 ... varN

Moves ∀-quantified variables from the goal into the goal's hypotheses

Useful in conjunction with the induction and rw tactic

induction var

Applies structural induction on the given variable of an inductive type

Induction can also be done by pattern matching:

• the induction hypothesis is then available under the name of the lemma we are proving
• well-foundedness of the argument is often proved automatically

Rules of thumb:

• perform induction following the structure of function definitions
• if the base case (e.g. 0, []) of an induction is difficult, this is a sign the wrong variable was picked or some lemmas are missing

Newly introduced syntax

Declaration

Proofs

Tactics

Tactic combinators

Reference

• Theorem Proving in Lean, Sections 5.1–5.7