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

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

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

`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`

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`

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

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

`rw`

[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`

[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`

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

Useful in conjunction with the `induction`

and `rw`

tactic

`induction`

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

Syntax | Description |
---|---|

`section` ... `end` |
surrounds an anonymous namespace |

`example` |
states a nameless lemma |

`instance` |
registers a type class instance (to guide proof automation) |

Syntax | Description |
---|---|

`by` |
applies a single tactic |

`begin` ... `end` |
applies a list of tactics in sequence |

`have` |
states an intermediate lemma |

`sorry` |
stands for a missing proof |

Name | Description |
---|---|

`refl` |
proves goals of the form `x = y` , where `x` and `y` are equal up to computation |

`ac_refl` |
proves goals of the form `x = y` , where `x` and `y` are equal up to associativity and commutativity |

`cases` |
destructs a record into its fields |

`rw` |
applies a single rewrite rule once |

`simp` |
applies a set of rewrite rules exhaustively |

`intros` |
moves ∀-quantified variables from the goal into the hypotheses |

`induction` |
performs structural induction on a variable of an inductive type |

Syntax | Description |
---|---|

`;` (semicolon) |
applies the second tactics to all subgoals emerging from the first tactic |

`{` ... `}` |
focuses on the first subgoal; needs to solve that goal |

*Theorem Proving in Lean*, Sections 5.1–5.7