From 0c72df404f71846a432064c60da760b530e65d5e Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Wed, 11 Feb 2026 13:59:28 +0100 Subject: [PATCH 1/2] document `clear` tactic --- doc/tactics/clear.rst | 60 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 doc/tactics/clear.rst diff --git a/doc/tactics/clear.rst b/doc/tactics/clear.rst new file mode 100644 index 000000000..9c2d89a91 --- /dev/null +++ b/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. From 694805429e0d491fe5a12382518d2ec15d91b6d0 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 13 Feb 2026 13:47:52 +0100 Subject: [PATCH 2/2] single backticks --- doc/tactics/clear.rst | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/doc/tactics/clear.rst b/doc/tactics/clear.rst index 9c2d89a91..1f60cf499 100644 --- a/doc/tactics/clear.rst +++ b/doc/tactics/clear.rst @@ -1,38 +1,38 @@ ======================================================================== -Tactic: ``clear`` +Tactic: `clear` ======================================================================== -The ``clear`` tactic can be used with any goal to remove hypotheses and +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 +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`` + `clear` -When given no arguments, the ``clear`` tactic removes all hypotheses and +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}`` + `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. +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. .. admonition:: Syntax - ``clear -{idents}`` + `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. +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. .. ecproof:: :title: Hoare logic example