diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/detailed-tactic-examples.rst | 32 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 26 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 496 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 229 |
5 files changed, 361 insertions, 440 deletions
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index bd16b70d02..63d6a229ed 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -53,7 +53,7 @@ rule of thumb, all the variables that appear inside constructors in the indices of the hypothesis should be generalized. This is exactly what the ``generalize_eqs_vars`` variant does: -.. coqtop:: all +.. coqtop:: all abort generalize_eqs_vars H. induction H. @@ -65,7 +65,7 @@ as well in this case, e.g.: .. coqtop:: none - Abort. + Require Import Coq.Program.Equality. .. coqtop:: in @@ -88,11 +88,7 @@ automatically do such simplifications (which may involve the axiom K). This is what the ``simplify_dep_elim`` tactic from ``Coq.Program.Equality`` does. For example, we might simplify the previous goals considerably: -.. coqtop:: all - - Require Import Coq.Program.Equality. - -.. coqtop:: all +.. coqtop:: all abort induction p ; simplify_dep_elim. @@ -105,10 +101,6 @@ are ``dependent induction`` and ``dependent destruction`` that do induction or simply case analysis on the generalized hypothesis. For example we can redo what we’ve done manually with dependent destruction: -.. coqtop:: none - - Abort. - .. coqtop:: in Lemma ex : forall n m:nat, Le (S n) m -> P n m. @@ -117,7 +109,7 @@ redo what we’ve done manually with dependent destruction: intros n m H. -.. coqtop:: all +.. coqtop:: all abort dependent destruction H. @@ -126,10 +118,6 @@ destructed hypothesis actually appeared in the goal, the tactic would still be able to invert it, contrary to dependent inversion. Consider the following example on vectors: -.. coqtop:: none - - Abort. - .. coqtop:: in Set Implicit Arguments. @@ -230,29 +218,21 @@ name. A term is either an application of: Once we have this datatype we want to do proofs on it, like weakening: -.. coqtop:: in +.. coqtop:: in abort Lemma weakening : forall G D tau, term (G ; D) tau -> forall tau', term (G , tau' ; D) tau. -.. coqtop:: none - - Abort. - The problem here is that we can’t just use induction on the typing derivation because it will forget about the ``G ; D`` constraint appearing in the instance. A solution would be to rewrite the goal as: -.. coqtop:: in +.. coqtop:: in abort Lemma weakening' : forall G' tau, term G' tau -> forall G D, (G ; D) = G' -> forall tau', term (G, tau' ; D) tau. -.. coqtop:: none - - Abort. - With this proper separation of the index from the instance and the right induction loading (putting ``G`` and ``D`` after the inducted-on hypothesis), the proof will go through, but it is a very tedious diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 442077616f..3e87e8acd8 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -602,7 +602,7 @@ Failing .. example:: - .. coqtop:: all + .. coqtop:: all fail Goal True. Proof. fail. Abort. @@ -701,7 +701,7 @@ tactic .. example:: - .. coqtop:: all + .. coqtop:: all abort Ltac time_constr1 tac := let eval_early := match goal with _ => restart_timer "(depth 1)" end in @@ -716,7 +716,6 @@ tactic let y := time_constr1 ltac:(fun _ => eval compute in x) in y) in pose v. - Abort. Local definitions ~~~~~~~~~~~~~~~~~ @@ -847,7 +846,7 @@ We can carry out pattern matching on terms with: .. example:: - .. coqtop:: all + .. coqtop:: all abort Ltac f x := match x with @@ -1022,7 +1021,7 @@ Counting the goals Goal True /\ True /\ True. split;[|split]. - .. coqtop:: all + .. coqtop:: all abort all:pr_numgoals. @@ -1154,6 +1153,15 @@ Printing |Ltac| tactics Debugging |Ltac| tactics ------------------------ +Backtraces +~~~~~~~~~~ + +.. flag:: Ltac Backtrace + + Setting this flag displays a backtrace on Ltac failures that can be useful + to find out what went wrong. It is disabled by default for performance + reasons. + Info trace ~~~~~~~~~~ @@ -1301,10 +1309,10 @@ performance issue. .. coqtop:: all - Set Ltac Profiling. - tac. - Show Ltac Profile. - Show Ltac Profile "omega". + Set Ltac Profiling. + tac. + Show Ltac Profile. + Show Ltac Profile "omega". .. coqtop:: in diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 24645a8cc3..2300a317f1 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -529,16 +529,12 @@ Requesting information .. example:: - .. coqtop:: all + .. coqtop:: all abort Goal exists n, n = 0. eexists ?[n]. Show n. - .. coqtop:: none - - Abort. - .. cmdv:: Show Script :name: Show Script @@ -739,14 +735,10 @@ Notes: split. - .. coqtop:: all + .. coqtop:: all abort 2: split. - .. coqtop:: none - - Abort. - .. .. coqtop:: none @@ -759,14 +751,10 @@ Notes: intros n. - .. coqtop:: all + .. coqtop:: all abort intros m. - .. coqtop:: none - - Abort. - This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal with 2 goals. Notice that the goal ``P 1`` is not highlighted at all after the split because it has not changed. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 483dbd311d..237b534d67 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -215,7 +215,7 @@ construct differs from the latter in that .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -233,7 +233,7 @@ construct differs from the latter in that .. coqtop:: reset all - Definition f u := let (m, n) := u in m + n. + Fail Definition f u := let (m, n) := u in m + n. The ``let:`` construct is just (more legible) notation for the primitive @@ -275,7 +275,7 @@ example, the null and all list function(al)s can be defined as follows: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -376,7 +376,7 @@ expressions such as .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -401,7 +401,7 @@ each point of use, e.g., the above definition can be written: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -413,7 +413,7 @@ each point of use, e.g., the above definition can be written: Variable all : (T -> bool) -> list T -> bool. - .. coqtop:: all undo + .. coqtop:: all Prenex Implicits null. Definition all_null (s : list T) := all null s. @@ -436,7 +436,7 @@ The syntax of the new declaration is a ``Set Printing All`` command). All |SSR| library files thus start with the incantation - .. coqtop:: all undo + .. coqdoc:: Set Implicit Arguments. Unset Strict Implicit. @@ -464,7 +464,7 @@ defined by the following declaration: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -505,7 +505,7 @@ Definitions |SSR| pose tactic supports *open syntax*: the body of the definition does not need surrounding parentheses. For instance: -.. coqtop:: in +.. coqdoc:: pose t := x + y. @@ -518,7 +518,7 @@ For example, the tactic :tacn:`pose <pose (ssreflect)>` supoprts parameters: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -534,7 +534,7 @@ The |SSR| pose tactic also supports (co)fixpoints, by providing the local counterpart of the ``Fixpoint f := …`` and ``CoFixpoint f := …`` constructs. For instance, the following tactic: -.. coqtop:: in +.. coqdoc:: pose fix f (x y : nat) {struct x} : nat := if x is S p then S (f p y) else 0. @@ -544,7 +544,7 @@ on natural numbers. Similarly, local cofixpoints can be defined by a tactic of the form: -.. coqtop:: in +.. coqdoc:: pose cofix f (arg : T) := … . @@ -553,26 +553,26 @@ offers a smooth way of defining local abstractions. The type of “holes” is guessed by type inference, and the holes are abstracted. For instance the tactic: -.. coqtop:: in +.. coqdoc:: pose f := _ + 1. is shorthand for: -.. coqtop:: in +.. coqdoc:: pose f n := n + 1. When the local definition of a function involves both arguments and holes, hole abstractions appear first. For instance, the tactic: -.. coqtop:: in +.. coqdoc:: pose f x := x + _. is shorthand for: -.. coqtop:: in +.. coqdoc:: pose f n x := x + n. @@ -580,13 +580,13 @@ The interaction of the pose tactic with the interpretation of implicit arguments results in a powerful and concise syntax for local definitions involving dependent types. For instance, the tactic: -.. coqtop:: in +.. coqdoc:: pose f x y := (x, y). adds to the context the local definition: -.. coqtop:: in +.. coqdoc:: pose f (Tx Ty : Type) (x : Tx) (y : Ty) := (x, y). @@ -639,7 +639,7 @@ The tactic: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -652,11 +652,7 @@ The tactic: Lemma test x : f x + f x = f x. set t := f _. - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart set t := {2}(f _). @@ -694,7 +690,7 @@ conditions: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -715,7 +711,7 @@ conditions: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -736,7 +732,7 @@ Moreover: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -756,7 +752,7 @@ Moreover: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -766,7 +762,7 @@ Moreover: .. coqtop:: all Lemma test : forall x : nat, x + 1 = 0. - set t := _ + 1. + Fail set t := _ + 1. + Typeclass inference should fill in any residual hole, but matching should never assign a value to a global existential variable. @@ -789,7 +785,7 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -810,7 +806,7 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -831,7 +827,7 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -862,7 +858,7 @@ selection. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -879,7 +875,7 @@ only one occurrence of the selected term. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -889,7 +885,7 @@ only one occurrence of the selected term. .. coqtop:: all Lemma test x y z : (x + y) + (z + z) = z + z. - set a := {2}(_ + _). + Fail set a := {2}(_ + _). .. _basic_localization_ssr: @@ -910,7 +906,7 @@ context of a goal thanks to the ``in`` tactical. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. @@ -926,7 +922,7 @@ context of a goal thanks to the ``in`` tactical. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. @@ -1042,7 +1038,7 @@ constants to the goal. For example, the proof of [#3]_ - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1079,7 +1075,7 @@ constants to the goal. Because they are tacticals, ``:`` and ``=>`` can be combined, as in -.. coqtop:: in +.. coqdoc:: move: m le_n_m => p le_n_p. @@ -1104,7 +1100,7 @@ The ``:`` tactical is used to operate on an element in the context. to encapsulate the inductive step in a single command: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1139,7 +1135,7 @@ Basic tactics like apply and elim can also be used without the ’:’ tactical: for example we can directly start a proof of ``subnK`` by induction on the top variable ``m`` with -.. coqtop:: in +.. coqdoc:: elim=> [|m IHm] n le_n. @@ -1150,7 +1146,7 @@ explained in terms of the goal stack:: is basically equivalent to -.. coqtop:: in +.. coqdoc:: move: a H1 H2; tactic => a H1 H2. @@ -1163,13 +1159,13 @@ temporary abbreviation to hide the statement of the goal from The general form of the in tactical can be used directly with the ``move``, ``case`` and ``elim`` tactics, so that one can write -.. coqtop:: in +.. coqdoc:: elim: n => [|n IHn] in m le_n_m *. instead of -.. coqtop:: in +.. coqdoc:: elim: n m le_n_m => [|n IHn] m le_n_m. @@ -1257,7 +1253,7 @@ The elim tactic .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1297,7 +1293,7 @@ existential metavariables of sort :g:`Prop`. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1398,7 +1394,7 @@ Switches affect the discharging of a :token:`d_item` as follows: For example, the tactic: -.. coqtop:: in +.. coqdoc:: move: n {2}n (refl_equal n). @@ -1409,7 +1405,7 @@ For example, the tactic: Therefore this tactic changes any goal ``G`` into -.. coqtop:: +.. coqdoc:: forall n n0 : nat, n = n0 -> G. @@ -1477,7 +1473,7 @@ context to interpret wildcards; in particular it can accommodate the .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1752,7 +1748,7 @@ Clears are deferred until the end of the intro pattern. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -1813,7 +1809,7 @@ Block introduction .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1843,7 +1839,7 @@ Generation of equations The generation of named equations option stores the definition of a new constant as an equation. The tactic: -.. coqtop:: in +.. coqdoc:: move En: (size l) => n. @@ -1851,7 +1847,7 @@ where ``l`` is a list, replaces ``size l`` by ``n`` in the goal and adds the fact ``En : size l = n`` to the context. This is quite different from: -.. coqtop:: in +.. coqdoc:: pose n := (size l). @@ -1866,7 +1862,7 @@ deal with the possible parameters of the constants introduced. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1885,7 +1881,7 @@ under fresh |SSR| names. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1936,7 +1932,7 @@ be substituted. inferred looking at the type of the top assumption. This allows for the compact syntax: - .. coqtop:: in + .. coqdoc:: case: {2}_ / eqP. @@ -1952,7 +1948,7 @@ be substituted. Here is a small example on lists. We define first a function which adds an element at the end of a given list. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1989,19 +1985,17 @@ be substituted. Lemma test l : (length l) * 2 = length (l ++ l). case: (lastP l). - Applied to the same goal, the command: - ``case: l / (lastP l).`` - generates the same subgoals but ``l`` has been cleared from both contexts. + Applied to the same goal, the tactc ``case: l / (lastP l)`` + generates the same subgoals but ``l`` has been cleared from both contexts: - Again applied to the same goal, the command. + .. coqtop:: all restart - .. coqtop:: none + case: l / (lastP l). - Abort. + Again applied to the same goal: - .. coqtop:: all + .. coqtop:: all restart abort - Lemma test l : (length l) * 2 = length (l ++ l). case: {1 3}l / (lastP l). Note that selected occurrences on the left of the ``/`` @@ -2015,10 +2009,6 @@ be substituted. .. example:: - .. coqtop:: none - - Abort. - .. coqtop:: all Lemma test l : (length l) * 2 = length (l ++ l). @@ -2112,7 +2102,7 @@ In the script provided as example in section :ref:`indentation_ssr`, the paragraph corresponding to each sub-case ends with a tactic line prefixed with a ``by``, like in: -.. coqtop:: in +.. coqdoc:: by apply/eqP; rewrite -dvdn1. @@ -2147,13 +2137,13 @@ A natural and common way of closing a goal is to apply a lemma which is the exact one needed for the goal to be solved. The defective form of the tactic: -.. coqtop:: in +.. coqdoc:: exact. is equivalent to: -.. coqtop:: in +.. coqdoc:: do [done | by move=> top; apply top]. @@ -2161,13 +2151,13 @@ where ``top`` is a fresh name assigned to the top assumption of the goal. This applied form is supported by the ``:`` discharge tactical, and the tactic: -.. coqtop:: in +.. coqdoc:: exact: MyLemma. is equivalent to: -.. coqtop:: in +.. coqdoc:: by apply: MyLemma. @@ -2179,19 +2169,19 @@ is equivalent to: follows the ``by`` keyword is considered to be a parenthesized block applied to the current goal. Hence for example if the tactic: - .. coqtop:: in + .. coqdoc:: by rewrite my_lemma1. succeeds, then the tactic: - .. coqtop:: in + .. coqdoc:: by rewrite my_lemma1; apply my_lemma2. usually fails since it is equivalent to: - .. coqtop:: in + .. coqdoc:: by (rewrite my_lemma1; apply my_lemma2). @@ -2247,7 +2237,7 @@ Finally, the tactics ``last`` and ``first`` combine with the branching syntax of Ltac: if the tactic generates n subgoals on a given goal, then the tactic -.. coqtop:: in +.. coqdoc:: tactic ; last k [ tactic1 |…| tacticm ] || tacticn. @@ -2260,9 +2250,8 @@ to the others. Here is a small example on lists. We define first a function which adds an element at the end of a given list. - .. coqtop:: reset + .. coqtop:: reset none - Abort. From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. @@ -2296,13 +2285,13 @@ Iteration A tactic of the form: -.. coqtop:: in +.. coqdoc:: do [ tactic 1 | … | tactic n ]. is equivalent to the standard Ltac expression: -.. coqtop:: in +.. coqdoc:: first [ tactic 1 | … | tactic n ]. @@ -2327,14 +2316,14 @@ Their meaning is: For instance, the tactic: -.. coqtop:: in +.. coqdoc:: tactic; do 1? rewrite mult_comm. rewrites at most one time the lemma ``mult_comm`` in all the subgoals generated by tactic , whereas the tactic: -.. coqtop:: in +.. coqdoc:: tactic; do 2! rewrite mult_comm. @@ -2380,7 +2369,7 @@ between standard Ltac in and the |SSR| tactical in. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2455,7 +2444,7 @@ the holes are abstracted in term. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2469,7 +2458,7 @@ the holes are abstracted in term. The invokation of ``have`` is equivalent to: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2487,7 +2476,7 @@ tactic: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2518,7 +2507,7 @@ tactics of the form: which behave like: -.. coqtop:: in +.. coqdoc:: have: term ; first by tactic. move=> clear_switch i_item. @@ -2531,7 +2520,7 @@ to introduce the new assumption itself. The ``by`` feature is especially convenient when the proof script of the statement is very short, basically when it fits in one line like in: -.. coqtop:: in +.. coqdoc:: have H23 : 3 + 2 = 2 + 3 by rewrite addnC. @@ -2540,7 +2529,7 @@ the further use of the intermediate step. For instance, .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2559,7 +2548,7 @@ the further use of the intermediate step. For instance, Thanks to the deferred execution of clears, the following idiom is also supported (assuming x occurs in the goal only): -.. coqtop:: in +.. coqdoc:: have {x} -> : x = y. @@ -2568,7 +2557,7 @@ destruction of existential assumptions like in the tactic: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2595,7 +2584,7 @@ term for the intermediate lemma, using tactics of the form: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2616,7 +2605,7 @@ After the :token:`i_pattern`, a list of binders is allowed. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. From Coq Require Import Omega. @@ -2635,7 +2624,7 @@ Since the :token:`i_pattern` can be omitted, to avoid ambiguity, bound variables can be surrounded with parentheses even if no type is specified: -.. coqtop:: in +.. coqtop:: all restart have (x) : 2 * x = x + x by omega. @@ -2649,13 +2638,8 @@ copying the goal itself. .. example:: - .. coqtop:: none - - Abort All. - - .. coqtop:: all + .. coqtop:: all restart abort - Lemma test : True. have suff H : 2 + 2 = 3; last first. Note that H is introduced in the second goal. @@ -2676,10 +2660,9 @@ context entry name. .. coqtop:: none - Abort All. Set Printing Depth 15. - .. coqtop:: all + .. coqtop:: all abort Inductive Ord n := Sub x of x < n. Notation "'I_ n" := (Ord n) (at level 8, n at level 2, format "''I_' n"). @@ -2695,11 +2678,7 @@ For this purpose the ``[: name ]`` intro pattern and the tactic .. example:: - .. coqtop:: none - - Abort All. - - .. coqtop:: all + .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; omega. @@ -2712,11 +2691,7 @@ with have and an explicit term, they must be used as follows: .. example:: - .. coqtop:: none - - Abort All. - - .. coqtop:: all + .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. have [:pm] @i : 'I_n := Sub m pm. @@ -2735,11 +2710,7 @@ makes use of it). .. example:: - .. coqtop:: none - - Abort All. - - .. coqtop:: all + .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; omega. @@ -2756,21 +2727,21 @@ typeclass inference. .. coqtop:: none - Abort All. - Axiom ty : Type. Axiom t : ty. Goal True. -+ .. coqtop:: in undo + .. coqtop:: all have foo : ty. Full inference for ``ty``. The first subgoal demands a proof of such instantiated statement. -+ .. coqdoc:: + .. A strange bug prevents using the coqtop directive here + + .. coqdoc:: have foo : ty := . @@ -2779,13 +2750,13 @@ typeclass inference. statement. Note that no proof term follows ``:=``, hence two subgoals are generated. -+ .. coqtop:: in undo + .. coqtop:: all restart have foo : ty := t. No inference for ``ty`` and ``t``. -+ .. coqtop:: in undo + .. coqtop:: all restart abort have foo := t. @@ -2816,7 +2787,7 @@ The + but the optional clear item is still performed in the *second* branch. This means that the tactic: - .. coqtop:: in + .. coqdoc:: suff {H} H : forall x : nat, x >= 0. @@ -2834,10 +2805,9 @@ The ``have`` modifier can follow the ``suff`` tactic. .. coqtop:: none - Abort All. Axioms G P : Prop. - .. coqtop:: all + .. coqtop:: all abort Lemma test : G. suff have H : P. @@ -2888,7 +2858,7 @@ name of the local definition with the ``@`` character. In the second subgoal, the tactic: -.. coqtop:: in +.. coqdoc:: move=> clear_switch i_item. @@ -2902,10 +2872,6 @@ are unique. .. example:: - .. coqtop:: none - - Abort All. - .. coqtop:: all Lemma quo_rem_unicity d q1 q2 r1 r2 : @@ -2927,7 +2893,7 @@ pattern will be used to process its instance. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. @@ -2976,7 +2942,7 @@ illustrated in the following example. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2995,10 +2961,13 @@ illustrated in the following example. the pattern ``id (addx x)``, that would produce the following first subgoal - .. coqtop:: none + .. coqtop:: reset none + + From Coq Require Import ssreflect Omega. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. - Abort All. - From Coq Require Import Omega. Section Test. Variable x : nat. Definition addx z := z + x. @@ -3126,14 +3095,14 @@ An :token:`r_item` can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. coqtop:: all abort Definition double x := x + x. Definition ddouble x := double (double x). @@ -3145,21 +3114,16 @@ An :token:`r_item` can be: The |SSR| terms containing holes are *not* typed as abstractions in this context. Hence the following script fails. - .. coqtop:: none - - Abort. - .. coqtop:: all Definition f := fun x y => x + y. Lemma test x y : x + y = f y x. - rewrite -[f y]/(y + _). - but the following script succeeds + .. coqtop:: all fail - .. coqtop:: none + rewrite -[f y]/(y + _). - Restart. + but the following script succeeds .. coqtop:: all @@ -3192,7 +3156,7 @@ tactics. In a rewrite tactic of the form: -.. coqtop:: in +.. coqdoc:: rewrite occ_switch [term1]term2. @@ -3235,7 +3199,7 @@ Performing rewrite and simplification operations in a single tactic enhances significantly the concision of scripts. For instance the tactic: -.. coqtop:: in +.. coqdoc:: rewrite /my_def {2}[f _]/= my_eq //=. @@ -3250,7 +3214,7 @@ proof of basic results on natural numbers arithmetic. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3286,7 +3250,7 @@ side of the equality the user wants to rewrite. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3306,7 +3270,7 @@ the equality. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3316,7 +3280,7 @@ the equality. .. coqtop:: all Lemma test (H : forall t u, t + u * 0 = t) x y : x + y * 4 + 2 * 0 = x + 2 * 0. - rewrite [x + _]H. + Fail rewrite [x + _]H. Indeed the left hand side of ``H`` does not match the redex identified by the pattern ``x + y * 4``. @@ -3329,7 +3293,7 @@ Occurrence switches and redex switches .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3358,7 +3322,7 @@ repetition. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3388,7 +3352,7 @@ rewrite operations prescribed by the rules on the current goal. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3397,7 +3361,7 @@ rewrite operations prescribed by the rules on the current goal. Section Test. - .. coqtop:: all + .. coqtop:: all abort Variables (a b c : nat). Hypothesis eqab : a = b. @@ -3411,10 +3375,6 @@ rewrite operations prescribed by the rules on the current goal. ``(eqab, eqac)`` is actually a |Coq| term and we can name it with a definition: - .. coqtop:: none - - Abort. - .. coqtop:: all Definition multi1 := (eqab, eqac). @@ -3431,7 +3391,7 @@ literal matches have priority. .. example:: - .. coqtop:: all + .. coqtop:: all abort Definition d := a. Hypotheses eqd0 : d = 0. @@ -3448,11 +3408,7 @@ repeated anew. .. example:: - .. coqtop:: none - - Abort. - - .. coqtop:: all + .. coqtop:: all abort Hypothesis eq_adda_b : forall x, x + a = b. Hypothesis eq_adda_c : forall x, x + a = c. @@ -3475,10 +3431,6 @@ tactic rewrite ``(=~ multi1)`` is equivalent to ``rewrite multi1_rev``. .. example:: - .. coqtop:: none - - Abort. - .. coqtop:: all Hypothesis eqba : b = a. @@ -3498,7 +3450,7 @@ reasoning purposes. The library also provides one lemma per such operation, stating that both versions return the same values when applied to the same arguments: -.. coqtop:: in +.. coqdoc:: Lemma addE : add =2 addn. Lemma doubleE : double =1 doublen. @@ -3514,7 +3466,7 @@ hand side. In order to reason conveniently on expressions involving the efficient operations, we gather all these rules in the definition ``trecE``: -.. coqtop:: in +.. coqdoc:: Definition trecE := (addE, (doubleE, oddE), (mulE, add_mulE, (expE, mul_expE))). @@ -3534,7 +3486,7 @@ Anyway this tactic is *not* equivalent to .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3550,11 +3502,7 @@ Anyway this tactic is *not* equivalent to while the other tactic results in - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart abort rewrite (_ : forall x, x * 0 = 0). @@ -3572,14 +3520,14 @@ cases: + |SSR| never accepts to rewrite indeterminate patterns like: - .. coqtop:: in + .. coqdoc:: Lemma foo (x : unit) : x = tt. |SSR| will however accept the ηζ expansion of this rule: - .. coqtop:: in + .. coqdoc:: Lemma fubar (x : unit) : (let u := x in u) = tt. @@ -3588,7 +3536,7 @@ cases: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3611,11 +3559,7 @@ cases: there is no occurrence of the head symbol ``f`` of the rewrite rule in the goal. - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart fail rewrite H. @@ -3625,21 +3569,13 @@ cases: occurrence), using tactic ``rewrite /f`` (for a global replacement of f by g) or ``rewrite pattern/f``, for a finer selection. - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart rewrite /f H. alternatively one can override the pattern inferred from ``H`` - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart rewrite [f _]H. @@ -3658,7 +3594,7 @@ corresponding new goals will be generated. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. @@ -3666,7 +3602,7 @@ corresponding new goals will be generated. Unset Printing Implicit Defensive. Set Warnings "-notation-overridden". - .. coqtop:: all + .. coqtop:: all abort Axiom leq : nat -> nat -> bool. Notation "m <= n" := (leq m n) : nat_scope. @@ -3689,10 +3625,6 @@ corresponding new goals will be generated. As in :ref:`apply_ssr`, the ``ssrautoprop`` tactic is used to try to solve the existential variable. - .. coqtop:: none - - Abort. - .. coqtop:: all Lemma test (x : 'I_2) y (H : y < 2) : Some x = insub 2 y. @@ -3729,7 +3661,7 @@ copy of any term t. However this copy is (on purpose) *not convertible* to t in the |Coq| system [#8]_. The job is done by the following construction: -.. coqtop:: in +.. coqdoc:: Lemma master_key : unit. Proof. exact tt. Qed. Definition locked A := let: tt := master_key in fun x : A => x. @@ -3741,7 +3673,7 @@ selective rewriting, blocking on the fly the reduction in the term ``t``. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrfun ssrbool. From Coq Require Import List. @@ -3765,7 +3697,7 @@ definition. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3793,14 +3725,14 @@ some functions by the partial evaluation switch ``/=``, unless this allowed the evaluation of a condition. This is possible thanks to another mechanism of term tagging, resting on the following *Notation*: -.. coqtop:: in +.. coqdoc:: Notation "'nosimpl' t" := (let: tt := tt in t). The term ``(nosimpl t)`` simplifies to ``t`` *except* in a definition. More precisely, given: -.. coqtop:: in +.. coqdoc:: Definition foo := (nosimpl bar). @@ -3816,7 +3748,7 @@ Note that ``nosimpl bar`` is simply notation for a term that reduces to The ``nosimpl`` trick only works if no reduction is apparent in ``t``; in particular, the declaration: - .. coqtop:: in + .. coqdoc:: Definition foo x := nosimpl (bar x). @@ -3824,14 +3756,14 @@ Note that ``nosimpl bar`` is simply notation for a term that reduces to function, and to use the following definition, which blocks the reduction as expected: - .. coqtop:: in + .. coqdoc:: Definition foo x := nosimpl bar x. A standard example making this technique shine is the case of arithmetic operations. We define for instance: -.. coqtop:: in +.. coqdoc:: Definition addn := nosimpl plus. @@ -3851,7 +3783,7 @@ Congruence Because of the way matching interferes with parameters of type families, the tactic: -.. coqtop:: in +.. coqdoc:: apply: my_congr_property. @@ -3875,7 +3807,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3902,7 +3834,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3925,7 +3857,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3946,7 +3878,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4047,7 +3979,7 @@ For a quick glance at what can be expressed with the last :token:`r_pattern` consider the goal ``a = b`` and the tactic -.. coqtop:: in +.. coqdoc:: rewrite [in X in _ = X]rule. @@ -4126,7 +4058,7 @@ parentheses are required around more complex patterns. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4148,14 +4080,14 @@ patterns over simple terms, but to interpret a pattern with double parentheses as a simple term. For example, the following tactic would capture any occurrence of the term ``a in A``. -.. coqtop:: in +.. coqdoc:: set t := ((a in A)). Contextual patterns can also be used as arguments of the ``:`` tactical. For example: -.. coqtop:: in +.. coqdoc:: elim: n (n in _ = n) (refl_equal n). @@ -4165,7 +4097,7 @@ Contextual patterns in rewrite .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4246,7 +4178,7 @@ context shortcuts. The following example is taken from ``ssreflect.v`` where the ``LHS`` and ``RHS`` shortcuts are defined. -.. coqtop:: in +.. coqdoc:: Notation RHS := (X in _ = X)%pattern. Notation LHS := (X in X = _)%pattern. @@ -4254,7 +4186,7 @@ The following example is taken from ``ssreflect.v`` where the Shortcuts defined this way can be freely used in place of the trailing ``ident in term`` part of any contextual pattern. Some examples follow: -.. coqtop:: in +.. coqdoc:: set rhs := RHS. rewrite [in RHS]rule. @@ -4287,13 +4219,13 @@ The view syntax combined with the ``elim`` tactic specifies an elimination scheme to be used instead of the default, generated, one. Hence the |SSR| tactic: -.. coqtop:: in +.. coqdoc:: elim/V. is a synonym for: -.. coqtop:: in +.. coqdoc:: intro top; elim top using V; clear top. @@ -4303,13 +4235,13 @@ Since an elimination view supports the two bookkeeping tacticals of discharge and introduction (see section :ref:`basic_tactics_ssr`), the |SSR| tactic: -.. coqtop:: in +.. coqdoc:: elim/V: x => y. is a synonym for: -.. coqtop:: in +.. coqdoc:: elim x using V; clear x; intro y. @@ -4329,7 +4261,7 @@ generation (see section :ref:`generation_of_equations_ssr`). The following script illustrates a toy example of this feature. Let us define a function adding an element at the end of a list: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect List. Set Implicit Arguments. @@ -4367,13 +4299,13 @@ command) can be combined with the type family switches described in section :ref:`type_families_ssr`. Consider an eliminator ``foo_ind`` of type: -.. coqtop:: in +.. coqdoc:: foo_ind : forall …, forall x : T, P p1 … pm. and consider the tactic: -.. coqtop:: in +.. coqdoc:: elim/foo_ind: e1 … / en. @@ -4404,7 +4336,7 @@ Here is an example of a regular, but nontrivial, eliminator. Here is a toy example illustrating this feature. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4424,14 +4356,14 @@ Here is an example of a regular, but nontrivial, eliminator. The following tactics are all valid and perform the same elimination on this goal. - .. coqtop:: in + .. coqdoc:: elim/plus_ind: z / (plus _ z). elim/plus_ind: {z}(plus _ z). elim/plus_ind: {z}_. elim/plus_ind: z / _. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4456,7 +4388,7 @@ Here is an example of a regular, but nontrivial, eliminator. ``plus (plus x y) z`` thus instantiating the last ``_`` with ``z``. Note that the tactic: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4473,7 +4405,7 @@ Here is an example of a regular, but nontrivial, eliminator. .. coqtop:: all - elim/plus_ind: y / _. + Fail elim/plus_ind: y / _. triggers an error: in the conclusion of the ``plus_ind`` eliminator, the first argument of the predicate @@ -4486,7 +4418,7 @@ Here is an example of a truncated eliminator: Consider the goal: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4494,7 +4426,7 @@ Here is an example of a truncated eliminator: Unset Printing Implicit Defensive. Section Test. - .. coqtop:: in + .. coqdoc:: Lemma test p n (n_gt0 : 0 < n) (pr_p : prime p) : p %| \prod_(i <- prime_decomp n | i \in prime_decomp n) i.1 ^ i.2 -> @@ -4505,7 +4437,7 @@ Here is an example of a truncated eliminator: where the type of the ``big_prop`` eliminator is - .. coqtop:: in + .. coqdoc:: big_prop: forall (R : Type) (Pb : R -> Type) (idx : R) (op1 : R -> R -> R), Pb idx -> @@ -4518,7 +4450,7 @@ Here is an example of a truncated eliminator: inferred one is used instead: ``big[_/_]_(i <- _ | _ i) _ i``, and after the introductions, the following goals are generated: - .. coqtop:: in + .. coqdoc:: subgoal 1 is: p %| 1 -> exists2 x : nat * nat, x \in prime_decomp n & p = x.1 @@ -4550,7 +4482,7 @@ disjunction. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4571,7 +4503,7 @@ disjunction. This operation is so common that the tactic shell has specific syntax for it. The following scripts: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4584,13 +4516,13 @@ disjunction. Lemma test a : P (a || a) -> True. - .. coqtop:: all undo + .. coqtop:: all move=> HPa; move/P2Q: HPa => HQa. or more directly: - .. coqtop:: all undo + .. coqtop:: all restart move/P2Q=> HQa. @@ -4606,7 +4538,7 @@ equation name generation mechanism (see section :ref:`generation_of_equations_ss .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4624,7 +4556,7 @@ equation name generation mechanism (see section :ref:`generation_of_equations_ss This view tactic performs: - .. coqtop:: in + .. coqdoc:: move=> HQ; case: {HQ}(Q2P HQ) => [HPa | HPb]. @@ -4639,7 +4571,7 @@ relevant for the current goal. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4661,14 +4593,14 @@ relevant for the current goal. the double implication into the expected simple implication. The last script is in fact equivalent to: - .. coqtop:: in + .. coqdoc:: Lemma test a b : P (a || b) -> True. move/(iffLR (PQequiv _ _)). where: - .. coqtop:: in + .. coqdoc:: Lemma iffLR P Q : (P <-> Q) -> P -> Q. @@ -4683,7 +4615,7 @@ assumption to some given arguments. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4712,7 +4644,7 @@ bookkeeping steps. The following example use the ``~~`` prenex notation for boolean negation: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4768,7 +4700,7 @@ analysis: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4785,7 +4717,7 @@ analysis .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4810,7 +4742,7 @@ decidable predicate to its boolean version. First, booleans are injected into propositions using the coercion mechanism: -.. coqtop:: in +.. coqdoc:: Coercion is_true (b : bool) := b = true. @@ -4827,7 +4759,7 @@ To get all the benefits of the boolean reflection, it is in fact convenient to introduce the following inductive predicate ``reflect`` to relate propositions and booleans: -.. coqtop:: in +.. coqdoc:: Inductive reflect (P: Prop): bool -> Type := | Reflect_true : P -> reflect P true @@ -4838,9 +4770,9 @@ logically equivalent propositions. For instance, the following lemma: -.. coqtop:: in +.. coqdoc:: - Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2). + Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2). relates the boolean conjunction to the logical one ``/\``. Note that in ``andP``, ``b1`` and ``b2`` are two boolean variables and the @@ -4853,20 +4785,20 @@ to the case analysis of |Coq|’s inductive types. Since the equivalence predicate is defined in |Coq| as: -.. coqtop:: in +.. coqdoc:: Definition iff (A B:Prop) := (A -> B) /\ (B -> A). where ``/\`` is a notation for ``and``: -.. coqtop:: in +.. coqdoc:: Inductive and (A B:Prop) : Prop := conj : A -> B -> and A B. This make case analysis very different according to the way an equivalence property has been defined. -.. coqtop:: in +.. coqdoc:: Lemma andE (b1 b2 : bool) : (b1 /\ b2) <-> (b1 && b2). @@ -4875,7 +4807,7 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4888,11 +4820,15 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. Lemma test (b1 b2 : bool) : if (b1 && b2) then b1 else ~~(b1||b2). - .. coqtop:: all undo + .. coqtop:: all case: (@andE b1 b2). - .. coqtop:: all undo + .. coqtop:: none + + Restart. + + .. coqtop:: all case: (@andP b1 b2). @@ -4912,7 +4848,7 @@ The view mechanism is compatible with reflect predicates. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4920,17 +4856,13 @@ The view mechanism is compatible with reflect predicates. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. coqtop:: all abort Lemma test (a b : bool) (Ha : a) (Hb : b) : a /\ b. apply/andP. Conversely - .. coqtop:: none - - Abort. - .. coqtop:: all Lemma test (a b : bool) : a /\ b -> a. @@ -4950,13 +4882,13 @@ Specializing assumptions The |SSR| tactic: -.. coqtop:: in +.. coqdoc:: move/(_ term1 … termn). is equivalent to the tactic: -.. coqtop:: in +.. coqdoc:: intro top; generalize (top term1 … termn); clear top. @@ -5013,13 +4945,13 @@ If ``term`` is a double implication, then the view hint will be one of the defined view hints for implication. These hints are by default the ones present in the file ``ssreflect.v``: -.. coqtop:: in +.. coqdoc:: Lemma iffLR : forall P Q, (P <-> Q) -> P -> Q. which transforms a double implication into the left-to-right one, or: -.. coqtop:: in +.. coqdoc:: Lemma iffRL : forall P Q, (P <-> Q) -> Q -> P. @@ -5034,7 +4966,7 @@ but they also allow complex transformation, involving negations. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5067,7 +4999,7 @@ actually uses its propositional interpretation. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5123,13 +5055,13 @@ equality, while the second term is the one applied to the right hand side. In this context, the identity view can be used when no view has to be applied: -.. coqtop:: in +.. coqdoc:: Lemma idP : reflect b1 b1. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5145,7 +5077,7 @@ In this context, the identity view can be used when no view has to be applied: The same goal can be decomposed in several ways, and the user may choose the most convenient interpretation. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5198,7 +5130,7 @@ in sequence. Both move and apply can be followed by an arbitrary number of ``/term``. The main difference between the following two tactics -.. coqtop:: in +.. coqdoc:: apply/v1/v2/v3. apply/v1; apply/v2; apply/v3. @@ -5210,7 +5142,7 @@ line would apply the view ``v2`` to all the goals generated by ``apply/v1``. Note that the NO-OP intro pattern ``-`` can be used to separate two views, making the two following examples equivalent: -.. coqtop:: in +.. coqdoc:: move=> /v1; move=> /v2. move=> /v1 - /v2. @@ -5221,7 +5153,7 @@ pass a given hypothesis to a lemma. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5280,7 +5212,7 @@ equivalences are indeed taken into account, otherwise only single looks for any notation that contains fragment as a substring. If the ``ssrbool.v`` library is imported, the command: ``Search "~~".`` answers : - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 081fef07b9..b5e9a902c6 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -749,39 +749,39 @@ Applying theorems The direct application of ``Rtrans`` with ``apply`` fails because no value for ``y`` in ``Rtrans`` is found by ``apply``: - .. coqtop:: all + .. coqtop:: all fail - Fail apply Rtrans. + apply Rtrans. A solution is to ``apply (Rtrans n m p)`` or ``(Rtrans n m)``. - .. coqtop:: all undo + .. coqtop:: all apply (Rtrans n m p). Note that ``n`` can be inferred from the goal, so the following would work too. - .. coqtop:: in undo + .. coqtop:: in restart apply (Rtrans _ m). More elegantly, ``apply Rtrans with (y:=m)`` allows only mentioning the unknown m: - .. coqtop:: in undo + .. coqtop:: in restart apply Rtrans with (y := m). Another solution is to mention the proof of ``(R x y)`` in ``Rtrans`` - .. coqtop:: all undo + .. coqtop:: all restart apply Rtrans with (1 := Rnm). ... or the proof of ``(R y z)``. - .. coqtop:: all undo + .. coqtop:: all restart apply Rtrans with (2 := Rmp). @@ -789,7 +789,7 @@ Applying theorems finding ``m``. Then one can apply the hypotheses ``Rnm`` and ``Rmp``. This instantiates the existential variable and completes the proof. - .. coqtop:: all + .. coqtop:: all restart abort eapply Rtrans. @@ -2332,6 +2332,7 @@ and an explanation of the underlying technique. where :n:`@ident` is the identifier for the last introduced hypothesis. .. tacv:: inversion_clear @ident + :name: inversion_clear This behaves as :n:`inversion` and then erases :n:`@ident` from the context. @@ -2490,47 +2491,51 @@ and an explanation of the underlying technique. *Non-dependent inversion*. - Let us consider the relation Le over natural numbers and the following - variables: + Let us consider the relation :g:`Le` over natural numbers: - .. coqtop:: all + .. coqtop:: reset in Inductive Le : nat -> nat -> Set := | LeO : forall n:nat, Le 0 n | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Variable P : nat -> nat -> Prop. - Variable Q : forall n m:nat, Le n m -> Prop. + Let us consider the following goal: .. coqtop:: none + Section Section. + Variable P : nat -> nat -> Prop. + Variable Q : forall n m:nat, Le n m -> Prop. Goal forall n m, Le (S n) m -> P n m. - intros. - .. coqtop:: all + .. coqtop:: out - Show. + intros. - To prove the goal, we may need to reason by cases on H and to derive - that m is necessarily of the form (S m 0 ) for certain m 0 and that - (Le n m 0 ). Deriving these conditions corresponds to proving that the - only possible constructor of (Le (S n) m) isLeS and that we can invert - the-> in the type of LeS. This inversion is possible because Le is the - smallest set closed by the constructors LeO and LeS. + To prove the goal, we may need to reason by cases on :g:`H` and to derive + that :g:`m` is necessarily of the form :g:`(S m0)` for certain :g:`m0` and that + :g:`(Le n m0)`. Deriving these conditions corresponds to proving that the only + possible constructor of :g:`(Le (S n) m)` is :g:`LeS` and that we can invert + the arrow in the type of :g:`LeS`. This inversion is possible because :g:`Le` + is the smallest set closed by the constructors :g:`LeO` and :g:`LeS`. - .. coqtop:: undo all + .. coqtop:: all inversion_clear H. - Note that m has been substituted in the goal for (S m0) and that the - hypothesis (Le n m0) has been added to the context. + Note that :g:`m` has been substituted in the goal for :g:`(S m0)` and that the + hypothesis :g:`(Le n m0)` has been added to the context. - Sometimes it is interesting to have the equality m=(S m0) in the - context to use it after. In that case we can use inversion that does + Sometimes it is interesting to have the equality :g:`m = (S m0)` in the + context to use it after. In that case we can use :tacn:`inversion` that does not clear the equalities: - .. coqtop:: undo all + .. coqtop:: none restart + + intros. + + .. coqtop:: all inversion H. @@ -2540,31 +2545,26 @@ and an explanation of the underlying technique. Let us consider the following goal: - .. coqtop:: reset none + .. coqtop:: none - Inductive Le : nat -> nat -> Set := - | LeO : forall n:nat, Le 0 n - | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Variable P : nat -> nat -> Prop. - Variable Q : forall n m:nat, Le n m -> Prop. + Abort. Goal forall n m (H:Le (S n) m), Q (S n) m H. - intros. - .. coqtop:: all + .. coqtop:: out - Show. + intros. - As H occurs in the goal, we may want to reason by cases on its - structure and so, we would like inversion tactics to substitute H by + As :g:`H` occurs in the goal, we may want to reason by cases on its + structure and so, we would like inversion tactics to substitute :g:`H` by the corresponding @term in constructor form. Neither :tacn:`inversion` nor - :n:`inversion_clear` do such a substitution. To have such a behavior we + :tacn:`inversion_clear` do such a substitution. To have such a behavior we use the dependent inversion tactics: .. coqtop:: all dependent inversion_clear H. - Note that H has been substituted by (LeS n m0 l) andm by (S m0). + Note that :g:`H` has been substituted by :g:`(LeS n m0 l)` and :g:`m` by :g:`(S m0)`. .. example:: @@ -2933,6 +2933,12 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. + .. tacv:: now_show @term + + This is a synonym of :n:`change @term`. It can be used to + make some proof steps explicit when refactoring a proof script + to make it readable. + .. seealso:: :ref:`Performing computations <performingcomputations>` .. _performingcomputations: @@ -3315,7 +3321,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. example:: - .. coqtop:: all + .. coqtop:: all abort Goal ~0=0. unfold not. @@ -3323,10 +3329,6 @@ the conversion in hypotheses :n:`{+ @ident}`. pattern (0 = 0). fold not. - .. coqtop:: none - - Abort. - .. tacv:: fold {+ @term} Equivalent to :n:`fold @term ; ... ; fold @term`. @@ -3406,129 +3408,140 @@ Automation This tactic implements a Prolog-like resolution procedure to solve the current goal. It first tries to solve the goal using the :tacn:`assumption` - tactic, then it reduces the goal to an atomic one using intros and + tactic, then it reduces the goal to an atomic one using :tacn:`intros` and introduces the newly generated hypotheses as hints. Then it looks at the list of tactics associated to the head symbol of the goal and tries to apply one of them (starting from the tactics with lower cost). This process is recursively applied to the generated subgoals. - By default, auto only uses the hypotheses of the current goal and the - hints of the database named core. + By default, :tacn:`auto` only uses the hypotheses of the current goal and + the hints of the database named ``core``. + + .. warning:: -.. tacv:: auto @num + :tacn:`auto` uses a weaker version of :tacn:`apply` that is closer to + :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will + fail even if applying manually one of the hints would succeed. - Forces the search depth to be :token:`num`. The maximal search depth - is 5 by default. + .. tacv:: auto @num -.. tacv:: auto with {+ @ident} + Forces the search depth to be :token:`num`. The maximal search depth + is 5 by default. - Uses the hint databases :n:`{+ @ident}` in addition to the database core. + .. tacv:: auto with {+ @ident} + + Uses the hint databases :n:`{+ @ident}` in addition to the database ``core``. + + .. note:: + + Use the fake database `nocore` if you want to *not* use the `core` + database. + + .. tacv:: auto with * + + Uses all existing hint databases. Using this variant is highly discouraged + in finished scripts since it is both slower and less robust than the variant + where the required databases are explicitly listed. .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of pre-defined databases and the way to create or extend a database. -.. tacv:: auto with * + .. tacv:: auto using {+ @ident__i} {? with {+ @ident } } - Uses all existing hint databases. + Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an + inductive type, it is the collection of its constructors which are added + as hints. - .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + .. note:: -.. tacv:: auto using {+ @ident__i} {? with {+ @ident } } + The hints passed through the `using` clause are used in the same + way as if they were passed through a hint database. Consequently, + they use a weaker version of :tacn:`apply` and :n:`auto using @ident` + may fail where :n:`apply @ident` succeeds. - Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an - inductive type, it is the collection of its constructors which are added - as hints. + Given that this can be seen as counter-intuitive, it could be useful + to have an option to use full-blown :tacn:`apply` for lemmas passed + through the `using` clause. Contributions welcome! -.. tacv:: info_auto + .. tacv:: info_auto - Behaves like auto but shows the tactics it uses to solve the goal. This - variant is very useful for getting a better understanding of automation, or - to know what lemmas/assumptions were used. + Behaves like :tacn:`auto` but shows the tactics it uses to solve the goal. This + variant is very useful for getting a better understanding of automation, or + to know what lemmas/assumptions were used. -.. tacv:: debug auto - :name: debug auto + .. tacv:: debug auto + :name: debug auto - Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, - including failing paths. + Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, + including failing paths. -.. tacv:: {? info_}auto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}auto {? @num} {? using {+ @lemma}} {? with {+ @ident}} - This is the most general form, combining the various options. + This is the most general form, combining the various options. .. tacv:: trivial :name: trivial - This tactic is a restriction of auto that is not recursive + This tactic is a restriction of :tacn:`auto` that is not recursive and tries only hints that cost `0`. Typically it solves trivial equalities like :g:`X=X`. -.. tacv:: trivial with {+ @ident} - :undocumented: - -.. tacv:: trivial with * - :undocumented: - -.. tacv:: trivial using {+ @lemma} - :undocumented: - -.. tacv:: debug trivial - :name: debug trivial - :undocumented: - -.. tacv:: info_trivial - :name: info_trivial - :undocumented: - -.. tacv:: {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} - :undocumented: + .. tacv:: trivial with {+ @ident} + trivial with * + trivial using {+ @lemma} + debug trivial + info_trivial + {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} + :name: _; _; _; debug trivial; info_trivial; _ + :undocumented: .. note:: - :tacn:`auto` either solves completely the goal or else leaves it - intact. :tacn:`auto` and :tacn:`trivial` never fail. - -The following options enable printing of informative or debug information for -the :tacn:`auto` and :tacn:`trivial` tactics: + :tacn:`auto` and :tacn:`trivial` either solve completely the goal or + else succeed without changing the goal. Use :g:`solve [ auto ]` and + :g:`solve [ trivial ]` if you would prefer these tactics to fail when + they do not manage to solve the goal. .. flag:: Info Auto Debug Auto Info Trivial Debug Trivial - :undocumented: -.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + These options enable printing of informative or debug information for + the :tacn:`auto` and :tacn:`trivial` tactics. .. tacn:: eauto :name: eauto This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try resolution hints which would leave existential variables in the goal, - :tacn:`eauto` does try them (informally speaking, it usessimple :tacn:`eapply` - where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto` + :tacn:`eauto` does try them (informally speaking, it internally uses a tactic + close to :tacn:`simple eapply` instead of a tactic close to :tacn:`simple apply` + in the case of :tacn:`auto`). As a consequence, :tacn:`eauto` can solve such a goal: .. example:: .. coqtop:: all - Hint Resolve ex_intro. + Hint Resolve ex_intro : core. Goal forall P:nat -> Prop, P 0 -> exists n, P n. eauto. Note that ``ex_intro`` should be declared as a hint. -.. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} - The various options for :tacn:`eauto` are the same as for :tacn:`auto`. + The various options for :tacn:`eauto` are the same as for :tacn:`auto`. -:tacn:`eauto` also obeys the following options: + :tacn:`eauto` also obeys the following options: -.. flag:: Info Eauto - Debug Eauto - :undocumented: + .. flag:: Info Eauto + Debug Eauto + :undocumented: -.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` .. tacn:: autounfold with {+ @ident} |