lean2/doc/lean/reducible.org
2014-09-20 07:44:48 -07:00

104 lines
3.8 KiB
Org Mode

* 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.
#+BEGIN_SRC
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 if irreducible(C) then
do not unfold
else if C was defined in the current module then
unfold
else
do not unfold
end
end
#+END_SRC
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=.
#+END_SRC
The following command declares a transparent definition =pr= and mark it as reducible.
#+BEGIN_SRC lean
definition pr1 [reducible] (A : Type) (a b : A) : A := a
#+END_SRC
The =reducible= mark is saved in the compiled .olean files. The user
can temporarily change the =reducible= and =irreducible= marks using
the following commands. The temporary modification is effective only in the
current file, and is not saved in the produced .olean file.
#+BEGIN_SRC lean
definition id (A : Type) (a : A) : A := a
definition pr2 (A : Type) (a b : A) : A := b
-- mark pr2 as reducible
reducible pr2
-- ...
-- mark id and pr2 as irreducible
irreducible id pr2
#+END_SRC
The annotation =[persistent]= can be used to instruct Lean to make the
modification permanent, and save it in the .olean file.
#+BEGIN_SRC lean
definition pr2 (A : Type) (a b : A) : A := b
-- Mark pr2 as irreducible.
-- The modification will affect modules that import this one.
irreducible [persistent] pr2
#+END_SRC
The reducible and irreducible annotations can be removed using the modifier =[none]=.
#+BEGIN_SRC lean
definition pr2 (A : Type) (a b : A) : A := b
-- temporarily remove any reducible and irreducible annotation from pr2
reducible [none] pr2
-- permanently remove any reducible and irreducible annotation from pr2
reducible [persistent] [none] pr2
#+END_SRC
Finally, the command =irreducible= is syntax sugar for =reducible [off]=.
The commands =reducible= and =reducible [on]= are equivalent.