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 } }
TODO
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]
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.not_and_iff_or_not ..) h₁ match this with | Or.inl h₁ => exact absurd h h₁ | Or.inr h₁ => have hgt : y > x := Nat.gt_of_not_le h₁ rw [← Nat.mod_eq_of_lt hgt] at hgt assumption
TODO
TODO
The split tactic can be used to split the cases of an if-then-else or match into new subgoals, which can then be discharged individually.
def addMoreIfOdd (n : Nat) := if n % 2 = 0 then n + 1 else n + 2 /- Examine each branch of the conditional to show that the result is always positive -/ example (n : Nat) : 0 < addMoreIfOdd n := by simp only [addMoreIfOdd] split next => exact Nat.zero_lt_succ _ next => exact Nat.zero_lt_succ _
def binToChar (n : Nat) : Option Char := match n with | 0 => some '0' | 1 => some '1' | _ => none example (n : Nat) : (binToChar n).isSome -> n = 0 ∨ n = 1 := by simp only [binToChar] split next => exact fun _ => Or.inl rfl next => exact fun _ => Or.inr rfl next => intro h; cases h /- Hypotheses about previous cases can be accessesd by assigning them a name, like `ne_zero` below. Information about the matched term can also be preserved using the `generalizing` tactic: -/ example (n : Nat) : (n = 0) -> (binToChar n = some '0') := by simp only [binToChar] split case h_1 => intro _; rfl case h_2 => intro h; cases h /- Here, we can introduce `n ≠ 0` and `n ≠ 1` this case assumes neither of the previous cases matched. -/ case h_3 ne_zero _ => intro eq_zero; exact absurd eq_zero ne_zero
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 (priority := high) "∈" => 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 (priority := high) "∈" => 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 (priority := high) "∈" => 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 (priority := high) "∈" => 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
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-recYou 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_replicateTR {α} (n : Nat) (a : α) : (List.replicateTR n a).length = n := by let rec aux (n : Nat) (as : List α) : (List.replicateTR.loop a n as).length = n + as.length := by match n with | 0 => rw [Nat.zero_add]; rfl | n+1 => show List.length (List.replicateTR.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_replicateTR {α} (n : Nat) (a : α) : (List.replicateTR n a).length = n := loop n [] where loop n as : (List.replicateTR.loop a n as).length = n + as.length := by match n with | 0 => rw [Nat.zero_add]; rfl | n+1 => show List.length (List.replicateTR.loop a n (a::as)) = Nat.succ n + as.length rw [loop n, List.length_cons, Nat.add_succ, Nat.succ_add]
begin-end loversIf 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.
{{#include ../tests/lean/beginEndAsMacro.lean:doc}}