aesop<clause>* tries to solve the current goal by applying a set of rules
registered with the @[aesop] attribute. See its
README for a tutorial and a
reference.
The variant aesop? prints the proof it found as a Trythis suggestion.
Clauses can be used to customise the behaviour of an Aesop call. Available
clauses are:
(add<phase><priority><builder><rule>) adds a rule. <phase> is
unsafe, safe or norm. <priority> is a percentage for unsafe rules and
an integer for safe and norm rules. <rule> is the name of a declaration or
local hypothesis. <builder> is the rule builder used to turn <rule> into
an Aesop rule. Example: (addunsafe50%applyOr.inl).
(erase<rule>) disables a globally registered Aesop rule. Example: (eraseAesop.BuiltinRules.assumption).
(rule_sets:=[<ruleset>,*]) enables or disables named sets of rules for
this Aesop call. Example: (rule_sets:=[-builtin,MyRuleSet]).
(config{<opt>:=<value>}) adjusts Aesop's search options. See
Aesop.Options.
(simp_config{<opt>:=<value>}) adjusts options for Aesop's built-in
simp rule. The given options are directly passed to simp. For example,
(simp_config:={zeta:=false}) makes Aesop use
simp(config:={zeta:=false}).
The omega tactic, for resolving integer and natural linear arithmetic problems.
It is not yet a full decision procedure (no "dark" or "grey" shadows),
but should be effective on many problems.
We handle hypotheses of the form x=y, x<y, x≤y, and k∣x for xy in Nat or Int
(and k a literal), along with negations of these statements.
We decompose the sides of the inequalities as linear combinations of atoms.
If we encounter x/k or x%k for literal integers k we introduce new auxiliary variables
and the relevant inequalities.
On the first pass, we do not perform case splits on natural subtraction.
If omega fails, we recursively perform a case split on
a natural subtraction appearing in a hypothesis, and try again.
decide attempts to prove the main goal (with target type p) by synthesizing an instance of Decidablep
and then reducing that instance to evaluate the truth value of p.
If it reduces to isTrueh, then h is a proof of p that closes the goal.
The target is not allowed to contain local variables or metavariables.
If there are local variables, you can first try using the revert tactic with these local variables to move them into the target,
or you can use the +revert option, described below.
Options:
decide+revert begins by reverting local variables that the target depends on,
after cleaning up the local context of irrelevant variables.
A variable is relevant if it appears in the target, if it appears in a relevant variable,
or if it is a proposition that refers to a relevant variable.
decide+kernel uses kernel for reduction instead of the elaborator.
It has two key properties: (1) since it uses the kernel, it ignores transparency and can unfold everything,
and (2) it reduces the Decidable instance only once instead of twice.
decide+native uses the native code compiler (#eval) to evaluate the Decidable instance,
admitting the result via the Lean.ofReduceBool axiom.
This can be significantly more efficient than using reduction, but it is at the cost of increasing the size
of the trusted code base.
Namely, it depends on the correctness of the Lean compiler and all definitions with an @[implemented_by] attribute.
Like with +kernel, the Decidable instance is evaluated only once.
Limitation: In the default mode or +kernel mode, since decide uses reduction to evaluate the term,
Decidable instances defined by well-founded recursion might not work because evaluating them requires reducing proofs.
Reduction can also get stuck on Decidable instances with Eq.rec terms.
These can appear in instances defined using tactics (such as rw and simp).
To avoid this, create such instances using definitions such as decidable_of_iff instead.
Examples
Proving inequalities:
example:2+2≠5:=⊢ 2 + 2 ≠ 5All goals completed! 🐙
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.
The simp tactic uses lemmas and hypotheses to simplify the main goal target or
non-dependent hypotheses. It has many variants:
simp simplifies the main goal target using lemmas tagged with the attribute [simp].
simp[h₁,h₂,...,hₙ] simplifies the main goal target using the lemmas tagged
with the attribute [simp] and the given hᵢ's, where the hᵢ's are expressions.-
If an hᵢ is a defined constant f, then f is unfolded. If f has equational lemmas associated
with it (and is not a projection or a reducible definition), these are used to rewrite with f.
simp[*] simplifies the main goal target using the lemmas tagged with the
attribute [simp] and all hypotheses.
simponly[h₁,h₂,...,hₙ] is like simp[h₁,h₂,...,hₙ] but does not use [simp] lemmas.
simp[-id₁,...,-idₙ] simplifies the main goal target using the lemmas tagged
with the attribute [simp], but removes the ones named idᵢ.
simpath₁h₂...hₙ simplifies the hypotheses h₁:T₁ ... hₙ:Tₙ. If
the target or another hypothesis depends on hᵢ, a new simplified hypothesis
hᵢ is introduced, but the old one remains in the local context.
simpat* simplifies all the hypotheses and the target.
simp[*]at* simplifies target and all (propositional) hypotheses using the
other hypotheses.
simp_all is a stronger version of simp[*]at* where the hypotheses and target
are simplified multiple times until no simplification is applicable.
Only non-dependent propositional hypotheses are considered.
tauto breaks down assumptions of the form _∧_, _∨_, _↔_ and ∃_,_
and splits a goal of the form _∧_, _↔_ or ∃_,_ until it can be discharged
using reflexivity or solve_by_elim.
This is a finishing tactic: it either closes the goal or raises an error.
The Lean 3 version of this tactic by default attempted to avoid classical reasoning
where possible. This Lean 4 version makes no such attempt. The itauto tactic
is designed for that purpose.
Close fixed-width BitVec and Bool goals by obtaining a proof from an external SAT solver and
verifying it inside Lean. The solvable goals are currently limited to
automatically splitting up structures that contain information about BitVec or Bool
example:∀(ab:BitVec64),(a&&&b)+(a^^^b)=a|||b:=⊢ ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| ba✝:BitVec 64b✝:BitVec 64⊢ (a✝ &&& b✝) + (a✝ ^^^ b✝) = a✝ ||| b✝All goals completed! 🐙
If bv_decide encounters an unknown definition it will be treated like an unconstrained BitVec
variable. Sometimes this enables solving goals despite not understanding the definition because
the precise properties of the definition do not matter in the specific proof.
If bv_decide fails to close a goal it provides a counter-example, containing assignments for all
terms that were considered as variables.
In order to avoid calling a SAT solver every time, the proof can be cached with bv_decide?.
If solving your problem relies inherently on using associativity or commutativity, consider enabling
the bv.ac_nf option.
Note: bv_decide uses ofReduceBool and thus trusts the correctness of the code generator.
trivial tries different simple tactics (e.g., rfl, contradiction, ...)
to close the current goal.
You can use the command macro_rules to extend the set of tactics used. Example:
The congruence closure tactic cc tries to solve the goal by chaining
equalities from context and applying congruence (i.e. if a=b, then fa=fb).
It is a finishing tactic, i.e. it is meant to close
the current goal, not to make some inconclusive progress.
A mostly trivial example would be:
linarith attempts to find a contradiction between hypotheses that are linear (in)equalities.
Equivalently, it can prove a linear inequality by assuming its negation and proving False.
In theory, linarith should prove any goal that is true in the theory of linear arithmetic over
the rationals. While there is some special handling for non-dense orders like Nat and Int,
this tactic is not complete for these theories and will not prove every true goal. It will solve
goals over arbitrary types that instantiate LinearOrderedCommRing.
An example:
example(xyz:ℚ)(h1:2*x<3*y)(h2:-4*x+2*z<0)(h3:12*y-4*z<0):False:=x:ℚy:ℚz:ℚh1:2 * x < 3 * yh2:-4 * x + 2 * z < 0h3:12 * y - 4 * z < 0⊢ FalseAll goals completed! 🐙
linarith will use all appropriate hypotheses and the negation of the goal, if applicable.
Disequality hypotheses require case splitting and are not normally considered
(see the splitNe option below).
linarith[t1,t2,t3] will additionally use proof terms t1,t2,t3.
linarithonly[h1,h2,h3,t1,t2,t3] will use only the goal (if relevant), local hypotheses
h1, h2, h3, and proofs t1, t2, t3. It will ignore the rest of the local context.
linarith! will use a stronger reducibility setting to try to identify atoms. For example,
example (x : ℚ) : id x ≥ x := by
linarith
will fail, because linarith will not identify x and idx. linarith! will.
This can sometimes be expensive.
linarith(config:={..}) takes a config object with five
optional arguments:
discharger specifies a tactic to be used for reducing an algebraic equation in the
proof stage. The default is ring. Other options include simp for basic
problems.
transparency controls how hard linarith will try to match atoms to each other. By default
it will only unfold reducible definitions.
If splitHypotheses is true, linarith will split conjunctions in the context into separate
hypotheses.
If splitNe is true, linarith will case split on disequality hypotheses.
For a given x≠y hypothesis, linarith is run with both x<y and x>y,
and so this runs linarith exponentially many times with respect to the number of
disequality hypotheses. (false by default.)
If exfalso is false, linarith will fail when the goal is neither an inequality nor False.
(true by default.)
restrict_type (not yet implemented in mathlib4)
will only use hypotheses that are inequalities over tp. This is useful
if you have e.g. both integer and rational valued inequalities in the local context, which can
sometimes confuse the tactic.
A variant, nlinarith, does some basic preprocessing to handle some nonlinear goals.
The option set_optiontrace.linarithtrue will trace certain intermediate stages of the linarith
routine.
Tactic solving goals of the form 0≤x, 0<x and x≠0. The tactic works recursively
according to the syntax of the expression x, if the atoms composing the expression all have
numeric lower bounds which can be proved positive/nonnegative/nonzero by norm_num. This tactic
either closes the goal or fails.