## Lean Cheat Sheets

### Tactics for Connectives & Quantifiers

Propositions | To introduce | To eliminate |
---|---|---|

`P β Q` | `intro` | function application |

`P β§ Q` | `split` | `cases` |

`P β¨ Q` | `left` , `right` | `cases` |

`β a : X, H` | `existsi` | `cases` |

`β a : X, H` | `intro` | function application |

`P β Q` | `split` | `cases` |

`Β¬P` | `intro` | function application |

### Other Tactics for Logic

#### `exact hp`

(prove a goal `β’ P`

if you have `hp : P`

by copying `hp`

)

## How does `exact` work?

If the goal is `β’ X`

then `exact hp`

will close the goal if and only if `hp : X`

```
theorem not_not_intro (P : Prop) :
P β Β¬Β¬ P :=
begin
intro hp,
apply not.intro,
intro hnp,
apply hnp,
exact hp,
end
```

#### `intro h`

(turns `β’ P β Q`

into `h : P, β’ Q`

)

## How does `intro` work?

`intro hp`

will turn a goal `β’ P β Q`

into a hypothesis `hp : P`

and goal `β’ Q`

. If `P`

and `Q`

are sets `intro p`

means βlet `p`

be an arbitrary element of `P`

β. If `P`

and `Q`

are propositions then `intro hp`

says βassume `P`

is trueβ (i.e. βlet `hp`

be a proof of `P`

). We also use `intro`

to prove a universally quantified statement.

```
theorem forall_impl
(A B : U β Prop) : (β x, A x β B x) β (β x, A x) β (β x, B x) :=
begin
intro h,
intro u,
intro a,
have e, from u a,
have h_a, from h a,
show B a, from h_a e,
-- exact h_a e,
end
```

#### `apply h`

(turns `h : P β Q, β’ Q`

into `β’ P`

)

## How does `apply` work?

If you have `h : P β Q`

and your goal is `β’ Q`

then `apply h`

changes the goal to `β’ P`

. If you are trying to create a proof of `Q`

, and `h`

is a rule which turns proofs of `P`

into proofs of `Q`

, then it will suffice to construct a proof of `P`

. It is the bottom-to-top version of application. Hereβs an example:

```
theorem curry (P Q R : Prop) : (P β§ Q β R) β (P β (Q β R) :=
begin
intro h,
intro hp,
intro hq,
apply h,
constructor,
exact hp,
exact hq,
end
```

Puzzle: figure out what `constructor`

does by examining what `Lean`

tells you about your goals.

### Proving Equalities With Tactics

#### `refl`

(prove `t = t`

goals)

## How does `refl` work?

`refl`

proves goals of the form `t = t`

, and more generally goals of the form `t ~ t`

where `~`

is any reflexive binary relation.

```
example (a b c d : β) : (a + b) * (c + d) = (a + b) * (c + d) :=
begin
refl,
end
```

#### `rw h`

(use a proof `h : x = y`

to change `x`

s to `y`

s)

## How does `rw` work?

The `rw`

tactic corresponds to the substitution rule of equality which we discussed in the lecture on the equality predicate. If `h`

is a proof of `A = B`

(i.e. `h : x = y`

), then `rw h`

will change all `x`

s in the goal to `y`

s. Variants: `rw βh`

(get the backward arrow with `\l`

) changes `y`

to `x`

and `rw h at u`

(changes `x`

to `y`

in hypothesis `u`

instead of the goal). Here is an example:

```
example (m n : β) (h : n = m + 6) : 2 * n = 2 * (m + 6) :=
begin
rw h,
end
```

Here is another example:

```
example (P Q : Prop) (h : P β Β¬ Q) : (P β Β¬ Β¬ P) β (Β¬ Q β Β¬ Β¬ Β¬ Q) :=
begin
rw β h,
intro u,
exact u,
end
```

Note that here Lean uses **propositional extensionality** to equate two equivalent proposition.

```
#check propext
```

#### `simp`

(use relevant lemmas and hypotheses to simplify the goal)

## How does `simp` work?

This tactic has several variants and it is used quite frequently. In its most basic form, simp will try to use relevant lemmas and hypotheses to simplify the goal. `dsimp`

is similar to simp, except that it only uses definitional equalities. See here for a full guide for all usages of `simp`

.

```
example : β n : β, 2 β 2 * 2 * n := begin
intro n,
cases n with d hd,
simp,
rw nat.succ_eq_add_one,
linarith,
end
```

and

```
example (n : β) (h : n + 1 - 1 β 0) : n + 1 β 1 :=
begin
simpa using h,
end
```