A work-in-progress replacement for Lean3's solve_by_elim
tactic.
We'll gradually bring it up to feature parity.
Visualize an Except
using a checkmark or a cross.
Equations
- exceptEmoji x = match x with | Except.error a => Lean.crossEmoji | Except.ok a => Lean.checkEmoji
applyFirst lemmas cont goal
will try to apply one of the lemmas
to the goal goal
,
and then call cont
on the resulting List MVarId
of subgoals.
It returns the result from cont
for the first such lemma for which
both the apply
and the call to cont
succeed.
applyFirst (trace := `name)
will construct trace nodes for ``nameindicating which calls to
apply` succeeded or failed.
Equations
- One or more equations did not get rendered due to their size.
Maximum recursion depth.
maxDepth : ℕIf
failAtDepth
, thensolve_by_elim
will fail (and backtrack) upon reaching the max depth. Otherwise, upon reaching the max depth, all remaining goals will be returned. (defaults totrue
)failAtMaxDepth : BoolTransparency mode for calls to
apply
.transparency : Lean.Meta.TransparencyModeAlso use symmetric versions (via
@[symm]
) of local hypotheses.symm : BoolTry proving the goal via
exfalso
ifsolve_by_elim
otherwise fails. This is only used when operating on a single goal.exfalso : BoolAn arbitrary procedure which can be used to modify the list of goals before each attempt to apply a lemma. Called as
proc goals curr
, wheregoals
are the original goals forsolve_by_elim
, andcurr
are the current goals. Returningsome l
will replace the current goals withl
and recurse (consuming one step of maximum depth). Returningnone
will proceed to applying lemmas without changing goals. Failure will cause backtracking. (defaults tonone
)proc : List Lean.MVarId → List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))If
suspend g
, then we do not attempt to apply any further lemmas, but returng
as a new subgoal. (defaults tofalse
)suspend : Lean.MVarId → Lean.MetaM Booldischarge g
is called on goals for which no lemmas apply. Ifnone
we returng
as a new subgoal. Ifsome l
, we replaceg
byl
in the list of active goals, and recurse. If failure, we backtrack. (defaults to failure)discharge : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
Configuration structure to control the behaviour of solve_by_elim
:
- control the maximum depth and behaviour (fail or return subgoals) at the maximum depth,
- whether to use
symm
on hypotheses andexfalso
on the goal as needed, - and hooks allowing
- modifying intermediate goals,
- returning goals as subgoals, and
- discharging subgoals.
Instances For
The default maxDepth
for apply_rules
is higher.
Instances For
Allow elaboration of Config
arguments to tactics.
Equations
- One or more equations did not get rendered due to their size.
Allow elaboration of ApplyRulesConfig
arguments to tactics.
Equations
- One or more equations did not get rendered due to their size.
Create or modify a Config
which allows a class of goals to be returned as subgoals.
Equations
- One or more equations did not get rendered due to their size.
Create or modify a Config
which does no backtracking.
Equations
Create or modify a Config
which runs a tactic on the main goal.
If that tactic fails, fall back to the proc
behaviour of cfg
.
Equations
- One or more equations did not get rendered due to their size.
Create or modify a Config
which calls intro
on each goal before applying lemmas.
Equations
- Mathlib.Tactic.SolveByElim.Config.intros cfg = Mathlib.Tactic.SolveByElim.Config.mainGoalProc cfg fun g => do let __do_lift ← Lean.MVarId.intro1P g pure [__do_lift.snd]
Create or modify a Config
which rejects branches for which test
,
applied to the instantiations of the original goals, fails or returns false
.
Equations
- One or more equations did not get rendered due to their size.
Create or modify a Config
which rejects complete solutions for which test
,
applied to the instantiations of the original goals, fails or returns false
.
Equations
- One or more equations did not get rendered due to their size.
Create or modify a Config
which only accept solutions
for which every expression in use
appears as a subexpression.
Equations
- One or more equations did not get rendered due to their size.
Elaborate a list of lemmas and local context.
See mkAssumptionSet
for an explanation of why this is needed.
Equations
- One or more equations did not get rendered due to their size.
Solve a collection of goals by repeatedly applying lemmas, backtracking as necessary.
Arguments:
cfg : Config
additional configuration options (options forapply
, maximum depth, and custom flow control)lemmas : List (TermElabM Expr)
lemmas to apply. These are thunks inTermElabM
to avoid stuck metavariables.ctx : TermElabM (List Expr)
monadic function returning the local hypotheses to use.goals : List MVarId
the initial list of goals forsolveByElim
Returns a list of suspended goals, if it succeeded on all other subgoals.
By default cfg.suspend
is false,
cfg.discharge
fails, and cfg.failAtMaxDepth
is true
,
and so the returned list is always empty.
Custom wrappers (e.g. apply_assumption
and apply_rules
) may modify this behaviour.
Equations
- One or more equations did not get rendered due to their size.
n : Nat
steps remaining.curr : List MVarId
the current list of unsolved goals.acc : List MVarId
a list of "suspended" goals, which will be returned as subgoals.
Equations
- One or more equations did not get rendered due to their size.
A MetaM
analogue of the apply_rules
user tactic.
Since apply_rules
does not backtrack, we don't need to worry about stuck metavariables
and can pass the lemmas as a List Expr
.
By default it uses all local hypotheses, but you can disable this with only := true
.
If you need to remove particular local hypotheses, call solveByElim
directly.
Equations
- One or more equations did not get rendered due to their size.
mkAssumptionSet
builds a collection of lemmas for use in
the backtracking search in solve_by_elim
.
- By default, it includes all local hypotheses, along with
rfl
,trivial
,congrFun
andcongrArg
. - The flag
noDefaults
removes these. - The flag
star
includes all local hypotheses, but notrfl
,trivial
,congrFun
, orcongrArg
. (It doesn't make sense to usestar
withoutnoDefaults
.) - The argument
add
is the list of terms inside the square brackets that did not have-
and can be used to add expressions or local hypotheses - The argument
remove
is the list of terms inside the square brackets that had a-
, and can be used to remove local hypotheses. (It doesn't make sense to remove expressions which are not local hypotheses, to remove local hypotheses unless!noDefaults || star
, and it does not make sense to usestar
unless you remove at least one local hypothesis.)
mkAssumptionSet
returns not a List expr
, but a List (TermElabM Expr) × TermElabM (List Expr)
.
There are two separate problems that need to be solved.
Stuck metavariables #
Lemmas with implicit arguments would be filled in with metavariables if we created the
Expr
objects immediately, so instead we return thunks that generate the expressions
on demand. This is the first component, with type List (TermElabM expr)
.
As an example, we have def rfl : ∀ {α : Sort u} {a : α}, a = a
, which on elaboration will become
@rfl ?m_1 ?m_2
.
Because solve_by_elim
works by repeated application of lemmas against subgoals,
the first time such a lemma is successfully applied,
those metavariables will be unified, and thereafter have fixed values.
This would make it impossible to apply the lemma
a second time with different values of the metavariables.
See https://github.com/leanprover-community/mathlib/issues/2269
Relevant local hypotheses #
solve_by_elim*
works with multiple goals,
and we need to use separate sets of local hypotheses for each goal.
The second component of the returned value provides these local hypotheses.
(Essentially using local_context
, along with some filtering to remove hypotheses
that have been explicitly removed via only
or [-h]
.)
Equations
- One or more equations did not get rendered due to their size.
Run elabTerm
.
Equations
Syntax for omitting a local hypothesis in solve_by_elim
.
Equations
- One or more equations did not get rendered due to their size.
Syntax for including all local hypotheses in solve_by_elim
.
Equations
- Mathlib.Tactic.SolveByElim.star = Lean.ParserDescr.nodeWithAntiquot "star" `Mathlib.Tactic.SolveByElim.star (Lean.ParserDescr.symbol "*")
Syntax for adding or removing a term, or *
, in solve_by_elim
.
Equations
- One or more equations did not get rendered due to their size.
Syntax for adding and removing terms in solve_by_elim
.
Equations
- One or more equations did not get rendered due to their size.
Syntax for using all lemmas labelled with an attribute in solve_by_elim
.
Equations
- One or more equations did not get rendered due to their size.
Parse the lemma argument of a call to solve_by_elim
.
The first component should be true if *
appears at least once.
The second component should contain each term t
in the arguments.
The third component should contain t
for each -t
in the arguments.
Equations
- One or more equations did not get rendered due to their size.
Parse the using ...
argument for solve_by_elim
.
Equations
- One or more equations did not get rendered due to their size.
solve_by_elim
calls apply
on the main goal to find an assumption whose head matches
and then repeatedly calls apply
on the generated subgoals until no subgoals remain,
performing at most maxDepth
(defaults to 6) recursive steps.
solve_by_elim
discharges the current goal or fails.
solve_by_elim
performs backtracking if subgoals can not be solved.
By default, the assumptions passed to apply
are the local context, rfl
, trivial
,
congrFun
and congrArg
.
The assumptions can be modified with similar syntax as for simp
:
solve_by_elim [h₁, h₂, ..., hᵣ]
also applies the given expressions.solve_by_elim only [h₁, h₂, ..., hᵣ]
does not include the local context,rfl
,trivial
,congrFun
, orcongrArg
unless they are explicitly included.solve_by_elim [-h₁, ... -hₙ]
removes the given local hypotheses.solve_by_elim using [a₁, ...]
uses all lemmas which have been labelled with the attributesaᵢ
(these attributes must be created usingregister_label_attr
).
solve_by_elim*
tries to solve all goals together, using backtracking if a solution for one goal
makes other goals impossible.
(Adding or removing local hypotheses may not be well-behaved when starting with multiple goals.)
Optional arguments passed via a configuration argument as solve_by_elim (config := { ... })
maxDepth
: number of attempts at discharging generated subgoalssymm
: adds all hypotheses derived bysymm
(defaults totrue
).exfalso
: allow callingexfalso
and trying again ifsolve_by_elim
fails (defaults totrue
).transparency
: change the transparency mode when callingapply
. Defaults to.default
, but it is often useful to change to.reducible
, so semireducible definitions will not be unfolded when trying to apply a lemma.
See also the doc-comment for Mathlib.Tactic.SolveByElim.Config
for the options
proc
, suspend
, and discharge
which allow further customization of solve_by_elim
.
Both apply_assumption
and apply_rules
are implemented via these hooks.
Equations
- One or more equations did not get rendered due to their size.
Wrapper for solveByElim
that processes a list of Term
s
that specify the lemmas to use.
Equations
- One or more equations did not get rendered due to their size.
apply_assumption
looks for an assumption of the form ... → ∀ _, ... → head
where head
matches the current goal.
You can specify additional rules to apply using apply_assumption [...]
.
By default apply_assumption
will also try rfl
, trivial
, congrFun
, and congrArg
.
If you don't want these, or don't want to use all hypotheses, use apply_assumption only [...]
.
You can use apply_assumption [-h]
to omit a local hypothesis.
You can use apply_assumption using [a₁, ...]
to use all lemmas which have been labelled
with the attributes aᵢ
(these attributes must be created using register_label_attr
).
apply_assumption
will use consequences of local hypotheses obtained via symm
.
If apply_assumption
fails, it will call exfalso
and try again.
Thus if there is an assumption of the form P → ¬ Q
, the new tactic state
will have two goals, P
and Q
.
You can pass a further configuration via the syntax apply_rules (config := {...}) lemmas
.
The options supported are the same as for solve_by_elim
(and include all the options for apply
).
Equations
- One or more equations did not get rendered due to their size.
apply_rules [l₁, l₂, ...]
tries to solve the main goal by iteratively
applying the list of lemmas [l₁, l₂, ...]
or by applying a local hypothesis.
If apply
generates new goals, apply_rules
iteratively tries to solve those goals.
You can use apply_rules [-h]
to omit a local hypothesis.
apply_rules
will also use rfl
, trivial
, congrFun
and congrArg
.
These can be disabled, as can local hypotheses, by using apply_rules only [...]
.
You can use apply_rules using [a₁, ...]
to use all lemmas which have been labelled
with the attributes aᵢ
(these attributes must be created using register_label_attr
).
You can pass a further configuration via the syntax apply_rules (config := {...})
.
The options supported are the same as for solve_by_elim
(and include all the options for apply
).
apply_rules
will try calling symm
on hypotheses and exfalso
on the goal as needed.
This can be disabled with apply_rules (config := {symm := false, exfalso := false})
.
You can bound the iteration depth using the syntax apply_rules (config := {maxDepth := n})
.
Unlike solve_by_elim
, apply_rules
does not perform backtracking, and greedily applies
a lemma from the list until it gets stuck.
Equations
- One or more equations did not get rendered due to their size.