doc(reducible): add documentation for reducible hints.

doc/lean/reducible.org

@@ -0,0 +1,104 @@
+* 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 simulateneous
+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 a 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 a
+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 decisition 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 modifer =[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.