# Tactics

Tactics are metaprograms, that is, programs that create programs.
Lean is implemented in Lean, you can import its implementation using `import Lean`

.
The `Lean`

package is part of the Lean distribution.
You can use the functions in the `Lean`

package to write your own metaprograms
that automate repetitive tasks when writing programs and proofs.

We provide the **tactic** domain specific language (DSL) for using the tactic framework.
The tactic DSL provides commands for creating terms (and proofs). You
don't need to import the `Lean`

package for using the tactic DSL.
Simple extensions can be implemented using macros. More complex extensions require
the `Lean`

package. Notation used to write Lean terms can be easily lifted to the tactic DSL.

Tactics are instructions that tell Lean how to construct a term or proof. Tactics operate on holes also known as goals. Each hole represents a missing part of the term you are trying to build. Internally these holes are represented as metavariables. They have a type and a local context. The local context contains all local variables in scope.

In the following example, we prove the same simple theorem using different tactics.
The keyword `by`

instructs Lean to use the tactic DSL to construct a term.
Our initial goal is a hole with type `p ∨ q → q ∨ p`

. The tactic `intro h`

fills this hole using the term `fun h => ?m`

where `?m`

is a new hole we need to solve.
This hole has type `q ∨ p`

, and the local context contains `h : p ∨ q`

.
The tactic `cases`

fills the hole using `Or.casesOn h (fun h1 => ?m1) (fun h2 => ?m2)`

where `?m1`

and `?m2`

are new holes. The tactic `apply Or.inr`

fills the hole `?m1`

with the application `Or.inr ?m3`

, and `exact h1`

fills `?m3`

with `h1`

.
The tactic `assumption`

tries to fill a hole by searching the local context for a term with the same type.

```
theorem ex1 : p ∨ q → q ∨ p := by
intro h
cases h with
| inl h1 =>
apply Or.inr
exact h1
| inr h2 =>
apply Or.inl
assumption
#print ex1
/-
theorem ex1 : {p q : Prop} → p ∨ q → q ∨ p :=
fun {p q : Prop} (h : p ∨ q) =>
Or.casesOn h (fun (h1 : p) => Or.inr h1) fun (h2 : q) => Or.inl h2
-/
-- You can use `match-with` in tactics.
theorem ex2 : p ∨ q → q ∨ p := by
intro h
match h with
| Or.inl _ => apply Or.inr; assumption
| Or.inr h2 => apply Or.inl; exact h2
-- As we have the `fun+match` syntax sugar for terms,
-- we have the `intro+match` syntax sugar
theorem ex3 : p ∨ q → q ∨ p := by
intro
| Or.inl h1 =>
apply Or.inr
exact h1
| Or.inr h2 =>
apply Or.inl
assumption
```

The examples above are all structured, but Lean 4 still supports unstructured proofs. Unstructured proofs are useful when creating reusable scripts that may discharge different goals. Here is an unstructured version of the example above.

```
theorem ex1 : p ∨ q → q ∨ p := by
intro h
cases h
apply Or.inr
assumption
apply Or.inl
assumption
done -- fails with an error here if there are unsolvable goals
theorem ex2 : p ∨ q → q ∨ p := by
intro h
cases h
focus -- instructs Lean to `focus` on the first goal,
apply Or.inr
assumption
-- it will fail if there are still unsolvable goals here
focus
apply Or.inl
assumption
theorem ex3 : p ∨ q → q ∨ p := by
intro h
cases h
-- You can still use curly braces and semicolons instead of
-- whitespace sensitive notation as in the previous example
{ apply Or.inr;
assumption
-- It will fail if there are unsolved goals
}
{ apply Or.inl;
assumption
}
-- Many tactics tag subgoals. The tactic `cases` tag goals using constructor names.
-- The tactic `case tag => tactics` instructs Lean to solve the goal
-- with the matching tag.
theorem ex4 : p ∨ q → q ∨ p := by
intro h
cases h
case inr =>
apply Or.inl
assumption
case inl =>
apply Or.inr
assumption
-- Same example for curly braces and semicolons aficionados
theorem ex5 : p ∨ q → q ∨ p := by {
intro h;
cases h;
case inr => {
apply Or.inl;
assumption
}
case inl => {
apply Or.inr;
assumption
}
}
```

## Rewrite

TODO

## Pattern matching

As a convenience, pattern-matching has been integrated into tactics such as `intro`

and `funext`

.

```
theorem ex1 : s ∧ q ∧ r → p ∧ r → q ∧ p := by
intro ⟨_, ⟨hq, _⟩⟩ ⟨hp, _⟩
exact ⟨hq, hp⟩
theorem ex2 :
(fun (x : Nat × Nat) (y : Nat × Nat) => x.1 + y.2)
=
(fun (x : Nat × Nat) (z : Nat × Nat) => z.2 + x.1) := by
funext (a, b) (c, d)
show a + d = d + a
rw [Nat.add_comm]
```

## Induction

The `induction`

tactic now supports user-defined induction principles with
multiple targets (aka major premises).

```
/-
theorem Nat.mod.inductionOn
{motive : Nat → Nat → Sort u}
(x y : Nat)
(ind : ∀ x y, 0 < y ∧ y ≤ x → motive (x - y) y → motive x y)
(base : ∀ x y, ¬(0 < y ∧ y ≤ x) → motive x y)
: motive x y :=
-/
theorem ex (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
induction x, y using Nat.mod.inductionOn with
| ind x y h₁ ih =>
rw [Nat.mod_eq_sub_mod h₁.2]
exact ih h
| base x y h₁ =>
have : ¬ 0 < y ∨ ¬ y ≤ x := Iff.mp (Decidable.notAndIffOrNot ..) h₁
match this with
| Or.inl h₁ => exact absurd h h₁
| Or.inr h₁ =>
have hgt : y > x := Nat.gtOfNotLe h₁
rw [← Nat.mod_eq_of_lt hgt] at hgt
assumption
```

## Cases

TODO

## Injection

TODO

## Dependent pattern matching

The `match-with`

expression implements dependent pattern matching. You can use it to create concise proofs.

```
inductive Mem : α → List α → Prop where
| head (a : α) (as : List α) : Mem a (a::as)
| tail (a b : α) (bs : List α) : Mem a bs → Mem a (b::bs)
infix:50 "∈" => Mem
theorem mem_split {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a :: t :=
match a, as, h with
| _, _, Mem.head a bs => ⟨[], ⟨bs, rfl⟩⟩
| _, _, Mem.tail a b bs h =>
match bs, mem_split h with
| _, ⟨s, ⟨t, rfl⟩⟩ => ⟨b::s, ⟨t, List.cons_append .. ▸ rfl⟩⟩
```

In the tactic DSL, the right-hand-side of each alternative in a `match-with`

is a sequence of tactics instead of a term.
Here is a similar proof using the tactic DSL.

```
inductive Mem : α → List α → Prop where
| head (a : α) (as : List α) : Mem a (a::as)
| tail (a b : α) (bs : List α) : Mem a bs → Mem a (b::bs)
infix:50 "∈" => Mem
theorem mem_split {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a :: t := by
match a, as, h with
| _, _, Mem.head a bs => exists []; exists bs; rfl
| _, _, Mem.tail a b bs h =>
match bs, mem_split h with
| _, ⟨s, ⟨t, rfl⟩⟩ =>
exists b::s; exists t;
rw [List.cons_append]
```

We can use `match-with`

nested in tactics.
Here is a similar proof that uses the `induction`

tactic instead of recursion.

```
inductive Mem : α → List α → Prop where
| head (a : α) (as : List α) : Mem a (a::as)
| tail (a b : α) (bs : List α) : Mem a bs → Mem a (b::bs)
infix:50 "∈" => Mem
theorem mem_split {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a :: t := by
induction as with
| nil => cases h
| cons b bs ih => cases h with
| head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
| tail a b bs h =>
match bs, ih h with
| _, ⟨s, ⟨t, rfl⟩⟩ =>
exists b::s; exists t
rw [List.cons_append]
```

You can create your own notation using existing tactics. In the following example,
we define a simple `obtain`

tactic using macros. We say it is simple because it takes only one
discriminant. Later, we show how to create more complex automation using macros.

```
inductive Mem : α → List α → Prop where
| head (a : α) (as : List α) : Mem a (a::as)
| tail (a b : α) (bs : List α) : Mem a bs → Mem a (b::bs)
infix:50 "∈" => Mem
macro "obtain " p:term " from " d:term : tactic =>
`(tactic| match $d:term with | $p:term => ?_)
theorem mem_split {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a :: t := by
induction as with
| cons b bs ih => cases h with
| tail a b bs h =>
obtain ⟨s, ⟨t, h⟩⟩ from ih h
exists b::s; exists t
rw [h, List.cons_append]
| head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
| nil => cases h
```

## Extensible tactics

In the following example, we define the notation `triv`

for the tactic DSL using
the command `syntax`

. Then, we use the command `macro_rules`

to specify what should
be done when `triv`

is used. You can provide different expansions, and the tactic DSL
interpreter will try all of them until one succeeds.

```
-- Define a new notation for the tactic DSL
syntax "triv" : tactic
macro_rules
| `(tactic| triv) => `(tactic| assumption)
theorem ex1 (h : p) : p := by
triv
-- You cannot prove the following theorem using `triv`
-- theorem ex2 (x : α) : x = x := by
-- triv
-- Let's extend `triv`. The `by` DSL interpreter
-- tries all possible macro extensions for `triv` until one succeeds
macro_rules
| `(tactic| triv) => `(tactic| rfl)
theorem ex2 (x : α) : x = x := by
triv
theorem ex3 (x : α) (h : p) : x = x ∧ p := by
apply And.intro <;> triv
```

`let-rec`

You can use `let rec`

to write local recursive functions. We lifted it to the tactic DSL,
and you can use it to create proofs by induction.

```
theorem length_replicate {α} (n : Nat) (a : α) : (List.replicate n a).length = n := by
let rec aux (n : Nat) (as : List α)
: (List.replicate.loop a n as).length = n + as.length := by
match n with
| 0 => rw [Nat.zero_add]; rfl
| n+1 =>
show List.length (List.replicate.loop a n (a::as)) = Nat.succ n + as.length
rw [aux n, List.length_cons, Nat.add_succ, Nat.succ_add]
exact aux n []
```

You can also introduce auxiliary recursive declarations using `where`

clause after your definition.
Lean converts them into a `let rec`

.

```
theorem length_replicate {α} (n : Nat) (a : α) : (List.replicate n a).length = n :=
loop n []
where
loop n as : (List.replicate.loop a n as).length = n + as.length := by
match n with
| 0 => rw [Nat.zero_add]; rfl
| n+1 =>
show List.length (List.replicate.loop a n (a::as)) = Nat.succ n + as.length
rw [loop n, List.length_cons, Nat.add_succ, Nat.succ_add]
```

`begin-end`

lovers

If you love Lean 3 `begin ... end`

tactic blocks and commas, you can define this notation
in Lean 4 using macros in a few lines of code.

```
open Lean in
macro "begin " ts:tactic,*,? "end"%i : term => do
-- preserve position of the last token, which is used
-- as the error position in case of an unfinished proof
`(by { $[$ts:tactic]* }%$i)
theorem ex1 (x : Nat) : x + 0 = 0 + x :=
begin
rw [Nat.zero_add],
rw [Nat.add_zero],
end
```