Documentation

Lean.Parser.Tactic

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For

match performs case analysis on one or more expressions. See Induction and Recursion. The syntax for the match tactic is the same as term-mode match, except that the match arms are tactics instead of expressions.

example (n : Nat) : n = n := by
match n with
| 0 => rfl
| i+1 => simp

Equations
• One or more equations did not get rendered due to their size.
Instances For

The tactic

intro
| pat1 => tac1
| pat2 => tac2


is the same as:

intro x
match x with
| pat1 => tac1
| pat2 => tac2


That is, intro can be followed by match arms and it introduces the values while doing a pattern match. This is equivalent to fun with match arms in term mode.

Equations
• One or more equations did not get rendered due to their size.
Instances For

decide attempts to prove the main goal (with target type p) by synthesizing an instance of Decidable p and then reducing that instance to evaluate the truth value of p. If it reduces to isTrue h, then h is a proof of p that closes the goal.

Limitations:

• The target is not allowed to contain local variables or metavariables. If there are local variables, you can try first using the revert tactic with these local variables to move them into the target, which may allow decide to succeed.
• Because this uses kernel reduction to evaluate the term, Decidable instances defined by well-founded recursion might not work, because evaluating them requires reducing proofs. The kernel can also get stuck reducing Decidable instances with Eq.rec terms for rewriting propositions. These can appear for instances defined using tactics (such as rw and simp). To avoid this, use definitions such as decidable_of_iff instead.

Examples #

Proving inequalities:

example : 2 + 2 ≠ 5 := by decide


Trying to prove a false proposition:

example : 1 ≠ 1 := by decide
/-
tactic 'decide' proved that the proposition
1 ≠ 1
is false
-/


Trying to prove a proposition whose Decidable instance fails to reduce

opaque unknownProp : Prop

open scoped Classical in
example : unknownProp := by decide
/-
tactic 'decide' failed for proposition
unknownProp
since its 'Decidable' instance reduced to
Classical.choice ⋯
rather than to the 'isTrue' constructor.
-/


Properties and relations #

For equality goals for types with decidable equality, usually rfl can be used in place of decide.

example : 1 + 1 = 2 := by decide
example : 1 + 1 = 2 := by rfl

Equations
• One or more equations did not get rendered due to their size.
Instances For

native_decide will attempt to prove a goal of type p by synthesizing an instance of Decidable p and then evaluating it to isTrue ... Unlike decide, this uses #eval to evaluate the decidability instance.

This should be used with care because it adds the entire lean compiler to the trusted part, and the axiom ofReduceBool will show up in #print axioms for theorems using this method or anything that transitively depends on them. Nevertheless, because it is compiled, this can be significantly more efficient than using decide, and for very large computations this is one way to run external programs and trust the result.

example : (List.range 1000).length = 1000 := by native_decide

Equations
• One or more equations did not get rendered due to their size.
Instances For