3.3 KiB
Reducible hints
Lean automation can be configured using different commands and
annotations. The reducible hint/annotation instructs automation
which declarations can be freely unfolded. One of the main components
of the Lean elaborator is a procedure for solving simultaneous
higher-order unification constraints. Higher-order unification is a
undecidable problem. Thus, the procedure implemented in Lean is
clearly incomplete, that is, it may fail to find a solution for a set
of constraints. One way to guide/help the procedure is to indicate
which declarations can be unfolded. We should not confuse the
reducible hint with whether a declaration is opaque or not. We say
opaqueness is part of the Lean logic, and is implemented inside of
its trusted kernel. The reducible hint is just a way to
control/guide Lean automation to fill missing gaps in our proofs and
definitions. The Lean kernel ignores this annotation.
The higher-order unification procedure has to perform case-analysis.
The procedure is essentially implementing a backtracking search. This
procedure has to decide whether a definition C should be unfolded or
not. Here, we roughly divide this decision in two groups: simple
and complex. We say an unfolding decision is simple if the
procedure does not have to consider an extra case (aka
case-split). That is, it does not increase the search space. We say an
unfolding decision is complex if it produces at least one extra
case, and consequently increases the search space.
Users can mark whether a definition is reducible or irreducible.
We write reducible(C) to denote that C was marked as reducible by the user,
and irreducible(C) to denote that C was marked as irreducible by the user.
Theorems are never unfolded. For a transparent definition C, the
higher-order unification procedure uses the following decision tree.
if simple unfolding decision then
if irreducible(C) then
do not unfold
else
unfold
end
else -- complex unfolding decision
if reducible(C) then
unfold
else
do not unfold
end
end
For an opaque definition D, the higher-order unification procedure uses the
same decision tree if D was declared in the current module. Otherwise, it does
not unfold D.
The following command declares a transparent definition pr and mark it as reducible.
definition pr1 [reducible] (A : Type) (a b : A) : A := a
The reducible attribute is saved in the compiled .olean files. The user
can change the reducible and irreducible attributes using
the attribute command. The modification is saved in the
produced .olean file.
definition id (A : Type) (a : A) : A := a
definition pr2 (A : Type) (a b : A) : A := b
-- mark pr2 as reducible
attribute pr2 [reducible]
-- ...
-- mark id and pr2 as irreducible
attribute id [irreducible]
attribute pr2 [irreducible]
The command local attribute can be used to instruct Lean to not save
the new attribute in the .olean file. If the attibute command is used
inside of a context, then the scope of its effect is the current scope.
definition pr2 (A : Type) (a b : A) : A := b
-- Mark pr2 as irreducible.
-- The modification will not affect modules that import this one.
local attribute pr2 [irreducible]