diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/detailed-tactic-examples.rst | 824 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 199 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 93 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 197 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 1309 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 234 |
6 files changed, 1339 insertions, 1517 deletions
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 84810ddba5..bd16b70d02 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -21,11 +21,11 @@ applied to the abstracted instance and after simplification of the equalities we get the expected goals. The abstracting tactic is called generalize_eqs and it takes as -argument an hypothesis to generalize. It uses the JMeq datatype +argument a hypothesis to generalize. It uses the JMeq datatype defined in Coq.Logic.JMeq, hence we need to require it before. For example, revisiting the first example of the inversion documentation: -.. coqtop:: in +.. coqtop:: in reset Require Import Coq.Logic.JMeq. @@ -63,6 +63,10 @@ to use an heterogeneous equality to relate the new hypothesis to the old one (which just disappeared here). However, the tactic works just as well in this case, e.g.: +.. coqtop:: none + + Abort. + .. coqtop:: in Variable Q : forall (n m : nat), Le n m -> Prop. @@ -80,7 +84,7 @@ to recover the needed equalities. Also, some subgoals should be directly solved because of inconsistent contexts arising from the constraints on indexes. The nice thing is that we can make a tactic based on discriminate, injection and variants of substitution to -automatically do such simplifications (which may involve the K axiom). +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: @@ -101,9 +105,9 @@ 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:: in +.. coqtop:: none - Require Import Coq.Program.Equality. + Abort. .. coqtop:: in @@ -122,9 +126,9 @@ 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:: in +.. coqtop:: none - Require Import Coq.Program.Equality. + Abort. .. coqtop:: in @@ -167,7 +171,7 @@ predicates on a real example. We will develop an example application to the theory of simply-typed lambda-calculus formalized in a dependently-typed style: -.. coqtop:: in +.. coqtop:: in reset Inductive type : Type := | base : type @@ -226,11 +230,15 @@ name. A term is either an application of: Once we have this datatype we want to do proofs on it, like weakening: -.. coqtop:: in undo +.. coqtop:: in 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: @@ -241,6 +249,10 @@ in the instance. A solution would be to rewrite the goal as: 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 @@ -252,6 +264,7 @@ back automatically. Indeed we can simply write: .. coqtop:: in Require Import Coq.Program.Tactics. + Require Import Coq.Program.Equality. .. coqtop:: in @@ -308,17 +321,14 @@ it can be used directly. apply weak, IHterm. -If there is an easy first-order solution to these equations as in this -subgoal, the ``specialize_eqs`` tactic can be used instead of giving -explicit proof terms: - -.. coqtop:: all +Now concluding this subgoal is easy. - specialize_eqs IHterm. +.. coqtop:: in -This concludes our example. + constructor; apply IHterm; reflexivity. -See also: The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics. +.. seealso:: + The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics. autorewrite @@ -331,301 +341,97 @@ involves conditional rewritings and shows how to deal with them using the optional tactic of the ``Hint Rewrite`` command. -Example 1: Ackermann function - -.. coqtop:: in - - Reset Initial. - -.. coqtop:: in - - Require Import Arith. - -.. coqtop:: in - - Variable Ack : nat -> nat -> nat. - -.. coqtop:: in - - Axiom Ack0 : forall m:nat, Ack 0 m = S m. - Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1. - Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m). - -.. coqtop:: in - - Hint Rewrite Ack0 Ack1 Ack2 : base0. - -.. coqtop:: all - - Lemma ResAck0 : Ack 3 2 = 29. - -.. coqtop:: all - - autorewrite with base0 using try reflexivity. - -Example 2: Mac Carthy function - -.. coqtop:: in - - Require Import Omega. - -.. coqtop:: in - - Variable g : nat -> nat -> nat. - -.. coqtop:: in - - Axiom g0 : forall m:nat, g 0 m = m. - Axiom g1 : forall n m:nat, (n > 0) -> (m > 100) -> g n m = g (pred n) (m - 10). - Axiom g2 : forall n m:nat, (n > 0) -> (m <= 100) -> g n m = g (S n) (m + 11). - - -.. coqtop:: in - - Hint Rewrite g0 g1 g2 using omega : base1. - -.. coqtop:: in - - Lemma Resg0 : g 1 110 = 100. - -.. coqtop:: out - - Show. - -.. coqtop:: all - - autorewrite with base1 using reflexivity || simpl. - -.. coqtop:: all - - Lemma Resg1 : g 1 95 = 91. - -.. coqtop:: all - - autorewrite with base1 using reflexivity || simpl. - - -.. _quote: - -quote ------ - -The tactic ``quote`` allows using Barendregt’s so-called 2-level approach -without writing any ML code. Suppose you have a language ``L`` of -'abstract terms' and a type ``A`` of 'concrete terms' and a function ``f : L -> A``. -If ``L`` is a simple inductive datatype and ``f`` a simple fixpoint, -``quote f`` will replace the head of current goal by a convertible term of -the form ``(f t)``. ``L`` must have a constructor of type: ``A -> L``. +.. example:: Ackermann function -Here is an example: + .. coqtop:: in reset -.. coqtop:: in - - Require Import Quote. - -.. coqtop:: all - - Parameters A B C : Prop. - -.. coqtop:: all - - Inductive formula : Type := - | f_and : formula -> formula -> formula (* binary constructor *) - | f_or : formula -> formula -> formula - | f_not : formula -> formula (* unary constructor *) - | f_true : formula (* 0-ary constructor *) - | f_const : Prop -> formula (* constructor for constants *). - -.. coqtop:: all - - Fixpoint interp_f (f:formula) : Prop := - match f with - | f_and f1 f2 => interp_f f1 /\ interp_f f2 - | f_or f1 f2 => interp_f f1 \/ interp_f f2 - | f_not f1 => ~ interp_f f1 - | f_true => True - | f_const c => c - end. - -.. coqtop:: all + Require Import Arith. - Goal A /\ (A \/ True) /\ ~ B /\ (A <-> A). + .. coqtop:: in -.. coqtop:: all + Variable Ack : nat -> nat -> nat. - quote interp_f. + .. coqtop:: in -The algorithm to perform this inversion is: try to match the term with -right-hand sides expression of ``f``. If there is a match, apply the -corresponding left-hand side and call yourself recursively on sub- -terms. If there is no match, we are at a leaf: return the -corresponding constructor (here ``f_const``) applied to the term. + Axiom Ack0 : forall m:nat, Ack 0 m = S m. + Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1. + Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m). + .. coqtop:: in -Error messages: + Hint Rewrite Ack0 Ack1 Ack2 : base0. + .. coqtop:: all -#. quote: not a simple fixpoint + Lemma ResAck0 : Ack 3 2 = 29. - Happens when ``quote`` is not able to perform inversion properly. + .. coqtop:: all + autorewrite with base0 using try reflexivity. +.. example:: MacCarthy function -Introducing variables map -~~~~~~~~~~~~~~~~~~~~~~~~~ + .. coqtop:: in reset -The normal use of quote is to make proofs by reflection: one defines a -function ``simplify : formula -> formula`` and proves a theorem -``simplify_ok: (f:formula)(interp_f (simplify f)) -> (interp_f f)``. Then, -one can simplify formulas by doing: + Require Import Omega. -.. coqtop:: in + .. coqtop:: in - quote interp_f. - apply simplify_ok. - compute. + Variable g : nat -> nat -> nat. -But there is a problem with leafs: in the example above one cannot -write a function that implements, for example, the logical -simplifications :math:`A \wedge A \rightarrow A` or :math:`A \wedge -\lnot A \rightarrow \mathrm{False}`. This is because ``Prop`` is -impredicative. + .. coqtop:: in -It is better to use that type of formulas: + Axiom g0 : forall m:nat, g 0 m = m. + Axiom g1 : forall n m:nat, (n > 0) -> (m > 100) -> g n m = g (pred n) (m - 10). + Axiom g2 : forall n m:nat, (n > 0) -> (m <= 100) -> g n m = g (S n) (m + 11). -.. coqtop:: in reset + .. coqtop:: in - Require Import Quote. + Hint Rewrite g0 g1 g2 using omega : base1. -.. coqtop:: in + .. coqtop:: in - Parameters A B C : Prop. + Lemma Resg0 : g 1 110 = 100. -.. coqtop:: all + .. coqtop:: out - Inductive formula : Set := - | f_and : formula -> formula -> formula - | f_or : formula -> formula -> formula - | f_not : formula -> formula - | f_true : formula - | f_atom : index -> formula. + Show. -``index`` is defined in module ``Quote``. Equality on that type is -decidable so we are able to simplify :math:`A \wedge A` into :math:`A` -at the abstract level. + .. coqtop:: all -When there are variables, there are bindings, and ``quote`` also -provides a type ``(varmap A)`` of bindings from index to any set -``A``, and a function ``varmap_find`` to search in such maps. The -interpretation function also has another argument, a variables map: + autorewrite with base1 using reflexivity || simpl. -.. coqtop:: all + .. coqtop:: none - Fixpoint interp_f (vm:varmap Prop) (f:formula) {struct f} : Prop := - match f with - | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2 - | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2 - | f_not f1 => ~ interp_f vm f1 - | f_true => True - | f_atom i => varmap_find True i vm - end. - -``quote`` handles this second case properly: - -.. coqtop:: all + Qed. - Goal A /\ (B \/ A) /\ (A \/ ~ B). + .. coqtop:: all -.. coqtop:: all + Lemma Resg1 : g 1 95 = 91. - quote interp_f. + .. coqtop:: all -It builds ``vm`` and ``t`` such that ``(f vm t)`` is convertible with the -conclusion of current goal. + autorewrite with base1 using reflexivity || simpl. + .. coqtop:: none -Combining variables and constants -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Qed. -One can have both variables and constants in abstracts terms; for -example, this is the case for the :tacn:`ring` tactic. Then one must provide to -``quote`` a list of *constructors of constants*. For example, if the list -is ``[O S]`` then closed natural numbers will be considered as constants -and other terms as variables. - -Example: - -.. coqtop:: in - - Inductive formula : Type := - | f_and : formula -> formula -> formula - | f_or : formula -> formula -> formula - | f_not : formula -> formula - | f_true : formula - | f_const : Prop -> formula (* constructor for constants *) - | f_atom : index -> formula. - -.. coqtop:: in - - Fixpoint interp_f (vm:varmap Prop) (f:formula) {struct f} : Prop := - match f with - | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2 - | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2 - | f_not f1 => ~ interp_f vm f1 - | f_true => True - | f_const c => c - | f_atom i => varmap_find True i vm - end. - -.. coqtop:: in - - Goal A /\ (A \/ True) /\ ~ B /\ (C <-> C). - -.. coqtop:: all - - quote interp_f [ A B ]. - - -.. coqtop:: all - - Undo. - -.. coqtop:: all - - quote interp_f [ B C iff ]. - -Warning: Since function inversion is undecidable in general case, -don’t expect miracles from it! - -.. tacv:: quote @ident in @term using @tactic - - ``tactic`` must be a functional tactic (starting with ``fun x =>``) and - will be called with the quoted version of term according to ``ident``. - -.. tacv:: quote @ident [{+ @ident}] in @term using @tactic - - Same as above, but will use the additional ``ident`` list to chose - which subterms are constants (see above). - -See also: comments of source file ``plugins/quote/quote.ml`` - -See also: the :tacn:`ring` tactic. - - -Using the tactical language ---------------------------- +Using the tactic language +------------------------- About the cardinality of the set of natural numbers ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A first example which shows how to use pattern matching over the -proof contexts is the proof that natural numbers have more than two -elements. The proof of such a lemma can be done as follows: +The first example which shows how to use pattern matching over the +proof context is a proof of the fact that natural numbers have more +than two elements. This can be done as follows: -.. coqtop:: in +.. coqtop:: in reset - Lemma card_nat : ~ (exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z). + Lemma card_nat : + ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z. Proof. .. coqtop:: in @@ -637,8 +443,8 @@ elements. The proof of such a lemma can be done as follows: elim (Hy 0); elim (Hy 1); elim (Hy 2); intros; match goal with - | [_:(?a = ?b),_:(?a = ?c) |- _ ] => - cut (b = c); [ discriminate | transitivity a; auto ] + | _ : ?a = ?b, _ : ?a = ?c |- _ => + cut (b = c); [ discriminate | transitivity a; auto ] end. .. coqtop:: in @@ -651,16 +457,14 @@ solved by a match goal structure and, in particular, with only one pattern (use of non-linear matching). -Permutation on closed lists +Permutations of lists ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Another more complex example is the problem of permutation on closed -lists. The aim is to show that a closed list is a permutation of -another one. - -First, we define the permutation predicate as shown here: +A more complex example is the problem of permutations of +lists. The aim is to show that a list is a permutation of +another list. -.. coqtop:: in +.. coqtop:: in reset Section Sort. @@ -670,205 +474,179 @@ First, we define the permutation predicate as shown here: .. coqtop:: in - Inductive permut : list A -> list A -> Prop := - | permut_refl : forall l, permut l l - | permut_cons : forall a l0 l1, permut l0 l1 -> permut (a :: l0) (a :: l1) - | permut_append : forall a l, permut (a :: l) (l ++ a :: nil) - | permut_trans : forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2. + Inductive perm : list A -> list A -> Prop := + | perm_refl : forall l, perm l l + | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1) + | perm_append : forall a l, perm (a :: l) (l ++ a :: nil) + | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2. .. coqtop:: in End Sort. -A more complex example is the problem of permutation on closed lists. -The aim is to show that a closed list is a permutation of another one. First, we define the permutation predicate as shown above. - .. coqtop:: none Require Import List. -.. coqtop:: all - - Ltac Permut n := - match goal with - | |- (permut _ ?l ?l) => apply permut_refl - | |- (permut _ (?a :: ?l1) (?a :: ?l2)) => - let newn := eval compute in (length l1) in - (apply permut_cons; Permut newn) - | |- (permut ?A (?a :: ?l1) ?l2) => - match eval compute in n with - | 1 => fail - | _ => - let l1' := constr:(l1 ++ a :: nil) in - (apply (permut_trans A (a :: l1) l1' l2); - [ apply permut_append | compute; Permut (pred n) ]) - end - end. - - -.. coqtop:: all - - Ltac PermutProve := - match goal with - | |- (permut _ ?l1 ?l2) => - match eval compute in (length l1 = length l2) with - | (?n = ?n) => Permut n - end - end. - -Next, we can write naturally the tactic and the result can be seen -above. We can notice that we use two top level definitions -``PermutProve`` and ``Permut``. The function to be called is -``PermutProve`` which computes the lengths of the two lists and calls -``Permut`` with the length if the two lists have the same -length. ``Permut`` works as expected. If the two lists are equal, it -concludes. Otherwise, if the lists have identical first elements, it -applies ``Permut`` on the tail of the lists. Finally, if the lists -have different first elements, it puts the first element of one of the -lists (here the second one which appears in the permut predicate) at -the end if that is possible, i.e., if the new first element has been -at this place previously. To verify that all rotations have been done -for a list, we use the length of the list as an argument for Permut -and this length is decremented for each rotation down to, but not -including, 1 because for a list of length ``n``, we can make exactly -``n−1`` rotations to generate at most ``n`` distinct lists. Here, it -must be noticed that we use the natural numbers of Coq for the -rotation counter. In :ref:`ltac-syntax`, we can -see that it is possible to use usual natural numbers but they are only -used as arguments for primitive tactics and they cannot be handled, in -particular, we cannot make computations with them. So, a natural -choice is to use Coq data structures so that Coq makes the -computations (reductions) by eval compute in and we can get the terms -back by match. - -With ``PermutProve``, we can now prove lemmas as follows: - .. coqtop:: in - Lemma permut_ex1 : permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). + Ltac perm_aux n := + match goal with + | |- (perm _ ?l ?l) => apply perm_refl + | |- (perm _ (?a :: ?l1) (?a :: ?l2)) => + let newn := eval compute in (length l1) in + (apply perm_cons; perm_aux newn) + | |- (perm ?A (?a :: ?l1) ?l2) => + match eval compute in n with + | 1 => fail + | _ => + let l1' := constr:(l1 ++ a :: nil) in + (apply (perm_trans A (a :: l1) l1' l2); + [ apply perm_append | compute; perm_aux (pred n) ]) + end + end. -.. coqtop:: in +Next we define an auxiliary tactic ``perm_aux`` which takes an argument +used to control the recursion depth. This tactic behaves as follows. If +the lists are identical (i.e. convertible), it concludes. Otherwise, if +the lists have identical heads, it proceeds to look at their tails. +Finally, if the lists have different heads, it rotates the first list by +putting its head at the end if the new head hasn't been the head previously. To check this, we keep track of the +number of performed rotations using the argument ``n``. We do this by +decrementing ``n`` each time we perform a rotation. It works because +for a list of length ``n`` we can make exactly ``n - 1`` rotations +to generate at most ``n`` distinct lists. Notice that we use the natural +numbers of Coq for the rotation counter. From :ref:`ltac-syntax` we know +that it is possible to use the usual natural numbers, but they are only +used as arguments for primitive tactics and they cannot be handled, so, +in particular, we cannot make computations with them. Thus the natural +choice is to use Coq data structures so that Coq makes the computations +(reductions) by ``eval compute in`` and we can get the terms back by match. + +.. coqtop:: in + + Ltac solve_perm := + match goal with + | |- (perm _ ?l1 ?l2) => + match eval compute in (length l1 = length l2) with + | (?n = ?n) => perm_aux n + end + end. - Proof. PermutProve. Qed. +The main tactic is ``solve_perm``. It computes the lengths of the two lists +and uses them as arguments to call ``perm_aux`` if the lengths are equal (if they +aren't, the lists cannot be permutations of each other). Using this tactic we +can now prove lemmas as follows: .. coqtop:: in - Lemma permut_ex2 : permut nat - (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) - (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). - - Proof. PermutProve. Qed. + Lemma solve_perm_ex1 : + perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). + Proof. solve_perm. Qed. +.. coqtop:: in + Lemma solve_perm_ex2 : + perm nat + (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) + (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). + Proof. solve_perm. Qed. Deciding intuitionistic propositional logic ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. _decidingintuitionistic1: +Pattern matching on goals allows a powerful backtracking when returning tactic +values. An interesting application is the problem of deciding intuitionistic +propositional logic. Considering the contraction-free sequent calculi LJT* of +Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the +tactic language as shown below. -.. coqtop:: all - - Ltac Axioms := - match goal with - | |- True => trivial - | _:False |- _ => elimtype False; assumption - | _:?A |- ?A => auto - end. - -.. _decidingintuitionistic2: - -.. coqtop:: all - - Ltac DSimplif := - repeat - (intros; - match goal with - | id:(~ _) |- _ => red in id - | id:(_ /\ _) |- _ => - elim id; do 2 intro; clear id - | id:(_ \/ _) |- _ => - elim id; intro; clear id - | id:(?A /\ ?B -> ?C) |- _ => - cut (A -> B -> C); - [ intro | intros; apply id; split; assumption ] - | id:(?A \/ ?B -> ?C) |- _ => - cut (B -> C); - [ cut (A -> C); - [ intros; clear id - | intro; apply id; left; assumption ] - | intro; apply id; right; assumption ] - | id0:(?A -> ?B),id1:?A |- _ => - cut B; [ intro; clear id0 | apply id0; assumption ] - | |- (_ /\ _) => split - | |- (~ _) => red - end). - -.. coqtop:: all - - Ltac TautoProp := - DSimplif; - Axioms || - match goal with - | id:((?A -> ?B) -> ?C) |- _ => - cut (B -> C); - [ intro; cut (A -> B); - [ intro; cut C; - [ intro; clear id | apply id; assumption ] - | clear id ] - | intro; apply id; intro; assumption ]; TautoProp - | id:(~ ?A -> ?B) |- _ => - cut (False -> B); - [ intro; cut (A -> False); - [ intro; cut B; - [ intro; clear id | apply id; assumption ] - | clear id ] - | intro; apply id; red; intro; assumption ]; TautoProp - | |- (_ \/ _) => (left; TautoProp) || (right; TautoProp) - end. - -The pattern matching on goals allows a complete and so a powerful -backtracking when returning tactic values. An interesting application -is the problem of deciding intuitionistic propositional logic. -Considering the contraction-free sequent calculi LJT* of Roy Dyckhoff -:cite:`Dyc92`, it is quite natural to code such a tactic -using the tactic language as shown on figures: :ref:`Deciding -intuitionistic propositions (1) <decidingintuitionistic1>` and -:ref:`Deciding intuitionistic propositions (2) -<decidingintuitionistic2>`. The tactic ``Axioms`` tries to conclude -using usual axioms. The tactic ``DSimplif`` applies all the reversible -rules of Dyckhoff’s system. Finally, the tactic ``TautoProp`` (the -main tactic to be called) simplifies with ``DSimplif``, tries to -conclude with ``Axioms`` and tries several paths using the -backtracking rules (one of the four Dyckhoff’s rules for the left -implication to get rid of the contraction and the right or). - -For example, with ``TautoProp``, we can prove tautologies like those: - -.. coqtop:: in - - Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B. - -.. coqtop:: in - - Proof. TautoProp. Qed. - -.. coqtop:: in +.. coqtop:: in reset - Lemma tauto_ex2 : - forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. + Ltac basic := + match goal with + | |- True => trivial + | _ : False |- _ => contradiction + | _ : ?A |- ?A => assumption + end. .. coqtop:: in - Proof. TautoProp. Qed. + Ltac simplify := + repeat (intros; + match goal with + | H : ~ _ |- _ => red in H + | H : _ /\ _ |- _ => + elim H; do 2 intro; clear H + | H : _ \/ _ |- _ => + elim H; intro; clear H + | H : ?A /\ ?B -> ?C |- _ => + cut (A -> B -> C); + [ intro | intros; apply H; split; assumption ] + | H: ?A \/ ?B -> ?C |- _ => + cut (B -> C); + [ cut (A -> C); + [ intros; clear H + | intro; apply H; left; assumption ] + | intro; apply H; right; assumption ] + | H0 : ?A -> ?B, H1 : ?A |- _ => + cut B; [ intro; clear H0 | apply H0; assumption ] + | |- _ /\ _ => split + | |- ~ _ => red + end). + +.. coqtop:: in + + Ltac my_tauto := + simplify; basic || + match goal with + | H : (?A -> ?B) -> ?C |- _ => + cut (B -> C); + [ intro; cut (A -> B); + [ intro; cut C; + [ intro; clear H | apply H; assumption ] + | clear H ] + | intro; apply H; intro; assumption ]; my_tauto + | H : ~ ?A -> ?B |- _ => + cut (False -> B); + [ intro; cut (A -> False); + [ intro; cut B; + [ intro; clear H | apply H; assumption ] + | clear H ] + | intro; apply H; red; intro; assumption ]; my_tauto + | |- _ \/ _ => (left; my_tauto) || (right; my_tauto) + end. + +The tactic ``basic`` tries to reason using simple rules involving truth, falsity +and available assumptions. The tactic ``simplify`` applies all the reversible +rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main +tactic to be called) simplifies with ``simplify``, tries to conclude with +``basic`` and tries several paths using the backtracking rules (one of the +four Dyckhoff’s rules for the left implication to get rid of the contraction +and the right ``or``). + +Having defined ``my_tauto``, we can prove tautologies like these: + +.. coqtop:: in + + Lemma my_tauto_ex1 : + forall A B : Prop, A /\ B -> A \/ B. + Proof. my_tauto. Qed. + +.. coqtop:: in + + Lemma my_tauto_ex2 : + forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. + Proof. my_tauto. Qed. Deciding type isomorphisms ~~~~~~~~~~~~~~~~~~~~~~~~~~ -A more tricky problem is to decide equalities between types and modulo +A more tricky problem is to decide equalities between types modulo isomorphisms. Here, we choose to use the isomorphisms of the simply typed λ-calculus with Cartesian product and unit type (see, for example, :cite:`RC95`). The axioms of this λ-calculus are given below. @@ -915,112 +693,104 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below. End Iso_axioms. +.. coqtop:: in + Ltac simplify_type ty := + match ty with + | ?A * ?B * ?C => + rewrite <- (Ass A B C); try simplify_type_eq + | ?A * ?B -> ?C => + rewrite (Cur A B C); try simplify_type_eq + | ?A -> ?B * ?C => + rewrite (Dis A B C); try simplify_type_eq + | ?A * unit => + rewrite (P_unit A); try simplify_type_eq + | unit * ?B => + rewrite (Com unit B); try simplify_type_eq + | ?A -> unit => + rewrite (AR_unit A); try simplify_type_eq + | unit -> ?B => + rewrite (AL_unit B); try simplify_type_eq + | ?A * ?B => + (simplify_type A; try simplify_type_eq) || + (simplify_type B; try simplify_type_eq) + | ?A -> ?B => + (simplify_type A; try simplify_type_eq) || + (simplify_type B; try simplify_type_eq) + end + with simplify_type_eq := + match goal with + | |- ?A = ?B => try simplify_type A; try simplify_type B + end. -.. _typeisomorphism1: - -.. coqtop:: all - - Ltac DSimplif trm := - match trm with - | (?A * ?B * ?C) => - rewrite <- (Ass A B C); try MainSimplif - | (?A * ?B -> ?C) => - rewrite (Cur A B C); try MainSimplif - | (?A -> ?B * ?C) => - rewrite (Dis A B C); try MainSimplif - | (?A * unit) => - rewrite (P_unit A); try MainSimplif - | (unit * ?B) => - rewrite (Com unit B); try MainSimplif - | (?A -> unit) => - rewrite (AR_unit A); try MainSimplif - | (unit -> ?B) => - rewrite (AL_unit B); try MainSimplif - | (?A * ?B) => - (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif) - | (?A -> ?B) => - (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif) - end - with MainSimplif := - match goal with - | |- (?A = ?B) => try DSimplif A; try DSimplif B - end. - -.. coqtop:: all +.. coqtop:: in - Ltac Length trm := - match trm with - | (_ * ?B) => let succ := Length B in constr:(S succ) - | _ => constr:(1) - end. + Ltac len trm := + match trm with + | _ * ?B => let succ := len B in constr:(S succ) + | _ => constr:(1) + end. -.. coqtop:: all +.. coqtop:: in Ltac assoc := repeat rewrite <- Ass. +.. coqtop:: in -.. _typeisomorphism2: - -.. coqtop:: all - - Ltac DoCompare n := - match goal with - | [ |- (?A = ?A) ] => reflexivity - | [ |- (?A * ?B = ?A * ?C) ] => - apply Cons; let newn := Length B in - DoCompare newn - | [ |- (?A * ?B = ?C) ] => - match eval compute in n with - | 1 => fail - | _ => - pattern (A * B) at 1; rewrite Com; assoc; DoCompare (pred n) - end - end. - -.. coqtop:: all + Ltac solve_type_eq n := + match goal with + | |- ?A = ?A => reflexivity + | |- ?A * ?B = ?A * ?C => + apply Cons; let newn := len B in solve_type_eq newn + | |- ?A * ?B = ?C => + match eval compute in n with + | 1 => fail + | _ => + pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n) + end + end. - Ltac CompareStruct := - match goal with - | [ |- (?A = ?B) ] => - let l1 := Length A - with l2 := Length B in - match eval compute in (l1 = l2) with - | (?n = ?n) => DoCompare n - end - end. +.. coqtop:: in -.. coqtop:: all + Ltac compare_structure := + match goal with + | |- ?A = ?B => + let l1 := len A + with l2 := len B in + match eval compute in (l1 = l2) with + | ?n = ?n => solve_type_eq n + end + end. - Ltac IsoProve := MainSimplif; CompareStruct. +.. coqtop:: in + Ltac solve_iso := simplify_type_eq; compare_structure. -The tactic to judge equalities modulo this axiomatization can be -written as shown on these figures: :ref:`type isomorphism tactic (1) -<typeisomorphism1>` and :ref:`type isomorphism tactic (2) -<typeisomorphism2>`. The algorithm is quite simple. Types are reduced -using axioms that can be oriented (this done by ``MainSimplif``). The -normal forms are sequences of Cartesian products without Cartesian -product in the left component. These normal forms are then compared -modulo permutation of the components (this is done by -``CompareStruct``). The main tactic to be called and realizing this -algorithm isIsoProve. +The tactic to judge equalities modulo this axiomatization is shown above. +The algorithm is quite simple. First types are simplified using axioms that +can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``). +The normal forms are sequences of Cartesian products without Cartesian product +in the left component. These normal forms are then compared modulo permutation +of the components by the tactic ``compare_structure``. If they have the same +lengths, the tactic ``solve_type_eq`` attempts to prove that the types are equal. +The main tactic that puts all these components together is called ``solve_iso``. -Here are examples of what can be solved by ``IsoProve``. +Here are examples of what can be solved by ``solve_iso``. .. coqtop:: in - Lemma isos_ex1 : - forall A B:Set, A * unit * B = B * (unit * A). + Lemma solve_iso_ex1 : + forall A B : Set, A * unit * B = B * (unit * A). Proof. - intros; IsoProve. + intros; solve_iso. Qed. .. coqtop:: in - Lemma isos_ex2 : - forall A B C:Set, - (A * unit -> B * (C * unit)) = (A * unit -> (C -> unit) * C) * (unit -> A -> B). + Lemma solve_iso_ex2 : + forall A B C : Set, + (A * unit -> B * (C * unit)) = + (A * unit -> (C -> unit) * C) * (unit -> A -> B). Proof. - intros; IsoProve. + intros; solve_iso. Qed. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 278a4ff012..edd83b7cee 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _ltac: The tactic language @@ -10,8 +7,8 @@ This chapter gives a compact documentation of |Ltac|, the tactic language available in |Coq|. We start by giving the syntax, and next, we present the informal semantics. If you want to know more regarding this language and especially about its foundations, you can refer to :cite:`Del00`. Chapter -:ref:`detailedexamplesoftactics` is devoted to giving examples of use of this -language on small but also with non-trivial problems. +:ref:`detailedexamplesoftactics` is devoted to giving small but nontrivial +use examples of this language. .. _ltac-syntax: @@ -27,14 +24,14 @@ represent respectively the natural and integer numbers, the authorized identificators and qualified names, Coq terms and patterns and all the atomic tactics described in Chapter :ref:`tactics`. The syntax of :token:`cpattern` is the same as that of terms, but it is extended with pattern matching -metavariables. In :token:`cpattern`, a pattern-matching metavariable is +metavariables. In :token:`cpattern`, a pattern matching metavariable is represented with the syntax :g:`?id` where :g:`id` is an :token:`ident`. The notation :g:`_` can also be used to denote metavariable whose instance is irrelevant. In the notation :g:`?id`, the identifier allows us to keep instantiations and to make constraints whereas :g:`_` shows that we are not -interested in what will be matched. On the right hand side of pattern-matching -clauses, the named metavariable are used without the question mark prefix. There -is also a special notation for second-order pattern-matching problems: in an +interested in what will be matched. On the right hand side of pattern matching +clauses, the named metavariables are used without the question mark prefix. There +is also a special notation for second-order pattern matching problems: in an applicative pattern of the form :g:`@?id id1 … idn`, the variable id matches any complex expression with (possible) dependencies in the variables :g:`id1 … idn` and returns a functional term of the form :g:`fun id1 … idn => term`. @@ -107,7 +104,7 @@ mode but it can also be used in toplevel definitions as shown below. : | solve [ `expr` | ... | `expr` ] : | idtac [ `message_token` ... `message_token`] : | fail [`natural`] [`message_token` ... `message_token`] - : | fresh | fresh `string` | fresh `qualid` + : | fresh [ `component` … `component` ] : | context `ident` [`term`] : | eval `redexpr` in `term` : | type of `term` @@ -125,6 +122,7 @@ mode but it can also be used in toplevel definitions as shown below. : | () : | `integer` : | ( `expr` ) + component : `string` | `qualid` message_token : `string` | `ident` | `integer` tacarg : `qualid` : | () @@ -144,10 +142,11 @@ mode but it can also be used in toplevel definitions as shown below. : | `integer` (< | <= | > | >=) `integer` selector : [`ident`] : | `integer` - : (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) + : | (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) toplevel_selector : `selector` - : | `all` - : | `par` + : | all + : | par + : | ! .. productionlist:: coq top : [Local] Ltac `ltac_def` with ... with `ltac_def` @@ -160,13 +159,13 @@ Semantics --------- Tactic expressions can only be applied in the context of a proof. The -evaluation yields either a term, an integer or a tactic. Intermediary +evaluation yields either a term, an integer or a tactic. Intermediate results can be terms or integers but the final result must be a tactic which is then applied to the focused goals. There is a special case for ``match goal`` expressions of which the clauses evaluate to tactics. Such expressions can only be used as end result of -a tactic expression (never as argument of a non recursive local +a tactic expression (never as argument of a non-recursive local definition or of an application). The rest of this section explains the semantics of every construction of @@ -177,7 +176,7 @@ Sequence A sequence is an expression of the following form: -.. tacn:: @expr ; @expr +.. tacn:: @expr__1 ; @expr__2 :name: ltac-seq The expression :n:`@expr__1` is evaluated to :n:`v__1`, which must be @@ -197,8 +196,8 @@ following form: :name: [> ... | ... | ... ] (dispatch) The expressions :n:`@expr__i` are evaluated to :n:`v__i`, for - i=0,...,n and all have to be tactics. The :n:`v__i` is applied to the - i-th goal, for =1,...,n. It fails if the number of focused goals is not + i = 0, ..., n and all have to be tactics. The :n:`v__i` is applied to the + i-th goal, for i = 1, ..., n. It fails if the number of focused goals is not exactly n. .. note:: @@ -207,11 +206,11 @@ following form: were given. For instance, ``[> | auto]`` is a shortcut for ``[> idtac | auto ]``. - .. tacv:: [> {*| @expr} | @expr .. | {*| @expr}] + .. tacv:: [> {*| @expr__i} | @expr .. | {*| @expr__j}] - In this variant, token:`expr` is used for each goal coming after those - covered by the first list of :n:`@expr` but before those coevered by the - last list of :n:`@expr`. + In this variant, :n:`@expr` is used for each goal coming after those + covered by the list of :n:`@expr__i` but before those covered by the + list of :n:`@expr__j`. .. tacv:: [> {*| @expr} | .. | {*| @expr}] @@ -221,15 +220,15 @@ following form: .. tacv:: [> @expr .. ] In this variant, the tactic :n:`@expr` is applied independently to each of - the goals, rather than globally. In particular, if there are no goal, the + the goals, rather than globally. In particular, if there are no goals, the tactic is not run at all. A tactic which expects multiple goals, such as ``swap``, would act as if a single goal is focused. - .. tacv:: expr ; [{*| @expr}] + .. tacv:: @expr__0 ; [{*| @expr__i}] This variant of local tactic application is paired with a sequence. In this - variant, there must be as many :n:`@expr` in the list as goals generated - by the application of the first :n:`@expr` to each of the individual goals + variant, there must be as many :n:`@expr__i` as goals generated + by the application of :n:`@expr__0` to each of the individual goals independently. All the above variants work in this form too. Formally, :n:`@expr ; [ ... ]` is equivalent to :n:`[> @expr ; [> ... ] .. ]`. @@ -247,20 +246,20 @@ focused goals with: We can also use selectors as a tactical, which allows to use them nested in a tactic expression, by using the keyword ``only``: - .. tacv:: only selector : expr + .. tacv:: only @selector : @expr :name: only ... : ... - When selecting several goals, the tactic expr is applied globally to all + When selecting several goals, the tactic :token:`expr` is applied globally to all selected goals. .. tacv:: [@ident] : @expr - In this variant, :n:`@expr` is applied locally to a goal previously named + In this variant, :token:`expr` is applied locally to a goal previously named by the user (see :ref:`existential-variables`). .. tacv:: @num : @expr - In this variant, :n:`@expr` is applied locally to the :token:`num`-th goal. + In this variant, :token:`expr` is applied locally to the :token:`num`-th goal. .. tacv:: {+, @num-@num} : @expr @@ -271,13 +270,13 @@ focused goals with: .. tacv:: all: @expr :name: all: ... - In this variant, :n:`@expr` is applied to all focused goals. ``all:`` can only + In this variant, :token:`expr` is applied to all focused goals. ``all:`` can only be used at the toplevel of a tactic expression. .. tacv:: !: @expr - In this variant, if exactly one goal is focused :n:`expr` is - applied to it. Otherwise the tactical fails. ``!:`` can only be + In this variant, if exactly one goal is focused, :token:`expr` is + applied to it. Otherwise the tactic fails. ``!:`` can only be used at the toplevel of a tactic expression. .. tacv:: par: @expr @@ -385,11 +384,12 @@ tactic to work (i.e. which does not fail) among a panel of tactics: :name: first The :n:`@expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be - tactic values, for i=1,...,n. Supposing n>1, it applies, in each focused - goal independently, :n:`v__1`, if it works, it stops otherwise it + tactic values for i = 1, ..., n. Supposing n > 1, + :n:`first [@expr__1 | ... | @expr__n]` applies :n:`v__1` in each + focused goal independently and stops if it succeeds; otherwise it tries to apply :n:`v__2` and so on. It fails when there is no applicable tactic. In other words, - :n:`first [:@expr__1 | ... | @expr__n]` behaves, in each goal, as the the first + :n:`first [@expr__1 | ... | @expr__n]` behaves, in each goal, as the first :n:`v__i` to have *at least* one success. .. exn:: No applicable tactic. @@ -397,7 +397,7 @@ tactic to work (i.e. which does not fail) among a panel of tactics: .. tacv:: first @expr This is an |Ltac| alias that gives a primitive access to the first - tactical as a |Ltac| definition without going through a parsing rule. It + tactical as an |Ltac| definition without going through a parsing rule. It expects to be given a list of tactics through a ``Tactic Notation``, allowing to write notations of the following form: @@ -454,7 +454,7 @@ single success *a posteriori*: :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied but only its first success is used. If ``v`` fails, - :n:`once @expr` fails like ``v``. If ``v`` has a least one success, + :n:`once @expr` fails like ``v``. If ``v`` has at least one success, :n:`once @expr` succeeds once, but cannot produce more successes. Checking the successes @@ -475,7 +475,7 @@ one* success: .. warning:: The experimental status of this tactic pertains to the fact if ``v`` - performs side effects, they may occur in a unpredictable way. Indeed, + performs side effects, they may occur in an unpredictable way. Indeed, normally ``v`` would only be executed up to the first success until backtracking is needed, however exactly_once needs to look ahead to see whether a second success exists, and may run further effects @@ -515,8 +515,9 @@ among a panel of tactics: :name: solve The :n:`@expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be - tactic values, for i=1,...,n. Supposing n>1, it applies :n:`v__1` to - each goal independently, if it doesn’t solve the goal then it tries to + tactic values, for i = 1, ..., n. Supposing n > 1, + :n:`solve [@expr__1 | ... | @expr__n]` applies :n:`v__1` to + each goal independently and stops if it succeeds; otherwise it tries to apply :n:`v__2` and so on. It fails if there is no solving tactic. .. exn:: Cannot solve the goal. @@ -546,18 +547,16 @@ Failing This is the always-failing tactic: it does not solve any goal. It is useful for defining other tacticals since it can be caught by - :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching tacticals. The - :tacn:`fail` tactic will, however, succeed if all the goals have already been - solved. + :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching tacticals. .. tacv:: fail @num The number is the failure level. If no level is specified, it defaults to 0. The level is used by :tacn:`try`, :tacn:`repeat`, :tacn:`match goal` and the branching - tacticals. If 0, it makes :tacn:`match goal` considering the next clause - (backtracking). If non zero, the current :tacn:`match goal` block, :tacn:`try`, + tacticals. If 0, it makes :tacn:`match goal` consider the next clause + (backtracking). If nonzero, the current :tacn:`match goal` block, :tacn:`try`, :tacn:`repeat`, or branching command is aborted and the level is decremented. In - the case of :n:`+`, a non-zero level skips the first backtrack point, even if + the case of :n:`+`, a nonzero level skips the first backtrack point, even if the call to :n:`fail @num` is not enclosed in a :n:`+` command, respecting the algebraic identity. @@ -572,7 +571,9 @@ Failing .. tacv:: gfail :name: gfail - This variant fails even if there are no goals left. + This variant fails even when used after :n:`;` and there are no goals left. + Similarly, ``gfail`` fails even when used after ``all:`` and there are no + goals left. See the example for clarification. .. tacv:: gfail {* message_token} @@ -582,10 +583,41 @@ Failing there are no goals left. Be careful however if Coq terms have to be printed as part of the failure: term construction always forces the tactic into the goals, meaning that if there are no goals when it is - evaluated, a tactic call like :n:`let x:=H in fail 0 x` will succeed. + evaluated, a tactic call like :n:`let x := H in fail 0 x` will succeed. .. exn:: Tactic Failure message (level @num). + .. exn:: No such goal. + :name: No such goal. (fail) + + .. example:: + + .. coqtop:: all + + Goal True. + Proof. fail. Abort. + + Goal True. + Proof. trivial; fail. Qed. + + Goal True. + Proof. trivial. fail. Abort. + + Goal True. + Proof. trivial. all: fail. Qed. + + Goal True. + Proof. gfail. Abort. + + Goal True. + Proof. trivial; gfail. Abort. + + Goal True. + Proof. trivial. gfail. Abort. + + Goal True. + Proof. trivial. all: gfail. Abort. + Timeout ~~~~~~~ @@ -605,7 +637,7 @@ amount of time: which is very machine-dependent: a script that works on a quick machine may fail on a slow one. The converse is even possible if you combine a timeout with some other tacticals. This tactical is hence proposed only - for convenience during debug or other development phases, we strongly + for convenience during debugging or other development phases, we strongly advise you to not leave any timeout in final scripts. Note also that this tactical isn’t available on the native Windows port of Coq. @@ -617,9 +649,9 @@ A tactic execution can be timed: .. tacn:: time @string @expr :name: time - evaluates :n:`@expr` and displays the time the tactic expression ran, whether it - fails or successes. In case of several successes, the time for each successive - runs is displayed. Time is in seconds and is machine-dependent. The :n:`@string` + evaluates :n:`@expr` and displays the running time of the tactic expression, whether it + fails or succeeds. In case of several successes, the time for each successive + run is displayed. Time is in seconds and is machine-dependent. The :n:`@string` argument is optional. When provided, it is used to identify this particular occurrence of time. @@ -682,15 +714,16 @@ Local definitions Local definitions can be done as follows: .. tacn:: let @ident__1 := @expr__1 {* with @ident__i := @expr__i} in @expr + :name: let ... := ... each :n:`@expr__i` is evaluated to :n:`v__i`, then, :n:`@expr` is evaluated by substituting :n:`v__i` to each occurrence of :n:`@ident__i`, for - i=1,...,n. There is no dependencies between the :n:`@expr__i` and the + i = 1, ..., n. There are no dependencies between the :n:`@expr__i` and the :n:`@ident__i`. - Local definitions can be recursive by using :n:`let rec` instead of :n:`let`. + Local definitions can be made recursive by using :n:`let rec` instead of :n:`let`. In this latter case, the definitions are evaluated lazily so that the rec - keyword can be used also in non recursive cases so as to avoid the eager + keyword can be used also in non-recursive cases so as to avoid the eager evaluation of local definitions. .. but rec changes the binding!! @@ -704,7 +737,7 @@ An application is an expression of the following form: The reference :n:`@qualid` must be bound to some defined tactic definition expecting at least as many arguments as the provided :n:`tacarg`. The - expressions :n:`@expr__i` are evaluated to :n:`v__i`, for i=1,...,n. + expressions :n:`@expr__i` are evaluated to :n:`v__i`, for i = 1, ..., n. .. what expressions ?? @@ -755,7 +788,7 @@ We can carry out pattern matching on terms with: evaluation of :n:`@expr__1` fails, or if the evaluation of :n:`@expr__1` succeeds but returns a tactic in execution position whose execution fails, then :n:`cpattern__2` is used and so on. The pattern - :n:`_` matches any term and shunts all remaining patterns if any. If all + :n:`_` matches any term and shadows all remaining patterns if any. If all clauses fail (in particular, there is no pattern :n:`_`) then a no-matching-clause error is raised. @@ -800,7 +833,7 @@ We can carry out pattern matching on terms with: matching subterm is tried. If no further subterm matches, the next clause is tried. Matching subterms are considered top-bottom and from left to right (with respect to the raw printing obtained by setting option - :opt:`Printing All`). + :flag:`Printing All`). .. example:: @@ -821,15 +854,15 @@ We can carry out pattern matching on terms with: Pattern matching on goals ~~~~~~~~~~~~~~~~~~~~~~~~~ -We can make pattern matching on goals using the following expression: +We can perform pattern matching on goals using the following expression: .. we should provide the full grammar here .. tacn:: match goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end :name: match goal - If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i=1,...,m\ :sub:`1` is - matched (non-linear first-order unification) by an hypothesis of the + If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is + matched (non-linear first-order unification) by a hypothesis of the goal and if :n:`cpattern_1` is matched by the conclusion of the goal, then :n:`@expr__1` is evaluated to :n:`v__1` by substituting the pattern matching to the metavariables and the real hypothesis names @@ -857,10 +890,10 @@ We can make pattern matching on goals using the following expression: It is important to know that each hypothesis of the goal can be matched by at most one hypothesis pattern. The order of matching is the - following: hypothesis patterns are examined from the right to the left + following: hypothesis patterns are examined from right to left (i.e. hyp\ :sub:`i,m`\ :sub:`i`` before hyp\ :sub:`i,1`). For each - hypothesis pattern, the goal hypothesis are matched in order (fresher - hypothesis first), but it possible to reverse this order (older first) + hypothesis pattern, the goal hypotheses are matched in order (newest + first), but it possible to reverse this order (oldest first) with the :n:`match reverse goal with` variant. .. tacv:: multimatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end @@ -896,6 +929,10 @@ produce subgoals but generates a term to be used in tactic expressions: value of :n:`@ident` by the value of :n:`@expr`. .. exn:: Not a context variable. + :undocumented: + + .. exn:: Unbound context identifier @ident. + :undocumented: Generating fresh hypothesis names ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -908,12 +945,10 @@ expression returns an identifier: .. tacn:: fresh {* component} It evaluates to an identifier unbound in the goal. This fresh identifier - is obtained by concatenating the value of the :n:`@component`s (each of them + is obtained by concatenating the value of the :n:`@component`\ s (each of them is, either a :n:`@qualid` which has to refer to a (unqualified) name, or directly a name denoted by a :n:`@string`). - .. I don't understand this component thing. Couldn't we give the grammar? - If the resulting name is already used, it is padded with a number so that it becomes fresh. If no component is given, the name is a fresh derivative of the name ``H``. @@ -951,7 +986,7 @@ Manipulating untyped terms An untyped term, in |Ltac|, can contain references to hypotheses or to |Ltac| variables containing typed or untyped terms. An untyped term can be - type-checked using the function type_term whose argument is parsed as an + type checked using the function type_term whose argument is parsed as an untyped term and returns a well-typed term which can be used in tactics. Untyped terms built using :n:`uconstr :` can also be used as arguments to the @@ -1152,6 +1187,7 @@ Info trace not printed. .. opt:: Info Level @num + :name: Info Level This option is an alternative to the :cmd:`Info` command. @@ -1162,12 +1198,12 @@ Info trace Interactive debugger ~~~~~~~~~~~~~~~~~~~~ -.. opt:: Ltac Debug +.. flag:: Ltac Debug This option governs the step-by-step debugger that comes with the |Ltac| interpreter When the debugger is activated, it stops at every step of the evaluation of -the current |Ltac| expression and it prints information on what it is doing. +the current |Ltac| expression and prints information on what it is doing. The debugger stops, prompting for a command which can be one of the following: @@ -1185,9 +1221,12 @@ following: | r string: | advance up to the next call to “idtac string” | +-----------------+-----------------------------------------------+ +.. exn:: Debug mode not available in the IDE + :undocumented: + A non-interactive mode for the debugger is available via the option: -.. opt:: Ltac Batch Debug +.. flag:: Ltac Batch Debug This option has the effect of presenting a newline at every prompt, when the debugger is on. The debug log thus created, which does not require @@ -1204,11 +1243,11 @@ which can sometimes be so slow as to impede interactive usage. The reasons for the performence degradation can be intricate, like a slowly performing |Ltac| match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and -indicates the time spent in a tactic depending its calling context. Thus +indicates the time spent in a tactic depending on its calling context. Thus it allows to locate the part of a tactic definition that contains the -performance bug. +performance issue. -.. opt:: Ltac Profiling +.. flag:: Ltac Profiling This option enables and disables the profiler. @@ -1240,8 +1279,12 @@ performance bug. Goal forall x y z A B C D E F G H I J K L M N O P Q R S T U V W X Y Z, max x (max y z) = max (max x y) z /\ max x (max y z) = max (max x y) z - /\ (A /\ B /\ C /\ D /\ E /\ F /\ G /\ H /\ I /\ J /\ K /\ L /\ M /\ N /\ O /\ P /\ Q /\ R /\ S /\ T /\ U /\ V /\ W /\ X /\ Y /\ Z - -> Z /\ Y /\ X /\ W /\ V /\ U /\ T /\ S /\ R /\ Q /\ P /\ O /\ N /\ M /\ L /\ K /\ J /\ I /\ H /\ G /\ F /\ E /\ D /\ C /\ B /\ A). + /\ + (A /\ B /\ C /\ D /\ E /\ F /\ G /\ H /\ I /\ J /\ K /\ L /\ M /\ + N /\ O /\ P /\ Q /\ R /\ S /\ T /\ U /\ V /\ W /\ X /\ Y /\ Z + -> + Z /\ Y /\ X /\ W /\ V /\ U /\ T /\ S /\ R /\ Q /\ P /\ O /\ N /\ + M /\ L /\ K /\ J /\ I /\ H /\ G /\ F /\ E /\ D /\ C /\ B /\ A). Proof. .. coqtop:: all @@ -1290,7 +1333,7 @@ performance bug. benchmarking purposes. You can also pass the ``-profile-ltac`` command line option to ``coqc``, which -turns the :opt:`Ltac Profiling` option on at the beginning of each document, +turns the :flag:`Ltac Profiling` option on at the beginning of each document, and performs a :cmd:`Show Ltac Profile` at the end. .. warning:: diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index eba0db3ff5..4b1b7719c5 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -1,4 +1,3 @@ -.. include:: ../replaces.rst .. _proofhandling: ------------------- @@ -84,7 +83,7 @@ list of assertion commands is given in :ref:`Assertions`. The command :name: Defined Same as :cmd:`Qed` but the proof is then declared transparent, which means - that its content can be explicitly used for type-checking and that it can be + that its content can be explicitly used for type checking and that it can be unfolded in conversion tactics (see :ref:`performingcomputations`, :cmd:`Opaque`, :cmd:`Transparent`). @@ -113,7 +112,7 @@ list of assertion commands is given in :ref:`Assertions`. The command Aborts the editing of the proof named :token:`ident` (in case you have nested proofs). - .. seealso:: :opt:`Nested Proofs Allowed` + .. seealso:: :flag:`Nested Proofs Allowed` .. cmdv:: Abort All @@ -201,13 +200,14 @@ The following options modify the behavior of ``Proof using``. .. opt:: Default Proof Using "@expression" + :name: Default Proof Using Use :n:`@expression` as the default ``Proof using`` value. E.g. ``Set Default Proof Using "a b"`` will complete all ``Proof`` commands not followed by a ``using`` part with ``using a b``. -.. opt:: Suggest Proof Using +.. flag:: Suggest Proof Using When :cmd:`Qed` is performed, suggest a ``using`` annotation if the user did not provide one. @@ -315,13 +315,16 @@ Navigation in the proof tree .. _curly-braces: +.. index:: { + } + .. cmd:: %{ %| %} The command ``{`` (without a terminating period) focuses on the first goal, much like :cmd:`Focus` does, however, the subproof can only be unfocused when it has been fully solved ( *i.e.* when there is no focused goal left). Unfocusing is then handled by ``}`` (again, without a - terminating period). See also example in next section. + terminating period). See also an example in the next section. Note that when a focused goal is proved a message is displayed together with a suggestion about the right bullet or ``}`` to unfocus it @@ -329,20 +332,47 @@ Navigation in the proof tree .. cmdv:: @num: %{ - This focuses on the :token:`num` th subgoal to prove. + This focuses on the :token:`num`\-th subgoal to prove. + + .. cmdv:: [@ident]: %{ + + This focuses on the named goal :token:`ident`. + + .. note:: + + Goals are just existential variables and existential variables do not + get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`. + + .. seealso:: :ref:`existential-variables` + + .. example:: + + This can also be a way of focusing on a shelved goal, for instance: - Error messages: + .. coqtop:: all + + Goal exists n : nat, n = n. + eexists ?[x]. + reflexivity. + [x]: exact 0. + Qed. .. exn:: This proof is focused, but cannot be unfocused this way. You are trying to use ``}`` but the current subproof has not been fully solved. - .. exn:: No such goal. - :name: No such goal. (Focusing) + .. exn:: No such goal (@num). + :undocumented: + + .. exn:: No such goal (@ident). + :undocumented: - .. exn:: Brackets only support the single numbered goal selector. + .. exn:: Brackets do not support multi-goal selectors. - See also error messages about bullets below. + Brackets are used to focus on a single goal given either by its position + or by its name if it has one. + + .. seealso:: The error messages about bullets below. .. _bullets: @@ -358,8 +388,10 @@ same bullet ``b``. See the example below. Different bullets can be used to nest levels. The scope of bullet does not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further -nesting levels provided they are delimited by these. Available bullets -are ``-``, ``+``, ``*``, ``--``, ``++``, ``**``, ``---``, ``+++``, ``***``, ... (without a terminating period). +nesting levels provided they are delimited by these. Bullets are made of +repeated ``-``, ``+`` or ``*`` symbols: + +.. prodn:: bullet ::= {+ - } %| {+ + } %| {+ * } Note again that when a focused goal is proved a message is displayed together with a suggestion about the right bullet or ``}`` to unfocus it @@ -375,6 +407,7 @@ or focus the next one. The following example script illustrates all these features: .. example:: + .. coqtop:: all Goal (((True /\ True) /\ True) /\ True) /\ True. @@ -391,27 +424,37 @@ The following example script illustrates all these features: - assert True. { trivial. } assumption. + Qed. +.. exn:: Wrong bullet @bullet__1: Current bullet @bullet__2 is not finished. -.. exn:: Wrong bullet @bullet1: Current bullet @bullet2 is not finished. - - Before using bullet :n:`@bullet1` again, you should first finish proving the current focused goal. Note that :n:`@bullet1` and :n:`@bullet2` may be the same. + Before using bullet :n:`@bullet__1` again, you should first finish proving + the current focused goal. + Note that :n:`@bullet__1` and :n:`@bullet__2` may be the same. -.. exn:: Wrong bullet @bullet1: Bullet @bullet2 is mandatory here. +.. exn:: Wrong bullet @bullet__1: Bullet @bullet__2 is mandatory here. - You must put :n:`@bullet2` to focus next goal. No other bullet is allowed here. + You must put :n:`@bullet__2` to focus on the next goal. No other bullet is + allowed here. .. exn:: No such goal. Focus next goal with bullet @bullet. - You tried to apply a tactic but no goal where under focus. Using :n:`@bullet` is mandatory here. + You tried to apply a tactic but no goals were under focus. + Using :n:`@bullet` is mandatory here. -.. exn:: No such goal. Try unfocusing with %{. +.. FIXME: the :noindex: below works around a Sphinx issue. + (https://github.com/sphinx-doc/sphinx/issues/4979) + It should be removed once that issue is fixed. + +.. exn:: No such goal. Try unfocusing with %}. + :noindex: You just finished a goal focused by ``{``, you must unfocus it with ``}``. Set Bullet Behavior ``````````````````` .. opt:: Bullet Behavior %( "None" %| "Strict Subproofs" %) + :name: Bullet Behavior This option controls the bullet behavior and can take two possible values: @@ -432,7 +475,7 @@ Requesting information .. cmdv:: Show @num - Displays only the :token:`num` th subgoal. + Displays only the :token:`num`\-th subgoal. .. exn:: No such goal. @@ -470,7 +513,7 @@ Requesting information constructed. These holes appear as a question mark indexed by an integer, and applied to the list of variables in the context, since it may depend on them. The types obtained by abstracting away the context - from the type of each hole-placer are also printed. + from the type of each placeholder are also printed. .. cmdv:: Show Conjectures :name: Show Conjectures @@ -511,6 +554,7 @@ Requesting information :token:`ident` .. example:: + .. coqtop:: all Show Match nat. @@ -543,6 +587,7 @@ Controlling the effect of proof editing commands .. opt:: Hyps Limit @num + :name: Hyps Limit This option controls the maximum number of hypotheses displayed in goals after the application of a tactic. All the hypotheses remain usable @@ -551,7 +596,7 @@ Controlling the effect of proof editing commands available hypotheses. -.. opt:: Automatic Introduction +.. flag:: Automatic Introduction This option controls the way binders are handled in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the @@ -563,7 +608,7 @@ Controlling the effect of proof editing commands has to be used to move the assumptions to the local context. -.. opt:: Nested Proofs Allowed +.. flag:: Nested Proofs Allowed When turned on (it is off by default), this option enables support for nested proofs: a new assertion command can be inserted before the current proof is diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 6fb73a030f..52609546d5 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _thessreflectprooflanguage: ------------------------------ @@ -37,7 +35,7 @@ bookkeeping is performed on the conclusion of the goal, using for that purpose a couple of syntactic constructions behaving similar to tacticals (and often named as such in this chapter). The ``:`` tactical moves hypotheses from the context to the conclusion, while ``=>`` moves hypotheses from the -conclusion to the context, and ``in`` moves back and forth an hypothesis from the +conclusion to the context, and ``in`` moves back and forth a hypothesis from the context to the conclusion for the time of applying an action to it. While naming hypotheses is commonly done by means of an ``as`` clause in the @@ -104,8 +102,8 @@ this corresponds to working in the following context: Unset Printing Implicit Defensive. .. seealso:: - :opt:`Implicit Arguments`, :opt:`Strict Implicit`, - :opt:`Printing Implicit Defensive` + :flag:`Implicit Arguments`, :flag:`Strict Implicit`, + :flag:`Printing Implicit Defensive` .. _compatibility_issues_ssr: @@ -303,7 +301,7 @@ the ``if`` construct to all binary data types; compare The latter appears to be marginally shorter, but it is quite ambiguous, and indeed often requires an explicit annotation -``(term : {_} + {_})`` to type-check, which evens the character count. +``(term : {_} + {_})`` to type check, which evens the character count. Therefore, |SSR| restricts by default the condition of a plain if construct to the standard ``bool`` type; this avoids spurious type @@ -385,7 +383,7 @@ expressions such as Unfortunately, such higher-order expressions are quite frequent in representation functions, especially those which use |Coq|'s -``Structures`` to emulate Haskell type classes. +``Structures`` to emulate Haskell typeclasses. Therefore, |SSR| provides a variant of |Coq|’s implicit argument declaration, which causes |Coq| to fill in some implicit parameters at @@ -444,11 +442,16 @@ not its name, one usually uses “arrow” abstractions for prenex arguments, or the ``(_ : term)`` syntax for inner arguments. In |SSR|, the latter can be replaced by the open syntax ``of term`` or (equivalently) ``& term``, which are both syntactically equivalent to a -``(_ : term)`` expression. +``(_ : term)`` expression. This feature almost behaves as the +following extension of the binder syntax: + +.. prodn:: + binder += & @term | of @term -For instance, the usual two-constructor polymorphic type list, i.e. -the one of the standard List library, can be defined by the following -declaration: +Caveat: ``& T`` and ``of T`` abbreviations have to appear at the end +of a binder list. For instance, the usual two-constructor polymorphic +type list, i.e. the one of the standard ``List`` library, can be +defined by the following declaration: .. example:: @@ -1285,7 +1288,7 @@ catch the appropriate number of wildcards to be inserted. Note that this use of the refine tactic implies that the tactic tries to match the goal up to expansion of constants and evaluation of subterms. -|SSR|’s apply has a special behaviour on goals containing +|SSR|’s apply has a special behavior on goals containing existential metavariables of sort Prop. .. example:: @@ -2064,26 +2067,27 @@ is equivalent to: (see section :ref:`discharge_ssr` for the documentation of the apply: combination). -Warning The list of tactics, possibly chained by semicolons, that -follows a by keyword is considered as a parenthesized block applied to -the current goal. Hence for example if the tactic: +.. warning:: -.. coqtop:: in + The list of tactics (possibly chained by semicolons) that + follows the ``by`` keyword is considered to be a parenthesized block applied to + the current goal. Hence for example if the tactic: - by rewrite my_lemma1. + .. coqtop:: in -succeeds, then the tactic: + by rewrite my_lemma1. -.. coqtop:: in + succeeds, then the tactic: - by rewrite my_lemma1; apply my_lemma2. + .. coqtop:: in -usually fails since it is equivalent to: + by rewrite my_lemma1; apply my_lemma2. -.. coqtop:: in + usually fails since it is equivalent to: - by (rewrite my_lemma1; apply my_lemma2). + .. coqtop:: in + by (rewrite my_lemma1; apply my_lemma2). .. _selectors_ssr: @@ -2522,7 +2526,8 @@ After the :token:`i_pattern`, a list of binders is allowed. .. coqtop:: reset - From Coq Require Import ssreflect Omega. + From Coq Require Import ssreflect. + From Coq Require Import Omega. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -2552,12 +2557,9 @@ copying the goal itself. .. example:: - .. coqtop:: reset + .. coqtop:: none - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Abort All. .. coqtop:: all @@ -2581,12 +2583,9 @@ context entry name. .. example:: - .. coqtop:: reset + .. coqtop:: none - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Abort All. Set Printing Depth 15. .. coqtop:: all @@ -2601,20 +2600,13 @@ context entry name. Note that the sub-term produced by ``omega`` is in general huge and uninteresting, and hence one may want to hide it. For this purpose the ``[: name ]`` intro pattern and the tactic -``abstract`` (see page :ref:`abstract_ssr`) are provided. +``abstract`` (see :ref:`abstract_ssr`) are provided. .. example:: - .. coqtop:: reset - - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + .. coqtop:: none - Inductive Ord n := Sub x of x < n. - Notation "'I_ n" := (Ord n) (at level 8, n at level 2, format "''I_' n"). - Arguments Sub {_} _ _. + Abort All. .. coqtop:: all @@ -2629,16 +2621,9 @@ with have and an explicit term, they must be used as follows: .. example:: - .. coqtop:: reset + .. coqtop:: none - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - - Inductive Ord n := Sub x of x < n. - Notation "'I_ n" := (Ord n) (at level 8, n at level 2, format "''I_' n"). - Arguments Sub {_} _ _. + Abort All. .. coqtop:: all @@ -2659,16 +2644,9 @@ makes use of it). .. example:: - .. coqtop:: reset - - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + .. coqtop:: none - Inductive Ord n := Sub x of x < n. - Notation "'I_ n" := (Ord n) (at level 8, n at level 2, format "''I_' n"). - Arguments Sub {_} _ _. + Abort All. .. coqtop:: all @@ -2679,18 +2657,15 @@ Last, notice that the use of intro patterns for abstract constants is orthogonal to the transparent flag ``@`` for have. -The have tactic and type classes resolution +The have tactic and typeclass resolution ``````````````````````````````````````````` -Since |SSR| 1.5 the have tactic behaves as follows with respect to -type classes inference. +Since |SSR| 1.5 the ``have`` tactic behaves as follows with respect to +typeclass inference. - .. coqtop:: reset + .. coqtop:: none - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Abort All. Axiom ty : Type. Axiom t : ty. @@ -2726,9 +2701,9 @@ type classes inference. No inference for ``t``. Unresolved instances are quantified in the (inferred) type of ``t`` and abstracted in ``t``. -.. opt:: SsrHave NoTCResolution +.. flag:: SsrHave NoTCResolution - This option restores the behavior of |SSR| 1.4 and below (never resolve type classes). + This option restores the behavior of |SSR| 1.4 and below (never resolve typeclasses). Variants: the suff and wlog tactics ``````````````````````````````````` @@ -2766,12 +2741,9 @@ The ``have`` modifier can follow the ``suff`` tactic. .. example:: - .. coqtop:: reset + .. coqtop:: none - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Abort All. Axioms G P : Prop. .. coqtop:: all @@ -2839,12 +2811,9 @@ are unique. .. example:: - .. coqtop:: reset + .. coqtop:: none - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Abort All. .. coqtop:: all @@ -2935,12 +2904,10 @@ illustrated in the following example. the pattern ``id (addx x)``, that would produce the following first subgoal - .. coqtop:: reset + .. coqtop:: 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. @@ -3046,6 +3013,15 @@ An :token:`r_item` can be: is equivalent to: ``change term1 with term2.`` If ``term2`` is a single constant and ``term1`` head symbol is not ``term2``, then the head symbol of ``term1`` is repeatedly unfolded until ``term2`` appears. ++ A :token:`term`, which can be: + + A term whose type has the form: + ``forall (x1 : A1 )…(xn : An ), eq term1 term2`` where + ``eq`` is the Leibniz equality or a registered setoid + equality. + + A list of terms ``(t1 ,…,tn)``, each ``ti`` having a type above. + The tactic: ``rewrite r_prefix (t1 ,…,tn ).`` + is equivalent to: ``do [rewrite r_prefix t1 | … | rewrite r_prefix tn ].`` + + An anonymous rewrite lemma ``(_ : term)``, where term has a type as above. tactic: ``rewrite (_ : term)`` is in fact synonym of: ``cutrewrite (term).``. .. example:: @@ -3063,9 +3039,10 @@ An :token:`r_item` can be: Lemma test x : ddouble x = 4 * x. rewrite [ddouble _]/double. - *Warning* The |SSR| - terms containing holes are *not* typed as abstractions in this - context. Hence the following script fails. + .. warning:: + + The |SSR| terms containing holes are *not* typed as + abstractions in this context. Hence the following script fails. .. coqtop:: none @@ -3087,17 +3064,6 @@ An :token:`r_item` can be: rewrite -[f y x]/(y + _). -+ A :token:`term`, which can be: - - + A term whose type has the form: - ``forall (x1 : A1 )…(xn : An ), eq term1 term2`` where - ``eq`` is the Leibniz equality or a registered setoid - equality. - + A list of terms ``(t1 ,…,tn)``, each ``ti`` having a type above. - The tactic: ``rewrite r_prefix (t1 ,…,tn ).`` - is equivalent to: ``do [rewrite r_prefix t1 | … | rewrite r_prefix tn ].`` - + An anonymous rewrite lemma ``(_ : term)``, where term has a type as above. tactic: ``rewrite (_ : term)`` is in fact synonym of: ``cutrewrite (term).``. - Remarks and examples ~~~~~~~~~~~~~~~~~~~~ @@ -3738,20 +3704,22 @@ Note that ``nosimpl bar`` is simply notation for a term that reduces to ``bar``; hence ``unfold foo`` will replace ``foo`` by ``bar``, and ``fold foo`` will replace ``bar`` by ``foo``. -*Warning* The ``nosimpl`` trick only works if no reduction is apparent in -``t``; in particular, the declaration: +.. warning:: -.. coqtop:: in + The ``nosimpl`` trick only works if no reduction is apparent in + ``t``; in particular, the declaration: - Definition foo x := nosimpl (bar x). + .. coqtop:: in -will usually not work. Anyway, the common practice is to tag only the -function, and to use the following definition, which blocks the -reduction as expected: + Definition foo x := nosimpl (bar x). -.. coqtop:: in + will usually not work. Anyway, the common practice is to tag only the + function, and to use the following definition, which blocks the + reduction as expected: - Definition foo x := nosimpl bar x. + .. coqtop:: in + + Definition foo x := nosimpl bar x. A standard example making this technique shine is the case of arithmetic operations. We define for instance: @@ -3897,7 +3865,7 @@ duplication of function arguments. These copies usually end up in types hidden by the implicit arguments machinery or by user-defined notations. In these situations computing the right occurrence numbers is very tedious because they must be counted on the goal as printed -after setting the Printing All flag. Moreover the resulting script is +after setting the :flag:`Printing All` flag. Moreover the resulting script is not really informative for the reader, since it refers to occurrence numbers he cannot easily see. @@ -4632,6 +4600,7 @@ bookkeeping steps. .. example:: + The following example use the ``~~`` prenex notation for boolean negation: @@ -4793,7 +4762,7 @@ equivalence property has been defined. Lemma andE (b1 b2 : bool) : (b1 /\ b2) <-> (b1 && b2). -Let us compare the respective behaviours of ``andE`` and ``andP``. +Let us compare the respective behaviors of ``andE`` and ``andP``. .. example:: @@ -4906,7 +4875,7 @@ The term , called the *view lemma* can be: Let ``top`` be the top assumption in the goal. -There are three steps in the behaviour of an assumption view tactic: +There are three steps in the behavior of an assumption view tactic: + It first introduces ``top``. + If the type of :token:`term` is neither a double implication nor an @@ -5421,7 +5390,7 @@ Tacticals discharge :ref:`discharge_ssr` -.. prodn:: tactic += @tacitc => {+ @i_item } +.. prodn:: tactic += @tactic => {+ @i_item } introduction see :ref:`introduction_ssr` diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 562f8568dc..f99c539251 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _tactics: Tactics @@ -26,8 +23,8 @@ address a particular goal in the list by writing n:tactic which means “apply tactic tactic to goal number n”. We can show the list of subgoals by typing Show (see Section :ref:`requestinginformation`). -Since not every rule applies to a given statement, every tactic cannot -be used to reduce any goal. In other words, before applying a tactic +Since not every rule applies to a given statement, not every tactic can +be used to reduce a given goal. In other words, before applying a tactic to a given goal, the system checks that some *preconditions* are satisfied. If it is not the case, the tactic raises an error message. @@ -51,7 +48,8 @@ specified, the default selector is used. tactic_invocation : toplevel_selector : tactic. : |tactic . -.. opt:: Default Goal Selector @toplevel_selector +.. opt:: Default Goal Selector "@toplevel_selector" + :name: Default Goal Selector This option controls the default selector, used when no selector is specified when applying a tactic. The initial value is 1, hence the @@ -107,37 +105,37 @@ bindings_list`` where ``bindings_list`` may be of two different forms: .. _occurencessets: -Occurrences sets and occurrences clauses +Occurrence sets and occurrence clauses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -An occurrences clause is a modifier to some tactics that obeys the +An occurrence clause is a modifier to some tactics that obeys the following syntax: -.. _tactic_occurence_grammar: - .. productionlist:: `sentence` - occurence_clause : in `goal_occurences` - goal_occurences : [ident [`at_occurences`], ... , ident [`at_occurences`] [|- [* [`at_occurences`]]]] - :| * |- [* [`at_occurences`]] + occurrence_clause : in `goal_occurrences` + goal_occurrences : [`ident` [`at_occurrences`], ... , ident [`at_occurrences`] [|- [* [`at_occurrences`]]]] + :| * |- [* [`at_occurrences`]] :| * at_occurrences : at `occurrences` - occurences : [-] `num` ... `num` - -The role of an occurrence clause is to select a set of occurrences of a term in -a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate that -occurrences have to be selected in the hypotheses named :n:`@ident`. If no -numbers are given for hypothesis :n:`@ident`, then all the occurrences of `term` -in the hypothesis are selected. If numbers are given, they refer to occurrences -of `term` when the term is printed using option :opt:`Printing All`, counting -from left to right. In particular, occurrences of `term` in implicit arguments -(see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are counted. - -If a minus sign is given between at and the list of occurrences, it + occurrences : [-] `num` ... `num` + +The role of an occurrence clause is to select a set of occurrences of a term +in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate +that occurrences have to be selected in the hypotheses named :token:`ident`. +If no numbers are given for hypothesis :token:`ident`, then all the +occurrences of :token:`term` in the hypothesis are selected. If numbers are +given, they refer to occurrences of :token:`term` when the term is printed +using option :flag:`Printing All`, counting from left to right. In particular, +occurrences of :token:`term` in implicit arguments +(see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are +counted. + +If a minus sign is given between ``at`` and the list of occurrences, it negates the condition so that the clause denotes all the occurrences except the ones explicitly mentioned after the minus sign. As an exception to the left-to-right order, the occurrences in -thereturn subexpression of a match are considered *before* the +the return subexpression of a match are considered *before* the occurrences in the matched term. In the second case, the ``*`` on the left of ``|-`` means that all occurrences @@ -146,18 +144,20 @@ of term are selected in every hypothesis. In the first and second case, if ``*`` is mentioned on the right of ``|-``, the occurrences of the conclusion of the goal have to be selected. If some numbers are given, then only the occurrences denoted by these numbers are selected. If -no numbers are given, all occurrences of :n:`@term` in the goal are selected. +no numbers are given, all occurrences of :token:`term` in the goal are selected. Finally, the last notation is an abbreviation for ``* |- *``. Note also that ``|-`` is optional in the first case when no ``*`` is given. -Here are some tactics that understand occurrences clauses: :tacn:`set`, :tacn:`remember` -, :tacn:`induction`, :tacn:`destruct`. +Here are some tactics that understand occurrence clauses: :tacn:`set`, +:tacn:`remember`, :tacn:`induction`, :tacn:`destruct`. + +.. seealso:: + + :ref:`Managingthelocalcontext`, :ref:`caseanalysisandinduction`, + :ref:`printing_constructions_full`. -See also: :ref:`Managingthelocalcontext`, -:ref:`caseanalysisandinduction`, -:ref:`printing_constructions_full`. .. _applyingtheorems: @@ -173,40 +173,45 @@ Applying theorems :ref:`Conversion-rules`). .. exn:: Not an exact proof. + :undocumented: .. tacv:: eexact @term. :name: eexact - This tactic behaves like exact but is able to handle terms and goals with - meta-variables. + This tactic behaves like :tacn:`exact` but is able to handle terms and + goals with existential variables. .. tacn:: assumption :name: assumption - This tactic looks in the local context for an hypothesis which type is equal to - the goal. If it is the case, the subgoal is proved. Otherwise, it fails. + This tactic looks in the local context for a hypothesis whose type is + convertible to the goal. If it is the case, the subgoal is proved. + Otherwise, it fails. .. exn:: No such assumption. + :undocumented: .. tacv:: eassumption :name: eassumption - This tactic behaves like assumption but is able to handle goals with - meta-variables. + This tactic behaves like :tacn:`assumption` but is able to handle + goals with existential variables. .. tacn:: refine @term :name: refine This tactic applies to any goal. It behaves like :tacn:`exact` with a big - difference: the user can leave some holes (denoted by ``_`` or ``(_:type)``) in - the term. :tacn:`refine` will generate as many subgoals as there are holes in - the term. The type of holes must be either synthesized by the system - or declared by an explicit cast like ``(_:nat->Prop)``. Any subgoal that + difference: the user can leave some holes (denoted by ``_`` + or :n:`(_ : @type)`) in the term. :tacn:`refine` will generate as many + subgoals as there are holes in the term. The type of holes must be either + synthesized by the system or declared by an explicit cast + like ``(_ : nat -> Prop)``. Any subgoal that occurs in other subgoals is automatically shelved, as if calling :tacn:`shelve_unifiable`. This low-level tactic can be useful to advanced users. .. example:: + .. coqtop:: reset all Inductive Option : Set := @@ -214,16 +219,13 @@ Applying theorems | Ok : bool -> Option. Definition get : forall x:Option, x <> Fail -> bool. - - refine - (fun x:Option => - match x return x <> Fail -> bool with - | Fail => _ - | Ok b => fun _ => b - end). - - intros; absurd (Fail = Fail); trivial. - + refine + (fun x:Option => + match x return x <> Fail -> bool with + | Fail => _ + | Ok b => fun _ => b + end). + intros; absurd (Fail = Fail); trivial. Defined. .. exn:: Invalid argument. @@ -251,41 +253,43 @@ Applying theorems .. tacv:: notypeclasses refine @term :name: notypeclasses refine - This tactic behaves like :tacn:`refine` except it performs typechecking without + This tactic behaves like :tacn:`refine` except it performs type checking without resolution of typeclasses. .. tacv:: simple notypeclasses refine @term :name: simple notypeclasses refine - This tactic behaves like :tacn:`simple refine` except it performs typechecking + This tactic behaves like :tacn:`simple refine` except it performs type checking without resolution of typeclasses. .. tacn:: apply @term :name: apply - This tactic applies to any goal. The argument term is a term well-formed in the - local context. The tactic apply tries to match the current goal against the - conclusion of the type of term. If it succeeds, then the tactic returns as many - subgoals as the number of non-dependent premises of the type of term. If the - conclusion of the type of term does not match the goal *and* the conclusion is - an inductive type isomorphic to a tuple type, then each component of the tuple - is recursively matched to the goal in the left-to-right order. - - The tactic :tacn:`apply` relies on first-order unification with dependent types - unless the conclusion of the type of :token:`term` is of the form :g:`P (t`:sub:`1` - :g:`...` :g:`t`:sub:`n` :g:`)` with `P` to be instantiated. In the latter case, the behavior - depends on the form of the goal. If the goal is of the form - :g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n` and the :g:`t`:sub:`i` and - :g:`u`:sub:`i` unifies, then :g:`P` is taken to be :g:`(fun x => Q)`. Otherwise, - :tacn:`apply` tries to define :g:`P` by abstracting over :g:`t`:sub:`1` :g:`...` - :g:`t`:sub:`n` in the goal. See :tacn:`pattern` to transform the goal so that it - gets the form :g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n`. - - .. exn:: Unable to unify ... with ... . - - The apply tactic failed to match the conclusion of :token:`term` and the - current goal. You can help the apply tactic by transforming your goal with - the :tacn:`change` or :tacn:`pattern` tactics. + This tactic applies to any goal. The argument term is a term well-formed in + the local context. The tactic :tacn:`apply` tries to match the current goal + against the conclusion of the type of :token:`term`. If it succeeds, then + the tactic returns as many subgoals as the number of non-dependent premises + of the type of term. If the conclusion of the type of :token:`term` does + not match the goal *and* the conclusion is an inductive type isomorphic to + a tuple type, then each component of the tuple is recursively matched to + the goal in the left-to-right order. + + The tactic :tacn:`apply` relies on first-order unification with dependent + types unless the conclusion of the type of :token:`term` is of the form + :n:`P (t__1 ... t__n)` with ``P`` to be instantiated. In the latter case, + the behavior depends on the form of the goal. If the goal is of the form + :n:`(fun x => Q) u__1 ... u__n` and the :n:`t__i` and :n:`u__i` unify, + then :g:`P` is taken to be :g:`(fun x => Q)`. Otherwise, :tacn:`apply` + tries to define :g:`P` by abstracting over :g:`t_1 ... t__n` in the goal. + See :tacn:`pattern` to transform the goal so that it + gets the form :n:`(fun x => Q) u__1 ... u__n`. + + .. exn:: Unable to unify @term with @term. + + The :tacn:`apply` tactic failed to match the conclusion of :token:`term` + and the current goal. You can help the :tacn:`apply` tactic by + transforming your goal with the :tacn:`change` or :tacn:`pattern` + tactics. .. exn:: Unable to find an instance for the variables {+ @ident}. @@ -301,6 +305,7 @@ Applying theorems according to the order of these dependent premises of the type of term. .. exn:: Not the right number of missing arguments. + :undocumented: .. tacv:: apply @term with @bindings_list @@ -310,11 +315,9 @@ Applying theorems .. tacv:: apply {+, @term} - This is a shortcut for :n:`apply @term`:sub:`1` - :n:`; [.. | ... ; [ .. | apply @term`:sub:`n` :n:`] ... ]`, - i.e. for the successive applications of :token:`term`:sub:`i+1` on the last subgoal - generated by :n:`apply @term`:sub:`i` , starting from the application of - :token:`term`:sub:`1`. + This is a shortcut for :n:`apply @term__1; [.. | ... ; [ .. | apply @term__n] ... ]`, + i.e. for the successive applications of :n:`@term`:sub:`i+1` on the last subgoal + generated by :n:`apply @term__i` , starting from the application of :n:`@term__1`. .. tacv:: eapply @term :name: eapply @@ -326,7 +329,6 @@ Applying theorems intended to be found later in the proof. .. tacv:: simple apply @term. - :name: simple apply This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms that contain no variables to instantiate. For instance, the following example @@ -348,8 +350,8 @@ Applying theorems does. .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} - .. tacv:: {? simple} eapply {+, @term {? with @bindings_list}} - :name: simple eapply + {? simple} eapply {+, @term {? with @bindings_list}} + :name: simple apply; simple eapply This summarizes the different syntaxes for :tacn:`apply` and :tacn:`eapply`. @@ -364,8 +366,10 @@ Applying theorems sequence ``cut B. 2:apply H.`` where ``cut`` is described below. .. warn:: When @term contains more than one non dependent product the tactic lapply only takes into account the first product. + :undocumented: .. example:: + Assume we have a transitive relation ``R`` on ``nat``: .. coqtop:: reset in @@ -445,7 +449,7 @@ Applying theorems ``forall A, ... -> A``. Excluding this kind of lemma can be avoided by setting the following option: -.. opt:: Universal Lemma Under Conjunction +.. flag:: Universal Lemma Under Conjunction This option, which preserves compatibility with versions of Coq prior to 8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply ... in`). @@ -453,164 +457,151 @@ Applying theorems .. tacn:: apply @term in @ident :name: apply ... in - This tactic applies to any goal. The argument ``term`` is a term well-formed in - the local context and the argument :n:`@ident` is an hypothesis of the context. - The tactic ``apply term in ident`` tries to match the conclusion of the type - of :n:`@ident` against a non-dependent premise of the type of ``term``, trying - them from right to left. If it succeeds, the statement of hypothesis - :n:`@ident` is replaced by the conclusion of the type of ``term``. The tactic - also returns as many subgoals as the number of other non-dependent premises - in the type of ``term`` and of the non-dependent premises of the type of - :n:`@ident`. If the conclusion of the type of ``term`` does not match the goal - *and* the conclusion is an inductive type isomorphic to a tuple type, then + This tactic applies to any goal. The argument :token:`term` is a term + well-formed in the local context and the argument :token:`ident` is an + hypothesis of the context. + The tactic :n:`apply @term in @ident` tries to match the conclusion of the + type of :token:`ident` against a non-dependent premise of the type + of :token:`term`, trying them from right to left. If it succeeds, the + statement of hypothesis :token:`ident` is replaced by the conclusion of + the type of :token:`term`. The tactic also returns as many subgoals as the + number of other non-dependent premises in the type of :token:`term` and of + the non-dependent premises of the type of :token:`ident`. If the conclusion + of the type of :token:`term` does not match the goal *and* the conclusion + is an inductive type isomorphic to a tuple type, then the tuple is (recursively) decomposed and the first component of the tuple of which a non-dependent premise matches the conclusion of the type of - :n:`@ident`. Tuples are decomposed in a width-first left-to-right order (for - instance if the type of :g:`H1` is a :g:`A <-> B` statement, and the type of - :g:`H2` is :g:`A` then ``apply H1 in H2`` transforms the type of :g:`H2` - into :g:`B`). The tactic ``apply`` relies on first-order pattern-matching + :token:`ident`. Tuples are decomposed in a width-first left-to-right order + (for instance if the type of :g:`H1` is :g:`A <-> B` and the type of + :g:`H2` is :g:`A` then :g:`apply H1 in H2` transforms the type of :g:`H2` + into :g:`B`). The tactic :tacn:`apply` relies on first-order pattern matching with dependent types. -.. exn:: Statement without assumptions. + .. exn:: Statement without assumptions. - This happens if the type of ``term`` has no non dependent premise. + This happens if the type of :token:`term` has no non-dependent premise. -.. exn:: Unable to apply. + .. exn:: Unable to apply. - This happens if the conclusion of :n:`@ident` does not match any of the non - dependent premises of the type of ``term``. + This happens if the conclusion of :token:`ident` does not match any of + the non-dependent premises of the type of :token:`term`. -.. tacv:: apply {+, @term} in @ident + .. tacv:: apply {+, @term} in @ident - This applies each of ``term`` in sequence in :n:`@ident`. + This applies each :token:`term` in sequence in :token:`ident`. -.. tacv:: apply {+, @term with @bindings_list} in @ident + .. tacv:: apply {+, @term with @bindings_list} in @ident - This does the same but uses the bindings in each :n:`(@id := @ val)` to - instantiate the parameters of the corresponding type of ``term`` (see - :ref:`bindings list <bindingslist>`). + This does the same but uses the bindings in each :n:`(@ident := @term)` to + instantiate the parameters of the corresponding type of :token:`term` + (see :ref:`bindings list <bindingslist>`). -.. tacv:: eapply {+, @term with @bindings_list} in @ident + .. tacv:: eapply {+, @term {? with @bindings_list } } in @ident - This works as :tacn:`apply ... in` but turns unresolved bindings into - existential variables, if any, instead of failing. + This works as :tacn:`apply ... in` but turns unresolved bindings into + existential variables, if any, instead of failing. -.. tacv:: apply {+, @term with @bindings_list} in @ident as @intro_pattern - :name: apply ... in ... as + .. tacv:: apply {+, @term {? with @bindings_list } } in @ident as @intro_pattern + :name: apply ... in ... as - This works as :tacn:`apply ... in` then applies the - :n:`@intro_pattern` to the hypothesis :n:`@ident`. + This works as :tacn:`apply ... in` then applies the :token:`intro_pattern` + to the hypothesis :token:`ident`. -.. tacv:: eapply {+, @term with @bindings_list} in @ident as @intro_pattern. + .. tacv:: simple apply @term in @ident - This works as :tacn:`apply ... in ... as` but using ``eapply``. + This behaves like :tacn:`apply ... in` but it reasons modulo conversion + only on subterms that contain no variables to instantiate. For instance, + if :g:`id := fun x:nat => x` and :g:`H: forall y, id y = y -> True` and + :g:`H0 : O = O` then :g:`simple apply H in H0` does not succeed because it + would require the conversion of :g:`id ?x` and :g:`O` where :g:`?x` is + an existential variable to instantiate. + Tactic :n:`simple apply @term in @ident` does not + either traverse tuples as :n:`apply @term in @ident` does. -.. tacv:: simple apply @term in @ident + .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} + {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} - This behaves like :tacn:`apply ... in` but it reasons modulo conversion only - on subterms that contain no variables to instantiate. For instance, if - :g:`id := fun x:nat => x` and :g:`H: forall y, id y = y -> True` and - :g:`H0 : O = O` then ``simple apply H in H0`` does not succeed because it - would require the conversion of :g:`id ?x` and :g:`O` where :g:`?x` is - an existential variable to instantiate. Tactic :n:`simple apply @term in @ident` does not - either traverse tuples as :n:`apply @term in @ident` does. - -.. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} -.. tacv:: {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} - - This summarizes the different syntactic variants of :n:`apply @term in @ident` - and :n:`eapply @term in @ident`. + This summarizes the different syntactic variants of :n:`apply @term in @ident` + and :n:`eapply @term in @ident`. .. tacn:: constructor @num :name: constructor This tactic applies to a goal such that its conclusion is an inductive - type (say :g:`I`). The argument :n:`@num` must be less or equal to the - numbers of constructor(s) of :g:`I`. Let :g:`c`:sub:`i` be the i-th - constructor of :g:`I`, then ``constructor i`` is equivalent to - ``intros; apply c``:sub:`i`. + type (say :g:`I`). The argument :token:`num` must be less or equal to the + numbers of constructor(s) of :g:`I`. Let :n:`c__i` be the i-th + constructor of :g:`I`, then :g:`constructor i` is equivalent to + :n:`intros; apply c__i`. -.. exn:: Not an inductive product. -.. exn:: Not enough constructors. + .. exn:: Not an inductive product. + :undocumented: -.. tacv:: constructor + .. exn:: Not enough constructors. + :undocumented: - This tries :g:`constructor`:sub:`1` then :g:`constructor`:sub:`2`, ..., then - :g:`constructor`:sub:`n` where `n` is the number of constructors of the head - of the goal. + .. tacv:: constructor -.. tacv:: constructor @num with @bindings_list + This tries :g:`constructor 1` then :g:`constructor 2`, ..., then + :g:`constructor n` where ``n`` is the number of constructors of the head + of the goal. - Let ``c`` be the i-th constructor of :g:`I`, then - :n:`constructor i with @bindings_list` is equivalent to - :n:`intros; apply c with @bindings_list`. + .. tacv:: constructor @num with @bindings_list - .. warn:: - The terms in the @bindings_list are checked in the context where constructor is executed and not in the context where @apply is executed (the introductions are not taken into account). + Let ``c`` be the i-th constructor of :g:`I`, then + :n:`constructor i with @bindings_list` is equivalent to + :n:`intros; apply c with @bindings_list`. -.. tacv:: split - :name: split - - This applies only if :g:`I` has a single constructor. It is then - equivalent to :n:`constructor 1.`. It is typically used in the case of a - conjunction :g:`A` :math:`\wedge` :g:`B`. - -.. exn:: Not an inductive goal with 1 constructor - -.. tacv:: exists @val - :name: exists - - This applies only if :g:`I` has a single constructor. It is then equivalent - to :n:`intros; constructor 1 with @bindings_list.` It is typically used in - the case of an existential quantification :math:`\exists`:g:`x, P(x).` - -.. exn:: Not an inductive goal with 1 constructor. - -.. tacv:: exists @bindings_list + .. warning:: - This iteratively applies :n:`exists @bindings_list`. + The terms in the :token:`bindings_list` are checked in the context + where constructor is executed and not in the context where :tacn:`apply` + is executed (the introductions are not taken into account). -.. tacv:: left - :name: left + .. tacv:: split {? with @bindings_list } + :name: split -.. tacv:: right - :name: right + This applies only if :g:`I` has a single constructor. It is then + equivalent to :n:`constructor 1 {? with @bindings_list }`. It is + typically used in the case of a conjunction :math:`A \wedge B`. - These tactics apply only if :g:`I` has two constructors, for - instance in the case of a disjunction :g:`A` :math:`\vee` :g:`B`. - Then, they are respectively equivalent to ``constructor 1`` and - ``constructor 2``. + .. tacv:: exists @bindings_list + :name: exists -.. exn:: Not an inductive goal with 2 constructors. + This applies only if :g:`I` has a single constructor. It is then equivalent + to :n:`intros; constructor 1 with @bindings_list.` It is typically used in + the case of an existential quantification :math:`\exists x, P(x).` -.. tacv:: left with @bindings_list -.. tacv:: right with @bindings_list -.. tacv:: split with @bindings_list + .. tacv:: exists {+, @bindings_list } - As soon as the inductive type has the right number of constructors, these - expressions are equivalent to calling :n:`constructor i with @bindings_list` - for the appropriate ``i``. + This iteratively applies :n:`exists @bindings_list`. -.. tacv:: econstructor - :name: econstructor + .. exn:: Not an inductive goal with 1 constructor. + :undocumented: -.. tacv:: eexists - :name: eexists + .. tacv:: left {? with @bindings_list } + right {? with @bindings_list } + :name: left; right -.. tacv:: esplit - :name: esplit + These tactics apply only if :g:`I` has two constructors, for + instance in the case of a disjunction :math:`A \vee B`. + Then, they are respectively equivalent to + :n:`constructor 1 {? with @bindings_list }` and + :n:`constructor 2 {? with @bindings_list }`. -.. tacv:: eleft - :name: eleft + .. exn:: Not an inductive goal with 2 constructors. -.. tacv:: eright - :name: eright + .. tacv:: econstructor + eexists + esplit + eleft + eright + :name: econstructor; eexists; esplit; eleft; eright - These tactics and their variants behave like :tacn:`constructor`, - :tacn:`exists`, :tacn:`split`, :tacn:`left`, :tacn:`right` and their variants - but they introduce existential variables instead of failing when the - instantiation of a variable cannot be found (cf. :tacn:`eapply` and - :tacn:`apply`). + These tactics and their variants behave like :tacn:`constructor`, + :tacn:`exists`, :tacn:`split`, :tacn:`left`, :tacn:`right` and their + variants but they introduce existential variables instead of failing + when the instantiation of a variable cannot be found + (cf. :tacn:`eapply` and :tacn:`apply`). .. _managingthelocalcontext: @@ -621,101 +612,107 @@ Managing the local context .. tacn:: intro :name: intro -This tactic applies to a goal that is either a product or starts with a let -binder. If the goal is a product, the tactic implements the "Lam" rule given in -:ref:`Typing-rules` [1]_. If the goal starts with a let binder, then the -tactic implements a mix of the "Let" and "Conv". + This tactic applies to a goal that is either a product or starts with a + let-binder. If the goal is a product, the tactic implements the "Lam" rule + given in :ref:`Typing-rules` [1]_. If the goal starts with a let-binder, + then the tactic implements a mix of the "Let" and "Conv". -If the current goal is a dependent product :g:`forall x:T, U` (resp -:g:`let x:=t in U`) then ``intro`` puts :g:`x:T` (resp :g:`x:=t`) in the local -context. The new subgoal is :g:`U`. + If the current goal is a dependent product :g:`forall x:T, U` + (resp :g:`let x:=t in U`) then :tacn:`intro` puts :g:`x:T` (resp :g:`x:=t`) + in the local context. The new subgoal is :g:`U`. -If the goal is a non-dependent product :g:`T`:math:`\rightarrow`:g:`U`, then it -puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or -:g:`Prop`) or :g:`Xn:T` (if the type of :g:`T` is :g:`Type`). The optional index -``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the -new subgoal is :g:`U`. + If the goal is a non-dependent product :math:`T \rightarrow U`, then it + puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` + or :g:`Prop`) or :g:`Xn:T` (if the type of :g:`T` is :g:`Type`). + The optional index ``n`` is such that ``Hn`` or ``Xn`` is a fresh + identifier. In both cases, the new subgoal is :g:`U`. -If the goal is an existential variable, ``intro`` forces the resolution of the -existential variable into a dependent product :math:`forall`:g:`x:?X, ?Y`, puts -:g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal allowed to -depend on :g:`x`. + If the goal is an existential variable, :tacn:`intro` forces the resolution + of the existential variable into a dependent product :math:`\forall`\ :g:`x:?X, ?Y`, + puts :g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal + allowed to depend on :g:`x`. -the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can -be applied or the goal is not head-reducible. + The tactic :tacn:`intro` applies the tactic :tacn:`hnf` + until :tacn:`intro` can be applied or the goal is not head-reducible. -.. exn:: No product even after head-reduction. -.. exn:: @ident is already used. + .. exn:: No product even after head-reduction. + :undocumented: -.. tacv:: intros - :name: intros + .. tacv:: intro @ident - This repeats ``intro`` until it meets the head-constant. It never - reduces head-constants and it never fails. + This applies :tacn:`intro` but forces :token:`ident` to be the name of + the introduced hypothesis. -.. tacn:: intro @ident + .. exn:: @ident is already used. + :undocumented: - This applies ``intro`` but forces :n:`@ident` to be the name of the - introduced hypothesis. + .. note:: -.. exn:: Name @ident is already used. + If a name used by intro hides the base name of a global constant then + the latter can still be referred to by a qualified name + (see :ref:`Qualified-names`). -.. note:: If a name used by intro hides the base name of a global - constant then the latter can still be referred to by a qualified name - (see :ref:`Qualified-names`). -.. tacv:: intros {+ @ident}. + .. tacv:: intros + :name: intros - This is equivalent to the composed tactic - :n:`intro @ident; ... ; intro @ident`. More generally, the ``intros`` tactic - takes a pattern as argument in order to introduce names for components - of an inductive definition or to clear introduced hypotheses. This is - explained in :ref:`Managingthelocalcontext`. + This repeats :tacn:`intro` until it meets the head-constant. It never + reduces head-constants and it never fails. -.. tacv:: intros until @ident + .. tacv:: intros {+ @ident}. - This repeats intro until it meets a premise of the goal having form - `(@ident:term)` and discharges the variable named `ident` of the current - goal. + This is equivalent to the composed tactic :n:`intro @ident; ... ; intro @ident`. -.. exn:: No such hypothesis in current goal. + .. tacv:: intros until @ident -.. tacv:: intros until @num + This repeats intro until it meets a premise of the goal having the + form :n:`(@ident : @type)` and discharges the variable + named :token:`ident` of the current goal. - This repeats intro until the `num`-th non-dependent product. For instance, - on the subgoal :g:`forall x y:nat, x=y -> y=x` the tactic - :n:`intros until 1` is equivalent to :n:`intros x y H`, as :g:`x=y -> y=x` - is the first non-dependent product. And on the subgoal :g:`forall x y - z:nat, x=y -> y=x` the tactic :n:`intros until 1` is equivalent to - :n:`intros x y z` as the product on :g:`z` can be rewritten as a - non-dependent product: :g:`forall x y:nat, nat -> x=y -> y=x` + .. exn:: No such hypothesis in current goal. + :undocumented: -.. exn:: No such hypothesis in current goal. + .. tacv:: intros until @num - This happens when `num` is 0 or is greater than the number of non-dependent - products of the goal. + This repeats :tacn:`intro` until the :token:`num`\-th non-dependent + product. -.. tacv:: intro after @ident -.. tacv:: intro before @ident -.. tacv:: intro at top -.. tacv:: intro at bottom + .. example:: - These tactics apply :n:`intro` and move the freshly introduced hypothesis - respectively after the hypothesis :n:`@ident`, before the hypothesis - :n:`@ident`, at the top of the local context, or at the bottom of the local - context. All hypotheses on which the new hypothesis depends are moved - too so as to respect the order of dependencies between hypotheses. - Note that :n:`intro at bottom` is a synonym for :n:`intro` with no argument. + On the subgoal :g:`forall x y : nat, x = y -> y = x` the + tactic :n:`intros until 1` is equivalent to :n:`intros x y H`, + as :g:`x = y -> y = x` is the first non-dependent product. -.. exn:: No such hypothesis: @ident. + On the subgoal :g:`forall x y z : nat, x = y -> y = x` the + tactic :n:`intros until 1` is equivalent to :n:`intros x y z` + as the product on :g:`z` can be rewritten as a non-dependent + product: :g:`forall x y : nat, nat -> x = y -> y = x`. -.. tacv:: intro @ident after @ident -.. tacv:: intro @ident before @ident -.. tacv:: intro @ident at top -.. tacv:: intro @ident at bottom + .. exn:: No such hypothesis in current goal. - These tactics behave as previously but naming the introduced hypothesis - :n:`@ident`. It is equivalent to :n:`intro @ident` followed by the - appropriate call to ``move`` (see :tacn:`move ... after ...`). + This happens when :token:`num` is 0 or is greater than the number of + non-dependent products of the goal. + + .. tacv:: intro {? @ident__1 } after @ident__2 + intro {? @ident__1 } before @ident__2 + intro {? @ident__1 } at top + intro {? @ident__1 } at bottom + + These tactics apply :n:`intro {? @ident__1}` and move the freshly + introduced hypothesis respectively after the hypothesis :n:`@ident__2`, + before the hypothesis :n:`@ident__2`, at the top of the local context, + or at the bottom of the local context. All hypotheses on which the new + hypothesis depends are moved too so as to respect the order of + dependencies between hypotheses. It is equivalent to :n:`intro {? @ident__1 }` + followed by the appropriate call to :tacn:`move ... after ...`, + :tacn:`move ... before ...`, :tacn:`move ... at top`, + or :tacn:`move ... at bottom`. + + .. note:: + + :n:`intro at bottom` is a synonym for :n:`intro` with no argument. + + .. exn:: No such hypothesis: @ident. + :undocumented: .. tacn:: intros @intro_pattern_list :name: intros ... @@ -764,24 +761,22 @@ be applied or the goal is not head-reducible. :n:`intros p` is defined inductively over the structure of the introduction pattern :n:`p`: -Introduction on :n:`?` performs the introduction, and lets Coq choose a fresh -name for the variable; - -Introduction on :n:`?ident` performs the introduction, and lets Coq choose a -fresh name for the variable based on :n:`@ident`; + Introduction on :n:`?` performs the introduction, and lets Coq choose a fresh + name for the variable; -Introduction on :n:`@ident` behaves as described in :tacn:`intro` + Introduction on :n:`?@ident` performs the introduction, and lets Coq choose a + fresh name for the variable based on :n:`@ident`; -Introduction over a disjunction of list of patterns -:n:`[@intro_pattern_list | ... | @intro_pattern_list ]` expects the product -to be over an inductive type whose number of constructors is `n` (or more -generally over a type of conclusion an inductive type built from `n` -constructors, e.g. :g:`C -> A\/B` with `n=2` since :g:`A\/B` has `2` -constructors): it destructs the introduced hypothesis as :n:`destruct` (see -:tacn:`destruct`) would and applies on each generated subgoal the -corresponding tactic; + Introduction on :n:`@ident` behaves as described in :tacn:`intro` -.. tacv:: intros @intro_pattern_list + Introduction over a disjunction of list of patterns + :n:`[@intro_pattern_list | ... | @intro_pattern_list ]` expects the product + to be over an inductive type whose number of constructors is `n` (or more + generally over a type of conclusion an inductive type built from `n` + constructors, e.g. :g:`C -> A\/B` with `n=2` since :g:`A\/B` has `2` + constructors): it destructs the introduced hypothesis as :n:`destruct` (see + :tacn:`destruct`) would and applies on each generated subgoal the + corresponding tactic; The introduction patterns in :n:`@intro_pattern_list` are expected to consume no more than the number of arguments of the `i`-th constructor. If it @@ -790,74 +785,75 @@ corresponding tactic; list of patterns :n:`[ | ] H` applied on goal :g:`forall x:nat, x=0 -> 0=x` behaves the same as the list of patterns :n:`[ | ? ] H`); -Introduction over a conjunction of patterns :n:`({+, p})` expects -the goal to be a product over an inductive type :g:`I` with a single -constructor that itself has at least `n` arguments: It performs a case -analysis over the hypothesis, as :n:`destruct` would, and applies the -patterns :n:`{+ p}` to the arguments of the constructor of :g:`I` (observe -that :n:`({+ p})` is an alternative notation for :n:`[{+ p}]`); - -Introduction via :n:`({+& p})` is a shortcut for introduction via -:n:`(p,( ... ,( ..., p ) ... ))`; it expects the hypothesis to be a sequence of -right-associative binary inductive constructors such as :g:`conj` or -:g:`ex_intro`; for instance, an hypothesis with type -:g:`A /\(exists x, B /\ C /\ D)` can be introduced via pattern -:n:`(a & x & b & c & d)`; - -If the product is over an equality type, then a pattern of the form -:n:`[= {+ p}]` applies either :tacn:`injection` or :tacn:`discriminate` -instead of :tacn:`destruct`; if :tacn:`injection` is applicable, the patterns -:n:`{+, p}` are used on the hypotheses generated by :tacn:`injection`; if the -number of patterns is smaller than the number of hypotheses generated, the -pattern :n:`?` is used to complete the list; - -.. tacv:: introduction over -> -.. tacv:: introduction over <- - + Introduction over a conjunction of patterns :n:`({+, p})` expects + the goal to be a product over an inductive type :g:`I` with a single + constructor that itself has at least `n` arguments: It performs a case + analysis over the hypothesis, as :n:`destruct` would, and applies the + patterns :n:`{+ p}` to the arguments of the constructor of :g:`I` (observe + that :n:`({+ p})` is an alternative notation for :n:`[{+ p}]`); + + Introduction via :n:`({+& p})` is a shortcut for introduction via + :n:`(p,( ... ,( ..., p ) ... ))`; it expects the hypothesis to be a sequence of + right-associative binary inductive constructors such as :g:`conj` or + :g:`ex_intro`; for instance, a hypothesis with type + :g:`A /\(exists x, B /\ C /\ D)` can be introduced via pattern + :n:`(a & x & b & c & d)`; + + If the product is over an equality type, then a pattern of the form + :n:`[= {+ p}]` applies either :tacn:`injection` or :tacn:`discriminate` + instead of :tacn:`destruct`; if :tacn:`injection` is applicable, the patterns + :n:`{+, p}` are used on the hypotheses generated by :tacn:`injection`; if the + number of patterns is smaller than the number of hypotheses generated, the + pattern :n:`?` is used to complete the list. + + Introduction over ``->`` (respectively over ``<-``) expects the hypothesis to be an equality and the right-hand-side (respectively the left-hand-side) is replaced by the left-hand-side (respectively the right-hand-side) in the conclusion of the goal; the hypothesis itself is erased; if the term to substitute is a variable, it - is substituted also in the context of goal and the variable is removed too; + is substituted also in the context of goal and the variable is removed too. -Introduction over a pattern :n:`p{+ %term}` first applies :n:`{+ term}` -on the hypothesis to be introduced (as in :n:`apply {+, term}`) prior to the -application of the introduction pattern :n:`p`; + Introduction over a pattern :n:`p{+ %term}` first applies :n:`{+ term}` + on the hypothesis to be introduced (as in :n:`apply {+, term}`) prior to the + application of the introduction pattern :n:`p`; -Introduction on the wildcard depends on whether the product is dependent or not: -in the non-dependent case, it erases the corresponding hypothesis (i.e. it -behaves as an :tacn:`intro` followed by a :tacn:`clear`) while in the -dependent case, it succeeds and erases the variable only if the wildcard is part -of a more complex list of introduction patterns that also erases the hypotheses -depending on this variable; + Introduction on the wildcard depends on whether the product is dependent or not: + in the non-dependent case, it erases the corresponding hypothesis (i.e. it + behaves as an :tacn:`intro` followed by a :tacn:`clear`) while in the + dependent case, it succeeds and erases the variable only if the wildcard is part + of a more complex list of introduction patterns that also erases the hypotheses + depending on this variable; -Introduction over :n:`*` introduces all forthcoming quantified variables -appearing in a row; introduction over :n:`**` introduces all forthcoming -quantified variables or hypotheses until the goal is not any more a -quantification or an implication. + Introduction over :n:`*` introduces all forthcoming quantified variables + appearing in a row; introduction over :n:`**` introduces all forthcoming + quantified variables or hypotheses until the goal is not any more a + quantification or an implication. -.. example:: - .. coqtop:: all + .. example:: + + .. coqtop:: reset all - Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. - intros * [a | (_,c)] f. + Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. + intros * [a | (_,c)] f. .. note:: + :n:`intros {+ p}` is not equivalent to :n:`intros p; ... ; intros p` for the following reason: If one of the :n:`p` is a wildcard pattern, it might succeed in the first case because the further hypotheses it - depends in are eventually erased too while it might fail in the second + depends on are eventually erased too while it might fail in the second case because of dependencies in hypotheses which are not yet introduced (and a fortiori not yet erased). .. note:: + In :n:`intros @intro_pattern_list`, if the last introduction pattern is a disjunctive or conjunctive pattern :n:`[{+| @intro_pattern_list}]`, the completion of :n:`@intro_pattern_list` so that all the arguments of the i-th constructors of the corresponding inductive type are introduced can be controlled with the following option: - .. opt:: Bracketing Last Introduction Pattern + .. flag:: Bracketing Last Introduction Pattern Force completion, if needed, when the last introduction pattern is a disjunctive or conjunctive pattern (on by default). @@ -869,38 +865,42 @@ quantification or an implication. the current goal. As a consequence, :n:`@ident` is no more displayed and no more usable in the proof development. -.. exn:: No such hypothesis. + .. exn:: No such hypothesis. + :undocumented: -.. exn:: @ident is used in the conclusion. + .. exn:: @ident is used in the conclusion. + :undocumented: -.. exn:: @ident is used in the hypothesis @ident. + .. exn:: @ident is used in the hypothesis @ident. + :undocumented: -.. tacv:: clear {+ @ident} + .. tacv:: clear {+ @ident} - This is equivalent to :n:`clear @ident. ... clear @ident.` + This is equivalent to :n:`clear @ident. ... clear @ident.` -.. tacv:: clear - {+ @ident} + .. tacv:: clear - {+ @ident} - This tactic clears all the hypotheses except the ones depending in the - hypotheses named :n:`{+ @ident}` and in the goal. + This variant clears all the hypotheses except the ones depending in the + hypotheses named :n:`{+ @ident}` and in the goal. -.. tacv:: clear + .. tacv:: clear - This tactic clears all the hypotheses except the ones the goal depends on. + This variants clears all the hypotheses except the ones the goal depends on. -.. tacv:: clear dependent @ident + .. tacv:: clear dependent @ident - This clears the hypothesis :n:`@ident` and all the hypotheses that depend on - it. + This clears the hypothesis :token:`ident` and all the hypotheses that + depend on it. -.. tacv:: clearbody {+ @ident} - :name: clearbody + .. tacv:: clearbody {+ @ident} + :name: clearbody - This tactic expects :n:`{+ @ident}` to be local definitions and clears their - respective bodies. - In other words, it turns the given definitions into assumptions. + This tactic expects :n:`{+ @ident}` to be local definitions and clears + their respective bodies. + In other words, it turns the given definitions into assumptions. -.. exn:: @ident is not a local definition. + .. exn:: @ident is not a local definition. + :undocumented: .. tacn:: revert {+ @ident} :name: revert @@ -909,171 +909,184 @@ quantification or an implication. (possibly defined) to the goal, if this respects dependencies. This tactic is the inverse of :tacn:`intro`. -.. exn:: No such hypothesis. + .. exn:: No such hypothesis. + :undocumented: -.. exn:: @ident is used in the hypothesis @ident. + .. exn:: @ident__1 is used in the hypothesis @ident__2. + :undocumented: -.. tacn:: revert dependent @ident + .. tacv:: revert dependent @ident + :name: revert dependent - This moves to the goal the hypothesis :n:`@ident` and all the hypotheses that - depend on it. + This moves to the goal the hypothesis :token:`ident` and all the + hypotheses that depend on it. -.. tacn:: move @ident after @ident +.. tacn:: move @ident__1 after @ident__2 :name: move ... after ... - This moves the hypothesis named :n:`@ident` in the local context after the - hypothesis named :n:`@ident`, where “after” is in reference to the + This moves the hypothesis named :n:`@ident__1` in the local context after + the hypothesis named :n:`@ident__2`, where “after” is in reference to the direction of the move. The proof term is not changed. - If :n:`@ident` comes before :n:`@ident` in the order of dependencies, then - all the hypotheses between :n:`@ident` and :n:`ident@` that (possibly - indirectly) depend on :n:`@ident` are moved too, and all of them are thus - moved after :n:`@ident` in the order of dependencies. + If :n:`@ident__1` comes before :n:`@ident__2` in the order of dependencies, + then all the hypotheses between :n:`@ident__1` and :n:`@ident__2` that + (possibly indirectly) depend on :n:`@ident__1` are moved too, and all of + them are thus moved after :n:`@ident__2` in the order of dependencies. - If :n:`@ident` comes after :n:`@ident` in the order of dependencies, then all - the hypotheses between :n:`@ident` and :n:`@ident` that (possibly indirectly) - occur in the type of :n:`@ident` are moved too, and all of them are thus - moved before :n:`@ident` in the order of dependencies. + If :n:`@ident__1` comes after :n:`@ident__2` in the order of dependencies, + then all the hypotheses between :n:`@ident__1` and :n:`@ident__2` that + (possibly indirectly) occur in the type of :n:`@ident__1` are moved too, + and all of them are thus moved before :n:`@ident__2` in the order of + dependencies. -.. tacv:: move @ident before @ident + .. tacv:: move @ident__1 before @ident__2 + :name: move ... before ... - This moves :n:`@ident` towards and just before the hypothesis named - :n:`@ident`. As for :tacn:`move ... after ...`, dependencies over - :n:`@ident` (when :n:`@ident` comes before :n:`@ident` in the order of - dependencies) or in the type of :n:`@ident` (when :n:`@ident` comes after - :n:`@ident` in the order of dependencies) are moved too. + This moves :n:`@ident__1` towards and just before the hypothesis + named :n:`@ident__2`. As for :tacn:`move ... after ...`, dependencies + over :n:`@ident__1` (when :n:`@ident__1` comes before :n:`@ident__2` in + the order of dependencies) or in the type of :n:`@ident__1` + (when :n:`@ident__1` comes after :n:`@ident__2` in the order of + dependencies) are moved too. -.. tacv:: move @ident at top + .. tacv:: move @ident at top + :name: move ... at top - This moves :n:`@ident` at the top of the local context (at the beginning of - the context). + This moves :token:`ident` at the top of the local context (at the beginning + of the context). -.. tacv:: move @ident at bottom + .. tacv:: move @ident at bottom + :name: move ... at bottom - This moves ident at the bottom of the local context (at the end of the - context). + This moves :token:`ident` at the bottom of the local context (at the end of + the context). -.. exn:: No such hypothesis. -.. exn:: Cannot move @ident after @ident : it occurs in the type of @ident. -.. exn:: Cannot move @ident after @ident : it depends on @ident. + .. exn:: No such hypothesis. + :undocumented: -.. example:: - .. coqtop:: all + .. exn:: Cannot move @ident__1 after @ident__2: it occurs in the type of @ident__2. + :undocumented: + + .. exn:: Cannot move @ident__1 after @ident__2: it depends on @ident__2. + :undocumented: - Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x. - intros x H z y H0. - move x after H0. - Undo. - move x before H0. - Undo. - move H0 after H. - Undo. - move H0 before H. - -.. tacn:: rename @ident into @ident + .. example:: + + .. coqtop:: reset all + + Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x. + intros x H z y H0. + move x after H0. + Undo. + move x before H0. + Undo. + move H0 after H. + Undo. + move H0 before H. + +.. tacn:: rename @ident__1 into @ident__2 :name: rename -This renames hypothesis :n:`@ident` into :n:`@ident` in the current context. -The name of the hypothesis in the proof-term, however, is left unchanged. + This renames hypothesis :n:`@ident__1` into :n:`@ident__2` in the current + context. The name of the hypothesis in the proof-term, however, is left + unchanged. -.. tacv:: rename {+, @ident into @ident} + .. tacv:: rename {+, @ident__i into @ident__j} - This renames the variables :n:`@ident` into :n:`@ident` in parallel. In - particular, the target identifiers may contain identifiers that exist in the - source context, as long as the latter are also renamed by the same tactic. + This renames the variables :n:`@ident__i` into :n:`@ident__j` in parallel. + In particular, the target identifiers may contain identifiers that exist in + the source context, as long as the latter are also renamed by the same + tactic. -.. exn:: No such hypothesis. -.. exn:: @ident is already used. + .. exn:: No such hypothesis. + :undocumented: + + .. exn:: @ident is already used. + :undocumented: .. tacn:: set (@ident := @term) :name: set - This replaces :n:`@term` by :n:`@ident` in the conclusion of the current goal - and adds the new definition :g:`ident := term` to the local context. - - If :n:`@term` has holes (i.e. subexpressions of the form “`_`”), the tactic - first checks that all subterms matching the pattern are compatible before - doing the replacement using the leftmost subterm matching the pattern. + This replaces :token:`term` by :token:`ident` in the conclusion of the + current goal and adds the new definition :n:`@ident := @term` to the + local context. -.. exn:: The variable @ident is already defined. + If :token:`term` has holes (i.e. subexpressions of the form “`_`”), the + tactic first checks that all subterms matching the pattern are compatible + before doing the replacement using the leftmost subterm matching the + pattern. -.. tacv:: set (@ident := @term ) in @goal_occurrences + .. exn:: The variable @ident is already defined. + :undocumented: - This notation allows specifying which occurrences of :n:`@term` have to be - substituted in the context. The :n:`in @goal_occurrences` clause is an - occurrence clause whose syntax and behavior are described in - :ref:`goal occurences <occurencessets>`. + .. tacv:: set (@ident := @term) in @goal_occurrences -.. tacv:: set (@ident {+ @binder} := @term ) + This notation allows specifying which occurrences of :token:`term` have + to be substituted in the context. The :n:`in @goal_occurrences` clause + is an occurrence clause whose syntax and behavior are described in + :ref:`goal occurences <occurencessets>`. - This is equivalent to :n:`set (@ident := funbinder {+ binder} => @term )`. + .. tacv:: set (@ident @binders := @term) {? in @goal_occurrences } -.. tacv:: set term - This behaves as :n:`set(@ident := @term)` but :n:`@ident` is generated by - Coq. This variant also supports an occurrence clause. + This is equivalent to :n:`set (@ident := fun @binders => @term) {? in @goal_occurrences }`. -.. tacv:: set (@ident {+ @binder} := @term) in @goal_occurrences -.. tacv:: set @term in @goal_occurrences + .. tacv:: set @term {? in @goal_occurrences } - These are the general forms that combine the previous possibilities. + This behaves as :n:`set (@ident := @term) {? in @goal_occurrences }` + but :token:`ident` is generated by Coq. -.. tacv:: eset (@ident {+ @binder} := @term ) in @goal_occurrences -.. tacv:: eset @term in @goal_occurrences - :name: eset + .. tacv:: eset (@ident {? @binders } := @term) {? in @goal_occurrences } + eset @term {? in @goal_occurrences } + :name: eset; _ - While the different variants of :tacn:`set` expect that no existential - variables are generated by the tactic, :n:`eset` removes this constraint. In - practice, this is relevant only when :n:`eset` is used as a synonym of - :tacn:`epose`, i.e. when the :`@term` does not occur in the goal. + While the different variants of :tacn:`set` expect that no existential + variables are generated by the tactic, :tacn:`eset` removes this + constraint. In practice, this is relevant only when :tacn:`eset` is + used as a synonym of :tacn:`epose`, i.e. when the :token:`term` does + not occur in the goal. -.. tacv:: remember @term as @ident +.. tacn:: remember @term as @ident__1 {? eqn:@ident__2 } :name: remember - This behaves as :n:`set (@ident:= @term ) in *` and using a logical + This behaves as :n:`set (@ident__1 := @term) in *`, using a logical (Leibniz’s) equality instead of a local definition. + If :n:`@ident__2` is provided, it will be the name of the new equation. -.. tacv:: remember @term as @ident eqn:@ident - - This behaves as :n:`remember @term as @ident`, except that the name of the - generated equality is also given. - -.. tacv:: remember @term as @ident in @goal_occurrences + .. tacv:: remember @term as @ident__1 {? eqn:@ident__2 } in @goal_occurrences - This is a more general form of :n:`remember` that remembers the occurrences - of term specified by an occurrences set. + This is a more general form of :tacn:`remember` that remembers the + occurrences of :token:`term` specified by an occurrence set. -.. tacv:: eremember @term as @ident -.. tacv:: eremember @term as @ident in @goal_occurrences -.. tacv:: eremember @term as @ident eqn:@ident - :name: eremember + .. tacv:: eremember @term as @ident__1 {? eqn:@ident__2 } {? in @goal_occurrences } + :name: eremember - While the different variants of :n:`remember` expect that no existential - variables are generated by the tactic, :n:`eremember` removes this constraint. + While the different variants of :tacn:`remember` expect that no + existential variables are generated by the tactic, :tacn:`eremember` + removes this constraint. -.. tacv:: pose ( @ident := @term ) +.. tacn:: pose (@ident := @term) :name: pose This adds the local definition :n:`@ident := @term` to the current context without performing any replacement in the goal or in the hypotheses. It is - equivalent to :n:`set ( @ident := @term ) in |-`. + equivalent to :n:`set (@ident := @term) in |-`. -.. tacv:: pose ( @ident {+ @binder} := @term ) + .. tacv:: pose (@ident @binders := @term) - This is equivalent to :n:`pose (@ident := funbinder {+ binder} => @term)`. + This is equivalent to :n:`pose (@ident := fun @binders => @term)`. -.. tacv:: pose @term + .. tacv:: pose @term - This behaves as :n:`pose (@ident := @term )` but :n:`@ident` is generated by - Coq. + This behaves as :n:`pose (@ident := @term)` but :token:`ident` is + generated by Coq. -.. tacv:: epose (@ident := @term ) -.. tacv:: epose (@ident {+ @binder} := @term ) -.. tacv:: epose term - :name: epose + .. tacv:: epose (@ident {? @binders} := @term) + .. tacv:: epose term + :name: epose - While the different variants of :tacn:`pose` expect that no - existential variables are generated by the tactic, epose removes this - constraint. + While the different variants of :tacn:`pose` expect that no + existential variables are generated by the tactic, :tacn:`epose` + removes this constraint. .. tacn:: decompose [{+ @qualid}] @term :name: decompose @@ -1081,24 +1094,30 @@ The name of the hypothesis in the proof-term, however, is left unchanged. This tactic recursively decomposes a complex proposition in order to obtain atomic ones. -.. example:: - .. coqtop:: all + .. example:: - Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C. - intros A B C H; decompose [and or] H; assumption. - Qed. + .. coqtop:: reset all + + Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C. + intros A B C H; decompose [and or] H. + all: assumption. + Qed. + + .. note:: -:n:`decompose` does not work on right-hand sides of implications or products. + :tacn:`decompose` does not work on right-hand sides of implications or + products. -.. tacv:: decompose sum @term + .. tacv:: decompose sum @term - This decomposes sum types (like or). + This decomposes sum types (like :g:`or`). -.. tacv:: decompose record @term + .. tacv:: decompose record @term + + This decomposes record types (inductive types with one constructor, + like :g:`and` and :g:`exists` and those defined with the :cmd:`Record` + command. - This decomposes record types (inductive types with one constructor, like - "and" and "exists" and those defined with the Record macro, see - :ref:`record-types`). .. _controllingtheproofflow: @@ -1252,6 +1271,7 @@ Controlling the proof flow respect to some term. .. example:: + .. coqtop:: reset none Goal forall x y:nat, 0 <= x + y + y. @@ -1276,7 +1296,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. This is equivalent to :n:`generalize @term` but it generalizes only over the specified occurrences of :n:`@term` (counting from left to right on the - expression printed using option :opt:`Printing All`). + expression printed using option :flag:`Printing All`). .. tacv:: generalize @term as @ident @@ -1323,8 +1343,8 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. changes in the goal, its use is strongly discouraged. .. tacv:: instantiate ( @num := @term ) in @ident -.. tacv:: instantiate ( @num := @term ) in ( Value of @ident ) -.. tacv:: instantiate ( @num := @term ) in ( Type of @ident ) +.. tacv:: instantiate ( @num := @term ) in ( value of @ident ) +.. tacv:: instantiate ( @num := @term ) in ( type of @ident ) These allow to refer respectively to existential variables occurring in a hypothesis or in the body or the type of a local definition. @@ -1362,7 +1382,7 @@ goals cannot be closed with :g:`Qed` but only with :g:`Admitted`. :name: contradiction This tactic applies to any goal. The contradiction tactic attempts to - find in the current context (after all intros) an hypothesis that is + find in the current context (after all intros) a hypothesis that is equivalent to an empty inductive type (e.g. :g:`False`), to the negation of a singleton inductive type (e.g. :g:`True` or :g:`x=x`), or two contradictory hypotheses. @@ -1404,94 +1424,101 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) .. tacn:: destruct @term :name: destruct - This tactic applies to any goal. The argument :n:`@term` must be of + This tactic applies to any goal. The argument :token:`term` must be of inductive or co-inductive type and the tactic generates subgoals, one - for each possible form of :n:`@term`, i.e. one for each constructor of the - inductive or co-inductive type. Unlike :n:`induction`, no induction - hypothesis is generated by :n:`destruct`. + for each possible form of :token:`term`, i.e. one for each constructor of the + inductive or co-inductive type. Unlike :tacn:`induction`, no induction + hypothesis is generated by :tacn:`destruct`. - There are special cases: + .. tacv:: destruct @ident - + If :n:`@term` is an identifier :n:`@ident` denoting a quantified variable - of the conclusion of the goal, then :n:`destruct @ident` behaves as - :n:`intros until @ident; destruct @ident`. If :n:`@ident` is not anymore - dependent in the goal after application of :n:`destruct`, it is erased - (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). + If :token:`ident` denotes a quantified variable of the conclusion + of the goal, then :n:`destruct @ident` behaves + as :n:`intros until @ident; destruct @ident`. If :token:`ident` is not + anymore dependent in the goal after application of :tacn:`destruct`, it + is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). - + If term is a num, then destruct num behaves as intros until num - followed by destruct applied to the last introduced hypothesis. + If :token:`ident` is a hypothesis of the context, and :token:`ident` + is not anymore dependent in the goal after application + of :tacn:`destruct`, it is erased (to avoid erasure, use parentheses, as + in :n:`destruct (@ident)`). + + .. tacv:: destruct @num + + :n:`destruct @num` behaves as :n:`intros until @num` + followed by destruct applied to the last introduced hypothesis. .. note:: - For destruction of a numeral, use syntax destruct (num) (not + For destruction of a numeral, use syntax :n:`destruct (@num)` (not very interesting anyway). - + In case term is an hypothesis :n:`@ident` of the context, and :n:`@ident` - is not anymore dependent in the goal after application of :n:`destruct`, it - is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). + .. tacv:: destruct @pattern - + The argument :n:`@term` can also be a pattern of which holes are denoted - by “_”. In this case, the tactic checks that all subterms matching the - pattern in the conclusion and the hypotheses are compatible and - performs case analysis using this subterm. + The argument of :tacn:`destruct` can also be a pattern of which holes are + denoted by “_”. In this case, the tactic checks that all subterms + matching the pattern in the conclusion and the hypotheses are compatible + and performs case analysis using this subterm. -.. tacv:: destruct {+, @term} + .. tacv:: destruct {+, @term} - This is a shortcut for :n:`destruct term; ...; destruct term`. + This is a shortcut for :n:`destruct @term; ...; destruct @term`. -.. tacv:: destruct @term as @disj_conj_intro_pattern + .. tacv:: destruct @term as @disj_conj_intro_pattern - This behaves as :n:`destruct @term` but uses the names in :n:`@intro_pattern` - to name the variables introduced in the context. The :n:`@intro_pattern` must - have the form :n:`[p11 ... p1n | ... | pm1 ... pmn ]` with `m` being the - number of constructors of the type of :n:`@term`. Each variable introduced - by :n:`destruct` in the context of the `i`-th goal gets its name from the - list :n:`pi1 ... pin` in order. If there are not enough names, - :n:`@destruct` invents names for the remaining variables to introduce. More - generally, the :n:`pij` can be any introduction pattern (see - :tacn:`intros`). This provides a concise notation for chaining destruction of - an hypothesis. + This behaves as :n:`destruct @term` but uses the names + in :token:`disj_conj_intro_pattern` to name the variables introduced in the + context. The :token:`disj_conj_intro_pattern` must have the + form :n:`[p11 ... p1n | ... | pm1 ... pmn ]` with ``m`` being the + number of constructors of the type of :token:`term`. Each variable + introduced by :tacn:`destruct` in the context of the ``i``-th goal + gets its name from the list :n:`pi1 ... pin` in order. If there are not + enough names, :tacn:`destruct` invents names for the remaining variables + to introduce. More generally, the :n:`pij` can be any introduction + pattern (see :tacn:`intros`). This provides a concise notation for + chaining destruction of a hypothesis. -.. tacv:: destruct @term eqn:@naming_intro_pattern + .. tacv:: destruct @term eqn:@naming_intro_pattern + :name: destruct ... eqn: - This behaves as :n:`destruct @term` but adds an equation between :n:`@term` - and the value that :n:`@term` takes in each of the possible cases. The name - of the equation is specified by :n:`@naming_intro_pattern` (see - :tacn:`intros`), in particular `?` can be used to let Coq generate a fresh - name. + This behaves as :n:`destruct @term` but adds an equation + between :token:`term` and the value that it takes in each of the + possible cases. The name of the equation is specified + by :token:`naming_intro_pattern` (see :tacn:`intros`), + in particular ``?`` can be used to let Coq generate a fresh name. -.. tacv:: destruct @term with @bindings_list + .. tacv:: destruct @term with @bindings_list - This behaves like :n:`destruct @term` providing explicit instances for the - dependent premises of the type of :n:`@term` (see :ref:`syntax of bindings <bindingslist>`). + This behaves like :n:`destruct @term` providing explicit instances for + the dependent premises of the type of :token:`term`. -.. tacv:: edestruct @term - :name: edestruct + .. tacv:: edestruct @term + :name: edestruct - This tactic behaves like :n:`destruct @term` except that it does not fail if - the instance of a dependent premises of the type of :n:`@term` is not - inferable. Instead, the unresolved instances are left as existential - variables to be inferred later, in the same way as :tacn:`eapply` does. + This tactic behaves like :n:`destruct @term` except that it does not + fail if the instance of a dependent premises of the type + of :token:`term` is not inferable. Instead, the unresolved instances + are left as existential variables to be inferred later, in the same way + as :tacn:`eapply` does. -.. tacv:: destruct @term using @term -.. tacv:: destruct @term using @term with @bindings_list + .. tacv:: destruct @term using @term {? with @bindings_list } - These are synonyms of :n:`induction @term using @term` and - :n:`induction @term using @term with @bindings_list`. + This is synonym of :n:`induction @term using @term {? with @bindings_list }`. -.. tacv:: destruct @term in @goal_occurrences + .. tacv:: destruct @term in @goal_occurrences - This syntax is used for selecting which occurrences of :n:`@term` the case - analysis has to be done on. The :n:`in @goal_occurrences` clause is an - occurrence clause whose syntax and behavior is described in - :ref:`occurences sets <occurencessets>`. + This syntax is used for selecting which occurrences of :token:`term` + the case analysis has to be done on. The :n:`in @goal_occurrences` + clause is an occurrence clause whose syntax and behavior is described + in :ref:`occurences sets <occurencessets>`. -.. tacv:: destruct @term with @bindings_list as @disj_conj_intro_pattern eqn:@naming_intro_pattern using @term with @bindings_list in @goal_occurrences -.. tacv:: edestruct @term with @bindings_list as @disj_conj_intro_pattern eqn:@naming_intro_pattern using @term with @bindings_list in @goal_occurrences + .. tacv:: destruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } + edestruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } - These are the general forms of :n:`destruct` and :n:`edestruct`. They combine - the effects of the `with`, `as`, `eqn:`, `using`, and `in` clauses. + These are the general forms of :tacn:`destruct` and :tacn:`edestruct`. + They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``, + and ``in`` clauses. -.. tacv:: case term +.. tacn:: case term :name: case The tactic :n:`case` is a more basic tactic to perform case analysis without @@ -1523,7 +1550,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) .. tacv:: case_eq @term - The tactic :n:`case_eq` is a variant of the :n:`case` tactic that allow to + The tactic :n:`case_eq` is a variant of the :n:`case` tactic that allows to perform case analysis on a term without completely forgetting its original form. This is done by generating equalities between the original form of the term and the outcomes of the case analysis. @@ -1557,7 +1584,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) For simple induction on a numeral, use syntax induction (num) (not very interesting anyway). - + In case term is an hypothesis :n:`@ident` of the context, and :n:`@ident` + + In case term is a hypothesis :n:`@ident` of the context, and :n:`@ident` is not anymore dependent in the goal after application of :n:`induction`, it is erased (to avoid erasure, use parentheses, as in :n:`induction (@ident)`). @@ -1567,6 +1594,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) performs induction using this subterm. .. example:: + .. coqtop:: reset all Lemma induction_test : forall n:nat, n = n -> n <= n. @@ -1636,6 +1664,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) those are generalized as well in the statement to prove. .. example:: + .. coqtop:: reset all Lemma comm x y : x + y = y + x. @@ -1744,6 +1773,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) still get enough information in the proofs. .. example:: + .. coqtop:: reset all Lemma le_minus : forall n:nat, n < 1 -> n = 0. @@ -1806,9 +1836,10 @@ and an explanation of the underlying technique. following the definition of a function. It makes use of a principle generated by ``Function`` (see :ref:`advanced-recursive-functions`) or ``Functional Scheme`` (see :ref:`functional-scheme`). - Note that this tactic is only available after a + Note that this tactic is only available after a ``Require Import FunInd``. .. example:: + .. coqtop:: reset all Require Import FunInd. @@ -1825,7 +1856,7 @@ and an explanation of the underlying technique. arguments explicitly. .. note:: - Parentheses over :n:`@qualid {+ @term}` are mandatory. + Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped. .. note:: :n:`functional induction (f x1 x2 x3)` is actually a wrapper for @@ -1845,9 +1876,7 @@ and an explanation of the underlying technique. :g:`Fixpoint` or :g:`Definition`. See :ref:`advanced-recursive-functions` for details. -See also: :ref:`advanced-recursive-functions` - :ref:`functional-scheme` - :tacn:`inversion` +.. seealso:: :ref:`advanced-recursive-functions`, :ref:`functional-scheme` and :tacn:`inversion` .. exn:: Cannot find induction information on @qualid. .. exn:: Not the right number of induction arguments. @@ -2008,16 +2037,16 @@ See also: :ref:`advanced-recursive-functions` the number of equalities newly generated. If it is smaller, fresh names are automatically generated to adjust the list of :n:`@intro_pattern` to the number of new equalities. The original equality is erased if it - corresponds to an hypothesis. + corresponds to a hypothesis. - .. opt:: Structural Injection + .. flag:: Structural Injection This option ensure that :n:`injection @term` erases the original hypothesis and leaves the generated equalities in the context rather than putting them as antecedents of the current goal, as if giving :n:`injection @term as` (with an empty list of names). This option is off by default. - .. opt:: Keep Proof Equalities + .. flag:: Keep Proof Equalities By default, :tacn:`injection` only creates new equalities between :n:`@terms` whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special @@ -2049,7 +2078,7 @@ See also: :ref:`advanced-recursive-functions` being processed. By default, no equalities are generated if they relate two proofs (i.e. equalities between :n:`@terms` whose type is in sort :g:`Prop`). This behavior can be turned off by using the option - :opt`Keep Proof Equalities`. + :flag`Keep Proof Equalities`. .. tacv:: inversion @num @@ -2237,7 +2266,7 @@ See also: :ref:`advanced-recursive-functions` 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 prove that the + (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. @@ -2279,8 +2308,8 @@ See also: :ref:`advanced-recursive-functions` 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 - the corresponding @term in constructor form. Neither Inversion nor - Inversion_clear make such a substitution. To have such a behavior we + the corresponding @term in constructor form. Neither :tacn:`inversion` nor + :n:`inversion_clear` do such a substitution. To have such a behavior we use the dependent inversion tactics: .. coqtop:: all @@ -2559,7 +2588,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``. - .. opt:: Regular Subst Tactic + .. flag:: Regular Subst Tactic This option controls the behavior of :tacn:`subst`. When it is activated (it is by default), :tacn:`subst` also deals with the following corner cases: @@ -2598,7 +2627,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. Adds :n:`@term` to the database used by :tacn:`stepl`. - The tactic is especially useful for parametric setoids which are not accepted + This tactic is especially useful for parametric setoids which are not accepted as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see :ref:`Generalizedrewriting`). @@ -2694,7 +2723,7 @@ the conversion in hypotheses :n:`{+ @ident}`. :math:`\beta` (reduction of functional application), :math:`\delta` (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`), :math:`\iota` (reduction of - pattern-matching over a constructed term, and unfolding of :g:`fix` and + pattern matching over a constructed term, and unfolding of :g:`fix` and :g:`cofix` expressions) and :math:`\zeta` (contraction of local definitions), the flags are either ``beta``, ``delta``, ``match``, ``fix``, ``cofix``, ``iota`` or ``zeta``. The ``iota`` flag is a shorthand for ``match``, ``fix`` @@ -2708,7 +2737,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Normalization according to the flags is done by first evaluating the head of the expression into a *weak-head* normal form, i.e. until the - evaluation is bloked by a variable (or an opaque constant, or an + evaluation is blocked by a variable (or an opaque constant, or an axiom), as e.g. in :g:`x u1 ... un` , or :g:`match x with ... end`, or :g:`(fix f x {struct x} := ...) x`, or is a constructed form (a :math:`\lambda`-expression, a constructor, a cofixpoint, an inductive type, a @@ -2777,12 +2806,13 @@ the conversion in hypotheses :n:`{+ @ident}`. compilation cost is higher, so it is worth using only for intensive computations. - .. opt:: NativeCompute Profiling + .. flag:: NativeCompute Profiling On Linux, if you have the ``perf`` profiler installed, this option makes it possible to profile ``native_compute`` evaluations. - .. opt:: NativeCompute Profile Filename + .. opt:: NativeCompute Profile Filename @string + :name: NativeCompute Profile Filename This option specifies the profile output; the default is ``native_compute_profile.data``. The actual filename used @@ -2793,7 +2823,7 @@ the conversion in hypotheses :n:`{+ @ident}`. on the profile file to see the results. Consult the ``perf`` documentation for more details. -.. opt:: Debug Cbv +.. flag:: Debug Cbv This option makes :tacn:`cbv` (and its derivative :tacn:`compute`) print information about the constants it encounters and the unfolding decisions it @@ -2804,14 +2834,18 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic applies to a goal that has the form:: - forall (x:T1) ... (xk:Tk), t + forall (x:T1) ... (xk:Tk), T - with :g:`t` :math:`\beta`:math:`\iota`:math:`\zeta`-reducing to :g:`c t`:sub:`1` :g:`... t`:sub:`n` and :g:`c` a + with :g:`T` :math:`\beta`:math:`\iota`:math:`\zeta`-reducing to :g:`c t`:sub:`1` :g:`... t`:sub:`n` and :g:`c` a constant. If :g:`c` is transparent then it replaces :g:`c` with its definition (say :g:`t`) and then reduces :g:`(t t`:sub:`1` :g:`... t`:sub:`n` :g:`)` according to :math:`\beta`:math:`\iota`:math:`\zeta`-reduction rules. .. exn:: Not reducible. + :undocumented: + +.. exn:: No head constant to reduce. + :undocumented: .. tacn:: hnf :name: hnf @@ -2821,8 +2855,7 @@ the conversion in hypotheses :n:`{+ @ident}`. reduces the head of the goal until it becomes a product or an irreducible term. All inner :math:`\beta`:math:`\iota`-redexes are also reduced. - Example: The term :g:`forall n:nat, (plus (S n) (S n))` is not reduced by - :n:`hnf`. + Example: The term :g:`fun n : nat => S n + S n` is not reduced by :n:`hnf`. .. note:: The :math:`\delta` rule only applies to transparent constants (see :ref:`vernac-controlling-the-reduction-strategies` @@ -2853,6 +2886,7 @@ the conversion in hypotheses :n:`{+ @ident}`. + A constant can be marked to be never unfolded by ``cbn`` or ``simpl``: .. example:: + .. coqtop:: all Arguments minus n m : simpl never. @@ -2862,9 +2896,10 @@ the conversion in hypotheses :n:`{+ @ident}`. + A constant can be marked to be unfolded only if applied to enough arguments. The number of arguments required can be specified using the - ``/`` symbol in the arguments list of the ``Arguments`` vernacular command. + ``/`` symbol in the argument list of the :cmd:`Arguments` vernacular command. .. example:: + .. coqtop:: all Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). @@ -2877,6 +2912,7 @@ the conversion in hypotheses :n:`{+ @ident}`. always unfolded. .. example:: + .. coqtop:: all Definition volatile := fun x : nat => x. @@ -2887,6 +2923,7 @@ the conversion in hypotheses :n:`{+ @ident}`. such arguments. .. example:: + .. coqtop:: all Arguments minus !n !m. @@ -2953,7 +2990,7 @@ the conversion in hypotheses :n:`{+ @ident}`. This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). -.. opt:: Debug RAKAM +.. flag:: Debug RAKAM This option makes :tacn:`cbn` print various debugging information. ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. @@ -3030,7 +3067,7 @@ the conversion in hypotheses :n:`{+ @ident}`. For instance, if the current goal :g:`T` is expressible as :math:`\varphi`:g:`(t)` where the notation captures all the instances of :g:`t` in :math:`\varphi`:g:`(t)`, then :n:`pattern t` transforms it into - :g:`(fun x:A =>` :math:`\varphi`:g:`(x)) t`. This command can be used, for + :g:`(fun x:A =>` :math:`\varphi`:g:`(x)) t`. This tactic can be used, for instance, when the tactic ``apply`` fails on matching. .. tacv:: pattern @term at {+ @num} @@ -3072,10 +3109,10 @@ Conversion tactics applied to hypotheses listed in this section. If :n:`@ident` is a local definition, then :n:`@ident` can be replaced by - (Type of :n:`@ident`) to address not the body but the type of the local + (type of :n:`@ident`) to address not the body but the type of the local definition. - Example: :n:`unfold not in (Type of H1) (Type of H3)`. + Example: :n:`unfold not in (type of H1) (type of H3)`. .. exn:: No such hypothesis: @ident. @@ -3160,12 +3197,13 @@ hints of the database named core. The following options enable printing of informative or debug information for the :tacn:`auto` and :tacn:`trivial` tactics: -.. opt:: Info Auto -.. opt:: Debug Auto -.. opt:: Info Trivial -.. opt:: Debug Trivial +.. flag:: Info Auto + Debug Auto + Info Trivial + Debug Trivial + :undocumented: -See also: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` +.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` .. tacn:: eauto :name: eauto @@ -3177,6 +3215,7 @@ where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto` can solve such a goal: .. example:: + .. coqtop:: all Hint Resolve ex_intro. @@ -3192,10 +3231,11 @@ Note that ``ex_intro`` should be declared as a hint. :tacn:`eauto` also obeys the following options: -.. opt:: Info Eauto -.. opt:: Debug Eauto +.. flag:: Info Eauto + Debug Eauto + :undocumented: -See also: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` +.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` .. tacn:: autounfold with {+ @ident} @@ -3216,10 +3256,10 @@ in the given databases. .. tacn:: autorewrite with {+ @ident} :name: autorewrite -This tactic [4]_ carries out rewritings according the rewriting rule +This tactic [4]_ carries out rewritings according to the rewriting rule bases :n:`{+ @ident}`. -Each rewriting rule of a base :n:`@ident` is applied to the main subgoal until +Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until it fails. Once all the rules have been processed, if the main subgoal has progressed (e.g., if it is distinct from the initial main goal) then the rules of this base are processed again. If the main subgoal has not progressed then @@ -3252,10 +3292,10 @@ command. Performs all the rewriting in the clause :n:`@clause`. The clause argument must not contain any ``type of`` nor ``value of``. -See also: :ref:`Hint-Rewrite <hintrewrite>` for feeding the database of lemmas used by -:tacn:`autorewrite`. +.. seealso:: -See also: :tacn:`autorewrite` for examples showing the use of this tactic. + :ref:`Hint-Rewrite <hintrewrite>` for feeding the database of lemmas used by + :tacn:`autorewrite` and :tacn:`autorewrite` for examples showing the use of this tactic. .. tacn:: easy :name: easy @@ -3312,7 +3352,7 @@ automatically created. (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`), making the retrieval more efficient. The legacy implementation (the default one for new databases) uses the DT only on goals without existentials (i.e., :tacn:`auto` - goals), for non-Immediate hints and do not make use of transparency + goals), for non-Immediate hints and does not make use of transparency hints, putting more work on the unification that is run after retrieval (it keeps a list of the lemmas in case the DT is not used). The new implementation enabled by the discriminated option makes use @@ -3496,7 +3536,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is The `emp` regexp does not match any search path while `eps` matches the empty path. During proof search, the path of successive successful hints on a search branch is recorded, as a - list of identifiers for the hints (note Hint Extern’s do not have + list of identifiers for the hints (note that Hint Extern’s do not have an associated identifier). Before applying any hint :n:`@ident` the current path `p` extended with :n:`@ident` is matched against the current cut expression `c` associated to @@ -3527,7 +3567,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. note:: - One can use an ``Extern`` hint with no pattern to do pattern-matching on + One can use an ``Extern`` hint with no pattern to do pattern matching on hypotheses using ``match goal`` with inside the tactic. @@ -3535,15 +3575,14 @@ Hint databases defined in the Coq standard library ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Several hint databases are defined in the Coq standard library. The -actual content of a database is the collection of the hints declared +actual content of a database is the collection of hints declared to belong to this database in each of the various modules currently -loaded. Especially, requiring new modules potentially extend a -database. At Coq startup, only the core database is non empty and can -be used. +loaded. Especially, requiring new modules may extend the database. +At Coq startup, only the core database is nonempty and can be used. :core: This special database is automatically used by ``auto``, except when pseudo-database ``nocore`` is given to ``auto``. The core database - contains only basic lemmas about negation, conjunction, and so on from. + contains only basic lemmas about negation, conjunction, and so on. Most of the hints in this database come from the Init and Logic directories. :arith: This database contains all lemmas about Peano’s arithmetic proved in the @@ -3552,7 +3591,7 @@ be used. :zarith: contains lemmas about binary signed integers from the directories theories/ZArith. When required, the module Omega also extends the database zarith with a high-cost hint that calls ``omega`` on equations - and inequalities in nat or Z. + and inequalities in ``nat`` or ``Z``. :bool: contains lemmas about booleans, mostly from directory theories/Bool. @@ -3562,7 +3601,7 @@ be used. :sets: contains lemmas about sets and relations from the directories Sets and Relations. -:typeclass_instances: contains all the type class instances declared in the +:typeclass_instances: contains all the typeclass instances declared in the environment, including those used for ``setoid_rewrite``, from the Classes directory. @@ -3655,7 +3694,7 @@ but this is a mere workaround and has some limitations (for instance, external hints cannot be removed). A proper way to fix this issue is to bind the hints to their module scope, as -for most of the other objects Coq uses. Hints should only made available when +for most of the other objects Coq uses. Hints should only be made available when the module they are defined in is imported, not just required. It is very difficult to change the historical behavior, as it would break a lot of scripts. We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior` @@ -3691,7 +3730,7 @@ Setting implicit automation tactics In this case the tactic command typed by the user is equivalent to ``tactic``:sub:`1` ``;tactic``. - See also: ``Proof.`` in :ref:`proof-editing-mode`. + .. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`. .. cmdv:: Proof with tactic using {+ @ident} @@ -3746,6 +3785,7 @@ The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would fail: .. example:: + .. coqtop:: reset all Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x. @@ -3774,9 +3814,9 @@ Therefore, the use of :tacn:`intros` in the previous proof is unnecessary. :name: dtauto While :tacn:`tauto` recognizes inductively defined connectives isomorphic to - the standard connective ``and, prod, or, sum, False, Empty_set, unit, True``, - :tacn:`dtauto` recognizes also all inductive types with one constructors and - no indices, i.e. record-style connectives. + the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, + ``Empty_set``, ``unit``, ``True``, :tacn:`dtauto` also recognizes all inductive + types with one constructor and no indices, i.e. record-style connectives. .. tacn:: intuition @tactic :name: intuition @@ -3792,7 +3832,7 @@ For instance, the tactic :g:`intuition auto` applied to the goal :: - (forall (x:nat), P x)/\B -> (forall (y:nat),P y)/\ P O \/B/\ P O + (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O internally replaces it by the equivalent one: @@ -3819,11 +3859,11 @@ some incompatibilities. :name: dintuition While :tacn:`intuition` recognizes inductively defined connectives - isomorphic to the standard connective ``and``, ``prod``, ``or``, ``sum``, ``False``, - ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` recognizes also all inductive - types with one constructors and no indices, i.e. record-style connectives. + isomorphic to the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, + ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` also recognizes all inductive + types with one constructor and no indices, i.e. record-style connectives. -.. opt:: Intuition Negation Unfolding +.. flag:: Intuition Negation Unfolding Controls whether :tacn:`intuition` unfolds inner negations which do not need to be unfolded. This option is on by default. @@ -3836,11 +3876,12 @@ The :tacn:`rtauto` tactic solves propositional tautologies similarly to what reflection scheme applied to a sequent calculus proof of the goal. The search procedure is also implemented using a different technique. -Users should be aware that this difference may result in faster proof- search +Users should be aware that this difference may result in faster proof-search but slower proof-checking, and :tacn:`rtauto` might not solve goals that :tacn:`tauto` would be able to solve (e.g. goals involving universal quantifiers). +Note that this tactic is only available after a ``Require Import Rtauto``. .. tacn:: firstorder :name: firstorder @@ -3851,6 +3892,7 @@ usual logical connectives but instead may reason about any first-order class inductive definition. .. opt:: Firstorder Solver @tactic + :name: Firstorder Solver The default tactic used by :tacn:`firstorder` when no rule applies is :g:`auto with *`, it can be reset locally or globally using this option. @@ -3879,6 +3921,7 @@ inductive definition. This combines the effects of the different variants of :tacn:`firstorder`. .. opt:: Firstorder Depth @num + :name: Firstorder Depth This option controls the proof-search depth bound. @@ -3887,7 +3930,7 @@ inductive definition. The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard Nelson and Oppen congruence closure algorithm, which is a decision procedure -for ground equalities with uninterpreted symbols. It also include the +for ground equalities with uninterpreted symbols. It also includes constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal is a non-quantified equality, congruence tries to prove it with non-quantified equalities in the context. Otherwise it tries to infer a discriminable equality @@ -3895,12 +3938,13 @@ from those in the context. Alternatively, congruence tries to prove that a hypothesis is equal to the goal or to the negation of another hypothesis. :tacn:`congruence` is also able to take advantage of hypotheses stating -quantified equalities, you have to provide a bound for the number of extra -equalities generated that way. Please note that one of the members of the +quantified equalities, but you have to provide a bound for the number of extra +equalities generated that way. Please note that one of the sides of the equality must contain all the quantified variables in order for congruence to match against it. .. example:: + .. coqtop:: reset all Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a. @@ -3932,7 +3976,7 @@ match against it. discriminable equality but this proof could not be built in Coq because of dependently-typed functions. -.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with ..., replacing metavariables by arbitrary terms. +.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms. The decision procedure could solve the goal with the provision that additional arguments are supplied for some partially applied constructors. Any term of an @@ -3940,7 +3984,7 @@ match against it. additional arguments can be given to congruence by filling in the holes in the terms given in the error message, using the :tacn:`congruence with` variant described above. -.. opt:: Congruence Verbose +.. flag:: Congruence Verbose This option makes :tacn:`congruence` print debug information. @@ -3976,7 +4020,7 @@ succeeds, and results in an error otherwise. This tactic checks whether its arguments are unifiable, potentially instantiating existential variables. -.. exn:: Not unifiable. +.. exn:: Unable to unify @term with @term. .. tacv:: unify @term @term with @ident @@ -4071,10 +4115,10 @@ symbol :g:`=`. .. tacn:: decide equality :name: decide equality - This tactic solves a goal of the form :g:`forall x y:R, {x=y}+{ ~x=y}`, + This tactic solves a goal of the form :g:`forall x y : R, {x = y} + {~ x = y}`, where :g:`R` is an inductive type such that its constructors do not take proofs or functions as arguments, nor objects in dependent types. It - solves goals of the form :g:`{x=y}+{ ~x=y}` as well. + solves goals of the form :g:`{x = y} + {~ x = y}` as well. .. tacn:: compare @term @term :name: compare @@ -4162,8 +4206,9 @@ available after a ``Require Import FunInd``. .. tacv:: functional inversion @num - This does the same thing as intros until num thenfunctional inversion ident - where ident is the identifier for the last introduced hypothesis. + This does the same thing as :n:`intros until @num` folowed by + :n:`functional inversion @ident` where :token:`ident` is the + identifier for the last introduced hypothesis. .. tacv:: functional inversion ident qualid .. tacv:: functional inversion num qualid @@ -4175,26 +4220,6 @@ available after a ``Require Import FunInd``. functional inversion, this variant allows choosing which :n:`@qualid` is inverted. -.. tacn:: quote @ident - :name: quote - -This kind of inversion has nothing to do with the tactic :tacn:`inversion` -above. This tactic does :g:`change (@ident t)`, where `t` is a term built in -order to ensure the convertibility. In other words, it does inversion of the -function :n:`@ident`. This function must be a fixpoint on a simple recursive -datatype: see :ref:`quote` for the full details. - - -.. exn:: quote: not a simple fixpoint. - - Happens when quote is not able to perform inversion properly. - - -.. tacv:: quote @ident {* @ident} - - All terms that are built only with :n:`{* @ident}` will be considered by quote - as constants rather than variables. - Classical tactics ----------------- @@ -4214,9 +4239,9 @@ using the ``Require Import`` command. Use ``classical_right`` to prove the right part of the disjunction with the assumption that the negation of left part holds. -.. _tactics-automatizing: +.. _tactics-automating: -Automatizing +Automating ------------ @@ -4245,6 +4270,12 @@ constructed over the following grammar: Internally, it uses a system very similar to the one of the ring tactic. + Note that this tactic is only available after a ``Require Import Btauto``. + +.. exn:: Cannot recognize a boolean equality. + + The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto` + doesn't introduce variables into the context on its own. .. tacn:: omega :name: omega @@ -4264,13 +4295,13 @@ and :g:`Z` of binary integers. This tactic must be loaded by the command :name: ring_simplify The :n:`ring` tactic solves equations upon polynomial expressions of a ring -(or semi-ring) structure. It proceeds by normalizing both hand sides +(or semiring) structure. It proceeds by normalizing both hand sides of the equation (w.r.t. associativity, commutativity and distributivity, constant propagation) and comparing syntactically the results. :n:`ring_simplify` applies the normalization procedure described above to -the terms given. The tactic then replaces all occurrences of the terms +the given terms. The tactic then replaces all occurrences of the terms given in the conclusion of the goal by their normal forms. If no term is given, then the conclusion should be an equation and both hand sides are normalized. @@ -4306,6 +4337,7 @@ declare new field structures. All declared field structures can be printed with the Print Fields command. .. example:: + .. coqtop:: reset all Require Import Reals. @@ -4316,8 +4348,10 @@ printed with the Print Fields command. intros; field. -See also: file plugins/setoid_ring/RealField.v for an example of instantiation, -theory theories/Reals for many examples of use of field. +.. seealso:: + + File plugins/setoid_ring/RealField.v for an example of instantiation, + theory theories/Reals for many examples of use of field. Non-logical tactics ------------------------ @@ -4417,6 +4451,7 @@ Simple tactic macros A simple example has more value than a long explanation: .. example:: + .. coqtop:: reset all Ltac Solve := simpl; intros; auto. @@ -4437,7 +4472,7 @@ user-defined tactics. other one can be automatically checked. .. [2] This corresponds to the cut rule of sequent calculus. .. [3] Reminder: opaque constants will not be expanded by δ reductions. -.. [4] The behavior of this tactic has much changed compared to the +.. [4] The behavior of this tactic has changed a lot compared to the versions available in the previous distributions (V6). This may cause significant changes in your theories to obtain the same result. As a drawback of the re-engineering of the code, this tactic has also been diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index c37233734b..837d3f10a2 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _vernacularcommands: Vernacular commands @@ -78,145 +75,106 @@ Displaying Flags, Options and Tables ----------------------------- -|Coq| configurability is based on flags (e.g. :opt:`Printing All`), options -(e.g. :opt:`Printing Width`), or tables (e.g. :cmd:`Add Printing Record`). The -names of flags, options and tables are made of non-empty sequences of -identifiers (conventionally with capital initial letter). The general commands -handling flags, options and tables are given below. - -.. TODO : flag is not a syntax entry - -.. cmd:: Set @flag - - This command switches :n:`@flag` on. The original state of :n:`@flag` - is restored when the current module ends. - - .. cmdv:: Local Set @flag - - This command switches :n:`@flag` on. The original state - of :n:`@flag` is restored when the current *section* ends. - - .. cmdv:: Global Set @flag - - This command switches :n:`@flag` on. The original state - of :n:`@flag` is *not* restored at the end of the module. Additionally, if - set in a file, :n:`@flag` is switched on when the file is `Require`-d. - - .. cmdv:: Export Set @flag +Coq has many settings to control its behavior. Setting types include flags, options +and tables: - This command switches :n:`@flag` on. The original state - of :n:`@flag` is restored at the end of the current module, but :n:`@flag` - is switched on when this module is imported. +* A :production:`flag` has a boolean value, such as :flag:`Asymmetric Patterns`. +* An :production:`option` generally has a numeric or string value, such as :opt:`Firstorder Depth`. +* A :production:`table` contains a set of strings or qualids. +* In addition, some commands provide settings, such as :cmd:`Extraction Language OCaml`. +.. FIXME Convert `Extraction Language OCaml` to an option. -.. cmd:: Unset @flag +Flags, options and tables are identified by a series of identifiers, each with an initial +capital letter. - This command switches :n:`@flag` off. The original state of - :n:`@flag` is restored when the current module ends. +.. cmd:: {? Local | Global | Export } Set @flag + :name: Set - .. cmdv:: Local Unset @flag + Sets :token:`flag` on. Scoping qualifiers are + described :ref:`here <set_unset_scope_qualifiers>`. - This command switches :n:`@flag` off. The original - state of :n:`@flag` is restored when the current *section* ends. - - .. cmdv:: Global Unset @flag - - This command switches :n:`@flag` off. The original - state of :n:`@flag` is *not* restored at the end of the module. Additionally, - if set in a file, :n:`@flag` is switched off when the file is `Require`-d. - - .. cmdv:: Export Unset @flag - - This command switches :n:`@flag` off. The original state - of :n:`@flag` is restored at the end of the current module, but :n:`@flag` - is switched off when this module is imported. +.. cmd:: {? Local | Global | Export } Unset @flag + :name: Unset + Sets :token:`flag` off. Scoping qualifiers are + described :ref:`here <set_unset_scope_qualifiers>`. .. cmd:: Test @flag - This command prints whether :n:`@flag` is on or off. - - -.. cmd:: Set @option @value - - This command sets :n:`@option` to :n:`@value`. The original value of ` option` is - restored when the current module ends. - - .. TODO : option and value are not syntax entries - - .. cmdv:: Local Set @option @value + Prints the current value of :token:`flag`. - This command sets :n:`@option` to :n:`@value`. The - original value of :n:`@option` is restored at the end of the module. - .. cmdv:: Global Set @option @value +.. cmd:: {? Local | Global | Export } Set @option ( @num | @string ) + :name: Set @option - This command sets :n:`@option` to :n:`@value`. The - original value of :n:`@option` is *not* restored at the end of the module. - Additionally, if set in a file, :n:`@option` is set to value when the file - is `Require`-d. + Sets :token:`option` to the specified value. Scoping qualifiers are + described :ref:`here <set_unset_scope_qualifiers>`. - .. cmdv:: Export Set @option +.. cmd:: {? Local | Global | Export } Unset @option + :name: Unset @option - This command set :n:`@option` to :n:`@value`. The original state - of :n:`@option` is restored at the end of the current module, but :n:`@option` - is set to :n:`@value` when this module is imported. + Sets :token:`option` to its default value. Scoping qualifiers are + described :ref:`here <set_unset_scope_qualifiers>`. +.. cmd:: Test @option -.. cmd:: Unset @option - - This command turns off :n:`@option`. - - .. cmdv:: Local Unset @option + Prints the current value of :token:`option`. - This command turns off :n:`@option`. The original state of :n:`@option` - is restored when the current *section* ends. +.. cmd:: Print Options - .. cmdv:: Global Unset @option + Prints the current value of all flags and options, and the names of all tables. - This command turns off :n:`@option`. The original state of :n:`@option` - is *not* restored at the end of the module. Additionally, if unset in a file, - :n:`@option` is reset to its default value when the file is `Require`-d. - .. cmdv:: Export Unset @option +.. cmd:: Add @table ( @string | @qualid ) + :name: Add @table - This command turns off :n:`@option`. The original state of :n:`@option` - is restored at the end of the current module, but :n:`@option` is set to - its default value when this module is imported. + Adds the specified value to :token:`table`. +.. cmd:: Remove @table ( @string | @qualid ) + :name: Remove @table -.. cmd:: Test @option + Removes the specified value from :token:`table`. - This command prints the current value of :n:`@option`. +.. cmd:: Test @table for ( @string | @qualid ) + :name: Test @table for + Reports whether :token:`table` contains the specified value. -.. TODO : table is not a syntax entry - -.. cmd:: Add @table @value - :name: Add `table` `value` +.. cmd:: Print Table @table + :name: Print Table @table -.. cmd:: Remove @table @value - :name: Remove `table` `value` + Prints the values in :token:`table`. -.. cmd:: Test @table @value - :name: Test `table` `value` +.. cmd:: Test @table -.. cmd:: Test @table for @value - :name: Test `table` for `value` + A synonym for :cmd:`Print Table @table`. -.. cmd:: Print Table @table +.. cmd:: Print Tables -These are general commands for tables. + A synonym for :cmd:`Print Options`. +.. _set_unset_scope_qualifiers: -.. cmd:: Print Options +Scope qualifiers for :cmd:`Set` and :cmd:`Unset` +````````````````````````````````````````````````` - This command lists all available flags, options and tables. +:n:`{? Local | Global | Export }` - .. cmdv:: Print Tables +Flag and option settings can be global in scope or local to nested scopes created by +:cmd:`Module` and :cmd:`Section` commands. There are four alternatives: - This is a synonymous of :cmd:`Print Options`. +* no qualifier: the original setting is *not* restored at the end of the current module or section. +* **Local**: the setting is applied within the current scope. The original value of the option + or flag is restored at the end of the current module or section. +* **Global**: similar to no qualifier, the original setting is *not* restored at the end of the current + module or section. In addition, if the value is set in a file, then :cmd:`Require`-ing + the file sets the option. +* **Export**: similar to **Local**, the original value of the option or flag is restored at the + end of the current module or section. In addition, if the value is set in a file, then :cmd:`Import`-ing + the file sets the option. +Newly opened scopes inherit the current settings. .. _requests-to-the-environment: @@ -246,7 +204,7 @@ Requests to the environment hypothesis introduced in the first subgoal (if a proof is in progress). - See also: Section :ref:`performingcomputations`. + .. seealso:: Section :ref:`performingcomputations`. .. cmd:: Compute @term @@ -255,7 +213,7 @@ Requests to the environment bytecode-based virtual machine. It is a shortcut for ``Eval vm_compute in`` :n:`@term`. - See also: Section :ref:`performingcomputations`. + .. seealso:: Section :ref:`performingcomputations`. .. cmd:: Print Assumptions @qualid @@ -502,26 +460,23 @@ Requests to the environment .. note:: - .. cmd:: Add Search Blacklist @string + .. table:: Search Blacklist @string - For the ``Search``, ``SearchHead``, ``SearchPattern`` and ``SearchRewrite`` - queries, it is possible to globally filter the search results using this - command. A lemma whose fully-qualified name - contains any of the declared strings will be removed from the - search results. The default blacklisted substrings are ``_subproof`` and + Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`, + :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose + fully-qualified name contains any of the strings will be excluded from the + search results. The default blacklisted substrings are ``_subterm``, ``_subproof`` and ``Private_``. - .. cmd:: Remove Search Blacklist @string - - This command allows expunging this blacklist. - + Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of + blacklisted strings. .. cmd:: Locate @qualid This command displays the full name of objects whose name is a prefix of the qualified identifier :n:`@qualid`, and consequently the |Coq| module in which they are defined. It searches for objects from the different - qualified name spaces of |Coq|: terms, modules, Ltac, etc. + qualified namespaces of |Coq|: terms, modules, Ltac, etc. .. example:: @@ -549,7 +504,7 @@ Requests to the environment As Locate but restricted to tactics. -See also: Section :ref:`locating-notations` +.. seealso:: Section :ref:`locating-notations` .. _loading-files: @@ -587,7 +542,9 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard Display, while loading, the answers of |Coq| to each command (including tactics) contained in - the loaded file See also: Section :ref:`controlling-display`. + the loaded file. + + .. seealso:: Section :ref:`controlling-display`. .. exn:: Can’t find file @ident on loadpath. @@ -699,10 +656,7 @@ file is a particular case of module called *library file*. that the commands ``Import`` and ``Export`` alone can be used inside modules (see Section :ref:`Import <import_qualid>`). - - -See also: Chapter :ref:`thecoqcommands` - + .. seealso:: Chapter :ref:`thecoqcommands` .. cmd:: Print Libraries @@ -930,7 +884,7 @@ Quitting and debugging .. cmd:: Drop - This is used mostly as a debug facility by |Coq|’s implementors and does + This is used mostly as a debug facility by |Coq|’s implementers and does not concern the casual user. This command permits to leave |Coq| temporarily and enter the OCaml toplevel. The OCaml command: @@ -980,6 +934,7 @@ Quitting and debugging displayed. .. opt:: Default Timeout @num + :name: Default Timeout This option controls a default timeout for subsequent commands, as if they were passed to a :cmd:`Timeout` command. Commands already starting by a @@ -1004,11 +959,12 @@ Quitting and debugging Controlling display ----------------------- -.. opt:: Silent +.. flag:: Silent This option controls the normal displaying. .. opt:: Warnings "{+, {? %( - %| + %) } @ident }" + :name: Warnings This option configures the display of warnings. It is experimental, and expects, between quotes, a comma-separated list of warning names or @@ -1018,7 +974,7 @@ Controlling display interpreted from left to right, so in case of an overlap, the flags on the right have higher priority, meaning that `A,-A` is equivalent to `-A`. -.. opt:: Search Output Name Only +.. flag:: Search Output Name Only This option restricts the output of search commands to identifier names; turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`, @@ -1039,7 +995,7 @@ Controlling display printing. Beyond this depth, display of subterms is replaced by dots. At the time of writing this documentation, the default value is 50. -.. opt:: Printing Compact Contexts +.. flag:: Printing Compact Contexts This option controls the compact display mode for goals contexts. When on, the printer tries to reduce the vertical size of goals contexts by putting @@ -1047,13 +1003,13 @@ Controlling display does not exceed the printing width (see :opt:`Printing Width`). At the time of writing this documentation, it is off by default. -.. opt:: Printing Unfocused +.. flag:: Printing Unfocused This option controls whether unfocused goals are displayed. Such goals are created by focusing other goals with bullets (see :ref:`bullets` or :ref:`curly braces <curly-braces>`). It is off by default. -.. opt:: Printing Dependent Evars Line +.. flag:: Printing Dependent Evars Line This option controls the printing of the “(dependent evars: …)” line when ``-emacs`` is passed. @@ -1097,8 +1053,10 @@ described first. The scope of :cmd:`Opaque` is limited to the current section, or current file, unless the variant :cmd:`Global Opaque` is used. - See also: sections :ref:`performingcomputations`, :ref:`tactics-automatizing`, - :ref:`proof-editing-mode` + .. seealso:: + + Sections :ref:`performingcomputations`, :ref:`tactics-automating`, + :ref:`proof-editing-mode` .. exn:: The reference @qualid was not found in the current environment. @@ -1130,8 +1088,10 @@ described first. There is no constant referred by :n:`@qualid` in the environment. - See also: sections :ref:`performingcomputations`, - :ref:`tactics-automatizing`, :ref:`proof-editing-mode` + .. seealso:: + + Sections :ref:`performingcomputations`, + :ref:`tactics-automating`, :ref:`proof-editing-mode` .. _vernac-strategy: @@ -1195,7 +1155,7 @@ described first. nothing prevents the user to also perform a ``Ltac`` `ident` ``:=`` `convtactic`. - See also: sections :ref:`performingcomputations` + .. seealso:: :ref:`performingcomputations` .. _controlling-locality-of-commands: @@ -1217,19 +1177,19 @@ scope of their effect. There are four kinds of commands: current section or module it occurs in. As an example, the :cmd:`Coercion` and :cmd:`Strategy` commands belong to this category. + Commands whose default behavior is to stop their effect at the end - of the section they occur in but to extent their effect outside the module or + of the section they occur in but to extend their effect outside the module or library file they occur in. For these commands, the Local modifier limits the effect of the command to the current module if the command does not occur in a section and the Global modifier extends the effect outside the current sections and current module if the command occurs in a section. As an example, the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong to this category. Notice that a subclass of these commands do not support - extension of their scope outside sections at all and the Global is not + extension of their scope outside sections at all and the Global modifier is not applicable to them. + Commands whose default behavior is to stop their effect at the end of the section or module they occur in. For these commands, the ``Global`` modifier extends their effect outside the sections and modules they - occurs in. The :cmd:`Transparent` and :cmd:`Opaque` + occur in. The :cmd:`Transparent` and :cmd:`Opaque` (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands belong to this category. + Commands whose default behavior is to extend their effect outside |