7.2 KiB
| date | draft | math | medium_enabled | medium_post_id | tags | title | |
|---|---|---|---|---|---|---|---|
| 2021-10-11 03:52:41 | false | false | true | adea1a69ddc8 |
|
Lean Theorem Prover Tactics |
I've recently been playing with the Lean Theorem Prover. I am impressed with how some of the mathematics community decided to extend this project via mathlib and really make proving theorems in this framework easy and enjoyable.
Normally one of the most frustrating parts of theorem proving is having to justify what may seem to be a simple goal. Luckily, mathlib helps us out by introducing tactics that can take some of these simple goals to the finish line.
Tactics
Here is a subset of tactics that I find myself using the most:
| hint | cases_type* | have | itauto |
| pretty_cases | squeeze_simp | tidy | solve_by_elim |
| finish | linarith |
hint
The first command to reach for. This will give you a tactic that is guaranteed to succeed.
theorem running_example1: ∀ P Q : Prop,
Q ∧ (Q → P) → P
:=
begin
intros P Q H,
hint,
-- the following tactics solve the goal:
-- Try this: tauto
-- Try this: itauto
-- Try this: finish
-- Try this: solve_by_elim
Documentation: https://leanprover-community.github.io/mathlib_docs/tactics.html#hint
cases_type*
The following destructs all (con/dis)junctions in the current context
cases_type* or and,
Example:
theorem running_example1: ∀ P Q : Prop,
Q ∧ (Q → P) → P
:=
begin
intros P Q H,
cases_type* or and,
The tactic state before:
P Q: Prop
H : Q ∧ (Q → P)
⊢ P
The tactic state after:
P Q: Prop
H_left: Q
H_right: (Q → P)
⊢ P
Documentation: https://leanprover-community.github.io/mathlib_docs/tactics.html#cases_type
have
If you want to add a hypothesis, this is a great way to introduce that and solve that goal. Combine this with library_search to try to find simple tactics to justify the hypothesis.
have H : EXAMPLE := by library_search,
Example:
theorem running_example1: ∀ P Q : Prop,
Q ∧ (Q → P) → P
:=
begin
intros P Q H,
cases_type* or and,
have H_P : P := by library_search,
-- Try this: exact H_right H_left
Documentation: https://leanprover-community.github.io/mathlib_docs/tactics.html#have
itauto
Tries to use intuitionist propositional logic to solve the goal. Also called constructivist logic, it does not allow the use of the law of excluded middle.
Example:
theorem running_example1: ∀ P Q : Prop,
Q ∧ (Q → P) → P
:=
begin
intros P Q H,
cases_type* or and,
itauto,
end
Documentation: https://leanprover-community.github.io/mathlib_docs/tactics.html#itauto
pretty_cases
Great to call after destruct, induction, injection, etc. This will give you a cleaner way of representing cases.
Example:
theorem running_example2: ∀ n : ℕ,
(∃ m : ℕ, n = 2 * m) ∨ (∃ m : ℕ, n = 2 * m + 1)
:=
begin
intros,
induction n,
pretty_cases,
-- Try this:
-- case nat.zero
-- { admit },
-- case nat.succ : n_n n_ih
-- { admit }
end
Documentation: https://leanprover-community.github.io/mathlib_docs/tactics.html#pretty_cases
squeeze_simp
This tactic will give you the sequence of rewrite rules that can simplify an expression.
Example:
theorem running_example2: ∀ n : ℕ,
(∃ m : ℕ , n = 2 * m) ∨ (∃ m : ℕ, n = 2 * m + 1)
:=
begin
intros,
induction n,
case nat.zero
{
left,
existsi 0,
squeeze_simp,
-- Try this: simp only [mul_zero]
},
tidy
Applies simple tactics to try to solve the goal. I like to use the query variant tidy? in order to get a list of tactics back.
The tactics it uses are: id_rhs, refl, exact, trivial, dismp, simp, injections_and_clear, solve_by_elim, norm_cast, unfold, fsplit.
Example:
theorem running_example3: ∀ n : ℕ,
(∃ m : ℕ , n = 2 * m) ∨ (∃ m : ℕ, n = 2 * m + 1)
:=
begin
intros,
induction n,
case nat.zero
{
left,
existsi 0,
simp only [mul_zero],
},
case nat.succ : n IH
{
cases_type* or,
case or.inl : IH
{
right,
cases IH with m IH,
tidy?,
-- Try this: fsplit, work_on_goal 1 { solve_by_elim }
},
Documentation: https://leanprover-community.github.io/mathlib_docs/tactics.html#tidy
solve_by_elim
This tactic tries to apply the current hypotheses in the context and apply congruence closure algorithms to solve your goal.
If you have multiple goals you can call solve_by_elim* to try to solve them all at once. I find though that it is often more successful to do all_goals{solve_by_elim} instead, unless you need results from one of the subproofs in the other.
This tactic is non-deterministic so it bounds the number of attempts to discharge subgoals. Here is how you increase the bound: solve_by_elim { max_depth := 5 }
Example:
theorem running_example3: ∀ n : ℕ,
(∃ m : ℕ , n = 2 * m) ∨ (∃ m : ℕ, n = 2 * m + 1)
:=
begin
intros,
induction n,
case nat.zero
{
left,
existsi 0,
simp only [mul_zero],
},
case nat.succ : n IH
{
cases_type* or,
case or.inl : IH
{
right,
cases IH with m IH,
fsplit, work_on_goal 1 { solve_by_elim },
},
case or.inr : IH
{
left,
cases IH with m IH,
rewrite IH,
existsi m + 1,
solve_by_elim,
},
}
end
Documentation: https://leanprover-community.github.io/mathlib_docs/tactics.html#solve_by_elim
finish
This tactic is like a black box to me, mainly because it performs many subtactics. It tries to finish off the goal. To give a hint of its power, it can actually solve the first theorem.
theorem running_example1: ∀ P Q: Prop,
Q ∧ (Q → P) → P :=
begin
finish,
end
Source: https://leanprover-community.github.io/mathlib_docs/tactics.html#finish%20/%20clarify%20/%20safe
linarith
This tactic solves linear (in)equalities.
Example:
theorem example3: ∀ n m : ℕ,
n > m → m < n :=
begin
intros,
linarith,
end
Documentation: https://leanprover-community.github.io/mathlib_docs/tactics.html#linarith
Conclusion
A common pattern of writing proofs for me is to use a combination of hint and have with library_search. Especially when you are not an expert in a theorem prover, it's nice to have the system fill in some of the simpler steps. I generally prefer tactics that give you a list of simpler tactics back as opposed to solving the goal in the background without any proof. Regardless, I'm glad that many of these decision procedures exist to help me deal with what can sometimes be the verbosity of theorem proving.