document clear tactic

doc/tactics/clear.rst

@@ -0,0 +1,60 @@
+========================================================================
+Tactic: ``clear``
+========================================================================
+
+The ``clear`` tactic can be used with any goal to remove hypotheses and
+variables from the context. This is useful to simplify the context by 
+removing assumptions and variables that are no longer needed.
+
+There are two variants of the ``clear`` tactic: an opt-in variant where
+specific hypotheses and variables are removed, and an opt-out variant 
+where all hypotheses and variables except for the specified ones are removed.
+
+.. admonition:: Syntax
+
+  ``clear``
+
+When given no arguments, the ``clear`` tactic removes all hypotheses and 
+all variables not transitively used in the goal from the context.
+
+.. admonition:: Syntax
+
+  ``clear {idents}``
+
+Here, ``{idents}`` is a non-empty space separated list of identifiers of
+the hypotheses and variables to be cleared. If one of these is transitively
+used in the goal, then it is not cleared and an error is raised.
+
+.. admonition:: Syntax
+
+  ``clear -{idents}``
+
+Here, ``{idents}`` is a non-empty space separated list of identifiers of
+the hypotheses and variables that should *not* be cleared. The tactic
+removes all hypotheses and variables except for those in the list, and
+those used transitively in the goal *or* in the objects in the list.
+
+.. ecproof::
+   :title: Hoare logic example
+
+   lemma L: true.
+   pose x:=false.
+   (*$*) clear x.
+   (* `x` is now unbound *)
+   pose x:=false.
+   pose y:=x.
+   pose z:=y.
+   clear -y. 
+   (* `z` is unbound, but `x` is not, since `y` depends on it *)
+   pose z:=x.
+   clear y.
+   pose y:=z.
+   clear. 
+   (* everything is unbound, since nothing is in the goal *)
+   pose x:=true.
+   pose y:=false.
+   clear. 
+   (* we cannot clear `x` since it is in the goal,
+       but `y` is not used so it becomes unbound *)
+   pose y:= x.
+   abort.