# Lecture 1.2: Basics — Proofs

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


## Demo

[`12_lecture.lean`](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

Syntax              | Description
------------------- | -----------
`section` ... `end` | surrounds an anonymous namespace
`example`           | states a nameless lemma
`instance`          | registers a type class instance (to guide proof automation)

### Proofs

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

### Tactics

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

### Tactic combinators

Syntax          | Description
--------------- | -----------
`;` (semicolon) | applies the second tactic to all subgoals emerging from the first tactic
`{` ... `}`     | focuses on the first subgoal; needs to solve that goal


## Reference

* [_Theorem Proving in Lean_](https://leanprover.github.io/theorem_proving_in_lean/), Sections 5.1–5.7
