diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/detailed-tactic-examples.rst | 378 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 446 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 22 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 84 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 32 |
7 files changed, 495 insertions, 489 deletions
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index b629d15b11..0ace9ef5b9 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -396,381 +396,3 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: none Qed. - -Using the tactic language -------------------------- - - -About the cardinality of the set of natural numbers -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -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 reset - - Lemma card_nat : - ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z. - Proof. - -.. coqtop:: in - - red; intros (x, (y, Hy)). - -.. coqtop:: in - - elim (Hy 0); elim (Hy 1); elim (Hy 2); intros; - - match goal with - | _ : ?a = ?b, _ : ?a = ?c |- _ => - cut (b = c); [ discriminate | transitivity a; auto ] - end. - -.. coqtop:: in - - Qed. - -We can notice that all the (very similar) cases coming from the three -eliminations (with three distinct natural numbers) are successfully -solved by a match goal structure and, in particular, with only one -pattern (use of non-linear matching). - - -Permutations of lists -~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -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 reset - - Section Sort. - -.. coqtop:: in - - Variable A : Set. - -.. coqtop:: in - - 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. - -First, we define the permutation predicate as shown above. - -.. coqtop:: none - - Require Import List. - - -.. coqtop:: in - - 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. - -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. - -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 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 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -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 reset - - Ltac basic := - match goal with - | |- True => trivial - | _ : False |- _ => contradiction - | _ : ?A |- ?A => assumption - end. - -.. coqtop:: in - - 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 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. - -.. coqtop:: in reset - - Open Scope type_scope. - -.. coqtop:: in - - Section Iso_axioms. - -.. coqtop:: in - - Variables A B C : Set. - -.. coqtop:: in - - Axiom Com : A * B = B * A. - - Axiom Ass : A * (B * C) = A * B * C. - - Axiom Cur : (A * B -> C) = (A -> B -> C). - - Axiom Dis : (A -> B * C) = (A -> B) * (A -> C). - - Axiom P_unit : A * unit = A. - - Axiom AR_unit : (A -> unit) = unit. - - Axiom AL_unit : (unit -> A) = A. - -.. coqtop:: in - - Lemma Cons : B = C -> A * B = A * C. - - Proof. - - intro Heq; rewrite Heq; reflexivity. - - Qed. - -.. coqtop:: in - - 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. - -.. coqtop:: in - - Ltac len trm := - match trm with - | _ * ?B => let succ := len B in constr:(S succ) - | _ => constr:(1) - end. - -.. coqtop:: in - - Ltac assoc := repeat rewrite <- Ass. - -.. coqtop:: in - - 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. - -.. coqtop:: in - - 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. - -.. coqtop:: in - - Ltac solve_iso := simplify_type_eq; compare_structure. - -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 ``solve_iso``. - -.. coqtop:: in - - Lemma solve_iso_ex1 : - forall A B : Set, A * unit * B = B * (unit * A). - Proof. - intros; solve_iso. - Qed. - -.. coqtop:: in - - Lemma solve_iso_ex2 : - forall A B C : Set, - (A * unit -> B * (C * unit)) = - (A * unit -> (C -> unit) * C) * (unit -> A -> B). - Proof. - intros; solve_iso. - Qed. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index d3562b52c5..bbd7e0ba3d 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -3,12 +3,25 @@ Ltac ==== -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 small but nontrivial -use examples of this language. +This chapter documents the tactic language |Ltac|. + +We start by giving the syntax, and next, we present the informal +semantics. To learn more about the language and +especially about its foundations, please refer to :cite:`Del00`. + +.. example:: Basic tactic macros + + Here are some examples of simple tactic macros that the + language lets you write. + + .. coqdoc:: + + Ltac reduce_and_try_to_solve := simpl; intros; auto. + + Ltac destruct_bool_and_rewrite b H1 H2 := + destruct b; [ rewrite H1; eauto | rewrite H2; eauto ]. + + See Section :ref:`ltac-examples` for more advanced examples. .. _ltac-syntax: @@ -347,7 +360,7 @@ Detecting progress We can check if a tactic made progress with: -.. tacn:: progress expr +.. tacn:: progress @expr :name: progress :n:`@expr` is evaluated to v which must be a tactic value. The tactic value ``v`` @@ -542,7 +555,7 @@ Identity The constant :n:`idtac` is the identity tactic: it leaves any goal unchanged but it appears in the proof script. -.. tacn:: idtac {* message_token} +.. tacn:: idtac {* @message_token} :name: idtac This prints the given tokens. Strings and integers are printed @@ -671,7 +684,7 @@ Timing a tactic that evaluates to a term Tactic expressions that produce terms can be timed with the experimental tactic -.. tacn:: time_constr expr +.. tacn:: time_constr @expr :name: time_constr which evaluates :n:`@expr ()` and displays the time the tactic expression @@ -867,7 +880,7 @@ 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 +.. tacn:: match goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end :name: match goal If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is @@ -905,7 +918,7 @@ We can perform pattern matching on goals using the following expression: 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 + .. tacv:: multimatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end Using :n:`multimatch` instead of :n:`match` will allow subsequent tactics to backtrack into a right-hand side tactic which has backtracking points @@ -916,7 +929,7 @@ We can perform pattern matching on goals using the following expression: The syntax :n:`match [reverse] goal …` is, in fact, a shorthand for :n:`once multimatch [reverse] goal …`. - .. tacv:: lazymatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end + .. tacv:: lazymatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end Using lazymatch instead of match will perform the same pattern matching procedure but will commit to the first matching branch with the first @@ -1122,33 +1135,33 @@ Defining |Ltac| functions Basically, |Ltac| toplevel definitions are made as follows: -.. cmd:: Ltac @ident {* @ident} := @expr +.. cmd:: {? Local} Ltac @ident {* @ident} := @expr + :name: Ltac This defines a new |Ltac| function that can be used in any tactic script or new |Ltac| toplevel definition. + If preceded by the keyword ``Local``, the tactic definition will not be + exported outside the current module. + .. note:: The preceding definition can equivalently be written: :n:`Ltac @ident := fun {+ @ident} => @expr` - Recursive and mutual recursive function definitions are also possible - with the syntax: - .. cmdv:: Ltac @ident {* @ident} {* with @ident {* @ident}} := @expr - It is also possible to *redefine* an existing user-defined tactic using the syntax: + This syntax allows recursive and mutual recursive function definitions. .. cmdv:: Ltac @qualid {* @ident} ::= @expr + This syntax *redefines* an existing user-defined tactic. + A previous definition of qualid must exist in the environment. The new definition will always be used instead of the old one and it goes across module boundaries. - If preceded by the keyword Local the tactic definition will not be - exported outside the current module. - Printing |Ltac| tactics ~~~~~~~~~~~~~~~~~~~~~~~ @@ -1160,6 +1173,399 @@ Printing |Ltac| tactics This command displays a list of all user-defined tactics, with their arguments. + +.. _ltac-examples: + +Examples of using |Ltac| +------------------------- + +Proof that the natural numbers have at least two elements +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. example:: Proof that the natural numbers have at least two elements + + The first example shows how to use pattern matching over the proof + context to prove that natural numbers have at least two + elements. This can be done as follows: + + .. coqtop:: reset all + + Lemma card_nat : + ~ exists x y : nat, forall z:nat, x = z \/ y = z. + Proof. + intros (x & y & Hz). + destruct (Hz 0), (Hz 1), (Hz 2). + + At this point, the :tacn:`congruence` tactic would finish the job: + + .. coqtop:: all abort + + all: congruence. + + But for the purpose of the example, let's craft our own custom + tactic to solve this: + + .. coqtop:: none + + Lemma card_nat : + ~ exists x y : nat, forall z:nat, x = z \/ y = z. + Proof. + intros (x & y & Hz). + destruct (Hz 0), (Hz 1), (Hz 2). + + .. coqtop:: all abort + + all: match goal with + | _ : ?a = ?b, _ : ?a = ?c |- _ => assert (b = c) by now transitivity a + end. + all: discriminate. + + Notice that all the (very similar) cases coming from the three + eliminations (with three distinct natural numbers) are successfully + solved by a ``match goal`` structure and, in particular, with only one + pattern (use of non-linear matching). + + +Proving that a list is a permutation of a second list +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. example:: Proving that a list is a permutation of a second list + + Let's first define the permutation predicate: + + .. coqtop:: in reset + + Section Sort. + + Variable A : Set. + + 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. + + End Sort. + + .. coqtop:: none + + Require Import List. + + + Next we define an auxiliary tactic :g:`perm_aux` which takes an + argument used to control the recursion depth. This tactic works as + follows: If the lists are identical (i.e. convertible), it + completes the proof. Otherwise, if the lists have identical heads, + it looks at their tails. Finally, if the lists have different + heads, it rotates the first list by putting its head at the end. + + Every time we perform a rotation, we decrement :g:`n`. When :g:`n` + drops down to :g:`1`, we stop performing rotations and we fail. + The idea is to give the length of the list as the initial value of + :g:`n`. This way of counting the number of rotations will avoid + going back to a head that had been considered before. + + From Section :ref:`ltac-syntax` we know that Ltac has a primitive + notion of integers, but they are only used as arguments for + primitive tactics and we cannot make computations with them. Thus, + instead, we use Coq's natural number type :g:`nat`. + + .. coqtop:: in + + 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. + + + The main tactic is :g:`solve_perm`. It computes the lengths of the + two lists and uses them as arguments to call :g:`perm_aux` if the + lengths are equal. (If they aren't, the lists cannot be + permutations of each other.) + + .. 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. + + And now, here is how we can use the tactic :g:`solve_perm`: + + .. coqtop:: out + + Goal perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). + + .. coqtop:: all abort + + solve_perm. + + .. coqtop:: out + + Goal perm nat + (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) + (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). + + .. coqtop:: all abort + + solve_perm. + + +Deciding intuitionistic propositional logic +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Pattern matching on goals allows 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 reset + + Ltac basic := + match goal with + | |- True => trivial + | _ : False |- _ => contradiction + | _ : ?A |- ?A => assumption + end. + +.. coqtop:: in + + 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 trickier 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. + +.. coqtop:: in reset + + Open Scope type_scope. + +.. coqtop:: in + + Section Iso_axioms. + +.. coqtop:: in + + Variables A B C : Set. + +.. coqtop:: in + + Axiom Com : A * B = B * A. + + Axiom Ass : A * (B * C) = A * B * C. + + Axiom Cur : (A * B -> C) = (A -> B -> C). + + Axiom Dis : (A -> B * C) = (A -> B) * (A -> C). + + Axiom P_unit : A * unit = A. + + Axiom AR_unit : (A -> unit) = unit. + + Axiom AL_unit : (unit -> A) = A. + +.. coqtop:: in + + Lemma Cons : B = C -> A * B = A * C. + + Proof. + + intro Heq; rewrite Heq; reflexivity. + + Qed. + +.. coqtop:: in + + 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. + +.. coqtop:: in + + Ltac len trm := + match trm with + | _ * ?B => let succ := len B in constr:(S succ) + | _ => constr:(1) + end. + +.. coqtop:: in + + Ltac assoc := repeat rewrite <- Ass. + +.. coqtop:: in + + 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. + +.. coqtop:: in + + 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. + +.. coqtop:: in + + Ltac solve_iso := simplify_type_eq; compare_structure. + +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 a 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 +length, the tactic ``solve_type_eq`` attempts to prove that the types are equal. +The main tactic that puts all these components together is ``solve_iso``. + +Here are examples of what can be solved by ``solve_iso``. + +.. coqtop:: in + + Lemma solve_iso_ex1 : + forall A B : Set, A * unit * B = B * (unit * A). + Proof. + intros; solve_iso. + Qed. + +.. coqtop:: in + + Lemma solve_iso_ex2 : + forall A B C : Set, + (A * unit -> B * (C * unit)) = + (A * unit -> (C -> unit) * C) * (unit -> A -> B). + Proof. + intros; solve_iso. + Qed. + + Debugging |Ltac| tactics ------------------------ diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 6e33862b39..aa603fc966 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -668,7 +668,7 @@ A scope is a name given to a grammar entry used to produce some Ltac2 expression at parsing time. Scopes are described using a form of S-expression. .. prodn:: - ltac2_scope ::= @string %| @integer %| @lident ({+, @ltac2_scope}) + ltac2_scope ::= {| @string | @integer | @lident ({+, @ltac2_scope}) } A few scopes contain antiquotation features. For sake of uniformity, all antiquotations are introduced by the syntax :n:`$@lident`. @@ -751,7 +751,7 @@ Notations The Ltac2 parser can be extended by syntactic notations. -.. cmd:: Ltac2 Notation {+ @lident (@ltac2_scope) %| @string } {? : @integer} := @ltac2_term +.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @integer} := @ltac2_term :name: Ltac2 Notation A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded @@ -823,9 +823,9 @@ Ltac2 features a toplevel loop that can be used to evaluate expressions. Debug ----- -.. opt:: Ltac2 Backtrace +.. flag:: Ltac2 Backtrace - When this option is set, toplevel failures will be printed with a backtrace. + When this flag is set, toplevel failures will be printed with a backtrace. Compatibility layer with Ltac1 ------------------------------ @@ -966,7 +966,7 @@ errors produced by the typechecker. In Ltac expressions +++++++++++++++++++ -.. exn:: Unbound ( value | constructor ) X +.. exn:: Unbound {| value | constructor } X * if `X` is meant to be a term from the current stactic environment, replace the problematic use by `'X`. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 16b158c397..4a2f9c0db3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -322,7 +322,7 @@ Navigation in the proof tree .. index:: { } -.. cmd:: %{ %| %} +.. cmd:: {| %{ | %} } The command ``{`` (without a terminating period) focuses on the first goal, much like :cmd:`Focus` does, however, the subproof can only be @@ -430,7 +430,7 @@ not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further nesting levels provided they are delimited by these. Bullets are made of repeated ``-``, ``+`` or ``*`` symbols: -.. prodn:: bullet ::= {+ - } %| {+ + } %| {+ * } +.. 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 @@ -492,7 +492,7 @@ The following example script illustrates all these features: Set Bullet Behavior ``````````````````` -.. opt:: Bullet Behavior %( "None" %| "Strict Subproofs" %) +.. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } :name: Bullet Behavior This option controls the bullet behavior and can take two possible values: @@ -544,9 +544,9 @@ Requesting information ``<Your Tactic Text here>``. - .. deprecated:: 8.10 + .. deprecated:: 8.10 - Please use a text editor. + Please use a text editor. .. cmdv:: Show Proof :name: Show Proof @@ -680,7 +680,7 @@ This image shows an error message with diff highlighting in CoqIDE: How to enable diffs ``````````````````` -.. opt:: Diffs %( "on" %| "off" %| "removed" %) +.. opt:: Diffs {| "on" | "off" | "removed" } :name: Diffs The “on” setting highlights added tokens in green, while the “removed” setting diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 4e40df6f94..75e019592f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -617,7 +617,7 @@ Abbreviations selected occurrences of a term. .. prodn:: - occ_switch ::= { {? + %| - } {* @num } } + occ_switch ::= { {? {| + | - } } {* @num } } where: @@ -2273,7 +2273,7 @@ to the others. Iteration ~~~~~~~~~ -.. tacn:: do {? @num } ( @tactic | [ {+| @tactic } ] ) +.. tacn:: do {? @num } {| @tactic | [ {+| @tactic } ] } :name: do (ssreflect) This tactical offers an accurate control on the repetition of tactics. @@ -2300,7 +2300,7 @@ tactic should be repeated on the current subgoal. There are four kinds of multipliers: .. prodn:: - mult ::= @num ! %| ! %| @num ? %| ? + mult ::= {| @num ! | ! | @num ? | ? } Their meaning is: @@ -2571,7 +2571,7 @@ destruction of existential assumptions like in the tactic: An alternative use of the ``have`` tactic is to provide the explicit proof term for the intermediate lemma, using tactics of the form: -.. tacv:: have {? @ident } := term +.. tacv:: have {? @ident } := @term This tactic creates a new assumption of type the type of :token:`term`. If the @@ -5444,7 +5444,7 @@ equivalences are indeed taken into account, otherwise only single |SSR| searching tool -------------------- -.. cmd:: Search {? @pattern } {* {? - } %( @string %| @pattern %) {? % @ident} } {? in {+ {? - } @qualid } } +.. cmd:: Search {? @pattern } {* {? - } {| @string | @pattern } {? % @ident} } {? in {+ {? - } @qualid } } :name: Search (ssreflect) This is the |SSR| extension of the Search command. :token:`qualid` is the @@ -5686,7 +5686,7 @@ respectively. local cofix definition -.. tacn:: set @ident {? : @term } := {? @occ_switch } %( @term %| ( @c_pattern) %) +.. tacn:: set @ident {? : @term } := {? @occ_switch } {| @term | ( @c_pattern) } abbreviation (see :ref:`abbreviations_ssr`) @@ -5714,26 +5714,26 @@ introduction see :ref:`introduction_ssr` localization see :ref:`localization_ssr` -.. prodn:: tactic += do {? @mult } %( @tactic %| [ {+| @tactic } ] %) +.. prodn:: tactic += do {? @mult } {| @tactic | [ {+| @tactic } ] } iteration see :ref:`iteration_ssr` -.. prodn:: tactic += @tactic ; %( first %| last %) {? @num } %( @tactic %| [ {+| @tactic } ] %) +.. prodn:: tactic += @tactic ; {| first | last } {? @num } {| @tactic | [ {+| @tactic } ] } selector see :ref:`selectors_ssr` -.. prodn:: tactic += @tactic ; %( first %| last %) {? @num } +.. prodn:: tactic += @tactic ; {| first | last } {? @num } rotation see :ref:`selectors_ssr` -.. prodn:: tactic += by %( @tactic %| [ {*| @tactic } ] %) +.. prodn:: tactic += by {| @tactic | [ {*| @tactic } ] } closing see :ref:`terminators_ssr` Commands ~~~~~~~~ -.. cmd:: Hint View for %( move %| apply %) / @ident {? | @num } +.. cmd:: Hint View for {| move | apply } / @ident {? | @num } view hint declaration (see :ref:`declaring_new_hints_ssr`) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 0f78a9b84a..4e47621938 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1749,7 +1749,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``, and ``in`` clauses. -.. tacn:: case term +.. tacn:: case @term :name: case The tactic :n:`case` is a more basic tactic to perform case analysis without @@ -1982,7 +1982,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) :n:`induction @ident; induction @ident` (or :n:`induction @ident ; destruct @ident` depending on the exact needs). -.. tacv:: double induction num1 num2 +.. tacv:: double induction @num__1 @num__2 This tactic is deprecated and should be replaced by :n:`induction num1; induction num3` where :n:`num3` is the result @@ -2271,11 +2271,11 @@ and an explanation of the underlying technique. :undocumented: .. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern} - injection @num as {+ simple_intropattern} - injection as {+ simple_intropattern} - einjection @term {? with @bindings_list} as {+ simple_intropattern} - einjection @num as {+ simple_intropattern} - einjection as {+ simple_intropattern} + injection @num as {+ @simple_intropattern} + injection as {+ @simple_intropattern} + einjection @term {? with @bindings_list} as {+ @simple_intropattern} + einjection @num as {+ @simple_intropattern} + einjection as {+ @simple_intropattern} These variants apply :n:`intros {+ @simple_intropattern}` after the call to :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in @@ -2637,7 +2637,7 @@ and an explanation of the underlying technique. is correct at some time of the interactive development of a proof, use the command ``Guarded`` (see Section :ref:`requestinginformation`). -.. tacv:: fix @ident @num with {+ (ident {+ @binder} [{struct @ident}] : @type)} +.. tacv:: fix @ident @num with {+ (@ident {+ @binder} [{struct @ident}] : @type)} This starts a proof by mutual induction. The statements to be simultaneously proved are respectively :g:`forall binder ... binder, type`. @@ -3561,7 +3561,7 @@ Automation .. tacn:: autorewrite with {+ @ident} :name: autorewrite - This tactic [4]_ carries out rewritings according to the rewriting rule + This tactic carries out rewritings according to the rewriting rule bases :n:`{+ @ident}`. Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until @@ -3777,8 +3777,8 @@ The general command to add a hint to some databases :n:`{+ @ident}` is discrimination network to relax or constrain it in the case of discriminated databases. - .. cmdv:: Hint Variables %( Transparent %| Opaque %) : @ident - Hint Constants %( Transparent %| Opaque %) : @ident + .. cmdv:: Hint Variables {| Transparent | Opaque } : @ident + Hint Constants {| Transparent | Opaque } : @ident :name: Hint Variables; Hint Constants This sets the transparency flag used during unification of @@ -3850,7 +3850,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is semantics of :n:`Hint Cut @regexp` is to set the cut expression to :n:`c | regexp`, the initial cut expression being `emp`. - .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident + .. cmdv:: Hint Mode @qualid {* {| + | ! | - } } : @ident :name: Hint Mode This sets an optional mode of use of the identifier :n:`@qualid`. When @@ -4016,7 +4016,7 @@ We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior option which accepts three flags allowing for a fine-grained handling of non-imported hints. -.. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %) +.. opt:: Loose Hint Behavior {| "Lax" | "Warn" | "Strict" } :name: Loose Hint Behavior This option accepts three values, which control the behavior of hints w.r.t. @@ -4048,7 +4048,7 @@ Setting implicit automation tactics .. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`. - .. cmdv:: Proof with tactic using {+ @ident} + .. cmdv:: Proof with @tactic using {+ @ident} Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` @@ -4400,6 +4400,11 @@ Equality This tactic applies to a goal that has the form :g:`t=u` and transforms it into the two subgoals :n:`t=@term` and :n:`@term=u`. + .. tacv:: etransitivity + + This tactic behaves like :tacn:`transitivity`, using a fresh evar instead of + a concrete :token:`term`. + Equality and inductive sets --------------------------- @@ -4661,9 +4666,12 @@ Non-logical tactics .. example:: - .. coqtop:: all reset + .. coqtop:: none reset Parameter P : nat -> Prop. + + .. coqtop:: all abort + Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. all: cycle 2. @@ -4679,9 +4687,8 @@ Non-logical tactics .. example:: - .. coqtop:: reset all + .. coqtop:: all abort - Parameter P : nat -> Prop. Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. all: swap 1 3. @@ -4694,9 +4701,8 @@ Non-logical tactics .. example:: - .. coqtop:: all reset + .. coqtop:: all abort - Parameter P : nat -> Prop. Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. all: revgoals. @@ -4717,7 +4723,7 @@ Non-logical tactics .. example:: - .. coqtop:: all reset + .. coqtop:: all abort Goal exists n, n=0. refine (ex_intro _ _ _). @@ -4746,39 +4752,6 @@ Non-logical tactics The ``give_up`` tactic can be used while editing a proof, to choose to write the proof script in a non-sequential order. -Simple tactic macros -------------------------- - -A simple example has more value than a long explanation: - -.. example:: - - .. coqtop:: reset all - - Ltac Solve := simpl; intros; auto. - - Ltac ElimBoolRewrite b H1 H2 := - elim b; [ intros; rewrite H1; eauto | intros; rewrite H2; eauto ]. - -The tactics macros are synchronous with the Coq section mechanism: a -tactic definition is deleted from the current environment when you -close the section (see also :ref:`section-mechanism`) where it was -defined. If you want that a tactic macro defined in a module is usable in the -modules that require it, you should put it outside of any section. - -:ref:`ltac` gives examples of more complex -user-defined tactics. - -.. [1] Actually, only the second subgoal will be generated since the - 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 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 - completely revised to get a very compact and readable version. - Delaying solving unification constraints ---------------------------------------- @@ -4917,3 +4890,8 @@ Performance-oriented tactic variants Goal False. native_cast_no_check I. Fail Qed. + +.. [1] Actually, only the second subgoal will be generated since the + 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. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index e207a072cc..26dc4e02cf 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -91,13 +91,13 @@ and tables: Flags, options and tables are identified by a series of identifiers, each with an initial capital letter. -.. cmd:: {? Local | Global | Export } Set @flag +.. cmd:: {? {| Local | Global | Export } } Set @flag :name: Set Sets :token:`flag` on. Scoping qualifiers are described :ref:`here <set_unset_scope_qualifiers>`. -.. cmd:: {? Local | Global | Export } Unset @flag +.. cmd:: {? {| Local | Global | Export } } Unset @flag :name: Unset Sets :token:`flag` off. Scoping qualifiers are @@ -108,13 +108,13 @@ capital letter. Prints the current value of :token:`flag`. -.. cmd:: {? Local | Global | Export } Set @option ( @num | @string ) +.. cmd:: {? {| Local | Global | Export } } Set @option {| @num | @string } :name: Set @option Sets :token:`option` to the specified value. Scoping qualifiers are described :ref:`here <set_unset_scope_qualifiers>`. -.. cmd:: {? Local | Global | Export } Unset @option +.. cmd:: {? {| Local | Global | Export } } Unset @option :name: Unset @option Sets :token:`option` to its default value. Scoping qualifiers are @@ -129,17 +129,17 @@ capital letter. Prints the current value of all flags and options, and the names of all tables. -.. cmd:: Add @table ( @string | @qualid ) +.. cmd:: Add @table {| @string | @qualid } :name: Add @table Adds the specified value to :token:`table`. -.. cmd:: Remove @table ( @string | @qualid ) +.. cmd:: Remove @table {| @string | @qualid } :name: Remove @table Removes the specified value from :token:`table`. -.. cmd:: Test @table for ( @string | @qualid ) +.. cmd:: Test @table for {| @string | @qualid } :name: Test @table for Reports whether :token:`table` contains the specified value. @@ -162,7 +162,7 @@ capital letter. Scope qualifiers for :cmd:`Set` and :cmd:`Unset` ````````````````````````````````````````````````` -:n:`{? Local | Global | Export }` +:n:`{? {| Local | Global | Export } }` 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: @@ -277,7 +277,7 @@ Requests to the environment :token:`term_pattern` (holes of the pattern are either denoted by `_` or by :n:`?@ident` when non linear patterns are expected). - .. cmdv:: Search { + [-]@term_pattern_string } + .. cmdv:: Search {+ {? -}@term_pattern_string} where :n:`@term_pattern_string` is a term_pattern, a string, or a string followed @@ -289,17 +289,17 @@ Requests to the environment prefixed by `-`, the search excludes the objects that mention that term_pattern or that string. - .. cmdv:: Search @term_pattern_string … @term_pattern_string inside {+ @qualid } + .. cmdv:: Search {+ {? -}@term_pattern_string} inside {+ @qualid } This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. - .. cmdv:: Search @term_pattern_string … @term_pattern_string outside {+ @qualid } + .. cmdv:: Search {+ {? -}@term_pattern_string} outside {+ @qualid } This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence. - .. cmdv:: @selector: Search [-]@term_pattern_string … [-]@term_pattern_string + .. cmdv:: @selector: Search {+ {? -}@term_pattern_string} This specifies the goal on which to search hypothesis (see Section :ref:`invocation-of-tactics`). @@ -353,7 +353,7 @@ Requests to the environment This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. - .. cmdv:: SearchHead term outside {+ @qualid } + .. cmdv:: SearchHead @term outside {+ @qualid } This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence. @@ -443,7 +443,7 @@ Requests to the environment SearchRewrite (_ + _ + _). - .. cmdv:: SearchRewrite term inside {+ @qualid } + .. cmdv:: SearchRewrite @term inside {+ @qualid } This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. @@ -622,7 +622,7 @@ file is a particular case of module called *library file*. but if a further module, say `A`, contains a command :cmd:`Require Export` `B`, then the command :cmd:`Require Import` `A` also imports the module `B.` - .. cmdv:: Require [Import | Export] {+ @qualid } + .. cmdv:: Require {| Import | Export } {+ @qualid } This loads the modules named by the :token:`qualid` sequence and their recursive @@ -988,7 +988,7 @@ Controlling display This option controls the normal displaying. -.. opt:: Warnings "{+, {? %( - %| + %) } @ident }" +.. opt:: Warnings "{+, {? {| - | + } } @ident }" :name: Warnings This option configures the display of warnings. It is experimental, and |