def Lean.Parser.Tactic.unknown : Lean.Parser.Parser

Equations

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

def Lean.Parser.Tactic.nestedTactic : Lean.Parser.Parser

Equations

• Lean.Parser.Tactic.nestedTactic = Lean.Parser.Tactic.tacticSeqBracketed

def Lean.Parser.Tactic.matchRhs : Lean.Parser.Parser

Equations

• Lean.Parser.Tactic.matchRhs = HOrElse.hOrElse Lean.Parser.Term.hole fun (x : Unit) => HOrElse.hOrElse Lean.Parser.Term.syntheticHole fun (x : Unit) => Lean.Parser.Tactic.tacticSeq

def Lean.Parser.Tactic.matchAlts : Lean.Parser.Parser

Equations

• Lean.Parser.Tactic.matchAlts = Lean.Parser.Term.matchAlts Lean.Parser.Tactic.matchRhs

def Lean.Parser.Tactic.match : Lean.Parser.Parser

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.

def Lean.Parser.Tactic.introMatch : Lean.Parser.Parser

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.

def Lean.Parser.Tactic.decide : Lean.Parser.Parser

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.

def Lean.Parser.Tactic.nativeDecide : Lean.Parser.Parser

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.