diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/detailed-tactic-examples.rst | 641 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 132 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 10 |
5 files changed, 402 insertions, 390 deletions
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 84810ddba5..225df8d54c 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -25,7 +25,7 @@ argument an 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,79 +341,81 @@ involves conditional rewritings and shows how to deal with them using the optional tactic of the ``Hint Rewrite`` command. -Example 1: Ackermann function +.. example:: Ackermann function -.. coqtop:: in + .. coqtop:: in reset - Reset Initial. + Require Import Arith. -.. coqtop:: in + .. coqtop:: in - Require Import Arith. + Variable Ack : nat -> nat -> nat. -.. coqtop:: in + .. coqtop:: in - Variable Ack : nat -> nat -> nat. + 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 + .. 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). + Hint Rewrite Ack0 Ack1 Ack2 : base0. -.. coqtop:: in + .. coqtop:: all - Hint Rewrite Ack0 Ack1 Ack2 : base0. + Lemma ResAck0 : Ack 3 2 = 29. -.. coqtop:: all + .. coqtop:: all - Lemma ResAck0 : Ack 3 2 = 29. + autorewrite with base0 using try reflexivity. -.. coqtop:: all +.. example:: MacCarthy function - autorewrite with base0 using try reflexivity. + .. coqtop:: in reset -Example 2: Mac Carthy function + Require Import Omega. -.. coqtop:: in + .. coqtop:: in - Require Import Omega. + Variable g : nat -> nat -> nat. -.. coqtop:: in + .. coqtop:: in - Variable g : nat -> nat -> nat. + 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 + .. 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). + Hint Rewrite g0 g1 g2 using omega : base1. + .. coqtop:: in -.. coqtop:: in + Lemma Resg0 : g 1 110 = 100. - Hint Rewrite g0 g1 g2 using omega : base1. + .. coqtop:: out -.. coqtop:: in + Show. - Lemma Resg0 : g 1 110 = 100. + .. coqtop:: all -.. coqtop:: out + autorewrite with base1 using reflexivity || simpl. - Show. + .. coqtop:: none -.. coqtop:: all + Qed. - autorewrite with base1 using reflexivity || simpl. + .. coqtop:: all -.. coqtop:: all + Lemma Resg1 : g 1 95 = 91. - Lemma Resg1 : g 1 95 = 91. + .. coqtop:: all -.. coqtop:: all + autorewrite with base1 using reflexivity || simpl. - autorewrite with base1 using reflexivity || simpl. + .. coqtop:: none + Qed. .. _quote: @@ -419,7 +431,7 @@ the form ``(f t)``. ``L`` must have a constructor of type: ``A -> L``. Here is an example: -.. coqtop:: in +.. coqtop:: in reset Require Import Quote. @@ -461,16 +473,11 @@ 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. - -Error messages: - - -#. quote: not a simple fixpoint +.. exn:: quote: not a simple fixpoint Happens when ``quote`` is not able to perform inversion properly. - Introducing variables map ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -553,7 +560,13 @@ example, this is the case for the :tacn:`ring` tactic. Then one must provide to is ``[O S]`` then closed natural numbers will be considered as constants and other terms as variables. -Example: +.. coqtop:: in reset + + Require Import Quote. + +.. coqtop:: in + + Parameters A B C : Prop. .. coqtop:: in @@ -594,8 +607,9 @@ Example: quote interp_f [ B C iff ]. -Warning: Since function inversion is undecidable in general case, -don’t expect miracles from it! +.. warning:: + Since functional inversion is undecidable in the general case, + don’t expect miracles from it! .. tacv:: quote @ident in @term using @tactic @@ -607,25 +621,28 @@ don’t expect miracles from it! 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`` +.. seealso:: + Comments from the source file ``plugins/quote/quote.ml`` -See also: the :tacn:`ring` tactic. +.. seealso:: + 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 +654,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 +668,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 +685,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: - -.. 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. +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:: 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 +904,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/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index eba0db3ff5..a9d0c16376 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -321,7 +321,7 @@ Navigation in the proof tree 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 @@ -375,6 +375,7 @@ or focus the next one. The following example script illustrates all these features: .. example:: + .. coqtop:: all Goal (((True /\ True) /\ True) /\ True) /\ True. @@ -403,7 +404,7 @@ The following example script illustrates all these features: .. 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 %{. @@ -470,7 +471,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 +512,7 @@ Requesting information :token:`ident` .. example:: + .. coqtop:: all Show Match nat. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 6fb73a030f..8a2fc3996a 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -4632,6 +4632,7 @@ bookkeeping steps. .. example:: + The following example use the ``~~`` prenex notation for boolean negation: diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 562f8568dc..fdb04bf9a0 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -26,8 +26,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. @@ -107,10 +107,10 @@ 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: @@ -137,7 +137,7 @@ 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 @@ -151,7 +151,7 @@ no numbers are given, all occurrences of :n:`@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` +Here are some tactics that understand occurrence clauses: :tacn:`set`, :tacn:`remember` , :tacn:`induction`, :tacn:`destruct`. @@ -207,6 +207,7 @@ Applying theorems useful to advanced users. .. example:: + .. coqtop:: reset all Inductive Option : Set := @@ -281,7 +282,7 @@ Applying theorems :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 ... . + .. exn:: Unable to unify @term with @term. 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 @@ -366,6 +367,7 @@ Applying theorems .. warn:: When @term contains more than one non dependent product the tactic lapply only takes into account the first product. .. example:: + Assume we have a transitive relation ``R`` on ``nat``: .. coqtop:: reset in @@ -466,7 +468,7 @@ Applying theorems 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 + instance if the type of :g:`H1` is :g:`A <-> B` 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 with dependent types. @@ -837,6 +839,7 @@ quantified variables or hypotheses until the goal is not any more a quantification or an implication. .. example:: + .. coqtop:: all Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. @@ -846,7 +849,7 @@ quantification or an implication. :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). @@ -958,6 +961,7 @@ quantification or an implication. .. exn:: Cannot move @ident after @ident : it depends on @ident. .. example:: + .. coqtop:: all Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x. @@ -1040,7 +1044,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged. .. tacv:: remember @term as @ident in @goal_occurrences This is a more general form of :n:`remember` that remembers the occurrences - of term specified by an occurrences set. + of term specified by an occurrence set. .. tacv:: eremember @term as @ident .. tacv:: eremember @term as @ident in @goal_occurrences @@ -1082,6 +1086,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged. obtain atomic ones. .. example:: + .. coqtop:: all Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C. @@ -1252,6 +1257,7 @@ Controlling the proof flow respect to some term. .. example:: + .. coqtop:: reset none Goal forall x y:nat, 0 <= x + y + y. @@ -1523,7 +1529,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. @@ -1567,6 +1573,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 +1643,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 +1752,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 +1815,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 +1835,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 @@ -2237,7 +2247,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. @@ -2598,7 +2608,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`). @@ -2708,7 +2718,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 @@ -2804,14 +2814,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 +2835,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 +2866,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 +2876,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 +2892,7 @@ the conversion in hypotheses :n:`{+ @ident}`. always unfolded. .. example:: + .. coqtop:: all Definition volatile := fun x : nat => x. @@ -2887,6 +2903,7 @@ the conversion in hypotheses :n:`{+ @ident}`. such arguments. .. example:: + .. coqtop:: all Arguments minus !n !m. @@ -3030,7 +3047,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 +3089,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. @@ -3177,6 +3194,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. @@ -3216,10 +3234,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 @@ -3312,7 +3330,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 +3514,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 @@ -3535,15 +3553,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 @@ -3655,7 +3672,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` @@ -3746,6 +3763,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 +3792,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 +3810,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,9 +3837,9 @@ 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 @@ -3836,11 +3854,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 @@ -3887,7 +3906,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 +3914,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 +3952,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 @@ -3976,7 +3996,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 +4091,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 @@ -4214,9 +4234,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 +4265,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 @@ -4270,7 +4296,7 @@ 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 +4332,7 @@ declare new field structures. All declared field structures can be printed with the Print Fields command. .. example:: + .. coqtop:: reset all Require Import Reals. @@ -4417,6 +4444,7 @@ Simple tactic macros A simple example has more value than a long explanation: .. example:: + .. coqtop:: reset all Ltac Solve := simpl; intros; auto. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index c37233734b..0a517973c2 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1097,7 +1097,7 @@ 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`, + See also: sections :ref:`performingcomputations`, :ref:`tactics-automating`, :ref:`proof-editing-mode` .. exn:: The reference @qualid was not found in the current environment. @@ -1131,7 +1131,7 @@ 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` + :ref:`tactics-automating`, :ref:`proof-editing-mode` .. _vernac-strategy: @@ -1217,19 +1217,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 |