From 9a6946d645ff2126235e7283d07e89f01147d43b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 13 Dec 2024 15:12:44 +0100 Subject: [PATCH] Doc: rename `coqtop::` -> `rocqtop::`, `coqdoc::` -> `rocqdoc::` The implementation is unchanged, ie it's still called coqdomain, calls coqtop, produces CSS classes named coqdoc-keyword etc --- doc/sphinx/README.rst | 36 +- doc/sphinx/README.template.rst | 20 +- doc/sphinx/addendum/extraction.rst | 20 +- doc/sphinx/addendum/generalized-rewriting.rst | 40 +- doc/sphinx/addendum/implicit-coercions.rst | 32 +- doc/sphinx/addendum/micromega.rst | 12 +- .../addendum/miscellaneous-extensions.rst | 4 +- doc/sphinx/addendum/program.rst | 14 +- doc/sphinx/addendum/rewrite-rules.rst | 8 +- doc/sphinx/addendum/ring.rst | 26 +- doc/sphinx/addendum/sprop.rst | 38 +- doc/sphinx/addendum/type-classes.rst | 46 +- doc/sphinx/addendum/universe-polymorphism.rst | 126 ++-- doc/sphinx/changes.rst | 2 +- doc/sphinx/language/cic.rst | 2 +- doc/sphinx/language/coq-library.rst | 42 +- doc/sphinx/language/core/assumptions.rst | 2 +- doc/sphinx/language/core/basic.rst | 14 +- doc/sphinx/language/core/coinductive.rst | 20 +- doc/sphinx/language/core/conversion.rst | 6 +- doc/sphinx/language/core/inductive.rst | 116 ++-- doc/sphinx/language/core/modules.rst | 48 +- doc/sphinx/language/core/primitive.rst | 20 +- doc/sphinx/language/core/records.rst | 26 +- doc/sphinx/language/core/sections.rst | 12 +- doc/sphinx/language/core/variants.rst | 20 +- .../language/extensions/arguments-command.rst | 30 +- doc/sphinx/language/extensions/canonical.rst | 52 +- doc/sphinx/language/extensions/evars.rst | 22 +- .../extensions/implicit-arguments.rst | 40 +- doc/sphinx/language/extensions/match.rst | 92 +-- doc/sphinx/practical-tools/coq-commands.rst | 2 +- doc/sphinx/practical-tools/coqide.rst | 2 +- doc/sphinx/proof-engine/ltac.rst | 170 ++--- doc/sphinx/proof-engine/ltac2.rst | 62 +- .../proof-engine/ssreflect-proof-language.rst | 610 +++++++++--------- doc/sphinx/proof-engine/tactics.rst | 180 +++--- .../proof-engine/vernacular-commands.rst | 44 +- doc/sphinx/proofs/automatic-tactics/auto.rst | 44 +- doc/sphinx/proofs/automatic-tactics/logic.rst | 6 +- doc/sphinx/proofs/writing-proofs/equality.rst | 48 +- .../proofs/writing-proofs/proof-mode.rst | 66 +- .../writing-proofs/reasoning-inductives.rst | 198 +++--- .../user-extensions/syntax-extensions.rst | 226 +++---- doc/sphinx/using/libraries/funind.rst | 34 +- doc/sphinx/using/libraries/writing.rst | 8 +- doc/tools/coqrst/coqdomain.py | 20 +- stdlib/doc/sphinx/README.template.rst | 20 +- stdlib/doc/sphinx/language/coq-library.rst | 18 +- stdlib/doc/tools/coqrst/coqdomain.py | 20 +- 50 files changed, 1383 insertions(+), 1383 deletions(-) diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index b99327914531..4200d61cd329 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -223,16 +223,16 @@ Coq directives In addition to the objects above, the ``coqrst`` Sphinx plugin defines the following directives: -``.. coqtop::`` A reST directive to describe interactions with Coqtop. +``.. rocqtop::`` A reST directive to describe interactions with Coqtop. Usage:: - .. coqtop:: options… + .. rocqtop:: options… Coq code to send to coqtop Example:: - .. coqtop:: in reset + .. rocqtop:: in reset Print nat. Definition a := 1. @@ -261,20 +261,20 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo Be careful when using it to surround the code block with a sentence explaining what extra requirement is needed to compile it. - ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks + ``coqtop``\ 's state is preserved across consecutive ``.. rocqtop::`` blocks of the same document (``coqrst`` creates a single ``coqtop`` process per reST source file). Use the ``reset`` option to reset Coq's state. -``.. coqdoc::`` A reST directive to display Coqtop-formatted source code. +``.. rocqdoc::`` A reST directive to display Coqtop-formatted source code. Usage:: - .. coqdoc:: + .. rocqdoc:: Coq code to highlight Example:: - .. coqdoc:: + .. rocqdoc:: Definition test := 1. @@ -292,7 +292,7 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo The following adds ``plus_comm`` to the ``plu`` database: - .. coqdoc:: + .. rocqdoc:: Hint Resolve plus_comm : plu. @@ -455,7 +455,7 @@ DON'T .. tacv:: assert form as simple_intropattern -Using the ``.. coqtop::`` directive for syntax highlighting +Using the ``.. rocqtop::`` directive for syntax highlighting ----------------------------------------------------------- DO @@ -463,13 +463,13 @@ DO A tactic of the form: - .. coqdoc:: + .. rocqdoc:: do [ t1 | … | tn ]. is equivalent to the standard Ltac expression: - .. coqdoc:: + .. rocqdoc:: first [ t1 | … | tn ]. @@ -478,13 +478,13 @@ DON'T A tactic of the form: - .. coqtop:: in + .. rocqtop:: in do [ t1 | … | tn ]. is equivalent to the standard Ltac expression: - .. coqtop:: in + .. rocqtop:: in first [ t1 | … | tn ]. @@ -513,7 +513,7 @@ DO Here is a useful axiom: - .. coqdoc:: + .. rocqdoc:: Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. @@ -531,7 +531,7 @@ DON'T .. example:: - .. coqdoc:: + .. rocqdoc:: Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. @@ -541,13 +541,13 @@ Tips and tricks Nested lemmas ------------- -The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas (which by default results in a failure):: +The ``.. rocqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas (which by default results in a failure):: - .. coqtop:: all + .. rocqtop:: all Lemma l1: 1 + 1 = 2. - .. coqtop:: all + .. rocqtop:: all Lemma l2: 2 + 2 <> 1. diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 9dd469d29d52..374f91c44542 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -190,7 +190,7 @@ DON'T .. tacv:: assert form as simple_intropattern -Using the ``.. coqtop::`` directive for syntax highlighting +Using the ``.. rocqtop::`` directive for syntax highlighting ----------------------------------------------------------- DO @@ -198,13 +198,13 @@ DO A tactic of the form: - .. coqdoc:: + .. rocqdoc:: do [ t1 | … | tn ]. is equivalent to the standard Ltac expression: - .. coqdoc:: + .. rocqdoc:: first [ t1 | … | tn ]. @@ -213,13 +213,13 @@ DON'T A tactic of the form: - .. coqtop:: in + .. rocqtop:: in do [ t1 | … | tn ]. is equivalent to the standard Ltac expression: - .. coqtop:: in + .. rocqtop:: in first [ t1 | … | tn ]. @@ -248,7 +248,7 @@ DO Here is a useful axiom: - .. coqdoc:: + .. rocqdoc:: Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. @@ -266,7 +266,7 @@ DON'T .. example:: - .. coqdoc:: + .. rocqdoc:: Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. @@ -276,13 +276,13 @@ Tips and tricks Nested lemmas ------------- -The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas (which by default results in a failure):: +The ``.. rocqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas (which by default results in a failure):: - .. coqtop:: all + .. rocqtop:: all Lemma l1: 1 + 1 = 2. - .. coqtop:: all + .. rocqtop:: all Lemma l2: 2 + 2 <> 1. diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index dd9ef6abc756..e0df34f1e864 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -18,7 +18,7 @@ to any of the three. the extraction framework should first be loaded explicitly via ``From Corelib Require Extraction``. -.. coqtop:: in +.. rocqtop:: in From Corelib Require Extraction. @@ -294,7 +294,7 @@ what ML term corresponds to a given axiom. The number of type variables is checked by the system. For example: - .. coqtop:: in + .. rocqtop:: in Axiom Y : Set -> Set -> Set. Extract Constant Y "'a" "'b" => " 'a * 'b ". @@ -303,7 +303,7 @@ what ML term corresponds to a given axiom. The extraction recognizes whether the realized axiom should become a ML type constant or a ML object declaration. For example: - .. coqtop:: in + .. rocqtop:: in Axiom X:Set. Axiom x:X. @@ -404,7 +404,7 @@ native boolean type instead of the Rocq one. The syntax is the following: Typical examples are the following: -.. coqtop:: in +.. rocqtop:: in Extract Inductive unit => "unit" [ "()" ]. Extract Inductive bool => "bool" [ "true" "false" ]. @@ -417,7 +417,7 @@ Typical examples are the following: OCaml's lexical criteria for an infix symbol, then the rest of the string is used as an infix constructor or type. -.. coqtop:: in +.. rocqtop:: in Extract Inductive list => "list" [ "[]" "(::)" ]. Extract Inductive prod => "(*)" [ "(,)" ]. @@ -425,7 +425,7 @@ Typical examples are the following: As an example of translation to a non-inductive datatype, let's turn ``nat`` into OCaml ``int`` (see caveat above): -.. coqtop:: in +.. rocqtop:: in Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))". @@ -448,7 +448,7 @@ OCaml code with C code, the linker needs to know For example: - .. coqtop:: in + .. rocqtop:: in From Corelib Require Extraction. Extract Inductive nat => int [ "0" "Stdlib.Int.succ" ]. @@ -629,7 +629,7 @@ alright but the generated code may be refused by the ML type checker. A very well known example is the ``distr-pair`` function: -.. coqtop:: in +.. rocqtop:: in Definition dp {A B:Type}(x:A)(y:B)(f:forall C:Type, C->C) := (f A x, f B y). @@ -651,7 +651,7 @@ Secondly, some Rocq definitions may have no counterpart in ML. This happens when there is a quantification over types inside the type of a constructor; for example: -.. coqtop:: in +.. rocqtop:: in Inductive anything : Type := dummy : forall A:Set, A -> anything. @@ -698,7 +698,7 @@ where ``diveucl`` is a type for the pair of the quotient and the modulo, plus some logical assertions that disappear during extraction. We can now extract this program to OCaml: -.. coqtop:: reset all extra +.. rocqtop:: reset all extra From Corelib Require Extraction. From Stdlib Require Import Euclid Wf_nat. diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 4d95638695f8..16dafbcf38c8 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -121,7 +121,7 @@ parameters is any term :math:`f \, t_1 \ldots t_n`. morphism parametric over ``A`` that respects the relation instance ``(set_eq A)``. The latter condition is proved by showing: - .. coqdoc:: + .. rocqdoc:: forall (A: Type) (S1 S1' S2 S2': list A), set_eq A S1 S1' -> @@ -216,7 +216,7 @@ They also support the :attr:`universes(polymorphic)` attributes. For Leibniz equality, we may declare: - .. coqdoc:: + .. rocqdoc:: Add Parametric Relation (A : Type) : A (@eq A) [reflexivity proved by @refl_equal A] @@ -247,7 +247,7 @@ following command. homogeneous sets and we declare set equality as a parametric equivalence relation and union of two sets as a parametric morphism. - .. coqtop:: in + .. rocqtop:: in Require Export Setoid. Require Export Relation_Definitions. @@ -286,7 +286,7 @@ following command. (maximally inserted) implicit arguments. If ``A`` is always set as maximally implicit in the previous example, one can write: - .. coqdoc:: + .. rocqdoc:: Add Parametric Relation A : (set A) eq_set reflexivity proved by eq_set_refl @@ -304,12 +304,12 @@ following command. properties over ``eq_set`` and ``union`` can be established from the two declarations above. - .. coqtop:: in + .. rocqtop:: in Goal forall (S : set nat), eq_set (union (union S (empty nat)) S) (union S S). - .. coqtop:: in + .. rocqtop:: in Proof. intros. rewrite empty_neutral. reflexivity. Qed. @@ -489,7 +489,7 @@ various combinations of properties on relations and morphisms are represented as records and instances of these classes are put in a hint database. For example, the declaration: -.. coqdoc:: +.. rocqdoc:: Add Parametric Relation (x1 : T1) ... (xn : Tn) : (A t1 ... tn) (Aeq t′1 ... t′m) [reflexivity proved by refl] @@ -500,7 +500,7 @@ hint database. For example, the declaration: is equivalent to an instance declaration: -.. coqdoc:: +.. rocqdoc:: Instance id (x1 : T1) ... (xn : Tn) : @Equivalence (A t1 ... tn) (Aeq t′1 ... t′m) := [Equivalence_Reflexive := refl] @@ -526,7 +526,7 @@ registered as parametric relations and morphisms. .. example:: First class setoids - .. coqtop:: in reset + .. rocqtop:: in reset Require Import Relation_Definitions Setoid. @@ -686,16 +686,16 @@ declared as morphisms in the ``Classes.Morphisms_Prop`` module. For example, to declare that universal quantification is a morphism for logical equivalence: -.. coqtop:: none +.. rocqtop:: none Require Import Morphisms. -.. coqtop:: in +.. rocqtop:: in Instance all_iff_morphism (A : Type) : Proper (pointwise_relation A iff ==> iff) (@all A). -.. coqtop:: all abort +.. rocqtop:: all abort Proof. simpl_relation. @@ -717,7 +717,7 @@ functional arguments (or whatever subrelation of the pointwise extension). For example, one could declare the ``map`` combinator on lists as a morphism: -.. coqdoc:: +.. rocqdoc:: Instance map_morphism `{Equivalence A eqA, Equivalence B eqB} : Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B). @@ -776,7 +776,7 @@ is used even when rewriting with individual lemmas. .. example:: - .. coqtop:: reset in + .. rocqtop:: reset in Require Setoid. Definition f x y := 2*x + y. @@ -787,7 +787,7 @@ is used even when rewriting with individual lemmas. 2 * g 1 8 = 20. Proof. - .. coqtop:: all + .. rocqtop:: all intros. (* By default, this rewrite succeeds by unifying f with g. *) assert_succeeds (setoid_rewrite double_f). @@ -808,7 +808,7 @@ is used even when rewriting with individual lemmas. assert_succeeds (setoid_rewrite double_f). assert_succeeds (rewrite_strat bottomup double_f). - .. coqtop:: none + .. rocqtop:: none exact eq_refl. Qed. @@ -1038,7 +1038,7 @@ on success. It is stronger than the tactic ``fold``. The type of `andbC` is `forall a b : bool, a && b = b && a`. - .. coqtop:: all + .. rocqtop:: all Require Import ssrbool. Set Printing Parentheses. @@ -1046,17 +1046,17 @@ on success. It is stronger than the tactic ``fold``. Goal forall a b c : bool, a && b && c = true. rewrite_strat innermost andbC. - .. coqtop:: none + .. rocqtop:: none Abort. Goal forall a b c : bool, a && b && c = true. Using :n:`outermost` instead gives this result: - .. coqtop:: all + .. rocqtop:: all rewrite_strat outermost andbC. - .. coqtop:: none + .. rocqtop:: none Abort. diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index ecad9176a3a5..08ad136b20a2 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -348,7 +348,7 @@ There are three situations: We first give an example of coercion between atomic inductive types - .. coqtop:: all + .. rocqtop:: all Definition bool_in_nat (b:bool) := if b then 0 else 1. Coercion bool_in_nat : bool >-> nat. @@ -365,7 +365,7 @@ There are three situations: We give an example of coercion between classes with parameters. - .. coqtop:: all + .. rocqtop:: all Parameters (C : nat -> Set) (D : nat -> bool -> Set) (E : bool -> Set). Parameter f : forall n:nat, C n -> D (S n) true. @@ -384,7 +384,7 @@ There are three situations: :g:`forall x : A', B'`, we have to coerce ``A'`` towards ``A`` and ``B`` towards ``B'``. An example is given below: - .. coqtop:: all + .. rocqtop:: all Parameters (A B : Set) (h : A -> B). Coercion h : A >-> B. @@ -398,7 +398,7 @@ There are three situations: Remark the changes in the result following the modification of the previous example. - .. coqtop:: all + .. rocqtop:: all Parameter U' : (C 0 -> B) -> nat. Parameter t' : E true -> A. @@ -418,7 +418,7 @@ There are three situations: functions. In :g:`forall x:A,B`, such a coercion path may also be applied to ``B`` if necessary. - .. coqtop:: all + .. rocqtop:: all Parameter Graph : Type. Parameter Node : Graph -> Type. @@ -438,7 +438,7 @@ There are three situations: ``f`` is replaced by the term obtained by applying to ``f`` the coercion path between ``A`` and ``Funclass`` if it exists. - .. coqtop:: all + .. rocqtop:: all Parameter bij : Set -> Set -> Set. Parameter ap : forall A B:Set, bij A B -> A -> B. @@ -455,7 +455,7 @@ There are three situations: Notice the :n:`:>` on `ssort` making it a :term:`reversible coercion`. - .. coqtop:: in + .. rocqtop:: in Structure S := { ssort :> Type; @@ -464,7 +464,7 @@ There are three situations: Definition test (s : S) := sstuff s. Canonical Structure S_nat := {| ssort := nat; sstuff := 0; |}. - .. coqtop:: all + .. rocqtop:: all Check test (nat : Type). @@ -475,7 +475,7 @@ There are three situations: Notice there is no `:>` on `ssort'` and the added :cmd:`Coercion` compared to the previous example. - .. coqtop:: in + .. rocqtop:: in Structure S' := { ssort' : Type; @@ -487,13 +487,13 @@ There are three situations: Since there's no `:>` on the definition of `ssort'`, the :attr:`reversible` attribute is not set: - .. coqtop:: all + .. rocqtop:: all Fail Check test' (nat : Type). The attribute can be set after declaring the coercion: - .. coqtop:: all + .. rocqtop:: all #[reversible] Coercion ssort'. Check test' (nat : Type). @@ -502,22 +502,22 @@ There are three situations: .. example:: Identity coercions. - .. coqtop:: in + .. rocqtop:: in Definition fct := nat -> nat. Parameter incr_fct : Set. Parameter fct_of_incr_fct : incr_fct -> fct. - .. coqtop:: all + .. rocqtop:: all Fail Coercion fct_of_incr_fct : incr_fct >-> Funclass. - .. coqtop:: in + .. rocqtop:: in Coercion fct_of_incr_fct : incr_fct >-> fct. Parameter f' : incr_fct. - .. coqtop:: all + .. rocqtop:: all Check f' : fct. Fail Check f' 0. @@ -528,6 +528,6 @@ There are three situations: Let us see the resulting graph after all these examples. - .. coqtop:: all + .. rocqtop:: all Print Graph. diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 16a50a87c7a0..7762c5dea753 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -324,7 +324,7 @@ proof by abstracting monomials by variables. following goal: .. needs csdp -.. coqdoc:: +.. rocqdoc:: Require Import ZArith Psatz. Open Scope Z_scope. @@ -430,7 +430,7 @@ obtain :math:`-1`. Thus, by Theorem :ref:`Psatz `, the goal is valid. The :tacn:`lra` tactic automatically proves the following goal. - .. coqtop:: in extra + .. rocqtop:: in extra From Stdlib Require Import QArith Lqa. #[local] Open Scope Q_scope. @@ -451,7 +451,7 @@ obtain :math:`-1`. Thus, by Theorem :ref:`Psatz `, the goal is valid. This is done thanks to the :term:`cone expression` :math:`p_2 + p_1 + 3 \times p_0 \equiv -1`. - .. coqtop:: all extra + .. rocqtop:: all extra From Stdlib.micromega Require Import RingMicromega QMicromega EnvRing Tauto. @@ -469,7 +469,7 @@ obtain :math:`-1`. Thus, by Theorem :ref:`Psatz `, the goal is valid. ``QTautoChecker ff wit`` returns ``true``, then the goal represented by ``ff`` is valid. - .. coqtop:: in extra + .. rocqtop:: in extra Lemma example_lra' x y : x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3. Proof. @@ -487,14 +487,14 @@ obtain :math:`-1`. Thus, by Theorem :ref:`Psatz `, the goal is valid. Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp). - .. coqtop:: all extra + .. rocqtop:: all extra pose (varmap := VarMap.Branch (VarMap.Elt y) x VarMap.Empty). let ff' := eval unfold ff in ff in wlra_Q wit ff'. change (eval_bf (Qeval_formula (@VarMap.find Q 0 varmap)) ff). apply (QTautoChecker_sound ff wit). - .. coqtop:: in extra + .. rocqtop:: in extra vm_compute. reflexivity. diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index cb5aec7283c1..9484f2826ce1 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -30,13 +30,13 @@ it provides the following command: .. example:: - .. coqtop:: none + .. rocqtop:: none Module Nat. Axiom mul_add_distr_l : forall n m p : nat, n * (m + p) = n * m + n * p. End Nat. - .. coqtop:: all + .. rocqtop:: all From Corelib Require Derive. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 2cf211d4ec85..91602990d9c2 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -121,11 +121,11 @@ if construct is not treated specially by |Program| so boolean tests in the code are not automatically reflected in the obligations. One can use the :g:`dec` combinator to get the correct hypotheses as in: -.. coqtop:: in +.. rocqtop:: in From Corelib.Program Require Import Basics Tactics. -.. coqtop:: all +.. rocqtop:: all Program Definition id (n : nat) : { x : nat | x = n } := if sumbool_of_bool (Nat.leb n 0) then 0 @@ -175,11 +175,11 @@ Program Fixpoint A :cmd:`Fixpoint` command with the :attr:`program` attribute may also generate obligations. It works with mutually recursive definitions too. For example: -.. coqtop:: reset in +.. rocqtop:: reset in From Corelib.Program Require Import Basics Tactics. -.. coqtop:: all +.. rocqtop:: all Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } := match n with @@ -202,18 +202,18 @@ Here we have one obligation for each branch (branches for :g:`0` and ``(S 0)`` are automatically generated by the pattern matching compilation algorithm). -.. coqtop:: all +.. rocqtop:: all Obligation 1. -.. coqtop:: reset none +.. rocqtop:: reset none From Corelib.Program Require Import Basics Tactics Wf. One can use a well-founded order or a measure as termination orders using the syntax: -.. coqtop:: in +.. rocqtop:: in Program Fixpoint div2 (n : nat) {measure n} : { x : nat | n = 2 * x \/ n = 2 * x + 1 } := match n with diff --git a/doc/sphinx/addendum/rewrite-rules.rst b/doc/sphinx/addendum/rewrite-rules.rst index 7118dac573f4..2c188ef7700f 100644 --- a/doc/sphinx/addendum/rewrite-rules.rst +++ b/doc/sphinx/addendum/rewrite-rules.rst @@ -36,7 +36,7 @@ but they may still reduce using the provided rules, unlike axioms. Binds an :n:`@ident` to a :n:`@type` as a symbol. - .. coqtop:: in + .. rocqtop:: in Symbol pplus : nat -> nat -> nat. Notation "a ++ b" := (pplus a b). @@ -61,7 +61,7 @@ When a rule is applied, the term is matched against the pattern, subterms aligned with pattern variables are collected and then substituted into the replacement, which is returned. - .. coqtop:: all + .. rocqtop:: all Rewrite Rule pplus_rewrite := | ?n ++ 0 => ?n @@ -112,7 +112,7 @@ Note that if in the replacement, the context was extended with a variable bearin this explicit substitution is inferred automatically (like for existential variable instantiations). - .. coqtop:: all warn + .. rocqtop:: all warn Symbol raise : forall (A : Type), A. Rewrite Rule raise_nat := @@ -139,7 +139,7 @@ which in turn must imply the constraints needed for the replacement. You can make the declared constraints extensible so all inferred constraints from the left-hand side are used for the replacement. - .. coqtop:: reset all warn + .. rocqtop:: reset all warn #[universes(polymorphic)] Symbol raise@{q|u|} : forall (A : Type@{q|u}), A. Rewrite Rule raise_nat := diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 6f756e91d1ac..927734bb3d31 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -159,7 +159,7 @@ Concrete usage .. example:: - .. coqtop:: all extra + .. rocqtop:: all extra From Stdlib Require Import ZArith. Open Scope Z_scope. @@ -211,7 +211,7 @@ be either Leibniz equality, or any relation declared as a setoid (see :ref:`tactics-enabled-on-user-provided-relations`). The definitions of ring and semiring (see module ``Ring_theory``) are: -.. coqdoc:: +.. rocqdoc:: Record ring_theory : Prop := mk_rt { Radd_0_l : forall x, 0 + x == x; @@ -249,7 +249,7 @@ coefficients could be the rational numbers, upon which the ring operations can be implemented. The fact that there exists a morphism is defined by the following properties: -.. coqdoc:: +.. rocqdoc:: Record ring_morph : Prop := mkmorph { morph0 : [cO] == 0; @@ -297,7 +297,7 @@ This implementation of ring can also recognize simple power expressions as ring expressions. A power function is specified by the following property: -.. coqtop:: in extra +.. rocqtop:: in extra From Stdlib Require Import Reals. Section POWER. @@ -451,7 +451,7 @@ The interested reader is strongly advised to have a look at the file ``Ring_polynom.v``. Here a type for polynomials is defined: -.. coqdoc:: +.. rocqdoc:: Inductive PExpr : Type := | PEc : C -> PExpr @@ -466,7 +466,7 @@ file ``Ring_polynom.v``. Here a type for polynomials is defined: Polynomials in normal form are defined as: -.. coqdoc:: +.. rocqdoc:: Inductive Pol : Type := | Pc : C -> Pol @@ -483,7 +483,7 @@ polynomial to an element of the concrete ring, and the second one that does the same for normal forms: -.. coqdoc:: +.. rocqdoc:: Definition PEeval : list R -> PExpr -> R := [...]. @@ -494,7 +494,7 @@ A function to normalize polynomials is defined, and the big theorem is its correctness w.r.t interpretation, that is: -.. coqdoc:: +.. rocqdoc:: Definition norm : PExpr -> Pol := [...]. Lemma Pphi_dev_ok : @@ -566,7 +566,7 @@ Dealing with fields .. example:: - .. coqtop:: all extra + .. rocqtop:: all extra From Stdlib Require Import Reals. Open Scope R_scope. @@ -582,7 +582,7 @@ Dealing with fields .. example:: :tacn:`field` that generates side goals - .. coqtop:: reset all extra + .. rocqtop:: reset all extra From Stdlib Require Import Reals. Goal forall x y:R, @@ -638,7 +638,7 @@ also supported. The equality can be either Leibniz equality, or any relation declared as a setoid (see :ref:`tactics-enabled-on-user-provided-relations`). The definition of fields and semifields is: -.. coqdoc:: +.. rocqdoc:: Record field_theory : Prop := mk_field { F_R : ring_theory rO rI radd rmul rsub ropp req; @@ -658,7 +658,7 @@ fields and semifields is: The result of the normalization process is a fraction represented by the following type: -.. coqdoc:: +.. rocqdoc:: Record linear : Type := mk_linear { num : PExpr C; @@ -717,7 +717,7 @@ First Samuel Boutin designed the tactic ``ACDSimpl``. This tactic did lot of rewriting. But the proofs terms generated by rewriting were too big for Coq’s type checker. Let us see why: -.. coqtop:: reset all extra +.. rocqtop:: reset all extra From Stdlib Require Import ZArith. Open Scope Z_scope. diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 1d22ce561d72..c6148927fcd0 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -36,7 +36,7 @@ Basic constructs The purpose of :math:`\SProp` is to provide types where all elements are convertible: -.. coqtop:: all +.. rocqtop:: all Theorem irrelevance (A : SProp) (P : A -> Prop) : forall x : A, P x -> forall y : A, P y. Proof. @@ -48,14 +48,14 @@ Since we have definitional :ref:`eta-expansion-sect` for functions, the property of being a type of definitionally irrelevant values is impredicative, and so is :math:`\SProp`: -.. coqtop:: all +.. rocqtop:: all Check fun (A:Type) (B:A -> SProp) => (forall x:A, B x) : SProp. In order to keep conversion tractable, cumulativity for :math:`\SProp` is forbidden. -.. coqtop:: all +.. rocqtop:: all Fail Check (fun (A:SProp) => A : Type). @@ -63,17 +63,17 @@ We can explicitly lift strict propositions into the relevant world by using a wrapping inductive type. The inductive stops definitional proof irrelevance from escaping. -.. coqtop:: in +.. rocqtop:: in Inductive Box (A:SProp) : Prop := box : A -> Box A. Arguments box {_} _. -.. coqtop:: all +.. rocqtop:: all Fail Check fun (A:SProp) (x y : Box A) => eq_refl : x = y. .. doesn't get merged with the above if coqdoc -.. coqtop:: in +.. rocqtop:: in Definition box_irrelevant (A:SProp) (x y : Box A) : x = y := match x, y with box x, box y => eq_refl end. @@ -81,7 +81,7 @@ proof irrelevance from escaping. In the other direction, we can use impredicativity to "squash" a relevant type, making an irrelevant approximation. -.. coqdoc:: +.. rocqdoc:: Definition iSquash (A:Type) : SProp := forall P : SProp, (A -> P) -> P. @@ -93,7 +93,7 @@ relevant type, making an irrelevant approximation. Or more conveniently (but equivalently) -.. coqdoc:: +.. rocqdoc:: Inductive Squash (A:Type) : SProp := squash : A -> Squash A. @@ -101,11 +101,11 @@ Most inductives types defined in :math:`\SProp` are squashed types, i.e. they can only be eliminated to construct proofs of other strict propositions. Empty types are the only exception. -.. coqtop:: in +.. rocqtop:: in Inductive sEmpty : SProp := . -.. coqtop:: all +.. rocqtop:: all Check sEmpty_rect. @@ -117,7 +117,7 @@ propositions. Empty types are the only exception. Primitive records in :math:`\SProp` are allowed when fields are strict propositions, for instance: -.. coqtop:: in +.. rocqtop:: in Set Primitive Projections. Record sProd (A B : SProp) : SProp := { sfst : A; ssnd : B }. @@ -126,12 +126,12 @@ On the other hand, to avoid having definitionally irrelevant types in non-:math:`\SProp` sorts (through record η-extensionality), primitive records in relevant sorts must have at least one relevant field. -.. coqtop:: all +.. rocqtop:: all Set Warnings "+non-primitive-record". Fail Record rBox (A:SProp) : Prop := rbox { runbox : A }. -.. coqdoc:: +.. rocqdoc:: Record ssig (A:Type) (P:A -> SProp) : Type := { spr1 : A; spr2 : P spr1 }. @@ -144,7 +144,7 @@ Encodings for strict propositions The elimination for unit types can be encoded by a trivial function thanks to proof irrelevance: -.. coqdoc:: +.. rocqdoc:: Inductive sUnit : SProp := stt. Definition sUnit_rect (P:sUnit->Type) (v:P stt) (x:sUnit) : P x := v. @@ -152,7 +152,7 @@ thanks to proof irrelevance: By using empty and unit types as base values, we can encode other strict propositions. For instance: -.. coqdoc:: +.. rocqdoc:: Definition is_true (b:bool) : SProp := if b then sUnit else sEmpty. @@ -182,7 +182,7 @@ Definitional UIP Definitional UIP involves a special reduction rule through which reduction depends on conversion. Consider the following code: -.. coqtop:: in +.. rocqtop:: in Set Definitional UIP. @@ -206,7 +206,7 @@ y` reduces if and only if `x` and `y` are convertible. Such matches are indicated in the printed representation by inserting a cast around the discriminee: -.. coqtop:: out +.. rocqtop:: out Print hidden_arrow. @@ -217,7 +217,7 @@ The special reduction rule of UIP combined with an impredicative sort breaks termination of reduction :cite:`abel19:failur_normal_impred_type_theor`: -.. coqtop:: all +.. rocqtop:: all Axiom all_eq : forall (P Q:Prop), P -> Q -> seq P Q. @@ -266,7 +266,7 @@ proof relevant. This :term:`flag` enables debug printing of relevance marks. It is off by default. Note that :flag:`Printing All` does not affect printing of relevance marks. - .. coqtop:: all + .. rocqtop:: all Set Printing Relevance Marks. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index f5f429813594..f09afc178396 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -17,7 +17,7 @@ Typeclass and instance declarations The syntax for typeclasses and instance declarations is the same as the record syntax: -.. coqdoc:: +.. rocqdoc:: Class classname (p1 : t1) ⋯ (pn : tn) [: sort] := { f1 : u1 ; ⋯ ; fm : um }. @@ -31,7 +31,7 @@ instantiation of the record type. We’ll use the following example typeclass in the rest of the chapter: -.. coqtop:: in +.. rocqtop:: in Class EqDec (A : Type) := { eqb : A -> A -> bool ; @@ -40,7 +40,7 @@ We’ll use the following example typeclass in the rest of the chapter: This typeclass implements a boolean equality test which is compatible with Leibniz equality on some type. An example implementation is: -.. coqtop:: in +.. rocqtop:: in Instance unit_EqDec : EqDec unit := { eqb x y := true ; @@ -54,7 +54,7 @@ finish the definition (e.g. due to a missing field or non-inferable hole) it must be finished in proof mode. If it is sufficient a trivial proof mode with no open goals is started. -.. coqtop:: in +.. rocqtop:: in #[refine] Instance unit_EqDec' : EqDec unit := { eqb x y := true }. Proof. intros [] [];reflexivity. Defined. @@ -66,13 +66,13 @@ Alternatively, in :flag:`Program Mode` if one does not give all the members in the Instance declaration, Rocq generates obligations for the remaining fields, e.g.: -.. coqtop:: in +.. rocqtop:: in Require Import Program.Tactics. Program Instance eq_bool : EqDec bool := { eqb x y := if x then y else negb y }. -.. coqtop:: all +.. rocqtop:: all Next Obligation. destruct x ; destruct y ; (discriminate || reflexivity). @@ -89,7 +89,7 @@ Binding typeclasses Once a typeclass is declared, one can use it in typeclass binders: -.. coqtop:: all +.. rocqtop:: all Definition neqb {A} {eqa : EqDec A} (x y : A) := negb (eqb x y). @@ -99,7 +99,7 @@ found. In the example above, a constraint ``EqDec A`` is generated and satisfied by ``eqa : EqDec A``. In case no satisfying constraint can be found, an error is raised: -.. coqtop:: all +.. rocqtop:: all Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y). @@ -109,7 +109,7 @@ will use local hypotheses as well as declared lemmas in the ``typeclass_instances`` database. Hence the example can also be written: -.. coqtop:: all +.. rocqtop:: all Definition neqb' A (eqa : EqDec A) (x y : A) := negb (eqb x y). @@ -127,7 +127,7 @@ particular support for typeclasses: Following the previous example, one can write: -.. coqtop:: all +.. rocqtop:: all Generalizable Variables A B C. @@ -142,14 +142,14 @@ Parameterized instances One can declare parameterized instances as in Haskell simply by giving the constraints as a binding context before the instance, e.g.: -.. coqtop:: in +.. rocqtop:: in Program Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := { eqb x y := match x, y with | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb) end }. -.. coqtop:: none +.. rocqtop:: none Admit Obligations. @@ -168,13 +168,13 @@ binding context as an argument, so variables can be implicit, and :ref:`implicit-generalization` can be used. For example: -.. coqtop:: all +.. rocqtop:: all Section EqDec_defs. Context `{EA : EqDec A}. -.. coqtop:: in +.. rocqtop:: in #[ global, program ] Instance option_eqb : EqDec (option A) := { eqb x y := match x, y with @@ -184,7 +184,7 @@ For example: end }. Admit Obligations. -.. coqtop:: all +.. rocqtop:: all End EqDec_defs. @@ -208,14 +208,14 @@ One can also parameterize typeclasses by other typeclasses, generating a hierarchy of typeclasses and superclasses. In the same way, we give the superclasses as a binding context: -.. coqtop:: all +.. rocqtop:: all Class Ord `(E : EqDec A) := { le : A -> A -> bool }. Contrary to Haskell, we have no special syntax for superclasses, but this declaration is equivalent to: -.. coqdoc:: +.. rocqdoc:: Class `(E : EqDec A) => Ord A := { le : A -> A -> bool }. @@ -230,7 +230,7 @@ as a record type with two parameters: a type ``A`` and an ``E`` of type parameter inside generalizing binders: the generalization of superclasses will be done automatically. -.. coqtop:: all +.. rocqtop:: all Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x). @@ -238,7 +238,7 @@ To specify sharing of structures, you may want to explicitly specify the superclasses. You can do this directly in regular binders, and with the ``!`` modifier before typeclass binders. For example: -.. coqtop:: all +.. rocqtop:: all Definition lt `{eqa : EqDec A, !Ord eqa} (x y : A) := andb (le x y) (neqb x y). @@ -253,11 +253,11 @@ Substructures Substructures are components of a typeclass which are themselves instances of a typeclass. They often arise when using typeclasses for logical properties, e.g.: -.. coqtop:: none +.. rocqtop:: none Require Import Relation_Definitions. -.. coqtop:: in +.. rocqtop:: in Class Reflexive (A : Type) (R : relation A) := reflexivity : forall x, R x x. @@ -269,7 +269,7 @@ This declares singleton typeclasses for reflexive and transitive relations, (see the :ref:`singleton class ` variant for an explanation). These may be used as parts of other typeclasses: -.. coqtop:: all +.. rocqtop:: all Class PreOrder (A : Type) (R : relation A) := { PreOrder_Reflexive :: Reflexive A R ; @@ -542,7 +542,7 @@ By default, all :term:`constants ` and local variables are considered should take care not to make opaque any constant that is used to abbreviate a type, like: -.. coqdoc:: +.. rocqdoc:: Definition relation A := A -> A -> Prop. .. versionadded:: 8.15 diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 1503322ca4a5..44e16c9f0479 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -20,7 +20,7 @@ incompatible universe levels. A standard example of the difference between universe *polymorphic* and *monomorphic* definitions is given by the identity function: -.. coqtop:: in +.. rocqtop:: in Definition identity {A : Type} (a : A) := a. @@ -29,7 +29,7 @@ function declares a global universe (automatically named ``identity.u0``) for it Subsequently, if we try to self-apply the identity, we will get an error: -.. coqtop:: all +.. rocqtop:: all Fail Definition selfid := identity (@identity). @@ -41,25 +41,25 @@ itself for this self-application to type check, as the type of A universe polymorphic identity function binds its domain universe level at the definition level instead of making it global. -.. coqtop:: in +.. rocqtop:: in Polymorphic Definition pidentity {A : Type} (a : A) := a. -.. coqtop:: all +.. rocqtop:: all About pidentity. It is then possible to reuse the constant at different levels, like so: -.. coqtop:: in +.. rocqtop:: in Polymorphic Definition selfpid := pidentity (@pidentity). Of course, the two instances of :g:`pidentity` in this definition are different. This can be seen when the :flag:`Printing Universes` flag is on: -.. coqtop:: all +.. rocqtop:: all Set Printing Universes. Print selfpid. @@ -85,11 +85,11 @@ universes appearing in their parameters or fields. A typical example is given by monoids. We first put ourselves in a mode where every declaration is universe-polymorphic: -.. coqtop:: in +.. rocqtop:: in Set Universe Polymorphism. -.. coqtop:: in +.. rocqtop:: in Record Monoid := { mon_car :> Type; mon_unit : mon_car; mon_op : mon_car -> mon_car -> mon_car }. @@ -97,7 +97,7 @@ is universe-polymorphic: A monoid is here defined by a carrier type, a unit in this type and a binary operation. -.. coqtop:: all +.. rocqtop:: all Print Monoid. @@ -105,7 +105,7 @@ The Monoid's carrier universe is polymorphic, hence it is possible to instantiate it for example with :g:`Monoid` itself. First we build the trivial unit monoid in any universe :g:`i >= Set`: -.. coqtop:: in +.. rocqtop:: in Definition unit_monoid@{i} : Monoid@{i} := {| mon_car := unit; mon_unit := tt; mon_op x y := tt |}. @@ -117,7 +117,7 @@ From this we can build a definition for the monoid of monoids, where multiplication is given by the product of monoids. To do so, we first need to define a universe-polymorphic variant of pairs: -.. coqtop:: in +.. rocqtop:: in Record pprod@{i j} (A : Type@{i}) (B : Type@{j}) : Type@{max(i,j)} := ppair { pfst : A; psnd : B }. @@ -128,7 +128,7 @@ first need to define a universe-polymorphic variant of pairs: The monoid of monoids uses the cartesian product of monoids as its operation: -.. coqtop:: in +.. rocqtop:: in Definition monoid_op@{i} (m m' : Monoid@{i}) (x y : mon_car m ** mon_car m') : mon_car m ** mon_car m' := @@ -146,7 +146,7 @@ The monoid of monoids uses the cartesian product of monoids as its operation: mon_unit := unit_monoid@{i}; mon_op := prod_monoid@{i} |}. -.. coqtop:: all +.. rocqtop:: all Print monoids_monoid. @@ -243,13 +243,13 @@ Cumulative, NonCumulative Consider the examples below. -.. coqtop:: in reset +.. rocqtop:: in reset Polymorphic Cumulative Inductive list {A : Type} := | nil : list | cons : A -> list -> list. -.. coqtop:: all +.. rocqtop:: all Set Printing Universes. Print list. @@ -272,7 +272,7 @@ they are comparable at the same type. See :ref:`Conversion-rules` for more details on convertibility and subtyping. The following is an example of a record with non-trivial subtyping relation: -.. coqtop:: all +.. rocqtop:: all Polymorphic Cumulative Record packType := {pk : Type}. About packType. @@ -287,7 +287,7 @@ The following is an example of a record with non-trivial subtyping relation: Looking back at the example of monoids, we can see that they are naturally covariant for cumulativity: -.. coqtop:: in +.. rocqtop:: in Set Universe Polymorphism. @@ -296,7 +296,7 @@ covariant for cumulativity: mon_unit : mon_car; mon_op : mon_car -> mon_car -> mon_car }. -.. coqtop:: all +.. rocqtop:: all Set Printing Universes. Print Monoid. @@ -304,12 +304,12 @@ covariant for cumulativity: This means that a monoid in a lower universe (like the unit monoid in set), can be seen as a monoid in any higher universe, without introducing explicit lifting. -.. coqtop:: in +.. rocqtop:: in Definition unit_monoid : Monoid@{Set} := {| mon_car := unit; mon_unit := tt; mon_op x y := tt |}. -.. coqtop:: all +.. rocqtop:: all Monomorphic Universe i. @@ -318,13 +318,13 @@ be seen as a monoid in any higher universe, without introducing explicit lifting Finally, invariant universes appear when there is no possible subtyping relation between different instances of the inductive. Consider: -.. coqtop:: in +.. rocqtop:: in Polymorphic Cumulative Record monad@{i} := { m : Type@{i} -> Type@{i}; unit : forall (A : Type@{i}), A -> m A }. -.. coqtop:: all +.. rocqtop:: all Set Printing Universes. Print monad. @@ -343,20 +343,20 @@ inferred (it is irrelevant), ``b`` is required to be irrelevant, ``c`` is covariant and ``d`` is invariant. With these annotations ``c`` and ``d`` have less general variances than would be inferred. -.. coqtop:: all +.. rocqtop:: all Polymorphic Cumulative Inductive Dummy@{a *b +c =d} : Prop := dummy. About Dummy. Insufficiently restrictive variance annotations lead to errors: -.. coqtop:: all +.. rocqtop:: all Fail Polymorphic Cumulative Record bad@{*a} := {p : Type@{a}}. .. example:: Demonstration of universe variances - .. coqtop:: in + .. rocqtop:: in Set Printing Universes. Set Universe Polymorphism. @@ -373,35 +373,35 @@ Insufficiently restrictive variance annotations lead to errors: (* An invariant universe blocks cumulativity from upper or lower levels. *) Axiom inv_low : Invariant@{low}. Axiom inv_high : Invariant@{high}. - .. coqtop:: all + .. rocqtop:: all Fail Check (inv_low : Invariant@{high}). Fail Check (inv_high : Invariant@{low}). - .. coqtop:: in + .. rocqtop:: in (* A covariant universe allows cumulativity from a lower level. *) Axiom co_low : Covariant@{low}. Axiom co_high : Covariant@{high}. - .. coqtop:: all + .. rocqtop:: all Check (co_low : Covariant@{high}). Fail Check (co_high : Covariant@{low}). - .. coqtop:: in + .. rocqtop:: in (* An irrelevant universe allows cumulativity from any level *) Axiom irr_low : Irrelevant@{low}. Axiom irr_high : Irrelevant@{high}. - .. coqtop:: all + .. rocqtop:: all Check (irr_low : Irrelevant@{high}). Check (irr_high : Irrelevant@{low}). - .. coqtop:: in + .. rocqtop:: in End Universes. .. example:: A proof using cumulativity - .. coqtop:: in reset + .. rocqtop:: in reset Set Universe Polymorphism. Set Polymorphic Inductive Cumulativity. @@ -409,14 +409,14 @@ Insufficiently restrictive variance annotations lead to errors: Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x. - .. coqtop:: all + .. rocqtop:: all Print eq. The universe of :g:`eq` is irrelevant here, hence proofs of equalities can inhabit any universe. The universe must be big enough to fit `A`. - .. coqtop:: in + .. rocqtop:: in Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b}) := forall f g : (forall a, B a), @@ -493,15 +493,15 @@ generated. It is however often the case that an equation :math:`j = i` would be more appropriate, when :g:`f`\'s universes are fresh for example. Consider the following example: -.. coqtop:: none +.. rocqtop:: none Polymorphic Definition pidentity {A : Type} (a : A) := a. -.. coqtop:: in +.. rocqtop:: in Definition id0 := @pidentity nat 0. -.. coqtop:: all +.. rocqtop:: all Set Printing Universes. Print id0. @@ -613,13 +613,13 @@ Printing universes controlled by providing `With Constraint Sources` or `Without Constraint Sources`. - .. coqtop:: in + .. rocqtop:: in Monomorphic Universes a b c. Monomorphic Definition make_b_lt_c : Type@{c} := Type@{b}. Monomorphic Definition make_a_le_b (F:Type@{b} -> Prop) (X:Type@{a}) := F X. - .. coqtop:: all + .. rocqtop:: all Print Universes Subgraph (a c). @@ -647,11 +647,11 @@ Polymorphic definitions For polymorphic definitions, the declaration of (all) universe levels introduced by a definition uses the following syntax: -.. coqtop:: in +.. rocqtop:: in Polymorphic Definition le@{i j} (A : Type@{i}) : Type@{j} := A. -.. coqtop:: all +.. rocqtop:: all Print le. @@ -666,7 +666,7 @@ can use :cmd:`Show Universes` to display the current context of universes. It is possible to provide only some universe levels and let Rocq infer the others by adding a :g:`+` in the list of bound universe levels: -.. coqtop:: all +.. rocqtop:: all Fail Definition foobar@{u} : Type@{u} := Type. Definition foobar@{u +} : Type@{u} := Type. @@ -679,7 +679,7 @@ definition. Definitions can also be instantiated explicitly, giving their full instance: -.. coqtop:: all +.. rocqtop:: all Check (pidentity@{Set}). Monomorphic Universes k l. @@ -690,7 +690,7 @@ an explicit :g:`Type` are considered rigid for unification and are never minimized. Flexible anonymous universes can be produced with an underscore or by omitting the annotation to a polymorphic definition. -.. coqtop:: all +.. rocqtop:: all Check (fun x => x) : Type -> Type. Check (fun x => x) : Type -> Type@{_}. @@ -716,12 +716,12 @@ underscore or by omitting the annotation to a polymorphic definition. Consider the following definition: - .. coqtop:: in + .. rocqtop:: in Lemma foo@{i} : Type@{i}. Proof. exact Type. Qed. - .. coqtop:: all + .. rocqtop:: all Print foo. @@ -732,14 +732,14 @@ underscore or by omitting the annotation to a polymorphic definition. using the :term:`constant` we don't need to put a value for the inner universe: - .. coqtop:: all + .. rocqtop:: all Check foo@{_}. and when not looking at the :term:`body` we don't mention the private universe: - .. coqtop:: all + .. rocqtop:: all About foo. @@ -747,13 +747,13 @@ underscore or by omitting the annotation to a polymorphic definition. :g:`Defined`, the :flag:`Private Polymorphic Universes` flag may be unset: - .. coqtop:: in + .. rocqtop:: in Unset Private Polymorphic Universes. Lemma bar : Type. Proof. exact Type. Qed. - .. coqtop:: all + .. rocqtop:: all About bar. Fail Check bar@{_}. @@ -761,14 +761,14 @@ underscore or by omitting the annotation to a polymorphic definition. Note that named universes are always public. - .. coqtop:: in + .. rocqtop:: in Set Private Polymorphic Universes. Unset Strict Universe Declaration. Lemma baz : Type@{outer}. Proof. exact Type@{inner}. Qed. - .. coqtop:: all + .. rocqtop:: all About baz. @@ -779,11 +779,11 @@ Sort polymorphism Quantifying over universes does not allow instantiation with `Prop` or `SProp`. For instance -.. coqtop:: in reset +.. rocqtop:: in reset Polymorphic Definition type@{u} := Type@{u}. -.. coqtop:: all +.. rocqtop:: all Fail Check type@{Prop}. @@ -793,7 +793,7 @@ sort qualities are called :gdef:`sort polymorphic`. All sort quality variables must be explicitly bound. -.. coqtop:: all +.. rocqtop:: all Polymorphic Definition sort@{s | u |} := Type@{s|u}. @@ -807,7 +807,7 @@ Instantiating `s` in `Type@{s|u}` with the impredicative `Prop` or `SProp` produces `Prop` or `SProp` respectively regardless of the instantiation fof `u`. -.. coqtop:: all +.. rocqtop:: all Eval cbv in sort@{Prop|Set}. Eval cbv in sort@{Type|Set}. @@ -820,12 +820,12 @@ runs (typically at the end of a definition). :cmd:`Check` and :cmd:`Eval` run minimization so we cannot use them to witness these temporary variables. -.. coqtop:: in +.. rocqtop:: in Goal True. Set Printing Universes. -.. coqtop:: all abort +.. rocqtop:: all abort let c := constr:(sort) in idtac c. @@ -847,7 +847,7 @@ UIP`. For instance -.. coqtop:: all reset +.. rocqtop:: all reset Set Universe Polymorphism. @@ -861,7 +861,7 @@ instantiation `s := Type` does not allow elimination to `Type`. However elimination to `Type` or to a polymorphic sort with `s := Prop` is allowed: -.. coqtop:: all +.. rocqtop:: all Definition Squash_Prop_rect A (P:Squash@{Prop|_} A -> Type) (H:forall x, P (squash _ x)) @@ -880,7 +880,7 @@ However elimination to `Type` or to a polymorphic sort with `s := Prop` is allow such as sigma types may be better defined as primitive records (which do not have this restriction) when possible. - .. coqtop:: all + .. rocqtop:: all Set Primitive Projections. Record sigma@{s|u v|} (A:Type@{s|u}) (B:A -> Type@{s|v}) @@ -907,7 +907,7 @@ sections, except in the following ways: - no monomorphic constraint may refer to a polymorphic universe: - .. coqtop:: all reset + .. rocqtop:: all reset Section Foo. @@ -918,7 +918,7 @@ sections, except in the following ways: :cmd:`Variable`, which may need to be used with universe polymorphism activated (locally by attribute or globally by option): - .. coqtop:: all + .. rocqtop:: all Fail Variable A : (Type@{i} : Type). Polymorphic Variable A : (Type@{i} : Type). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 95084f0aa14c..58bf3894a60f 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -8050,7 +8050,7 @@ Changes in 8.11+beta1 The following features an implicit argument after a local definition. It was wrongly rejected. - .. coqtop:: in + .. rocqtop:: in Definition f := fix f (o := true) {n : nat} m {struct m} := match m with 0 => 0 | S m' => f (n:=n+1) m' end. diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 61195eb94281..dc25694e86b3 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -439,7 +439,7 @@ command, the following is rejected, .. example:: - .. coqtop:: all + .. rocqtop:: all Fail Definition id: Set := forall X:Set,X->X. diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index b5df96154359..df2ea60bd667 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -136,7 +136,7 @@ Propositional Connectives First, we find propositional calculus connectives. At times, it's helpful to know exactly what these notations represent. -.. coqdoc:: +.. rocqdoc:: Inductive True : Prop := I. Inductive False : Prop := . @@ -157,7 +157,7 @@ We also have the `Type` level negation: .. index:: single: notT (term) -.. coqtop:: in +.. rocqtop:: in Definition notT (A:Type) := A -> False. @@ -176,7 +176,7 @@ Quantifiers Then we find first-order quantifiers: -.. coqtop:: in +.. rocqtop:: in Definition all (A:Set) (P:A -> Prop) := forall x:A, P x. Inductive ex (A: Set) (P:A -> Prop) : Prop := @@ -213,7 +213,7 @@ This definition, due to Christine Paulin-Mohring, is equivalent to define ``eq`` as the smallest reflexive relation, and it is also equivalent to Leibniz' equality. -.. coqtop:: in +.. rocqtop:: in Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : eq A x x. @@ -234,7 +234,7 @@ Finally, a few easy lemmas are provided. single: eq_rect (term) single: eq_rect_r (term) -.. coqdoc:: +.. rocqdoc:: Theorem absurd : forall A C:Prop, A -> ~ A -> C. Section equality. @@ -262,7 +262,7 @@ arguments. The theorem are names ``f_equal2``, ``f_equal3``, ``f_equal4`` and ``f_equal5``. For instance ``f_equal3`` is defined the following way. -.. coqtop:: in abort +.. rocqtop:: in abort Theorem f_equal3 : forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) @@ -315,7 +315,7 @@ Programming single: identity (term) single: refl_identity (term) -.. coqtop:: in +.. rocqtop:: in Inductive unit : Set := tt. Inductive bool : Set := true | false. @@ -340,7 +340,7 @@ We then define the disjoint sum of ``A+B`` of two sets ``A`` and single: fst (term) single: snd (term) -.. coqtop:: in +.. rocqtop:: in Inductive sum (A B:Set) : Set := inl (_:A) | inr (_:B). Inductive prod (A B:Set) : Set := pair (_:A) (_:B). @@ -386,7 +386,7 @@ provided. single: sig2 (term) single: exist2 (term) -.. coqtop:: in +.. rocqtop:: in Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x). Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := @@ -405,7 +405,7 @@ constructor of types in ``Type``. single: projT1 (term) single: projT2 (term) -.. coqtop:: in +.. rocqtop:: in Inductive sigT (A:Type) (P:A -> Type) : Type := existT (x:A) (_:P x). Section Projections2. @@ -429,7 +429,7 @@ A related non-dependent construct is the constructive sum single: right (term) single: {A}+{B} (term) -.. coqtop:: in +.. rocqtop:: in Inductive sumbool (A B:Prop) : Set := left (_:A) | right (_:B). @@ -444,7 +444,7 @@ in the construction :g:`A+{B}` in ``Set``. single: inright (term) single: A+{B} (term) -.. coqtop:: in +.. rocqtop:: in Inductive sumor (A:Set) (B:Prop) : Set := | inleft (_:A) @@ -458,7 +458,7 @@ Intuitionistic Type Theory. single: Choice2 (term) single: bool_choice (term) -.. coqdoc:: +.. rocqdoc:: Lemma Choice : forall (S S':Set) (R:S -> S' -> Prop), @@ -482,7 +482,7 @@ an exceptional value encoding errors: single: value (term) single: error (term) -.. coqtop:: in +.. rocqtop:: in Definition Exc := option. Definition value := Some. @@ -499,7 +499,7 @@ realizability interpretation. single: absurd_set (term) single: and_rect (term) -.. coqdoc:: +.. rocqdoc:: Definition except := False_rec. Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. @@ -525,7 +525,7 @@ section :tacn:`refine`). This scope is opened by default. The following example is not part of the standard library, but it shows the usage of the notations: - .. coqtop:: in reset + .. rocqtop:: in reset Fixpoint even (n:nat) : bool := match n with @@ -552,7 +552,7 @@ section :tacn:`refine`). This scope is opened by default. Now comes the content of module ``Peano``: -.. coqdoc:: +.. rocqdoc:: Theorem eq_S : forall x y:nat, x = y -> S x = S y. Definition pred (n:nat) : nat := @@ -603,7 +603,7 @@ Finally, it gives the definition of the usual orderings ``le``, .. This emits a notation already used warning but it won't be shown to the user. -.. coqtop:: in warn +.. rocqtop:: in warn Inductive le (n:nat) : nat -> Prop := | le_n : le n n @@ -622,7 +622,7 @@ induction principle. single: nat_case (term) single: nat_double_ind (term) -.. coqdoc:: +.. rocqdoc:: Theorem nat_case : forall (n:nat) (P:nat -> Prop), @@ -649,7 +649,7 @@ well-founded induction, in module ``Wf.v``. single: Acc_rect (term) single: well_founded (term) -.. coqdoc:: +.. rocqdoc:: Section Well_founded. Variable A : Type. @@ -678,7 +678,7 @@ fixpoint equation can be proved. single: Fix_F_inv (term) single: Fix_F_eq (term) -.. coqdoc:: +.. rocqdoc:: Section FixPoint. Variable P : A -> Type. diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index 59c521ca9bfd..b6467e232c62 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -203,7 +203,7 @@ has type :n:`@type`. .. example:: Simple assumptions - .. coqtop:: reset in + .. rocqtop:: reset in Parameter X Y : Set. Parameter (R : X -> Y -> Prop) (S : Y -> X -> Prop). diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 927efabbb087..b107d3b18991 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -159,15 +159,15 @@ Numbers .. example:: Stack overflow with :n:`nat` - .. coqtop:: all reset extra + .. rocqtop:: all reset extra Fail Eval compute in 100000 + 100000. (* gives a stack overflow (not shown) *) - .. coqtop:: in extra + .. rocqtop:: in extra From Stdlib Require Import ZArith. (* for definition of Z *) - .. coqtop:: all extra + .. rocqtop:: all extra Eval compute in (1000000000000000000000000000000000 + 1)%Z. @@ -456,11 +456,11 @@ boldface label "Attribute:". Attributes are listed in the This warning is configured to behave as an error by default. You may turn it into a normal warning by using the :opt:`Warnings` option: - .. coqtop:: none + .. rocqtop:: none Set Silent. - .. coqtop:: all warn + .. rocqtop:: all warn Set Warnings "unsupported-attributes". #[ foo ] Comments. @@ -478,13 +478,13 @@ The following attribute is supported by every command: the command. For instance if the current warning state is `some-warnings,-other-warning`, - .. coqdoc:: + .. rocqdoc:: #[warnings="+other-warning"] Command. is equivalent to - .. coqdoc:: + .. rocqdoc:: Set Warnings "+other-warning". Command. diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index a0e9eefca23e..bb6761f8dc8c 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -39,14 +39,14 @@ More information on coinductive definitions can be found in The type of infinite sequences of natural numbers, usually called streams, is an example of a coinductive type. - .. coqtop:: in + .. rocqtop:: in CoInductive Stream : Set := Seq : nat -> Stream -> Stream. The usual destructors on streams :g:`hd:Stream->nat` and :g:`tl:Str->Str` can be defined as follows: - .. coqtop:: in + .. rocqtop:: in Definition hd (x:Stream) := let (a,s) := x in a. Definition tl (x:Stream) := let (a,s) := x in s. @@ -58,7 +58,7 @@ coinductive definitions are also allowed. The extensional equality on streams is an example of a coinductive type: - .. coqtop:: in + .. rocqtop:: in CoInductive EqSt : Stream -> Stream -> Prop := eqst : forall s1 s2:Stream, @@ -87,11 +87,11 @@ found in e.g. Agda, and preserves subject reduction. The above example can be rewritten in the following way. -.. coqtop:: none +.. rocqtop:: none Reset Stream. -.. coqtop:: all +.. rocqtop:: all Set Primitive Projections. CoInductive Stream : Set := Seq { hd : nat; tl : Stream }. @@ -106,7 +106,7 @@ For instance, propositional η-equality is lost when going to the negative presentation. It is nonetheless logically consistent to recover it through an axiom. -.. coqtop:: all +.. rocqtop:: all Axiom Stream_eta : forall s: Stream, s = Seq (hd s) (tl s). @@ -114,7 +114,7 @@ More generally, as in the case of positive coinductive types, it is consistent to further identify extensional equality of coinductive types with propositional equality: -.. coqtop:: all +.. rocqtop:: all Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2. @@ -162,7 +162,7 @@ Top-level definitions of corecursive functions Section :ref:`coinductive-types` for the definition of :g:`Stream`, :g:`hd` and :g:`tl`): - .. coqtop:: all + .. rocqtop:: all CoFixpoint from (n:nat) : Stream := Seq n (from (S n)). @@ -177,7 +177,7 @@ Top-level definitions of corecursive functions On the contrary, the following recursive function does not satisfy the guard condition: - .. coqtop:: all + .. rocqtop:: all Fail CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream := if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s). @@ -189,7 +189,7 @@ Top-level definitions of corecursive functions evaluated. We can test this using the command :cmd:`Eval`, which computes the normal forms of a term: - .. coqtop:: all + .. rocqtop:: all Eval compute in (from 0). Eval compute in (hd (from 0)). diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst index 71d857526e30..f382294e8238 100644 --- a/doc/sphinx/language/core/conversion.rst +++ b/doc/sphinx/language/core/conversion.rst @@ -19,7 +19,7 @@ closer to its normal form. For example, :term:`zeta-reduction` removes :n:`@ident` with :n:`@term__1` wherever :n:`@ident` appears in :n:`@term__2`. The resulting term may be longer or shorter than the original. -.. coqtop:: all +.. rocqtop:: all Eval cbv zeta in let i := 1 in i + i. @@ -222,7 +222,7 @@ Examples ``+`` is a :ref:`notation ` for ``Nat.add``, which is defined with a :cmd:`Fixpoint`. - .. coqtop:: all abort + .. rocqtop:: all abort Print Nat.add. Goal 1 + 1 = 2. @@ -233,7 +233,7 @@ Examples The term can be fully reduced with `cbv`: - .. coqtop:: all abort + .. rocqtop:: all abort Goal 1 + 1 = 2. cbv. diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 2982dbe63a90..4750a7e631bf 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -121,7 +121,7 @@ A simple inductive type belongs to a universe that is a simple :n:`@sort`. The set of natural numbers is defined as: - .. coqtop:: reset all + .. rocqtop:: reset all Inductive nat : Set := | O : nat @@ -134,7 +134,7 @@ A simple inductive type belongs to a universe that is a simple :n:`@sort`. This definition generates four :term:`induction principles `: :g:`nat_rect`, :g:`nat_ind`, :g:`nat_rec` and :g:`nat_sind`. The type of :g:`nat_ind` is: - .. coqtop:: all + .. rocqtop:: all Check nat_ind. @@ -154,11 +154,11 @@ by giving the type of its arguments alone. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none Reset nat. - .. coqtop:: in + .. rocqtop:: in Inductive nat : Set := O | S (_:nat). @@ -182,7 +182,7 @@ which is a type whose conclusion is a :n:`@sort`. As an example of indexed inductive types, let us define the :g:`even` predicate: - .. coqtop:: all + .. rocqtop:: all Inductive even : nat -> Prop := | even_0 : even O @@ -192,7 +192,7 @@ which is a type whose conclusion is a :n:`@sort`. defined) over natural numbers. The type of its two constructors are the defining clauses of the predicate :g:`even`. The type of :g:`even_ind` is: - .. coqtop:: all + .. rocqtop:: all Check even_ind. @@ -223,7 +223,7 @@ the same parameter values of its specification. A typical example is the definition of polymorphic lists: - .. coqtop:: all + .. rocqtop:: all Inductive list (A:Set) : Set := | nil : list A @@ -232,7 +232,7 @@ the same parameter values of its specification. In the type of :g:`nil` and :g:`cons`, we write ":g:`list A`" and not just ":g:`list`". The constructors :g:`nil` and :g:`cons` have these types: - .. coqtop:: all + .. rocqtop:: all Check nil. Check cons. @@ -240,17 +240,17 @@ the same parameter values of its specification. Observe that the induction principles are also quantified with :g:`(A:Set)`, for example: - .. coqtop:: all + .. rocqtop:: all Check list_ind. Once again, the names of the constructor arguments and the type of the conclusion can be omitted: - .. coqtop:: none + .. rocqtop:: none Reset list. - .. coqtop:: in + .. rocqtop:: in Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A). @@ -261,7 +261,7 @@ the same parameter values of its specification. One can define : - .. coqtop:: all + .. rocqtop:: all Inductive list2 (A:Set) : Set := | nil2 : list2 A @@ -269,7 +269,7 @@ the same parameter values of its specification. that can also be written by specifying only the type of the arguments: - .. coqtop:: all reset + .. rocqtop:: all reset Inductive list2 (A:Set) : Set := | nil2 @@ -277,7 +277,7 @@ the same parameter values of its specification. But the following definition will give an error: - .. coqtop:: all + .. rocqtop:: all Fail Inductive listw (A:Set) : Set := | nilw : listw (A*A) @@ -297,7 +297,7 @@ the same parameter values of its specification. inductive definitions are abstracted over their parameters before type checking constructors, allowing to write: - .. coqtop:: all + .. rocqtop:: all Set Uniform Inductive Parameters. Inductive list3 (A:Set) : Set := @@ -308,7 +308,7 @@ the same parameter values of its specification. and using :cmd:`Context` to give the uniform parameters, like so (cf. :ref:`section-mechanism`): - .. coqtop:: all reset + .. rocqtop:: all reset Section list3. Context (A:Set). @@ -320,7 +320,7 @@ the same parameter values of its specification. For finer control, you can use a ``|`` between the uniform and the non-uniform parameters: - .. coqtop:: in reset + .. rocqtop:: in reset Inductive Acc {A:Type} (R:A->A->Prop) | (x:A) : Prop := Acc_in : (forall y, R y x -> Acc y) -> Acc x. @@ -348,7 +348,7 @@ useful. Use the :cmd:`Scheme` command to generate a useful induction principle. forests. We assume two types :g:`A` and :g:`B` that are given as variables. The types can be declared like this: - .. coqtop:: in + .. rocqtop:: in Parameters A B : Set. @@ -364,7 +364,7 @@ useful. Use the :cmd:`Scheme` command to generate a useful induction principle. To illustrate this point on our example, here are the types of :g:`tree_rec` and :g:`forest_rec`. - .. coqtop:: all + .. rocqtop:: all Check tree_rec. @@ -374,7 +374,7 @@ useful. Use the :cmd:`Scheme` command to generate a useful induction principle. two type variables :g:`A` and :g:`B`, the declaration should be done as follows: - .. coqdoc:: + .. rocqdoc:: Inductive tree (A B:Set) : Set := node : A -> forest A B -> tree A B @@ -495,7 +495,7 @@ constructions. One can define the addition function as : - .. coqtop:: all + .. rocqtop:: all Fixpoint add (n m:nat) {struct n} : nat := match n with @@ -519,7 +519,7 @@ constructions. The following definition is not correct and generates an error message: - .. coqtop:: all + .. rocqtop:: all Fail Fixpoint wrongplus (n m:nat) {struct n} : nat := match m with @@ -534,7 +534,7 @@ constructions. The function computing the addition over the second argument should rather be written: - .. coqtop:: all + .. rocqtop:: all Fixpoint plus (n m:nat) {struct m} : nat := match m with @@ -545,21 +545,21 @@ constructions. **Aside**: Observe that `plus n 0` is reducible but `plus 0 n` is not, the reverse of `Nat.add`, for which `0 + n` is reducible and `n + 0` is not. - .. coqtop:: all + .. rocqtop:: all Goal forall n:nat, plus n 0 = plus 0 n. intros; simpl. (* plus 0 n not reducible *) - .. coqtop:: none + .. rocqtop:: none Abort. - .. coqtop:: all + .. rocqtop:: all Goal forall n:nat, n + 0 = 0 + n. intros; simpl. (* n + 0 not reducible *) - .. coqtop:: none + .. rocqtop:: none Abort. @@ -570,7 +570,7 @@ constructions. the function :g:`mod2` which gives the remainder modulo 2 of a natural number. - .. coqtop:: all + .. rocqtop:: all Fixpoint mod2 (n:nat) : nat := match n with @@ -587,7 +587,7 @@ constructions. The size of trees and forests can be defined the following way: - .. coqtop:: all + .. rocqtop:: all Fixpoint tree_size (t:tree) : nat := match t with @@ -637,7 +637,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` which corresponds to the result of the Rocq declaration: - .. coqtop:: in reset + .. rocqtop:: in reset Inductive list (A:Set) : Set := | nil : list A @@ -658,7 +658,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` which corresponds to the result of the Rocq declaration: - .. coqtop:: in + .. rocqtop:: in Inductive tree : Set := | node : forest -> tree @@ -681,7 +681,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` which corresponds to the result of the Rocq declaration: - .. coqtop:: in + .. rocqtop:: in Inductive even : nat -> Prop := | even_O : even 0 @@ -846,7 +846,7 @@ cases: For instance, if one considers the following variant of a tree type branching over the natural numbers: - .. coqtop:: in + .. rocqtop:: in Inductive nattree (A:Type) : Type := | leaf : nattree A @@ -911,14 +911,14 @@ between universes for inductive types in the Type hierarchy. inductive definition. The following declaration introduces the second-order existential quantifier :math:`∃ X.P(X)`. - .. coqtop:: in + .. rocqtop:: in Inductive exProp (P:Prop->Prop) : Prop := | exP_intro : forall X:Prop, P X -> exProp P. The same definition on :math:`\Set` is not allowed and fails: - .. coqtop:: all + .. rocqtop:: all Fail Inductive exSet (P:Set->Prop) : Set := exS_intro : forall X:Set, P X -> exSet P. @@ -928,7 +928,7 @@ between universes for inductive types in the Type hierarchy. :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT}_{\kw{intro}}` has type :math:`\Type(k)` with :math:`kProp) : Type := exT_intro : forall X:Type, P X -> exType P. @@ -939,7 +939,7 @@ between universes for inductive types in the Type hierarchy. The following inductive definition is rejected because it does not satisfy the positivity condition: - .. coqtop:: all + .. rocqtop:: all Fail Inductive I : Prop := not_I_I (not_I : I -> False) : I. @@ -947,16 +947,16 @@ between universes for inductive types in the Type hierarchy. contradiction from it (we can test this by disabling the :flag:`Positivity Checking` flag): - .. coqtop:: in + .. rocqtop:: in #[bypass_check(positivity)] Inductive I : Prop := not_I_I (not_I : I -> False) : I. - .. coqtop:: all + .. rocqtop:: all Definition I_not_I : I -> ~ I := fun i => match i with not_I_I not_I => not_I end. - .. coqtop:: in + .. rocqtop:: in Lemma contradiction : False. Proof. @@ -974,18 +974,18 @@ between universes for inductive types in the Type hierarchy. Here is another example of an inductive definition which is rejected because it does not satify the positivity condition: - .. coqtop:: all + .. rocqtop:: all Fail Inductive Lam := lam (_ : Lam -> Lam). Again, if we were to accept it, we could derive a contradiction (this time through a non-terminating recursive function): - .. coqtop:: in + .. rocqtop:: in #[bypass_check(positivity)] Inductive Lam := lam (_ : Lam -> Lam). - .. coqtop:: all + .. rocqtop:: all Fixpoint infinite_loop l : False := match l with lam x => infinite_loop (x l) end. @@ -999,7 +999,7 @@ between universes for inductive types in the Type hierarchy. We will see that in presence of an impredicative type they are unsound: - .. coqtop:: all + .. rocqtop:: all Fail Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A. @@ -1010,15 +1010,15 @@ between universes for inductive types in the Type hierarchy. the type :math:`A` with the function :math:`λx. λz. z = x` injecting any type :math:`T` into :math:`T → \Prop`. - .. coqtop:: in + .. rocqtop:: in #[bypass_check(positivity)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A. - .. coqtop:: all + .. rocqtop:: all Definition f (x: A -> Prop): A := introA (fun z => z = x). - .. coqtop:: in + .. rocqtop:: in Lemma f_inj: forall x y, f x = f y -> x = y. Proof. @@ -1034,12 +1034,12 @@ between universes for inductive types in the Type hierarchy. injective function :math:`f` we use Cantor's classic diagonal argument. - .. coqtop:: all + .. rocqtop:: all Definition d: A -> Prop := fun x => exists s, x = f s /\ ~s x. Definition fd: A := f d. - .. coqtop:: in + .. rocqtop:: in Lemma cantor: (d fd) <-> ~(d fd). Proof. @@ -1211,7 +1211,7 @@ example, let us consider the following definition: .. example:: - .. coqtop:: in + .. rocqtop:: in Inductive option (A:Type) : Type := | None : option A @@ -1228,7 +1228,7 @@ if set in :math:`\Prop`. .. example:: - .. coqtop:: all + .. rocqtop:: all Check (fun A:Set => option A). Check (fun A:Prop => option A). @@ -1237,7 +1237,7 @@ Here is another example. .. example:: - .. coqtop:: in + .. rocqtop:: in Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B. @@ -1248,7 +1248,7 @@ eliminations schemes are allowed. .. example:: - .. coqtop:: all + .. rocqtop:: all Check (fun A:Set => prod A). Check (fun A:Prop => prod A A). @@ -1439,7 +1439,7 @@ logical disjunction :math:`A ∨ B` is defined inductively by: .. example:: - .. coqtop:: in + .. rocqtop:: in Inductive or (A B:Prop) : Prop := or_introl : A -> or A B | or_intror : B -> or A B. @@ -1450,7 +1450,7 @@ the proof of :g:`or A B` is not accepted: .. example:: - .. coqtop:: all + .. rocqtop:: all Fail Definition choice (A B: Prop) (x:or A B) := match x with or_introl _ _ a => true | or_intror _ _ b => false end. @@ -1474,7 +1474,7 @@ proof-irrelevance property which is sometimes a useful axiom: .. example:: - .. coqtop:: all + .. rocqtop:: all Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. @@ -1508,7 +1508,7 @@ type. .. example:: - .. coqtop:: all + .. rocqtop:: all Print eq_rec. Require Extraction. @@ -1765,7 +1765,7 @@ command and show the internal representation. .. example:: - .. coqtop:: all + .. rocqtop:: all Fixpoint plus (n m:nat) {struct n} : nat := match n with diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index f5d9bc99ac2d..ab10f21beb83 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -205,7 +205,7 @@ are now available through the dot notation. .. example:: - .. coqtop:: reset in + .. rocqtop:: reset in Module Mod. Definition T:=nat. @@ -213,7 +213,7 @@ are now available through the dot notation. End Mod. Check Mod.T. - .. coqtop:: all + .. rocqtop:: all Fail Check T. Import Mod. @@ -228,7 +228,7 @@ are now available through the dot notation. .. example:: - .. coqtop:: in + .. rocqtop:: in Module A. Module B. @@ -237,7 +237,7 @@ are now available through the dot notation. End A. Import A. - .. coqtop:: all fail + .. rocqtop:: all fail Check B.T. @@ -263,7 +263,7 @@ are now available through the dot notation. .. example:: - .. coqtop:: reset in + .. rocqtop:: reset in Module A. Module B. @@ -274,7 +274,7 @@ are now available through the dot notation. End A. Import A(B.T(..), Z). - .. coqtop:: all + .. rocqtop:: all Check B.T. Check B.C. @@ -359,7 +359,7 @@ are now available through the dot notation. .. example:: - .. coqtop:: reset in + .. rocqtop:: reset in Module A. Definition foo := 0. @@ -368,7 +368,7 @@ are now available through the dot notation. End B. End A. - .. coqtop:: all + .. rocqtop:: all Print Namespace Top. Print Namespace Top.A. @@ -381,18 +381,18 @@ Examples .. example:: Defining a simple module interactively - .. coqtop:: in + .. rocqtop:: in Module M. Definition T := nat. Definition x := 0. - .. coqtop:: all + .. rocqtop:: all Definition y : bool. exact true. - .. coqtop:: in + .. rocqtop:: in Defined. End M. @@ -401,7 +401,7 @@ Inside a module one can define :term:`constants `, prove theorems and else that can be done in the toplevel. Components of a closed module can be accessed using the dot notation: -.. coqtop:: all +.. rocqtop:: all Print M.x. @@ -409,7 +409,7 @@ module can be accessed using the dot notation: .. example:: Defining a simple module type interactively - .. coqtop:: in + .. rocqtop:: in Module Type SIG. Parameter T : Set. @@ -423,7 +423,7 @@ module can be accessed using the dot notation: Since :n:`SIG`, the type of the new module :n:`N`, doesn't define :n:`y` or give the body of :n:`x`, which are not included in :n:`N`. - .. coqtop:: all + .. rocqtop:: all Module N : SIG with Definition T := nat := M. Print N.T. @@ -431,7 +431,7 @@ module can be accessed using the dot notation: Fail Print N.y. .. reset to remove N (undo in last coqtop block doesn't seem to do that), invisibly redefine M, SIG - .. coqtop:: none reset + .. rocqtop:: none reset Module M. Definition T := nat. @@ -449,7 +449,7 @@ module can be accessed using the dot notation: The definition of :g:`N` using the module type expression :g:`SIG` with :g:`Definition T := nat` is equivalent to the following one: -.. coqtop:: in +.. rocqtop:: in Module Type SIG'. Definition T : Set := nat. @@ -468,17 +468,17 @@ If we just want to be sure that our implementation satisfies a given module type without restricting the interface, we can use a transparent constraint -.. coqtop:: in +.. rocqtop:: in Module P <: SIG := M. -.. coqtop:: all +.. rocqtop:: all Print P.y. .. example:: Creating a functor (a module with parameters) - .. coqtop:: in + .. rocqtop:: in Module Two (X Y: SIG). Definition T := (X.T * Y.T)%type. @@ -487,18 +487,18 @@ transparent constraint and apply it to our modules and do some computations: - .. coqtop:: in + .. rocqtop:: in Module Q := Two M N. - .. coqtop:: all + .. rocqtop:: all Eval compute in (fst Q.x + snd Q.x). .. example:: A module type with two sub-modules, sharing some fields - .. coqtop:: in + .. rocqtop:: in Module Type SIG2. Declare Module M1 : SIG. @@ -508,7 +508,7 @@ transparent constraint End M2. End SIG2. - .. coqtop:: in + .. rocqtop:: in Module Mod <: SIG2. Module M1. @@ -592,7 +592,7 @@ their fully qualified name (see :ref:`gallina-definitions`). .. example:: - .. coqtop:: all + .. rocqtop:: all Check 0. diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst index 357735d0e71a..230c8fa9ee59 100644 --- a/doc/sphinx/language/core/primitive.rst +++ b/doc/sphinx/language/core/primitive.rst @@ -10,7 +10,7 @@ The language of terms features 63-bit machine integers as values. The type of such a value is *axiomatized*; it is declared through the following sentence (excerpt from the :g:`PrimInt63` module): -.. coqdoc:: +.. rocqdoc:: Primitive int := #int63_type. @@ -23,7 +23,7 @@ The :g:`PrimInt63` module declares the available operators for this type. For instance, equality of two unsigned primitive integers can be determined using the :g:`Uint63.eqb` function, declared and specified as follows: -.. coqdoc:: +.. rocqdoc:: Primitive eqb := #int63_eq. Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : uint63_scope. @@ -37,13 +37,13 @@ modules. These primitive declarations are regular axioms. As such, they must be trusted and are listed by the :g:`Print Assumptions` command, as in the following example. -.. coqtop:: in reset +.. rocqtop:: in reset From Corelib Require Import PrimInt63 Uint63Axioms. Lemma one_minus_one_is_zero : (sub 1 1 = 0)%uint63. Proof. apply eqb_correct; vm_compute; reflexivity. Qed. -.. coqtop:: all +.. rocqtop:: all Print Assumptions one_minus_one_is_zero. @@ -73,7 +73,7 @@ The language of terms features Binary64 floating-point numbers as values. The type of such a value is *axiomatized*; it is declared through the following sentence (excerpt from the :g:`PrimFloat` module): -.. coqdoc:: +.. rocqdoc:: Primitive float := #float64_type. @@ -81,7 +81,7 @@ This type is equipped with a few operators, that must be similarly declared. For instance, the product of two primitive floats can be computed using the :g:`PrimFloat.mul` function, declared and specified as follows: -.. coqdoc:: +.. rocqdoc:: Primitive mul := #float64_mul. Notation "x * y" := (mul x y) : float_scope. @@ -120,7 +120,7 @@ The language of terms features persistent arrays as values. The type of such a value is *axiomatized*; it is declared through the following sentence (excerpt from the :g:`PArray` module): -.. coqdoc:: +.. rocqdoc:: Primitive array := #array_type. @@ -129,7 +129,7 @@ For instance, elements in an array can be accessed and updated using the :g:`PArray.get` and :g:`PArray.set` functions, declared and specified as follows: -.. coqdoc:: +.. rocqdoc:: Primitive get := #array_get. Primitive set := #array_set. @@ -179,7 +179,7 @@ The language of terms supports immutable strings as values. Primitive strings are *axiomatized*. The type is declared through the following sentence (excerpt from the :g:`PrimString` module): -.. coqdoc:: +.. rocqdoc:: Primitive string := #string_type. @@ -188,7 +188,7 @@ the length of a string can be computed with :g:`PrimString.length`, and the char (i.e., byte) at a given position can be obtained with :g:`PrimString.get`. These functions are defined as follows: -.. coqdoc:: +.. rocqdoc:: Definition char63 := int. diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index 4e29b6e74757..52a525e72126 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -121,7 +121,7 @@ Defining record types The set of rational numbers may be defined as: - .. coqtop:: reset all + .. rocqtop:: reset all Record Rat : Set := mkRat { negative : bool @@ -141,12 +141,12 @@ Defining record types .. example:: Reusing a field name in multiple records - .. coqtop:: in + .. rocqtop:: in Module A. Record R := { f : nat }. End A. Module B. Record S := { f : nat }. End B. - .. coqtop:: all + .. rocqtop:: all Check {| A.f := 0 |}. Check {| B.f := 0 |}. @@ -155,7 +155,7 @@ Defining record types .. example:: Using the "as" clause in a record definition - .. coqtop:: all + .. rocqtop:: all Record MyRecord := { myfield : nat } as VarName. About myfield. (* observe the MyRecord variable is named "VarName" *) @@ -172,7 +172,7 @@ Defining record types Compare to :cmd:`Record` in the previous example: - .. coqtop:: all + .. rocqtop:: all Class MyClass := { myfield2 : nat }. About myfield2. (* Argument name defaults to the class name and is marked implicit *) @@ -252,7 +252,7 @@ Constructing records Constructing the rational :math:`1/2` using either the record or application syntax: - .. coqtop:: in + .. rocqtop:: in Theorem one_two_irred : forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1. Admitted. @@ -295,7 +295,7 @@ Accessing fields (projections) .. example:: Accessing record fields - .. coqtop:: all + .. rocqtop:: all (* projection form *) Eval compute in half.(top). @@ -305,7 +305,7 @@ Accessing fields (projections) .. example:: Matching on records - .. coqtop:: all + .. rocqtop:: all Eval compute in ( match half with @@ -315,13 +315,13 @@ Accessing fields (projections) .. example:: Accessing anonymous record fields with match - .. coqtop:: in + .. rocqtop:: in Record T := const { _ : nat }. Definition gett x := match x with const n => n end. Definition inst := const 3. - .. coqtop:: all + .. rocqtop:: all Eval compute in gett inst. @@ -353,7 +353,7 @@ You can override the display format for specified record types by adding entries .. example:: - .. coqtop:: all + .. rocqtop:: all Check top half. (* off: application form *) Set Printing Projections. @@ -440,7 +440,7 @@ desugared using the unfolded primitive projections and `let` bindings. .. example:: - .. coqtop:: reset all + .. rocqtop:: reset all #[projections(primitive)] Record Sigma A B := sigma { p1 : A; p2 : B p1 }. Arguments sigma {_ _} _ _. @@ -455,7 +455,7 @@ desugared using the unfolded primitive projections and `let` bindings. Matches which are equivalent to just a projection have adhoc handling to avoid generating useless ``let``: - .. coqtop:: all + .. rocqtop:: all Arguments p1 {_ _} _. Check fun x : Sigma nat (fun x => x = 0) => diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst index bc44de158863..07f1142b1d89 100644 --- a/doc/sphinx/language/core/sections.rst +++ b/doc/sphinx/language/core/sections.rst @@ -83,7 +83,7 @@ usable outside the section as shown in this :ref:`example option A. Variant sum (A B : Type) : Type := inl : A -> sum A B | inr : B -> sum A B. @@ -69,13 +69,13 @@ be defined using :cmd:`Variant`. defined as a two-constructor type family over :g:`bool` parameterized by the proposition :n:`P`: - .. coqtop:: in + .. rocqtop:: in Variant reflect (P : Prop) : bool -> Set := | ReflectT : P -> reflect P true | ReflectF : ~ P -> reflect P false. - .. coqtop:: none + .. rocqtop:: none End FreshNameSpace. @@ -111,7 +111,7 @@ Private (matching) inductive types .. example:: - .. coqtop:: all + .. rocqtop:: all Module Foo. #[ private(matching) ] Inductive my_nat := my_O : my_nat | my_S : my_nat -> my_nat. @@ -189,7 +189,7 @@ the term being matched. This dependency of the term being matched in the return type is expressed with an :n:`@ident` clause where :n:`@ident` is dependent in the return type. For instance, in the following example: -.. coqtop:: in +.. rocqtop:: in Inductive bool : Type := true : bool | false : bool. Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : eq A x x. @@ -215,11 +215,11 @@ the identifier :g:`b` being used to represent the dependency. the return type. For instance, the following alternative definition is accepted and has the same meaning as the previous one. - .. coqtop:: none + .. rocqtop:: none Reset bool_case. - .. coqtop:: in + .. rocqtop:: in Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := match b return or (eq bool b true) (eq bool b false) with @@ -252,7 +252,7 @@ is expressed with a clause in the form For instance, in the following example: -.. coqtop:: in +.. rocqtop:: in Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x := match H in eq _ _ z return eq A z x with diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index 5e5486ac1487..2712e97e3827 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -172,7 +172,7 @@ Manual declaration of implicit arguments .. example:: - .. coqtop:: reset all + .. rocqtop:: reset all Inductive list (A : Type) : Type := | nil : list A @@ -202,7 +202,7 @@ Manual declaration of implicit arguments .. example:: Multiple alternatives with :n:`@implicits_alt` - .. coqtop:: all + .. rocqtop:: all Arguments map [A B] f l, [A] B f l, A B f l. @@ -223,7 +223,7 @@ Automatic declaration of implicit arguments .. example:: Default implicits - .. coqtop:: reset all + .. rocqtop:: reset all Inductive list (A:Set) : Set := | nil : list A @@ -249,7 +249,7 @@ of :term:`constants `. For instance, the variable ``p`` below has type ``forall x,y:U, R x y -> forall z:U, R y z -> R x z``. As the variables ``x``, ``y`` and ``z`` appear strictly in the :term:`body` of the type, they are implicit. -.. coqtop:: all +.. rocqtop:: all Parameter X : Type. @@ -277,7 +277,7 @@ Renaming implicit arguments .. example:: (continued) Renaming implicit arguments - .. coqtop:: all + .. rocqtop:: all Arguments p [s t] _ [u] _: rename. @@ -298,7 +298,7 @@ Binding arguments to scopes the key ``R``, then in ``F`` (when a notation has no interpretation in ``R``). - .. coqdoc:: + .. rocqdoc:: Arguments plus_fct (f1 f2)%_F x%_R%_F. @@ -317,7 +317,7 @@ Binding arguments to scopes occurred at the time of the declaration of the notation. Here is an example: - .. coqtop:: all + .. rocqtop:: all Parameter g : bool -> bool. Declare Scope mybool_scope. @@ -346,7 +346,7 @@ Effects of :cmd:`Arguments` on unfolding .. example:: - .. coqtop:: all + .. rocqtop:: all Arguments Nat.sub n m : simpl never. @@ -362,7 +362,7 @@ Effects of :cmd:`Arguments` on unfolding .. example:: - .. coqtop:: all + .. rocqtop:: all Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). Arguments fcomp {A B C} f g x /. @@ -375,7 +375,7 @@ Effects of :cmd:`Arguments` on unfolding .. example:: - .. coqtop:: all + .. rocqtop:: all Definition volatile := fun x : nat => x. Arguments volatile / x. @@ -386,7 +386,7 @@ Effects of :cmd:`Arguments` on unfolding .. example:: - .. coqtop:: all + .. rocqtop:: all Arguments minus !n !m. @@ -399,7 +399,7 @@ Effects of :cmd:`Arguments` on unfolding .. example:: - .. coqtop:: all + .. rocqtop:: all Arguments minus n m : simpl nomatch. @@ -452,7 +452,7 @@ type check the remaining arguments (in :n:`@arg_specs__2`). In a context where a coercion was declared from ``bool`` to ``nat``: - .. coqtop:: in reset + .. rocqtop:: in reset Definition b2n (b : bool) := if b then 1 else 0. Coercion b2n : bool >-> nat. @@ -461,13 +461,13 @@ type check the remaining arguments (in :n:`@arg_specs__2`). statements over ``nat``, because the need for inserting a coercion is known only from the expected type of a subterm: - .. coqtop:: all + .. rocqtop:: all Fail Check (ex_intro _ true _ : exists n : nat, n > 0). However, a suitable bidirectionality hint makes the example work: - .. coqtop:: all + .. rocqtop:: all Arguments ex_intro _ _ & _ _. Check (ex_intro _ true _ : exists n : nat, n > 0). diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index fbd808637d1f..9ae6bf91c1cd 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -101,7 +101,7 @@ in :ref:`canonicalstructures`; here only a simple example is given. Here is an example. - .. coqtop:: all reset + .. rocqtop:: all reset Require Import Relation_Definitions. @@ -124,7 +124,7 @@ in :ref:`canonicalstructures`; here only a simple example is given. Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A` and :g:`B` can be synthesized in the next statement. - .. coqtop:: all abort + .. rocqtop:: all abort Lemma is_law_S : is_law S. @@ -148,7 +148,7 @@ in :ref:`canonicalstructures`; here only a simple example is given. For instance, when declaring the :g:`Setoid` structure above, the :g:`Prf_equiv` field declaration could be written as follows. - .. coqdoc:: + .. rocqdoc:: #[canonical=no] Prf_equiv : equivalence Carrier Equal @@ -166,11 +166,11 @@ in :ref:`canonicalstructures`; here only a simple example is given. For instance, the above example gives the following output: - .. coqtop:: all + .. rocqtop:: all Print Canonical Projections. - .. coqtop:: all + .. rocqtop:: all Print Canonical Projections nat. @@ -187,7 +187,7 @@ We build an infix notation == for a comparison predicate. Such notation will be overloaded, and its meaning will depend on the types of the terms that are compared. -.. coqtop:: all reset +.. rocqtop:: all reset Module EQ. Record class (T : Type) := Class { cmp : T -> T -> Prop }. @@ -218,20 +218,20 @@ coercion, but we will not do that here. The following line tests that, when we assume a type ``e`` that is in the ``EQ`` class, we can relate two of its objects with ``==``. -.. coqtop:: all +.. rocqtop:: all Import EQ.theory. Check forall (e : EQ.type) (a b : EQ.obj e), a == b. Still, no concrete type is in the ``EQ`` class. -.. coqtop:: all +.. rocqtop:: all Fail Check 3 == 3. We amend that by equipping ``nat`` with a comparison relation. -.. coqtop:: all +.. rocqtop:: all Definition nat_eq (x y : nat) := Nat.compare x y = Eq. Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq. @@ -262,7 +262,7 @@ how to deal with type constructors, i.e. how to make the following example work: -.. coqtop:: all +.. rocqtop:: all Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b). @@ -270,7 +270,7 @@ The error message is telling that Rocq has no idea on how to compare pairs of objects. The following construction is telling Rocq exactly how to do that. -.. coqtop:: all +.. rocqtop:: all Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) := fst x == fst y /\ snd x == snd y. @@ -300,7 +300,7 @@ To get to an interesting example we need another base class to be available. We choose the class of types that are equipped with an order relation, to which we associate the infix ``<=`` notation. -.. coqtop:: all +.. rocqtop:: all Module LE. @@ -325,7 +325,7 @@ order relation, to which we associate the infix ``<=`` notation. As before we register a canonical ``LE`` class for ``nat``. -.. coqtop:: all +.. rocqtop:: all Import LE.theory. @@ -337,7 +337,7 @@ As before we register a canonical ``LE`` class for ``nat``. And we enable Rocq to relate pair of terms with ``<=``. -.. coqtop:: all +.. rocqtop:: all Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) := fst x <= fst y /\ snd x <= snd y. @@ -353,7 +353,7 @@ At the current stage we can use ``==`` and ``<=`` on concrete types, like tuples of natural numbers, but we can’t develop an algebraic theory over the types that are equipped with both relations. -.. coqtop:: all +.. rocqtop:: all Check 2 <= 3 /\ 2 == 2. @@ -364,7 +364,7 @@ over the types that are equipped with both relations. We need to define a new class that inherits from both ``EQ`` and ``LE``. -.. coqtop:: all +.. rocqtop:: all Module LEQ. @@ -392,7 +392,7 @@ it plays no role in the search for instances. Unfortunately there is still an obstacle to developing the algebraic theory of this new class. -.. coqtop:: all +.. rocqtop:: all Module theory. @@ -407,7 +407,7 @@ The following two constructions tell Rocq how to canonically build the ``LE.type`` and ``EQ.type`` structure given an ``LEQ.type`` structure on the same type. -.. coqtop:: all +.. rocqtop:: all Definition to_EQ (e : type) : EQ.type := EQ.Pack (obj e) (EQ_class _ (class_of e)). @@ -422,7 +422,7 @@ type. We can now formulate out first theorem on the objects of the ``LEQ`` structure. -.. coqtop:: all +.. rocqtop:: all Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y. @@ -443,7 +443,7 @@ structure. Of course one would like to apply results proved in the algebraic setting to any concrete instate of the algebraic structure. -.. coqtop:: all +.. rocqtop:: all Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m. @@ -462,7 +462,7 @@ Again one has to tell Rocq that the type ``nat`` is in the ``LEQ`` class, and how the type constructor ``*`` interacts with the ``LEQ`` class. In the following proofs are omitted for brevity. -.. coqtop:: all +.. rocqtop:: all Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m. @@ -483,7 +483,7 @@ constructor ``*``. It also tests that they work as expected. Unfortunately, these declarations are very verbose. In the following subsection we show how to make them more compact. -.. coqtop:: all +.. rocqtop:: all Module Add_instance_attempt. @@ -521,7 +521,7 @@ Compact declaration of Canonical Structures We need some infrastructure for that. -.. coqtop:: all +.. rocqtop:: all Module infrastructure. @@ -560,7 +560,7 @@ They are explained in more details in :cite:`CSwcu`. We now have all we need to create a compact “packager” to declare instances of the ``LEQ`` class. -.. coqtop:: all +.. rocqtop:: all Import infrastructure. @@ -589,7 +589,7 @@ the reader can refer to :cite:`CSwcu`. The declaration of canonical instances can now be way more compact: -.. coqtop:: all +.. rocqtop:: all Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. @@ -599,6 +599,6 @@ The declaration of canonical instances can now be way more compact: Error messages are also quite intelligible (if one skips to the end of the message). -.. coqtop:: all +.. rocqtop:: all Fail Canonical Structure err := Eval hnf in Pack bool nat_LEQmx. diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst index d97f40474b0d..85efe17b0915 100644 --- a/doc/sphinx/language/extensions/evars.rst +++ b/doc/sphinx/language/extensions/evars.rst @@ -37,7 +37,7 @@ placeholder which generated it, or is used in the same context as the one in which it was generated, the context is not displayed and the existential variable is represented by “?” followed by an identifier. -.. coqtop:: all +.. rocqtop:: all Parameter identity : forall (X:Set), X -> X. @@ -54,7 +54,7 @@ this is why an existential variable used in the same context as its context of definition is written with no instance. This behavior may be changed: see :ref:`explicit-display-existentials`. -.. coqtop:: all +.. rocqtop:: all Check (fun x y => _) 0 1. @@ -110,12 +110,12 @@ it will create new existential variable(s) when :tacn:`apply` would fail. unspecified. This makes :tacn:`apply` fail, while :tacn:`eapply` creates a new existential variable :n:`?y`. - .. coqtop:: none reset + .. rocqtop:: none reset Goal forall i j : nat, i = j. intros. - .. coqtop:: all + .. rocqtop:: all (* Theorem eq_trans : forall (A : Type) (x y z : A), x = y -> y = z -> x = z. *) @@ -173,13 +173,13 @@ automatically as a side effect of other tactics. shown below determines the value of this variable by unification, which resolves it. - .. coqtop:: reset in + .. rocqtop:: reset in Set Printing Goal Names. Goal forall p n m : nat, n = p -> p = m -> n = m. - .. coqtop:: all + .. rocqtop:: all intros x y z H1 H2. eapply eq_trans. (* creates ?y : nat as a shelved goal *) @@ -192,7 +192,7 @@ automatically as a side effect of other tactics. However if you choose poorly, you can end up with unprovable goals (in this case :n:`x = 0`). Like this: - .. coqtop:: reset none + .. rocqtop:: reset none Set Printing Goal Names. @@ -200,11 +200,11 @@ automatically as a side effect of other tactics. intros x y z H1 H2. eapply eq_trans. (* creates ?y : nat as a shelved goal *) - .. coqtop:: out + .. rocqtop:: out Unshelve. (* moves the shelved goals into focus--not needed and usually not done *) - .. coqtop:: all + .. rocqtop:: all 3: apply 0. (* assigns value to ?y *) @@ -221,7 +221,7 @@ Explicit display of existential instances for pretty-printing context of an existential variable is instantiated at each of the occurrences of the existential variable. Off by default. -.. coqtop:: all +.. rocqtop:: all Check (fun x y => _) 0 1. @@ -244,7 +244,7 @@ between variables introduced by term binding as well as those introduced by tactic binding. The expression `tacexpr` can be any tactic expression as described in :ref:`ltac`. -.. coqtop:: all +.. rocqtop:: all Definition foo (x : nat) : nat := ltac:(exact x). diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index 8b8e02acf725..63d89ac41973 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -131,7 +131,7 @@ otherwise they would never be inserted. For instance: - .. coqtop:: all fail + .. rocqtop:: all fail Fail Definition double [n] := n + n. @@ -172,7 +172,7 @@ form, with square brackets, makes :token:`name` a non-maximally inserted implici For example: -.. coqtop:: all +.. rocqtop:: all Definition id {A : Type} (x : A) : A := x. @@ -180,7 +180,7 @@ declares the argument `A` of `id` as a maximally inserted implicit argument. `A` may be omitted in applications of `id` but may be specified if needed: -.. coqtop:: all abort +.. rocqtop:: all abort Definition compose {A B C} (g : B -> C) (f : A -> B) := fun x => g (f x). @@ -188,7 +188,7 @@ in applications of `id` but may be specified if needed: For non-maximally inserted implicit arguments, use square brackets: -.. coqtop:: all +.. rocqtop:: all Fixpoint map [A B : Type] (f : A -> B) (l : list A) : list B := match l with @@ -204,7 +204,7 @@ declared as an implicit argument need not be repeated in the inductive definition and will become implicit for the inductive type and the constructors. For example: -.. coqtop:: all +.. rocqtop:: all Inductive list {A : Type} : Type := | nil : list @@ -228,7 +228,7 @@ implicit: Here is an example: -.. coqtop:: all +.. rocqtop:: all Axiom Ax : forall (f:forall {A} (a:A), A * A), @@ -241,7 +241,7 @@ Here is an example: expression which does not correspond to the type of an assumption or to the :term:`body` of a definition. Here is an example: - .. coqtop:: all warn + .. rocqtop:: all warn Definition f := forall {y}, y = 0. @@ -251,7 +251,7 @@ Here is an example: in the same block of binders, in which case the first occurrence is considered to be unnamed. Here is an example: - .. coqtop:: all warn + .. rocqtop:: all warn Check let g {x:nat} (H:x=x) {x} (H:x=x) := x in 0. @@ -331,7 +331,7 @@ this case, they are converted to maximally inserted ones. .. example:: - .. coqtop:: all + .. rocqtop:: all Set Implicit Arguments. Axiom eq0_le0 : forall (n : nat) (x : n = 0), n <= 0. @@ -365,7 +365,7 @@ the hiding of implicit arguments for a single function application using the .. example:: Syntax for explicitly giving implicit arguments (continued) - .. coqtop:: all + .. rocqtop:: all Parameter X : Type. Definition Relation := X -> X -> Prop. @@ -434,13 +434,13 @@ arguments is taken into account, and not an upper type of all of them. As a consequence, the inference of the implicit argument of “=” fails in -.. coqtop:: all +.. rocqtop:: all Fail Check nat = Prop. but succeeds in -.. coqtop:: all +.. rocqtop:: all Check Prop = nat. @@ -462,14 +462,14 @@ function. The function `id` has one implicit argument and one explicit argument. - .. coqtop:: all reset + .. rocqtop:: all reset Check (id 0). Definition id' := @id. The function `id'` has no implicit argument. - .. coqtop:: all + .. rocqtop:: all Check (id' nat 0). @@ -487,7 +487,7 @@ function. We can reproduce the example above using the :flag:`Parsing Explicit` flag: - .. coqtop:: all reset + .. rocqtop:: all reset Set Parsing Explicit. Definition id' := id. @@ -520,7 +520,7 @@ or :g:`m` to the type :g:`nat` of natural numbers). .. example:: - .. coqtop:: all + .. rocqtop:: all Require Import ListDef. @@ -584,7 +584,7 @@ In the following statement, ``A`` and ``y`` are automatically generalized, ``A`` is implicit and ``x``, ``y`` and the anonymous equality argument are explicit. -.. coqtop:: all reset +.. rocqtop:: all reset Generalizable All Variables. @@ -594,7 +594,7 @@ equality argument are explicit. Dually to normal binders, the name is optional but the type is required: -.. coqtop:: all +.. rocqtop:: all Check (forall `{x = y :> A}, y = x). @@ -606,7 +606,7 @@ this behavior may be disabled by prefixing the type with a ``!`` or by forcing the typeclass name to be an explicit application using ``@`` (however the later ignores implicit argument information). -.. coqtop:: all +.. rocqtop:: all Class Op (A:Type) := op : A -> A -> A. @@ -624,7 +624,7 @@ by forcing the typeclass name to be an explicit application using Multiple binders can be merged using ``,`` as a separator: -.. coqtop:: all +.. rocqtop:: all Check (forall `{Commutative A, Hnat : !Commutative nat}, True). diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index 750f391a3f4b..5bfaf76ddc97 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -43,7 +43,7 @@ For inductive types with exactly two constructors and for pattern matching expressions that do not depend on the arguments of the constructors, it is possible to use a ``if … then … else`` notation. For instance, the definition -.. coqtop:: all +.. rocqtop:: all Definition not (b:bool) := match b with @@ -53,7 +53,7 @@ to use a ``if … then … else`` notation. For instance, the definition can be alternatively written -.. coqtop:: reset all +.. rocqtop:: reset all Definition not (b:bool) := if b then false else true. @@ -66,7 +66,7 @@ and :n:`@ident__2`, the following terms are equal: .. example:: - .. coqtop:: all + .. rocqtop:: all Check (fun x (H:{x=0}+{x<>0}) => match H with @@ -109,7 +109,7 @@ constructor. Then, in :n:`@term__1`, these variables are bound to the arguments of the constructor in :n:`@term__0`. For instance, the definition -.. coqtop:: reset all +.. rocqtop:: reset all Definition fst (A B:Set) (H:A * B) := match H with | pair x y => x @@ -117,7 +117,7 @@ definition can be alternatively written -.. coqtop:: reset all +.. rocqtop:: reset all Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x. @@ -153,7 +153,7 @@ one constructor by giving an arbitrary pattern instead of just a tuple for all the arguments. For example, the preceding example can be written: -.. coqtop:: reset all +.. rocqtop:: reset all Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x. @@ -161,7 +161,7 @@ This is useful to match deeper inside tuples and also to use notations for the pattern, as the syntax :g:`let ’p := t in b` allows arbitrary patterns to do the deconstruction. For example: -.. coqtop:: all +.. rocqtop:: all Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A := let '((a,b), (c, d)) := x in (a,b,c,d). @@ -262,13 +262,13 @@ Printing of hidden subterms .. example:: - .. coqtop:: in + .. rocqtop:: in Polymorphic Inductive eqT@{u} {A:Type@{u}} (a:A) : A -> Type@{u} := reflT : eqT a a. Set Definitional UIP. Inductive seq {A} (a:A) : A -> SProp := srefl : seq a a. - .. coqtop:: all + .. rocqtop:: all Print eqT_rect. Print seq_rect. @@ -311,7 +311,7 @@ This example emphasizes what the printing settings offer. .. example:: - .. coqtop:: all + .. rocqtop:: all Definition snd (A B:Set) (H:A * B) := match H with | pair x y => y @@ -351,7 +351,7 @@ a warning is issued in such situations. .. example:: - .. coqtop:: all warn + .. rocqtop:: all warn Definition is_zero (o : option nat) := match o with | Some _ => true @@ -406,7 +406,7 @@ pattern matching. Consider for example the function that computes the maximum of two natural numbers. We can write it in primitive syntax by: -.. coqtop:: in +.. rocqtop:: in Fixpoint max (n m:nat) {struct m} : nat := match n with @@ -424,7 +424,7 @@ Multiple patterns Using multiple patterns in the definition of ``max`` lets us write: -.. coqtop:: in reset +.. rocqtop:: in reset Fixpoint max (n m:nat) {struct m} : nat := match n, m with @@ -440,7 +440,7 @@ to right. A match expression is generated **only** when there is at least one constructor in the column of patterns. E.g. the following example does not build a match expression. -.. coqtop:: all +.. rocqtop:: all Check (fun x:nat => match x return nat with | y => y @@ -452,7 +452,7 @@ Aliasing subpatterns We can also use :n:`as @ident` to associate a name to a sub-pattern: -.. coqtop:: in reset +.. rocqtop:: in reset Fixpoint max (n m:nat) {struct n} : nat := match n, m with @@ -468,7 +468,7 @@ Nested patterns Here is now an example of nested patterns: -.. coqtop:: in +.. rocqtop:: in Fixpoint even (n:nat) : bool := match n with @@ -479,12 +479,12 @@ Here is now an example of nested patterns: This is compiled into: -.. coqtop:: all +.. rocqtop:: all Unset Printing Matching. Print even. -.. coqtop:: none +.. rocqtop:: none Set Printing Matching. @@ -494,7 +494,7 @@ superposition. Consider the boolean function :g:`lef` that given two natural numbers yields :g:`true` if the first one is less or equal than the second one and :g:`false` otherwise. We can write it as follows: -.. coqtop:: in +.. rocqtop:: in Fixpoint lef (n m:nat) {struct m} : bool := match n, m with @@ -513,7 +513,7 @@ is matched by the first pattern, and so :g:`(lef O O)` yields true. Another way to write this function is: -.. coqtop:: in reset +.. rocqtop:: in reset Fixpoint lef (n m:nat) {struct m} : bool := match n, m with @@ -529,7 +529,7 @@ not match neither the first nor the second one. Terms with useless patterns are not accepted by the system. Here is an example: -.. coqtop:: all +.. rocqtop:: all Fail Check (fun x:nat => match x with @@ -546,7 +546,7 @@ Multiple patterns that share the same right-hand-side can be factorized using the notation :n:`{+| {+, @pattern } }`. For instance, :g:`max` can be rewritten as follows: -.. coqtop:: in reset +.. rocqtop:: in reset Fixpoint max (n m:nat) {struct m} : nat := match n, m with @@ -558,7 +558,7 @@ Similarly, factorization of (not necessarily multiple) patterns that share the same variables is possible by using the notation :n:`{+| @pattern}`. Here is an example: -.. coqtop:: in +.. rocqtop:: in Definition filter_2_4 (n:nat) : nat := match n with @@ -570,7 +570,7 @@ Here is an example: Nested disjunctive patterns are allowed, inside parentheses, with the notation :n:`({+| @pattern})`, as in: -.. coqtop:: in +.. rocqtop:: in Definition filter_some_square_corners (p:nat*nat) : nat*nat := match p with @@ -588,7 +588,7 @@ When matching objects of a parametric type, parameters do not bind in patterns. They must be substituted by “``_``”. Consider for example the type of polymorphic lists: -.. coqtop:: in +.. rocqtop:: in Inductive List (A:Set) : Set := | nil : List A @@ -596,7 +596,7 @@ type of polymorphic lists: We can check the function *tail*: -.. coqtop:: all +.. rocqtop:: all Check (fun l:List nat => @@ -607,7 +607,7 @@ We can check the function *tail*: When we use parameters in patterns there is an error message: -.. coqtop:: all +.. rocqtop:: all Fail Check (fun l:List nat => @@ -620,7 +620,7 @@ When we use parameters in patterns there is an error message: This :term:`flag` (off by default) removes parameters from constructors in patterns: -.. coqtop:: all +.. rocqtop:: all Set Asymmetric Patterns. Check (fun l:List nat => @@ -635,7 +635,7 @@ Implicit arguments in patterns By default, implicit arguments are omitted in patterns. So we write: -.. coqtop:: all +.. rocqtop:: all Arguments nil {A}. Arguments cons [A] _ _. @@ -649,7 +649,7 @@ By default, implicit arguments are omitted in patterns. So we write: But the possibility to use all the arguments is given by “``@``” implicit explicitations (as for terms, see :ref:`explicit-applications`). -.. coqtop:: all +.. rocqtop:: all Check (fun l:List nat => @@ -669,7 +669,7 @@ dependent types, but we can also use the expansion strategy to destructure objects of dependent types. Consider the type :g:`listn` of lists of a certain length: -.. coqtop:: in reset +.. rocqtop:: in reset Inductive listn : nat -> Set := | niln : listn 0 @@ -681,14 +681,14 @@ Understanding dependencies in patterns We can define the function length over :g:`listn` by: -.. coqdoc:: +.. rocqdoc:: Definition length (n:nat) (l:listn n) := n. Just for illustrating pattern matching, we can define it by case analysis: -.. coqtop:: in +.. rocqtop:: in Definition length (n:nat) (l:listn n) := match l with @@ -714,7 +714,7 @@ of the |rhs| are different instances of the elimination predicate. The function :g:`concat` for :g:`listn` is an example where the branches have different types and we need to provide the elimination predicate: -.. coqtop:: in +.. rocqtop:: in Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : listn (n + m) := @@ -723,7 +723,7 @@ different types and we need to provide the elimination predicate: | consn n' a y => consn (n' + m) a (concat n' y m l') end. -.. coqtop:: none +.. rocqtop:: none Reset concat. @@ -750,7 +750,7 @@ a dependent product. For example, an equivalent definition for :g:`concat` (even though the matching on the second term is trivial) would have been: -.. coqtop:: in +.. rocqtop:: in Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : listn (n + m) := @@ -763,7 +763,7 @@ Even without real matching over the second term, this construction can be used to keep types linked. If :g:`a` and :g:`b` are two :g:`listn` of the same length, by writing -.. coqtop:: in +.. rocqtop:: in Check (fun n (a b: listn n) => match a, b with @@ -789,7 +789,7 @@ anything. To be concrete: the ``tail`` function can be written: -.. coqtop:: in +.. rocqtop:: in Definition tail n (v: listn (S n)) := match v in listn (S m) return listn m with @@ -811,7 +811,7 @@ in the description of the tactic :tacn:`refine`. For example, we can write the function :g:`buildlist` that given a natural number :g:`n` builds a list of length :g:`n` containing zeros as follows: -.. coqtop:: in +.. rocqtop:: in Fixpoint buildlist (n:nat) : listn n := match n return listn n with @@ -822,7 +822,7 @@ number :g:`n` builds a list of length :g:`n` containing zeros as follows: We can also use multiple patterns. Consider the following definition of the predicate less-equal :g:`Le`: -.. coqtop:: in +.. rocqtop:: in Inductive LE : nat -> nat -> Prop := | LEO : forall n:nat, LE 0 n @@ -831,7 +831,7 @@ of the predicate less-equal :g:`Le`: We can use multiple patterns to write the proof of the lemma :g:`forall (n m:nat), (LE n m) \/ (LE m n)`: -.. coqtop:: in +.. rocqtop:: in Fixpoint dec (n m:nat) {struct n} : LE n m \/ LE m n := match n, m return LE n m \/ LE m n with @@ -862,7 +862,7 @@ can also be caught in the matching. .. example:: - .. coqtop:: in reset + .. rocqtop:: in reset Inductive list : nat -> Set := | nil : list 0 @@ -870,7 +870,7 @@ can also be caught in the matching. In the next example, the local definition is not caught. - .. coqtop:: in + .. rocqtop:: in Fixpoint length n (l:list n) {struct l} : nat := match l with @@ -880,7 +880,7 @@ can also be caught in the matching. But in this example, it is. - .. coqtop:: in + .. rocqtop:: in Fixpoint length' n (l:list n) {struct l} : nat := match l with @@ -908,7 +908,7 @@ pattern. .. example:: - .. coqtop:: in + .. rocqtop:: in Inductive I : Set := | C1 : nat -> I @@ -916,7 +916,7 @@ pattern. Coercion C1 : nat >-> I. - .. coqtop:: all + .. rocqtop:: all Check (fun x => match x with | C2 O => 0 diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 30b924d3426f..2192f2c6a4ad 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -78,7 +78,7 @@ See :ref:`coq_makefile` and :ref:`building_dune`. or restart `CoqIDE`. The project file name is configurable in `Edit / Preferences / Project`. - .. coqdoc:: + .. rocqdoc:: -R Mod1 Customization at launch time diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 472078e98020..c5cc02aa5ffc 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -430,7 +430,7 @@ You just need to define suitable notations as described in the chapter :ref:`syntax-extensions-and-notation-scopes`. For example, to use the mathematical symbols ∀ and ∃, you may define: -.. coqtop:: in +.. rocqtop:: in Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity) diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 3f282dd0bbb5..5bd744f6b370 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -30,7 +30,7 @@ since the paper was written.) Here are some examples of simple tactic macros you can create with |Ltac|: - .. coqdoc:: + .. rocqdoc:: Ltac reduce_and_try_to_solve := simpl; intros; auto. @@ -290,11 +290,11 @@ as a :token:`tactic_arg`. Local symbols are also substituted into tactics: .. example:: Substitution of global and local symbols - .. coqtop:: reset none + .. rocqtop:: reset none Goal True. - .. coqtop:: all + .. rocqtop:: all Ltac n := 1. let n2 := n in idtac n2. @@ -458,11 +458,11 @@ Selectors can also be used nested within a tactic expression with the .. example:: Selector reordering goals - .. coqtop:: reset in + .. rocqtop:: reset in Goal 1=0 /\ 2=0 /\ 3=0. - .. coqtop:: all + .. rocqtop:: all repeat split. 1,3: idtac. @@ -479,15 +479,15 @@ separately. They succeed only if there is a success for each goal. For example This tactic fails because there no match for the second goal (`False`). - .. coqtop:: reset none fail + .. rocqtop:: reset none fail Goal True /\ False. - .. coqtop:: out + .. rocqtop:: out split. - .. coqtop:: all + .. rocqtop:: all Fail all: let n := numgoals in idtac "numgoals =" n; match goal with @@ -514,7 +514,7 @@ when subsequent tactics outside these constructs fail. For example: .. example:: Backtracking - .. coqtop:: all + .. rocqtop:: all Fail multimatch True with | True => idtac "branch 1" @@ -673,11 +673,11 @@ We can branch with backtracking with the following structure: equivalent to :n:`@ltac_expr__1 + (@ltac_expr__2 + @ltac_expr__3)`. Here's an example where the behavior differs slightly: - .. coqtop:: reset none + .. rocqtop:: reset none Goal True. - .. coqtop:: all + .. rocqtop:: all Fail (fail 2 + idtac) + idtac. Fail fail 2 + (idtac + idtac). @@ -687,11 +687,11 @@ We can branch with backtracking with the following structure: In the first tactic, `idtac "2"` is not executed. In the second, the subsequent `fail` causes backtracking and the execution of `idtac "B"`. - .. coqtop:: reset none + .. rocqtop:: reset none Goal True. - .. coqtop:: all + .. rocqtop:: all idtac "1" + idtac "2". assert_fails ((idtac "A" + idtac "B"); fail). @@ -773,20 +773,20 @@ In some cases backtracking may be too expensive. .. example:: Backtracking inside a non-backtracking construct - .. coqtop:: reset none + .. rocqtop:: reset none Goal True. The :tacn:`fail` doesn't trigger the second :tacn:`idtac`: - .. coqtop:: all + .. rocqtop:: all assert_fails (first [ idtac "1" | idtac "2" ]; fail). This backtracks within `(idtac "1A" + idtac "1B" + fail)` but :tacn:`first` won't consider the `idtac "2"` alternative: - .. coqtop:: all + .. rocqtop:: all assert_fails (first [ (idtac "1A" + idtac "1B" + fail) | idtac "2" ]; fail). @@ -796,7 +796,7 @@ In some cases backtracking may be too expensive. This works similarly for the :tacn:`solve` tactic. - .. coqtop:: reset all + .. rocqtop:: reset all Tactic Notation "myfirst" "[" tactic_list_sep(tacl,"|") "]" := first tacl. Goal True. @@ -887,11 +887,11 @@ Rocq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*: This is due to the order in which parts of the :token:`ltac_expr3` are evaluated and executed. For example: - .. coqtop:: reset none + .. rocqtop:: reset none Goal True. - .. coqtop:: all fail + .. rocqtop:: all fail assert_fails match True with _ => fail end. @@ -900,14 +900,14 @@ Rocq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*: the :tacn:`match` to find its first success earlier. One workaround is to prefix :token:`ltac_expr3` with "`idtac;`". - .. coqtop:: all + .. rocqtop:: all assert_fails (idtac; match True with _ => fail end). Alternatively, substituting the :tacn:`match` into the definition of :tacn:`assert_fails` works as expected: - .. coqtop:: all + .. rocqtop:: all tryif (once match True with _ => fail end) then gfail 0 (* tac *) "succeeds" else idtac. @@ -966,7 +966,7 @@ Failing explanations/generalizations (e.g. gfail always fails; "tac; fail" succeeds but "fail." alone fails. - .. coqtop:: reset all fail + .. rocqtop:: reset all fail Goal True. Proof. fail. Abort. @@ -1198,18 +1198,18 @@ Pattern matching on terms: match it doesn't look for further matches. In :tacn:`match`, if :token:`ltac_expr` fails in a matching branch, it will try to match on subsequent branches. - .. coqtop:: reset none + .. rocqtop:: reset none Goal True. - .. coqtop:: all + .. rocqtop:: all Fail lazymatch True with | True => idtac "branch 1"; fail | _ => idtac "branch 2" end. - .. coqtop:: all + .. rocqtop:: all match True with | True => idtac "branch 1"; fail @@ -1223,7 +1223,7 @@ Pattern matching on terms: match :tacn:`match` tactics are only evaluated once, whereas :tacn:`multimatch` tactics may be evaluated more than once if the following constructs trigger backtracking: - .. coqtop:: all + .. rocqtop:: all Fail match True with | True => idtac "branch 1" @@ -1231,7 +1231,7 @@ Pattern matching on terms: match end ; idtac "branch A"; fail. - .. coqtop:: all + .. rocqtop:: all Fail multimatch True with | True => idtac "branch 1" @@ -1246,11 +1246,11 @@ Pattern matching on terms: match Notice the :tacn:`idtac` prints ``(z + 1)`` while the :tacn:`pose` substitutes ``(x + 1)``. - .. coqtop:: in reset + .. rocqtop:: in reset Goal True. - .. coqtop:: all + .. rocqtop:: all match constr:(fun x => (x + 1) * 3) with | fun z => ?y * 3 => idtac "y =" y; pose (fun z: nat => y * 5) @@ -1263,7 +1263,7 @@ Pattern matching on terms: match Internally "x <> y" is represented as "(~ (x = y))", which produces the first match. - .. coqtop:: in reset + .. rocqtop:: in reset Ltac f t := match t with | context [ (~ ?t) ] => idtac "?t = " t; fail @@ -1271,7 +1271,7 @@ Pattern matching on terms: match end. Goal True. - .. coqtop:: all + .. rocqtop:: all f ((~ True) <> (~ False)). @@ -1378,7 +1378,7 @@ Examples: Hypotheses are matched from the last hypothesis (which is by default the newest hypothesis) to the first until the :tacn:`apply` succeeds. - .. coqtop:: reset all + .. rocqtop:: reset all Goal forall A B : Prop, A -> B -> (A->B). intros. @@ -1392,7 +1392,7 @@ Examples: Hypotheses are matched from the first hypothesis to the last until the :tacn:`apply` succeeds. - .. coqtop:: reset all + .. rocqtop:: reset all Goal forall A B : Prop, A -> B -> (A->B). intros. @@ -1409,7 +1409,7 @@ Examples: Observe that the number of permutations can grow as the factorial of the number of hypotheses and hypothesis patterns. - .. coqtop:: reset all + .. rocqtop:: reset all Goal forall A B : Prop, A -> B -> (A->B). intros A B H. @@ -1446,7 +1446,7 @@ produce subgoals but generates a term to be used in tactic expressions: .. example:: Substituting a matched context - .. coqtop:: reset all + .. rocqtop:: reset all Goal True /\ True. match goal with @@ -1480,15 +1480,15 @@ expression returns an identifier: Successive calls to :tacn:`fresh` give distinct names even if the names haven't yet been added to the local context: - .. coqtop:: reset none + .. rocqtop:: reset none Goal True -> True. - .. coqtop:: out + .. rocqtop:: out intro x. - .. coqtop:: all + .. rocqtop:: all let a := fresh "x" in let b := fresh "x" in @@ -1497,7 +1497,7 @@ expression returns an identifier: When applying :tacn:`fresh` in a function, the name is chosen based on the tactic context at the point where the function was defined: - .. coqtop:: all + .. rocqtop:: all let a := fresh "x" in let f := fun _ => fresh "x" in @@ -1553,14 +1553,14 @@ Counting goals: numgoals .. example:: - .. coqtop:: reset in + .. rocqtop:: reset in Ltac pr_numgoals := let n := numgoals in idtac "There are" n "goals". Goal True /\ True /\ True. split;[|split]. - .. coqtop:: all abort + .. rocqtop:: all abort all:pr_numgoals. @@ -1589,12 +1589,12 @@ Testing boolean expressions: guard .. example:: guard - .. coqtop:: in + .. rocqtop:: in Goal True /\ True /\ True. split;[|split]. - .. coqtop:: all + .. rocqtop:: all all:let n:= numgoals in guard n<4. Fail all:let n:= numgoals in guard n=2. @@ -1698,7 +1698,7 @@ succeeds, and results in an error otherwise. .. example:: is_fix - .. coqtop:: reset in + .. rocqtop:: reset in Goal True. is_fix (fix f (n : nat) := match n with S n => f n | O => O end). @@ -1714,7 +1714,7 @@ succeeds, and results in an error otherwise. .. example:: is_cofix - .. coqtop:: reset in + .. rocqtop:: reset in CoInductive Stream (A : Type) : Type := Cons : A -> Stream A -> Stream A. Goal True. @@ -1748,7 +1748,7 @@ succeeds, and results in an error otherwise. .. example:: is_proj - .. coqtop:: reset in + .. rocqtop:: reset in Set Primitive Projections. Record Box {T : Type} := box { unbox : T }. @@ -1831,7 +1831,7 @@ different :token:`string` parameters to :tacn:`restart_timer` and .. example:: - .. coqtop:: all reset abort + .. rocqtop:: all reset abort Ltac time_constr1 tac := let eval_early := match goal with _ => restart_timer "(depth 1)" end in @@ -1950,7 +1950,7 @@ Proof that the natural numbers have at least two elements context to prove that natural numbers have at least two elements. This can be done as follows: - .. coqtop:: reset all + .. rocqtop:: reset all Lemma card_nat : ~ exists x y : nat, forall z:nat, x = z \/ y = z. @@ -1960,14 +1960,14 @@ Proof that the natural numbers have at least two elements At this point, the :tacn:`congruence` tactic would finish the job: - .. coqtop:: all abort + .. rocqtop:: all abort all: congruence. But for the purpose of the example, let's craft our own custom tactic to solve this: - .. coqtop:: none + .. rocqtop:: none Lemma card_nat : ~ exists x y : nat, forall z:nat, x = z \/ y = z. @@ -1975,7 +1975,7 @@ Proof that the natural numbers have at least two elements intros (x & y & Hz). destruct (Hz 0), (Hz 1), (Hz 2). - .. coqtop:: all abort + .. rocqtop:: all abort all: match goal with | _ : ?a = ?b, _ : ?a = ?c |- _ => assert (b = c) by now transitivity a @@ -1995,7 +1995,7 @@ Proving that a list is a permutation of a second list Let's first define the permutation predicate: - .. coqtop:: in reset + .. rocqtop:: in reset Section Sort. @@ -2009,7 +2009,7 @@ Proving that a list is a permutation of a second list End Sort. - .. coqtop:: none + .. rocqtop:: none Require Import ListDef. @@ -2032,7 +2032,7 @@ Proving that a list is a permutation of a second list primitive tactics and we cannot make computations with them. Thus, instead, we use Rocq's natural number type :g:`nat`. - .. coqtop:: in + .. rocqtop:: in Ltac perm_aux n := match goal with @@ -2056,7 +2056,7 @@ Proving that a list is a permutation of a second list lengths are equal. (If they aren't, the lists cannot be permutations of each other.) - .. coqtop:: in + .. rocqtop:: in Ltac solve_perm := match goal with @@ -2068,21 +2068,21 @@ Proving that a list is a permutation of a second list And now, here is how we can use the tactic :g:`solve_perm`: - .. coqtop:: out + .. rocqtop:: out Goal perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). - .. coqtop:: all abort + .. rocqtop:: all abort solve_perm. - .. coqtop:: out + .. rocqtop:: 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 + .. rocqtop:: all abort solve_perm. @@ -2096,7 +2096,7 @@ 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 +.. rocqtop:: in reset Ltac basic := match goal with @@ -2105,7 +2105,7 @@ tactic language as shown below. | _ : ?A |- ?A => assumption end. -.. coqtop:: in +.. rocqtop:: in Ltac simplify := repeat (intros; @@ -2130,7 +2130,7 @@ tactic language as shown below. | |- ~ _ => red end). -.. coqtop:: in +.. rocqtop:: in Ltac my_tauto := simplify; basic || @@ -2162,13 +2162,13 @@ and the right ``or``). Having defined ``my_tauto``, we can prove tautologies like these: -.. coqtop:: in +.. rocqtop:: in Lemma my_tauto_ex1 : forall A B : Prop, A /\ B -> A \/ B. Proof. my_tauto. Qed. -.. coqtop:: in +.. rocqtop:: in Lemma my_tauto_ex2 : forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. @@ -2183,19 +2183,19 @@ 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 +.. rocqtop:: in reset Open Scope type_scope. -.. coqtop:: in +.. rocqtop:: in Section Iso_axioms. -.. coqtop:: in +.. rocqtop:: in Variables A B C : Set. -.. coqtop:: in +.. rocqtop:: in Axiom Com : A * B = B * A. @@ -2211,7 +2211,7 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below. Axiom AL_unit : (unit -> A) = A. -.. coqtop:: in +.. rocqtop:: in Lemma Cons : B = C -> A * B = A * C. @@ -2221,11 +2221,11 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below. Qed. -.. coqtop:: in +.. rocqtop:: in End Iso_axioms. -.. coqtop:: in +.. rocqtop:: in Ltac simplify_type ty := match ty with @@ -2255,7 +2255,7 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below. | |- ?A = ?B => try simplify_type A; try simplify_type B end. -.. coqtop:: in +.. rocqtop:: in Ltac len trm := match trm with @@ -2263,11 +2263,11 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below. | _ => constr:(1) end. -.. coqtop:: in +.. rocqtop:: in Ltac assoc := repeat rewrite <- Ass. -.. coqtop:: in +.. rocqtop:: in Ltac solve_type_eq n := match goal with @@ -2282,7 +2282,7 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below. end end. -.. coqtop:: in +.. rocqtop:: in Ltac compare_structure := match goal with @@ -2294,7 +2294,7 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below. end end. -.. coqtop:: in +.. rocqtop:: in Ltac solve_iso := simplify_type_eq; compare_structure. @@ -2309,7 +2309,7 @@ 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 +.. rocqtop:: in Lemma solve_iso_ex1 : forall A B : Set, A * unit * B = B * (unit * A). @@ -2317,7 +2317,7 @@ Here are examples of what can be solved by ``solve_iso``. intros; solve_iso. Qed. -.. coqtop:: in +.. rocqtop:: in Lemma solve_iso_ex2 : forall A B C : Set, @@ -2357,20 +2357,20 @@ Tracing execution .. example:: - .. coqtop:: in reset + .. rocqtop:: in reset Ltac t x := exists x; reflexivity. Goal exists n, n=0. - .. coqtop:: all + .. rocqtop:: all Info 0 t 1||t 0. - .. coqtop:: in + .. rocqtop:: in Undo. - .. coqtop:: all + .. rocqtop:: all Info 1 t 1||t 0. @@ -2482,7 +2482,7 @@ performance issue. The following example requires the Stdlib library to use the :tacn:`lia` tactic. -.. coqtop:: reset in extra +.. rocqtop:: reset in extra From Stdlib Require Import Lia. @@ -2501,14 +2501,14 @@ The following example requires the Stdlib library to use the :tacn:`lia` tactic. M /\ L /\ K /\ J /\ I /\ H /\ G /\ F /\ E /\ D /\ C /\ B /\ A). Proof. -.. coqtop:: all extra +.. rocqtop:: all extra Set Ltac Profiling. tac. Show Ltac Profile. Show Ltac Profile "lia". -.. coqtop:: in extra +.. rocqtop:: in extra Abort. Unset Ltac Profiling. diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 178830919b4b..79c3eb6c2c91 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -62,7 +62,7 @@ by a value. Use the following command to import Ltac2: -.. coqtop:: in +.. rocqtop:: in From Ltac2 Require Import Ltac2. @@ -166,7 +166,7 @@ One can define new types with the following commands. .. example:: - .. coqtop:: in + .. rocqtop:: in Module PositiveInt. #[abstract] Ltac2 Type t := int. @@ -175,7 +175,7 @@ One can define new types with the following commands. Ltac2 get (x:t) : int := x. End PositiveInt. - .. coqtop:: all + .. rocqtop:: all Ltac2 Eval PositiveInt.get (PositiveInt.make 3). Fail Ltac2 Eval PositiveInt.get (PositiveInt.make -1). @@ -196,11 +196,11 @@ Ltac2 provides over 150 API functions that provide various capabilities. These are declared with :cmd:`Ltac2 external` in :n:`lib/coq/user-contrib/Ltac2/*.v`. For example, `Message.print` defined in `Message.v` is used to print messages: -.. coqtop:: none +.. rocqtop:: none Goal True. -.. coqtop:: all abort +.. rocqtop:: all abort Message.print (Message.of_string "fully qualified calls"). From Ltac2 Require Import Message. @@ -315,7 +315,7 @@ Ltac2 Definitions .. example:: Dynamic nature of mutable cells - .. coqtop:: all + .. rocqtop:: all Ltac2 mutable x := true. Ltac2 y () := x. @@ -325,7 +325,7 @@ Ltac2 Definitions .. example:: Interaction with recursive calls - .. coqtop:: all + .. rocqtop:: all Ltac2 mutable rec f b := if b then 0 else f true. Ltac2 Set f := fun b => if b then 1 else f true. @@ -662,7 +662,7 @@ is potentially ill-typed as a runtime **Rocq** term. The following term is valid (with type `unit -> constr`), but will fail at runtime: - .. coqtop:: in + .. rocqtop:: in Ltac2 myconstr () := constr:(nat -> 0). @@ -673,7 +673,7 @@ of the corresponding term expression. The following will type check, with type `constr`. - .. coqdoc:: + .. rocqdoc:: let x := '0 in constr:(1 + ltac2:(exact $x)) @@ -718,7 +718,7 @@ current context using the `Ltac2.Constr.pretype` function. The following notation is essentially the identity. - .. coqtop:: in + .. rocqtop:: in Notation "[ x ]" := ltac2:(let x := Ltac2.Constr.pretype x in exact $x) (only parsing). @@ -909,12 +909,12 @@ one from Ltac1, except that it requires the goal to be focused. These lines define a `msg` tactic that's used in several examples as a more-succinct alternative to `print (to_string "...")`: - .. coqtop:: in + .. rocqtop:: in From Ltac2 Require Import Message. Ltac2 msg x := print (of_string x). - .. coqtop:: none + .. rocqtop:: none Goal True. @@ -923,7 +923,7 @@ one from Ltac1, except that it requires the goal to be focused. in a matching branch, it will try to match on subsequent branches. Note that :n:`'@term` below is equivalent to :n:`open_constr:(@term)`. - .. coqtop:: all + .. rocqtop:: all Fail lazy_match! 'True with | True => msg "branch 1"; fail @@ -944,7 +944,7 @@ one from Ltac1, except that it requires the goal to be focused. :tacn:`match!` tactics are only evaluated once, whereas :tacn:`multi_match!` tactics may be evaluated more than once if the following constructs trigger backtracking: - .. coqtop:: all + .. rocqtop:: all Fail match! 'True with | True => msg "branch 1" @@ -952,7 +952,7 @@ one from Ltac1, except that it requires the goal to be focused. end ; msg "branch A"; fail. - .. coqtop:: all + .. rocqtop:: all Fail multi_match! 'True with | True => msg "branch 1" @@ -970,7 +970,7 @@ one from Ltac1, except that it requires the goal to be focused. Notice the :tacn:`idtac` prints ``(z + 1)`` while the :tacn:`pose` substitutes ``(x + 1)``. - .. coqtop:: all + .. rocqtop:: all match! constr:(fun x => (x + 1) * 3) with | fun z => ?y * 3 => print (of_constr y); pose (fun z: nat => $y * 5) @@ -985,14 +985,14 @@ one from Ltac1, except that it requires the goal to be focused. Internally "x <> y" is represented as "(~ (x = y))", which produces the first match. - .. coqtop:: in + .. rocqtop:: in Ltac2 f2 t := match! t with | context [ (~ ?t) ] => print (of_constr t); fail | _ => () end. - .. coqtop:: all abort + .. rocqtop:: all abort f2 constr:((~ True) <> (~ False)). @@ -1099,7 +1099,7 @@ Match over goals Hypotheses are matched from the last hypothesis (which is by default the newest hypothesis) to the first until the :tacn:`apply` succeeds. - .. coqtop:: all abort + .. rocqtop:: all abort Goal forall A B : Prop, A -> B -> (A->B). intros. @@ -1115,7 +1115,7 @@ Match over goals Hypotheses are matched from the first hypothesis to the last until the :tacn:`apply` succeeds. - .. coqtop:: all abort + .. rocqtop:: all abort Goal forall A B : Prop, A -> B -> (A->B). intros. @@ -1134,7 +1134,7 @@ Match over goals Observe that the number of permutations can grow as the factorial of the number of hypotheses and hypothesis patterns. - .. coqtop:: all abort + .. rocqtop:: all abort Goal forall A B : Prop, A -> B -> (A->B). intros A B H. @@ -1235,11 +1235,11 @@ Notations .. example:: Printing a :n:`@term` - .. coqtop:: none + .. rocqtop:: none Goal True. - .. coqtop:: all + .. rocqtop:: all From Ltac2 Require Import Message. Ltac2 Notation "ex1" x(constr) := print (of_constr x). @@ -1248,7 +1248,7 @@ Notations You can also print terms with a regular Ltac2 definition, but then the :n:`@term` must be in the quotation `constr:( … )`: - .. coqtop:: all + .. rocqtop:: all Ltac2 ex2 x := print (of_constr x). ex2 constr:(1+2). @@ -1259,7 +1259,7 @@ Notations .. example:: Parsing a list of :n:`@term`\s - .. coqtop:: abort all + .. rocqtop:: abort all Ltac2 rec print_list x := match x with | a :: t => print (of_constr a); print_list t @@ -1276,7 +1276,7 @@ Notations Assume we perform: - .. coqdoc:: + .. rocqdoc:: Ltac2 Notation "foo" c(thunk(constr)) ids(list0(ident)) := Bar.f c ids. @@ -1363,7 +1363,7 @@ in the documentation are defined with Ltac1.) You can make them accessible in Ltac2 with commands similar to the following (the example requires the Stdlib library for the :tacn:`lia` tactic): -.. coqtop:: in extra +.. rocqtop:: in extra From Stdlib Require Import Lia. Local Ltac2 lia_ltac1 () := ltac1:(lia). @@ -1791,7 +1791,7 @@ Ltac1 **cannot** implicitly access variables from the Ltac2 scope, but this can be done with an explicit annotation on the :n:`ltac1:({* @ident } |- @ltac_expr)` quotation. See :ref:`ltac2_built-in-quotations`. For example: -.. coqtop:: in +.. rocqtop:: in Local Ltac2 replace_with (lhs: constr) (rhs: constr) := ltac1:(lhs rhs |- replace lhs with rhs) (Ltac1.of_constr lhs) (Ltac1.of_constr rhs). @@ -1844,12 +1844,12 @@ eagerly, if one wants to use it as an argument to a Ltac1 function, one has to resort to the good old :n:`idtac; ltac2:(foo)` trick. For instance, the code below will fail immediately and won't print anything. -.. coqtop:: in +.. rocqtop:: in From Ltac2 Require Import Ltac2. Set Default Proof Mode "Classic". -.. coqtop:: all +.. rocqtop:: all Ltac mytac tac := idtac "I am being evaluated"; tac. @@ -1872,7 +1872,7 @@ Use the `ltac2val` quotation to return values to Ltac1 from Ltac2. It has the same typing rules as `ltac2:()` except the expression must have type `Ltac2.Ltac1.t`. -.. coqtop:: all +.. rocqtop:: all Import Constr.Unsafe. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index d01ecbcdef6d..a68316849001 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -94,7 +94,7 @@ specific to the authors of |SSR| and which requires a few options to be set in a different way than in their default way. All in all, this corresponds to working in the following context: -.. coqtop:: in +.. rocqtop:: in From Corelib Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. @@ -135,7 +135,7 @@ compatible with the rest of Rocq, up to a few discrepancies. + New constant and theorem names might clash with the user theory. This can be avoided by not importing all of |SSR|: - .. coqtop:: in + .. rocqtop:: in From Corelib Require ssreflect. Import ssreflect.SsrSyntax. @@ -206,7 +206,7 @@ construct differs from the latter as follows. + The pattern can be nested (deep pattern matching); in particular, this allows expression of the form: -.. coqdoc:: +.. rocqdoc:: let: exist (x, y) p_xy := Hp in … . @@ -215,14 +215,14 @@ construct differs from the latter as follows. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Definition f u := let: (m, n) := u in m + n. Check f. @@ -231,7 +231,7 @@ construct differs from the latter as follows. whereas with a usual ``let`` the same term requires an extra type annotation in order to type check. - .. coqtop:: reset all + .. rocqtop:: reset all Fail Definition f u := let (m, n) := u in m + n. @@ -275,7 +275,7 @@ example, the null and all list function(al)s can be defined as follows: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -283,7 +283,7 @@ example, the null and all list function(al)s can be defined as follows: Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Variable d: Set. Definition null (s : list d) := @@ -319,7 +319,7 @@ annotations. .. example:: - .. coqtop:: all + .. rocqtop:: all Definition orb b1 b2 := if b1 then true else b2. @@ -376,7 +376,7 @@ expressions such as .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -387,7 +387,7 @@ expressions such as Variable null : forall T : Type, T -> bool. Variable all : (T -> bool) -> list T -> bool. - .. coqtop:: all + .. rocqtop:: all Definition all_null (s : list T) := all (@null T) s. @@ -401,7 +401,7 @@ each point of use; e.g., the above definition can be written: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -413,7 +413,7 @@ each point of use; e.g., the above definition can be written: Variable all : (T -> bool) -> list T -> bool. - .. coqtop:: all + .. rocqtop:: all Prenex Implicits null. Definition all_null (s : list T) := all null s. @@ -436,7 +436,7 @@ The syntax of the new declaration is a ``Set Printing All`` command). All |SSR| library files thus start with the incantation - .. coqdoc:: + .. rocqdoc:: Set Implicit Arguments. Unset Strict Implicit. @@ -464,14 +464,14 @@ defined by the following declaration: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Inductive list (A : Type) : Type := nil | cons of A & list A. @@ -505,7 +505,7 @@ Definitions |SSR| :tacn:`pose (ssreflect)` tactic supports *open syntax*: the body of the definition does not need surrounding parentheses. For instance: -.. coqdoc:: +.. rocqdoc:: pose t := x + y. @@ -518,14 +518,14 @@ For example, the tactic :tacn:`pose (ssreflect)` supports parameters: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test : True. pose f x y := x + y. @@ -534,7 +534,7 @@ The |SSR| :tacn:`pose (ssreflect)` tactic also supports (co)fixpoints, by provid the local counterpart of the ``Fixpoint f := …`` and ``CoFixpoint f := …`` constructs. For instance, the following tactic: -.. coqdoc:: +.. rocqdoc:: pose fix f (x y : nat) {struct x} : nat := if x is S p then S (f p y) else 0. @@ -544,7 +544,7 @@ on natural numbers. Similarly, local cofixpoints can be defined by a tactic of the form: -.. coqdoc:: +.. rocqdoc:: pose cofix f (arg : T) := … . @@ -553,26 +553,26 @@ offers a smooth way of defining local abstractions. The type of “holes” is guessed by type inference, and the holes are abstracted. For instance the tactic: -.. coqdoc:: +.. rocqdoc:: pose f := _ + 1. is shorthand for: -.. coqdoc:: +.. rocqdoc:: pose f n := n + 1. When the local definition of a function involves both arguments and holes, hole abstractions appear first. For instance, the tactic: -.. coqdoc:: +.. rocqdoc:: pose f x := x + _. is shorthand for: -.. coqdoc:: +.. rocqdoc:: pose f n x := x + n. @@ -580,13 +580,13 @@ The interaction of the :tacn:`pose (ssreflect)` tactic with the interpretation o arguments results in a powerful and concise syntax for local definitions involving dependent types. For instance, the tactic: -.. coqdoc:: +.. rocqdoc:: pose f x y := (x, y). adds to the context the local definition: -.. coqdoc:: +.. rocqdoc:: pose f (Tx Ty : Type) (x : Tx) (y : Ty) := (x, y). @@ -639,7 +639,7 @@ The tactic: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -647,12 +647,12 @@ The tactic: Unset Printing Implicit Defensive. Axiom f : nat -> nat. - .. coqtop:: all + .. rocqtop:: all Lemma test x : f x + f x = f x. set t := f _. - .. coqtop:: all restart + .. rocqtop:: all restart set t := {2}(f _). @@ -690,14 +690,14 @@ conditions. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test (x y z : nat) : x + y = z. set t := _ x. @@ -711,14 +711,14 @@ conditions. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test : (let f x y z := x + y + z in f 1) 2 3 = 6. set t := (let g y z := S y + z in g) 2. @@ -732,14 +732,14 @@ Moreover: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test x y z : x + y = z. set t := _ + _. @@ -752,14 +752,14 @@ Moreover: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test : forall x : nat, x + 1 = 0. Fail set t := _ + 1. @@ -785,7 +785,7 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -793,7 +793,7 @@ An *occurrence switch* can be: Unset Printing Implicit Defensive. Axiom f : nat -> nat. - .. coqtop:: all + .. rocqtop:: all Lemma test : f 2 + f 8 = f 2 + f 2. set x := {+1 3}(f 2). @@ -807,14 +807,14 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Notation "a < b":= (le (S a) b). Lemma test x y : x < y -> S x < S y. @@ -828,7 +828,7 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -836,7 +836,7 @@ An *occurrence switch* can be: Unset Printing Implicit Defensive. Axiom f : nat -> nat. - .. coqtop:: all + .. rocqtop:: all Lemma test : f 2 + f 8 = f 2 + f 2. set x := {-2}(f 2). @@ -859,14 +859,14 @@ selection. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test x y z : x + y = x + y + z. set a := {2}(_ + _). @@ -876,14 +876,14 @@ only one occurrence of the selected term. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test x y z : (x + y) + (z + z) = z + z. Fail set a := {2}(_ + _). @@ -907,11 +907,11 @@ context of a goal thanks to the ``in`` tactical. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. - .. coqtop:: all + .. rocqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. set z := 3 in Hx. @@ -923,11 +923,11 @@ context of a goal thanks to the ``in`` tactical. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. - .. coqtop:: all + .. rocqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. set z := 3 in Hx * . @@ -1039,20 +1039,20 @@ constants to the goal. For example, the proof of [#3]_ - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma subnK : forall m n, n <= m -> m - n + n = m. might start with - .. coqtop:: all + .. rocqtop:: all move=> m n le_n_m. @@ -1065,7 +1065,7 @@ constants to the goal. constants from the context by turning them into variables and assumptions. - .. coqtop:: all + .. rocqtop:: all move: m le_n_m. @@ -1076,7 +1076,7 @@ constants to the goal. Because they are tacticals, ``:`` and ``=>`` can be combined, as in -.. coqdoc:: +.. rocqdoc:: move: m le_n_m => p le_n_p. @@ -1101,14 +1101,14 @@ The ``:`` tactical is used to operate on an element in the context. to encapsulate the inductive step in a single command: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma subnK : forall m n, n <= m -> m - n + n = m. move=> m n le_n_m. @@ -1136,7 +1136,7 @@ Basic tactics like ``apply`` and ``elim`` can also be used without the ’:’ tactical: for example, we can directly start a proof of ``subnK`` by induction on the top variable ``m`` with -.. coqdoc:: +.. rocqdoc:: elim=> [|m IHm] n le_n. @@ -1147,7 +1147,7 @@ explained in terms of the goal stack:: is basically equivalent to -.. coqdoc:: +.. rocqdoc:: move: a H1 H2; tactic => a H1 H2. @@ -1160,13 +1160,13 @@ temporary abbreviation to hide the statement of the goal from The general form of the ``in`` tactical can be used directly with the ``move``, ``case`` and ``elim`` tactics, so that one can write -.. coqdoc:: +.. rocqdoc:: elim: n => [|n IHn] in m le_n_m *. instead of -.. coqdoc:: +.. rocqdoc:: elim: n m le_n_m => [|n IHn] m le_n_m. @@ -1196,7 +1196,7 @@ The move tactic. .. example:: - .. coqtop:: reset all + .. rocqtop:: reset all Require Import ssreflect. Goal not False. @@ -1266,14 +1266,14 @@ The elim tactic .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test m : forall n : nat, m <= n. elim. @@ -1306,7 +1306,7 @@ existential metavariables of sort :g:`Prop`. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -1314,7 +1314,7 @@ existential metavariables of sort :g:`Prop`. Unset Printing Implicit Defensive. Axiom lt_trans : forall a b c, a < b -> b < c -> a < c. - .. coqtop:: all + .. rocqtop:: all Lemma test : forall y, 1 < y -> y < 2 -> exists x : { n | n < 3 }, 0 < proj1_sig x. move=> y y_gt1 y_lt2; apply: (ex_intro _ (exist _ y _)). @@ -1407,7 +1407,7 @@ Switches affect the discharging of a :token:`d_item` as follows. For example, the tactic: -.. coqdoc:: +.. rocqdoc:: move: n {2}n (refl_equal n). @@ -1418,7 +1418,7 @@ For example, the tactic: Therefore, this tactic changes any goal ``G`` into -.. coqdoc:: +.. rocqdoc:: forall n n0 : nat, n = n0 -> G. @@ -1486,7 +1486,7 @@ context to interpret wildcards; in particular, it can accommodate the .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -1495,7 +1495,7 @@ context to interpret wildcards; in particular, it can accommodate the Axiom f : nat -> nat. Axiom g : nat -> nat. - .. coqtop:: all + .. rocqtop:: all Lemma test (Hfg : forall x, f x = g x) a b : f a = g b. apply: trans_equal (Hfg _) _. @@ -1639,11 +1639,11 @@ The second entry in the :token:`i_view` grammar rule, ``/ltac:(`` :token:`tactic` ``)``, executes :token:`tactic`. Notations can be used to name tactics, for example -.. coqtop:: none +.. rocqtop:: none Tactic Notation "my" "ltac" "code" := idtac. -.. coqtop:: in warn +.. rocqtop:: in warn Notation "'myop'" := (ltac:(my ltac code)) : ssripat_scope. @@ -1778,14 +1778,14 @@ Clears are deferred until the end of the intro pattern. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect ssrbool. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test x y : Nat.leb 0 x = true -> (Nat.leb 0 x) && (Nat.leb y 2) = true. move=> {x} ->. @@ -1839,14 +1839,14 @@ Block introduction .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Record r := { a : nat; b := (a, 3); _ : bool; }. @@ -1869,7 +1869,7 @@ Generation of equations The generation of named equations option stores the definition of a new constant as an equation. The tactic: -.. coqdoc:: +.. rocqdoc:: move En: (size l) => n. @@ -1877,7 +1877,7 @@ where ``l`` is a list, replaces ``size l`` by ``n`` in the goal and adds the fact ``En : size l = n`` to the context. This is quite different from: -.. coqdoc:: +.. rocqdoc:: pose n := (size l). @@ -1892,14 +1892,14 @@ deal with the possible parameters of the constants introduced. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test (a b :nat) : a <> b. case E : a => [|n]. @@ -1911,14 +1911,14 @@ under fresh |SSR| names. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test (a b :nat) : a <> b. case E : a => H. @@ -1962,7 +1962,7 @@ be substituted. inferred by looking at the type of the top assumption. This allows for the compact syntax: - .. coqdoc:: + .. rocqdoc:: case: {2}_ / eqP. @@ -1978,14 +1978,14 @@ be substituted. Here is a small example on lists. We define first a function that adds an element at the end of a given list. - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all From Corelib Require Import ListDef. Section LastCases. @@ -1999,7 +1999,7 @@ be substituted. Then we define an inductive predicate for case analysis on lists according to their last element: - .. coqtop:: all + .. rocqtop:: all Inductive last_spec : list A -> Type := | LastSeq0 : last_spec nil @@ -2010,7 +2010,7 @@ be substituted. We are now ready to use ``lastP`` in conjunction with ``case``. - .. coqtop:: all + .. rocqtop:: all Lemma test l : (length l) * 2 = length (l ++ l). case: (lastP l). @@ -2018,13 +2018,13 @@ be substituted. Applied to the same goal, the tactic ``case: l / (lastP l)`` generates the same subgoals, but ``l`` has been cleared from both contexts: - .. coqtop:: all restart + .. rocqtop:: all restart case: l / (lastP l). Again applied to the same goal: - .. coqtop:: all restart abort + .. rocqtop:: all restart abort case: {1 3}l / (lastP l). @@ -2039,7 +2039,7 @@ be substituted. .. example:: - .. coqtop:: all + .. rocqtop:: all Lemma test l : (length l) * 2 = length (l ++ l). case E: {1 3}l / (lastP l) => [|s x]. @@ -2132,7 +2132,7 @@ In the script provided as example in Section :ref:`indentation_ssr`, the paragraph corresponding to each sub-case ends with a tactic line prefixed with a ``by``, like in: -.. coqdoc:: +.. rocqdoc:: by apply/eqP; rewrite -dvdn1. @@ -2149,7 +2149,7 @@ with a ``by``, like in: The default implementation of the :tacn:`done` tactic, in the ``ssreflect.v`` file, is: - .. coqdoc:: + .. rocqdoc:: Ltac done := trivial; hnf; intros; solve @@ -2165,13 +2165,13 @@ A natural and common way of closing a goal is to apply a lemma that is the exact one needed for the goal to be solved. The defective form of the tactic: -.. coqdoc:: +.. rocqdoc:: exact. is equivalent to: -.. coqdoc:: +.. rocqdoc:: do [done | by move=> top; apply top]. @@ -2179,13 +2179,13 @@ where ``top`` is a fresh name assigned to the top assumption of the goal. This applied form is supported by the ``:`` discharge tactical, and the tactic: -.. coqdoc:: +.. rocqdoc:: exact: MyLemma. is equivalent to: -.. coqdoc:: +.. rocqdoc:: by apply: MyLemma. @@ -2197,19 +2197,19 @@ is equivalent to: follows the ``by`` keyword is considered to be a parenthesized block applied to the current goal. Hence for example if the tactic: - .. coqdoc:: + .. rocqdoc:: by rewrite my_lemma1. succeeds, then the tactic: - .. coqdoc:: + .. rocqdoc:: by rewrite my_lemma1; apply my_lemma2. usually fails since it is equivalent to: - .. coqdoc:: + .. rocqdoc:: by (rewrite my_lemma1; apply my_lemma2). @@ -2266,7 +2266,7 @@ Finally, the tactics ``last`` and ``first`` combine with the branching syntax of Ltac: if the tactic generates n subgoals on a given goal, then the tactic -.. coqdoc:: +.. rocqdoc:: tactic ; last k [ tactic1 |…| tacticm ] || tacticn. @@ -2279,14 +2279,14 @@ to the others. Here is a small example on lists. We define first a function that adds an element at the end of a given list. - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Inductive test : nat -> Prop := | C1 n of n = 1 : test n @@ -2314,13 +2314,13 @@ Iteration A tactic of the form: -.. coqdoc:: +.. rocqdoc:: do [ tactic 1 | … | tactic n ]. is equivalent to the standard Ltac expression: -.. coqdoc:: +.. rocqdoc:: first [ tactic 1 | … | tactic n ]. @@ -2345,14 +2345,14 @@ Their meaning is as follows. For instance, the tactic: -.. coqdoc:: +.. rocqdoc:: tactic; do 1? rewrite mult_comm. rewrites at most one time the lemma ``mult_comm`` in all the subgoals generated by tactic, whereas the tactic: -.. coqdoc:: +.. rocqdoc:: tactic; do 2! rewrite mult_comm. @@ -2398,14 +2398,14 @@ between standard Ltac ``in`` and the |SSR| tactical in. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Ltac mytac H := rewrite H. @@ -2473,21 +2473,21 @@ the holes are abstracted in term. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test : True. have: _ * 0 = 0. The invocation of ``have`` is equivalent to: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -2495,7 +2495,7 @@ the holes are abstracted in term. Unset Printing Implicit Defensive. Lemma test : True. - .. coqtop:: all + .. rocqtop:: all have: forall n : nat, n * 0 = 0. @@ -2505,7 +2505,7 @@ tactic: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -2513,7 +2513,7 @@ tactic: Unset Printing Implicit Defensive. Lemma test : True. - .. coqtop:: all + .. rocqtop:: all have: forall x y, (x, y) = (x, y + 0). @@ -2536,7 +2536,7 @@ tactics of the form: which behaves like: -.. coqdoc:: +.. rocqdoc:: have: term ; first by tactic. move=> clear_switch i_item. @@ -2549,7 +2549,7 @@ to introduce the new assumption itself. The ``by`` feature is especially convenient when the proof script of the statement is very short, basically when it fits in one line like in: -.. coqdoc:: +.. rocqdoc:: have H23 : 3 + 2 = 2 + 3 by rewrite addnC. @@ -2558,14 +2558,14 @@ the further use of the intermediate step. For instance, .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test a : 3 * a - 1 = a. have -> : forall x, x * a = a. @@ -2577,7 +2577,7 @@ the further use of the intermediate step. For instance, Thanks to the deferred execution of clears, the following idiom is also supported (assuming x occurs in the goal only): -.. coqdoc:: +.. rocqdoc:: have {x} -> : x = y. @@ -2586,14 +2586,14 @@ destruction of existential assumptions like in the tactic: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test : True. have [x Px]: exists x : nat, x > 0; last first. @@ -2613,14 +2613,14 @@ term for the intermediate lemma, using tactics of the form: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test : True. have H := forall x, (x, x) = (x, x). @@ -2635,7 +2635,7 @@ The following example requires the mathcomp and mczify libraries. .. example:: - .. coqtop:: reset none warn extra + .. rocqtop:: reset none warn extra From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat zify. @@ -2643,7 +2643,7 @@ The following example requires the mathcomp and mczify libraries. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all extra + .. rocqtop:: all extra Lemma test : True. have H x (y : nat) : 2 * x + y = x + x + y by lia. @@ -2654,7 +2654,7 @@ Since the :token:`i_pattern` can be omitted, to avoid ambiguity, bound variables can be surrounded with parentheses even if no type is specified: -.. coqtop:: all restart extra +.. rocqtop:: all restart extra have (x) : 2 * x = x + x by lia. @@ -2668,7 +2668,7 @@ copying the goal itself. .. example:: - .. coqtop:: all restart abort extra + .. rocqtop:: all restart abort extra have suff H : 2 + 2 = 3; last first. @@ -2688,11 +2688,11 @@ context entry name. .. example:: - .. coqtop:: none + .. rocqtop:: none Set Printing Depth 15. - .. coqtop:: all abort extra + .. rocqtop:: all abort extra Inductive Ord n := Sub x of x < n. Notation "'I_ n" := (Ord n) (at level 8, n at level 2, format "''I_' n"). @@ -2708,7 +2708,7 @@ For this purpose the ``[: name]`` intro pattern and the tactic .. example:: - .. coqtop:: all abort extra + .. rocqtop:: all abort extra Lemma test n m (H : m + 1 < n) : True. have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; lia. @@ -2721,7 +2721,7 @@ with`` have`` and an explicit term, they must be used as follows: .. example:: - .. coqtop:: all abort extra + .. rocqtop:: all abort extra Lemma test n m (H : m + 1 < n) : True. have [:pm] @i : 'I_n := Sub m pm. @@ -2740,7 +2740,7 @@ makes use of it). .. example:: - .. coqtop:: all abort extra + .. rocqtop:: all abort extra Lemma test n m (H : m + 1 < n) : True. have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; lia. @@ -2755,7 +2755,7 @@ The have tactic and typeclass resolution Since |SSR| 1.5, the ``have`` tactic behaves as follows with respect to typeclass inference. - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. @@ -2764,7 +2764,7 @@ typeclass inference. Goal True. - .. coqtop:: all + .. rocqtop:: all have foo : ty. @@ -2773,7 +2773,7 @@ typeclass inference. .. A strange bug prevents using the coqtop directive here - .. coqdoc:: + .. rocqdoc:: have foo : ty := . @@ -2782,13 +2782,13 @@ typeclass inference. statement. Note that no proof term follows ``:=``; hence two subgoals are generated. - .. coqtop:: all restart + .. rocqtop:: all restart have foo : ty := t. No inference for ``ty`` and ``t``. - .. coqtop:: all restart abort + .. rocqtop:: all restart abort have foo := t. @@ -2819,7 +2819,7 @@ The + the optional clear item is still performed in the *second* branch, which means that the tactic: - .. coqdoc:: + .. rocqdoc:: suff {H} H : forall x : nat, x >= 0. @@ -2835,11 +2835,11 @@ The ``have`` modifier can follow the ``suff`` tactic. .. example:: - .. coqtop:: none + .. rocqtop:: none Axioms G P : Prop. - .. coqtop:: all abort + .. rocqtop:: all abort Lemma test : G. suff have H : P. @@ -2890,7 +2890,7 @@ name of the local definition with the ``@`` character. In the second subgoal, the tactic: -.. coqdoc:: +.. rocqdoc:: move=> clear_switch i_item. @@ -2906,11 +2906,11 @@ The following example requires the mathcomp and mczify libraries. .. example:: - .. coqtop:: reset none warn extra + .. rocqtop:: reset none warn extra From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat. - .. coqtop:: all extra + .. rocqtop:: all extra Lemma quo_rem_unicity d q1 q2 r1 r2 : q1*d + r1 = q2*d + r2 -> r1 < d -> r2 < d -> (q1, r1) = (q2, r2). @@ -2931,7 +2931,7 @@ pattern will be used to process its instance. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. @@ -2945,7 +2945,7 @@ pattern will be used to process its instance. Notation "a <= b" := (leqn a b) (at level 70) : this_scope. Open Scope this_scope. - .. coqtop:: all + .. rocqtop:: all Lemma simple n (ngt0 : 0 < n ) : P n. gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0); last first. @@ -2981,14 +2981,14 @@ illustrated in the following example. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Section Test. Variable x : nat. @@ -3000,7 +3000,7 @@ illustrated in the following example. the pattern ``id (addx x)``, which would produce the following first subgoal - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -3012,7 +3012,7 @@ illustrated in the following example. Definition addx z := z + x. Lemma test : x <= addx x. - .. coqtop:: all + .. rocqtop:: all wlog H : (y := x) (@twoy := id (addx x)) / twoy = 2 * y. @@ -3134,14 +3134,14 @@ A :token:`r_item` can be one of the following. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all abort + .. rocqtop:: all abort Definition double x := x + x. Definition ddouble x := double (double x). @@ -3153,18 +3153,18 @@ A :token:`r_item` can be one of the following. The |SSR| terms containing holes are *not* typed as abstractions in this context. Hence the following script fails. - .. coqtop:: all + .. rocqtop:: all Definition f := fun x y => x + y. Lemma test x y : x + y = f y x. - .. coqtop:: all fail + .. rocqtop:: all fail rewrite -[f y]/(y + _). but the following script succeeds - .. coqtop:: all + .. rocqtop:: all rewrite -[f y x]/(y + _). @@ -3195,7 +3195,7 @@ tactics. In a rewrite tactic of the form: -.. coqdoc:: +.. rocqdoc:: rewrite occ_switch [term1]term2. @@ -3238,7 +3238,7 @@ Performing rewrite and simplification operations in a single tactic enhances significantly the concision of scripts. For instance the tactic: -.. coqdoc:: +.. rocqdoc:: rewrite /my_def {2}[f _]/= my_eq //=. @@ -3253,14 +3253,14 @@ proof of basic results on natural numbers arithmetic. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Axiom addn0 : forall m, m + 0 = m. Axiom addnS : forall m n, m + S n = S (m + n). @@ -3289,14 +3289,14 @@ side of the equality the user wants to rewrite. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test (H : forall t u, t + u = u + t) x y : x + y = y + x. rewrite [y + _]H. @@ -3309,14 +3309,14 @@ the equality. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test (H : forall t u, t + u * 0 = t) x y : x + y * 4 + 2 * 0 = x + 2 * 0. Fail rewrite [x + _]H. @@ -3332,14 +3332,14 @@ Occurrence switches and redex switches .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test x y : x + y + 0 = x + y + y + 0 + 0 + (x + y + 0). rewrite {2}[_ + y + 0](_: forall z, z + 0 = z). @@ -3361,14 +3361,14 @@ repetition. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. rocqtop:: all Lemma test x y (z : nat) : x + 1 = x + y + 1. rewrite 2!(_ : _ + 1 = z). @@ -3391,7 +3391,7 @@ rewrite operations prescribed by the rules on the current goal. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -3400,7 +3400,7 @@ rewrite operations prescribed by the rules on the current goal. Section Test. - .. coqtop:: all abort + .. rocqtop:: all abort Variables (a b c : nat). Hypothesis eqab : a = b. @@ -3414,7 +3414,7 @@ rewrite operations prescribed by the rules on the current goal. ``(eqab, eqac)`` is actually a Rocq term and we can name it with a definition: - .. coqtop:: all + .. rocqtop:: all Definition multi1 := (eqab, eqac). @@ -3430,7 +3430,7 @@ literal matches have priority. .. example:: - .. coqtop:: all abort + .. rocqtop:: all abort Definition d := a. Hypotheses eqd0 : d = 0. @@ -3447,7 +3447,7 @@ repeated anew. .. example:: - .. coqtop:: all abort + .. rocqtop:: all abort Hypothesis eq_adda_b : forall x, x + a = b. Hypothesis eq_adda_c : forall x, x + a = c. @@ -3470,7 +3470,7 @@ tactic rewrite ``(=^~ multi1)`` is equivalent to ``rewrite multi1_rev``. .. example:: - .. coqtop:: all + .. rocqtop:: all Hypothesis eqba : b = a. Hypothesis eqca : c = a. @@ -3489,7 +3489,7 @@ reasoning purposes. The library also provides one lemma per such operation, stating that both versions return the same values when applied to the same arguments: -.. coqdoc:: +.. rocqdoc:: Lemma addE : add =2 addn. Lemma doubleE : double =1 doublen. @@ -3505,7 +3505,7 @@ In order to reason conveniently on expressions involving the efficient operations, we gather all these rules in the definition ``trecE``: -.. coqdoc:: +.. rocqdoc:: Definition trecE := (addE, (doubleE, oddE), (mulE, add_mulE, (expE, mul_expE))). @@ -3525,7 +3525,7 @@ Anyway this tactic is *not* equivalent to .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -3534,14 +3534,14 @@ Anyway this tactic is *not* equivalent to Section Test. - .. coqtop:: all + .. rocqtop:: all Lemma test y z : y * 0 + y * (z * 0) = 0. rewrite (_ : _ * 0 = 0). while the other tactic results in - .. coqtop:: all restart abort + .. rocqtop:: all restart abort rewrite (_ : forall x, x * 0 = 0). @@ -3559,14 +3559,14 @@ cases. + |SSR| never accepts to rewrite indeterminate patterns like: - .. coqdoc:: + .. rocqdoc:: Lemma foo (x : unit) : x = tt. |SSR| will however accept the ηζ expansion of this rule: - .. coqdoc:: + .. rocqdoc:: Lemma fubar (x : unit) : (let u := x in u) = tt. @@ -3575,7 +3575,7 @@ cases. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -3584,7 +3584,7 @@ cases. Section Test. - .. coqtop:: all + .. rocqtop:: all Variable g : nat -> nat. Definition f := g. @@ -3598,7 +3598,7 @@ cases. there is no occurrence of the head symbol ``f`` of the rewrite rule in the goal. - .. coqtop:: all restart fail + .. rocqtop:: all restart fail rewrite H. @@ -3608,13 +3608,13 @@ cases. occurrence), using tactic ``rewrite /f`` (for a global replacement of ``f`` by ``g``) or ``rewrite pattern/f``, for a finer selection. - .. coqtop:: all restart + .. rocqtop:: all restart rewrite /f H. Alternatively, one can override the pattern inferred from ``H`` - .. coqtop:: all restart + .. rocqtop:: all restart rewrite [f _]H. @@ -3633,7 +3633,7 @@ corresponding new goals will be generated. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. @@ -3641,7 +3641,7 @@ corresponding new goals will be generated. Unset Printing Implicit Defensive. Set Warnings "-notation-overridden". - .. coqtop:: all abort + .. rocqtop:: all abort Axiom leq : nat -> nat -> bool. Notation "m <= n" := (leq m n) : nat_scope. @@ -3664,7 +3664,7 @@ corresponding new goals will be generated. As in :ref:`apply_ssr`, the ``ssrautoprop`` tactic is used to try to solve the existential variable. - .. coqtop:: all abort + .. rocqtop:: all abort Lemma test (x : 'I_2) y (H : y < 2) : Some x = insub 2 y. rewrite insubT. @@ -3690,14 +3690,14 @@ complete terms, as shown by the simple example below. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: in + .. rocqtop:: in Axiom subnn : forall n : nat, n - n = 0. Parameter map : (nat -> nat) -> list nat -> list nat. @@ -3707,13 +3707,13 @@ complete terms, as shown by the simple example below. (forall n : nat, F1 n = F2 n) -> forall l : list nat, map F1 l = map F2 l. - .. coqtop:: all + .. rocqtop:: all Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. In this context, one cannot directly use ``eq_map``: - .. coqtop:: all fail + .. rocqtop:: all fail rewrite eq_map. @@ -3722,7 +3722,7 @@ complete terms, as shown by the simple example below. rewriting step. In order to perform the rewrite step, one has to provide the term by hand as follows: - .. coqtop:: all abort + .. rocqtop:: all abort rewrite (@eq_map _ (fun _ : nat => 0)). by move=> m; rewrite subnn. @@ -3730,7 +3730,7 @@ complete terms, as shown by the simple example below. The :tacn:`under` tactic lets one perform the same operation in a more convenient way: - .. coqtop:: all abort + .. rocqtop:: all abort Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. under eq_map => m do rewrite subnn. @@ -3767,7 +3767,7 @@ Let us redo the running example in interactive mode. .. example:: - .. coqtop:: all abort + .. rocqtop:: all abort Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. under eq_map => m. @@ -3881,7 +3881,7 @@ Notes: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -3932,12 +3932,12 @@ Notes: Parameter odd : nat -> bool. Parameter prime : nat -> bool. - .. coqtop:: in + .. rocqtop:: in Parameter addnC : forall m n : nat, m + n = n + m. Parameter muln1 : forall n : nat, n * 1 = n. - .. coqtop:: all + .. rocqtop:: all Check eq_bigr. Check eq_big. @@ -3976,7 +3976,7 @@ copy of any term ``t``. However this copy is (on purpose) *not convertible* to ``t`` in the Rocq system [#8]_. The job is done by the following construction: -.. coqdoc:: +.. rocqdoc:: Lemma master_key : unit. Proof. exact tt. Qed. Definition locked A := let: tt := master_key in fun x : A => x. @@ -3988,7 +3988,7 @@ selective rewriting, blocking on the fly the reduction in the term ``t``. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect ssrfun ssrbool. From Corelib Require Import ListDef. @@ -3997,7 +3997,7 @@ selective rewriting, blocking on the fly the reduction in the term ``t``. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Variable A : Type. Fixpoint has (p : A -> bool) (l : list A) : bool := @@ -4012,7 +4012,7 @@ definition. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4020,7 +4020,7 @@ definition. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Definition lid := locked (fun x : nat => x). @@ -4040,14 +4040,14 @@ some functions by the partial evaluation switch ``/=``, unless this allowed the evaluation of a condition. This is possible thanks to another mechanism of term tagging, resting on the following *Notation*: -.. coqdoc:: +.. rocqdoc:: Notation "'nosimpl' t" := (let: tt := tt in t). The term ``(nosimpl t)`` simplifies to ``t`` *except* in a definition. More precisely, given: -.. coqdoc:: +.. rocqdoc:: Definition foo := (nosimpl bar). @@ -4063,7 +4063,7 @@ Note that ``nosimpl bar`` is simply notation for a term that reduces to The ``nosimpl`` trick only works if no reduction is apparent in ``t``; in particular, the declaration: - .. coqdoc:: + .. rocqdoc:: Definition foo x := nosimpl (bar x). @@ -4071,14 +4071,14 @@ Note that ``nosimpl bar`` is simply notation for a term that reduces to function, and to use the following definition, which blocks the reduction as expected: - .. coqdoc:: + .. rocqdoc:: Definition foo x := nosimpl bar x. A standard example making this technique shine is the case of arithmetic operations. We define for instance: -.. coqdoc:: +.. rocqdoc:: Definition addn := nosimpl plus. @@ -4098,7 +4098,7 @@ Congruence Because of the way matching interferes with parameters of type families, the tactic: -.. coqdoc:: +.. rocqdoc:: apply: my_congr_property. @@ -4125,7 +4125,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4133,7 +4133,7 @@ which the function is supplied: Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Lemma test (x y z : nat) (H : x = y) : x = z. congr (_ = _) : H. @@ -4152,7 +4152,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4160,7 +4160,7 @@ which the function is supplied: Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Definition f n := if n is 0 then plus else mult. @@ -4175,7 +4175,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4183,7 +4183,7 @@ which the function is supplied: Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Lemma test n m (Hnm : m <= n) : S m + (S n - S m) = S n. congr S; rewrite -/plus. @@ -4196,7 +4196,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4204,7 +4204,7 @@ which the function is supplied: Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Lemma test x y : x + (y * (y + x - x)) = x * 1 + (y + 0) * y. congr ( _ + (_ * _)). @@ -4297,7 +4297,7 @@ For a quick glance at what can be expressed with the last :token:`r_pattern`, consider the goal ``a = b`` and the tactic -.. coqdoc:: +.. rocqdoc:: rewrite [in X in _ = X]rule. @@ -4376,7 +4376,7 @@ parentheses are required around more complex patterns. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4384,7 +4384,7 @@ parentheses are required around more complex patterns. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Lemma test a b : a + b + 1 = b + (a + 1). set t := (X in _ = X). @@ -4398,14 +4398,14 @@ patterns over simple terms, but to interpret a pattern with double parentheses as a simple term. For example, the following tactic would capture any occurrence of the term ``a in A``. -.. coqdoc:: +.. rocqdoc:: set t := ((a in A)). Contextual patterns can also be used as arguments of the ``:`` tactical. For example: -.. coqdoc:: +.. rocqdoc:: elim: n (n in _ = n) (refl_equal n). @@ -4415,7 +4415,7 @@ Contextual patterns in rewrite .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4423,7 +4423,7 @@ Contextual patterns in rewrite Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Notation "n .+1" := (Datatypes.S n) (at level 2, left associativity, format "n .+1") : nat_scope. @@ -4439,7 +4439,7 @@ Contextual patterns in rewrite symbol. Then, we simplify also the first addition and expand ``0`` into ``0 + 0``. - .. coqtop:: all + .. rocqtop:: all rewrite addSn -[X in _ = X]addn0. @@ -4452,13 +4452,13 @@ Contextual patterns in rewrite entire region; hence the rewrite rule has to be instantiated explicitly. Thus the tactic: - .. coqtop:: all + .. rocqtop:: all rewrite -{2}[in X in _ = X](addn0 0). The following tactic is quite tricky: - .. coqtop:: all + .. rocqtop:: all rewrite [_.+1 in X in f _ X](addnC x.+1). @@ -4478,7 +4478,7 @@ Contextual patterns in rewrite term identified by X, which is thus unified with the left-hand side of the rewrite rule. - .. coqtop:: all + .. rocqtop:: all rewrite [x.+1 + y as X in f X _]addnC. @@ -4496,7 +4496,7 @@ context shortcuts. The following example is taken from ``ssreflect.v``, where the ``LHS`` and ``RHS`` shortcuts are defined. -.. coqdoc:: +.. rocqdoc:: Notation RHS := (X in _ = X)%pattern. Notation LHS := (X in X = _)%pattern. @@ -4504,7 +4504,7 @@ The following example is taken from ``ssreflect.v``, where the Shortcuts defined this way can be freely used in place of the trailing ``ident in term`` part of any contextual pattern. Some examples follow: -.. coqdoc:: +.. rocqdoc:: set rhs := RHS. rewrite [in RHS]rule. @@ -4537,13 +4537,13 @@ The view syntax combined with the ``elim`` tactic specifies an elimination scheme to be used instead of the default, generated, one. Hence, the |SSR| tactic: -.. coqdoc:: +.. rocqdoc:: elim/V. is a synonym for: -.. coqdoc:: +.. rocqdoc:: intro top; elim top using V; clear top. @@ -4553,13 +4553,13 @@ Since an elimination view supports the two bookkeeping tacticals of discharge and introduction (see Section :ref:`basic_tactics_ssr`), the |SSR| tactic: -.. coqdoc:: +.. rocqdoc:: elim/V: x => y. is a synonym for: -.. coqdoc:: +.. rocqdoc:: elim x using V; clear x; intro y. @@ -4579,7 +4579,7 @@ generation (see Section :ref:`generation_of_equations_ssr`). The following script illustrates a toy example of this feature. Let us define a function adding an element at the end of a list: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect ListDef. Set Implicit Arguments. @@ -4587,7 +4587,7 @@ generation (see Section :ref:`generation_of_equations_ssr`). Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Variable d : Type. Fixpoint add_last (s : list d) (z : d) {struct s} : list d := @@ -4596,7 +4596,7 @@ generation (see Section :ref:`generation_of_equations_ssr`). One can define an alternative, reversed, induction principle on inductively defined lists, by proving the following lemma: - .. coqtop:: all + .. rocqtop:: all Axiom last_ind_list : forall P : list d -> Prop, P nil -> (forall s (x : d), P s -> P (add_last s x)) -> @@ -4606,7 +4606,7 @@ generation (see Section :ref:`generation_of_equations_ssr`). in a concise syntax for reasoning inductively using the user-defined elimination scheme. - .. coqtop:: all + .. rocqtop:: all Lemma test (x : d) (l : list d): l = l. elim/last_ind_list E : l=> [| u v]; last first. @@ -4617,13 +4617,13 @@ command) can be combined with the type family switches described in Section :ref:`type_families_ssr`. Consider an eliminator ``foo_ind`` of type: -.. coqdoc:: +.. rocqdoc:: foo_ind : forall …, forall x : T, P p1 … pm. and consider the tactic: -.. coqdoc:: +.. rocqdoc:: elim/foo_ind: e1 … / en. @@ -4654,7 +4654,7 @@ Here is an example of a regular, but nontrivial, eliminator. Here is a toy example illustrating this feature. - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4672,7 +4672,7 @@ Here is an example of a regular, but nontrivial, eliminator. Section Test. - .. coqtop:: all + .. rocqtop:: all Fixpoint plus (m n : nat) {struct n} : nat := if n is S p then S (plus m p) else m. @@ -4684,14 +4684,14 @@ Here is an example of a regular, but nontrivial, eliminator. The following tactics are all valid and perform the same elimination on this goal. - .. coqdoc:: + .. rocqdoc:: elim/plus_ind: z / (plus _ z). elim/plus_ind: {z}(plus _ z). elim/plus_ind: {z}_. elim/plus_ind: z / _. - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4712,7 +4712,7 @@ Here is an example of a regular, but nontrivial, eliminator. Lemma test x y z : plus (plus x y) z = plus x (plus y z). - .. coqtop:: all + .. rocqtop:: all elim/plus_ind: z / _. @@ -4722,7 +4722,7 @@ Here is an example of a regular, but nontrivial, eliminator. ``plus (plus x y) z``, thus instantiating the last ``_`` with ``z``. Note that the tactic: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4743,7 +4743,7 @@ Here is an example of a regular, but nontrivial, eliminator. Lemma test x y z : plus (plus x y) z = plus x (plus y z). - .. coqtop:: all + .. rocqtop:: all Fail elim/plus_ind: y / _. @@ -4758,7 +4758,7 @@ Here is an example of a truncated eliminator: Consider the goal: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4766,7 +4766,7 @@ Here is an example of a truncated eliminator: Unset Printing Implicit Defensive. Section Test. - .. coqdoc:: + .. rocqdoc:: Lemma test p n (n_gt0 : 0 < n) (pr_p : prime p) : p %| \prod_(i <- prime_decomp n | i \in prime_decomp n) i.1 ^ i.2 -> @@ -4777,7 +4777,7 @@ Here is an example of a truncated eliminator: where the type of the ``big_prop`` eliminator is - .. coqdoc:: + .. rocqdoc:: big_prop: forall (R : Type) (Pb : R -> Type) (idx : R) (op1 : R -> R -> R), Pb idx -> @@ -4790,7 +4790,7 @@ Here is an example of a truncated eliminator: inferred one, ``big[_/_]_(i <- _ | _ i) _ i``, is used instead, and after the introductions, the following goals are generated: - .. coqdoc:: + .. rocqdoc:: subgoal 1 is: p %| 1 -> exists2 x : nat * nat, x \in prime_decomp n & p = x.1 @@ -4822,7 +4822,7 @@ disjunction. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4830,7 +4830,7 @@ disjunction. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Variables P Q : bool -> Prop. Hypothesis P2Q : forall a b, P (a || b) -> Q a. @@ -4843,7 +4843,7 @@ disjunction. This operation is so common that the tactic shell has specific syntax for it. The following scripts: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4856,13 +4856,13 @@ disjunction. Lemma test a : P (a || a) -> True. - .. coqtop:: all + .. rocqtop:: all move=> HPa; move/P2Q: HPa => HQa. or more directly: - .. coqtop:: all restart + .. rocqtop:: all restart move/P2Q=> HQa. @@ -4878,7 +4878,7 @@ equation-name generation mechanism (see Section :ref:`generation_of_equations_ss .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4886,7 +4886,7 @@ equation-name generation mechanism (see Section :ref:`generation_of_equations_ss Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Variables P Q: bool -> Prop. Hypothesis Q2P : forall a b, Q (a || b) -> P a \/ P b. @@ -4896,7 +4896,7 @@ equation-name generation mechanism (see Section :ref:`generation_of_equations_ss This view tactic performs: - .. coqdoc:: + .. rocqdoc:: move=> HQ; case: {HQ}(Q2P HQ) => [HPa | HPb]. @@ -4911,7 +4911,7 @@ relevant for the current goal. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4919,7 +4919,7 @@ relevant for the current goal. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Variables P Q: bool -> Prop. Hypothesis PQequiv : forall a b, P (a || b) <-> Q a. @@ -4933,14 +4933,14 @@ relevant for the current goal. the double implication into the expected simple implication. The last script is in fact equivalent to: - .. coqdoc:: + .. rocqdoc:: Lemma test a b : P (a || b) -> True. move/(iffLR (PQequiv _ _)). where: - .. coqdoc:: + .. rocqdoc:: Lemma iffLR P Q : (P <-> Q) -> P -> Q. @@ -4955,7 +4955,7 @@ assumption to some given arguments. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -4963,7 +4963,7 @@ assumption to some given arguments. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Lemma test z : (forall x y, x + y = z -> z = x) -> z = 0. move/(_ 0 z). @@ -4984,7 +4984,7 @@ bookkeeping steps. The following example use the ``~~`` prenex notation for boolean negation: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4992,7 +4992,7 @@ bookkeeping steps. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Variables P Q: bool -> Prop. Hypothesis PQequiv : forall a b, P (a || b) <-> Q a. @@ -5040,7 +5040,7 @@ analysis: .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect. Set Implicit Arguments. @@ -5048,7 +5048,7 @@ analysis: Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Definition orb (b1 b2 : bool) := if b1 then true else b2. @@ -5057,7 +5057,7 @@ analysis .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5065,7 +5065,7 @@ analysis Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Lemma test b : b || ~~ b = true. by case: b. @@ -5082,7 +5082,7 @@ decidable predicate to its boolean version. First, booleans are injected into propositions using the coercion mechanism: -.. coqdoc:: +.. rocqdoc:: Coercion is_true (b : bool) := b = true. @@ -5099,7 +5099,7 @@ To get all the benefits of the boolean reflection, it is in fact convenient to introduce the following inductive predicate ``reflect`` to relate propositions and booleans: -.. coqdoc:: +.. rocqdoc:: Inductive reflect (P: Prop): bool -> Type := | Reflect_true : P -> reflect P true @@ -5110,7 +5110,7 @@ logically equivalent propositions. For instance, the following lemma: -.. coqdoc:: +.. rocqdoc:: Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2). @@ -5125,20 +5125,20 @@ to the case analysis of Rocq's inductive types. Since the equivalence predicate is defined in Rocq as: -.. coqdoc:: +.. rocqdoc:: Definition iff (A B:Prop) := (A -> B) /\ (B -> A). where ``/\`` is a notation for ``and``: -.. coqdoc:: +.. rocqdoc:: Inductive and (A B:Prop) : Prop := conj : A -> B -> and A B. This makes case analysis very different according to the way an equivalence property has been defined. -.. coqdoc:: +.. rocqdoc:: Lemma andE (b1 b2 : bool) : (b1 /\ b2) <-> (b1 && b2). @@ -5147,7 +5147,7 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5156,19 +5156,19 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. Section Test. Axiom andE : forall (b1 b2 : bool), (b1 /\ b2) <-> (b1 && b2). - .. coqtop:: all + .. rocqtop:: all Lemma test (b1 b2 : bool) : if (b1 && b2) then b1 else ~~(b1||b2). - .. coqtop:: all + .. rocqtop:: all case: (@andE b1 b2). - .. coqtop:: none + .. rocqtop:: none Restart. - .. coqtop:: all + .. rocqtop:: all case: (@andP b1 b2). @@ -5188,7 +5188,7 @@ The view mechanism is compatible with reflect predicates. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5196,14 +5196,14 @@ The view mechanism is compatible with reflect predicates. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all abort + .. rocqtop:: all abort Lemma test (a b : bool) (Ha : a) (Hb : b) : a /\ b. apply/andP. Conversely - .. coqtop:: all + .. rocqtop:: all Lemma test (a b : bool) : a /\ b -> a. move/andP. @@ -5222,13 +5222,13 @@ Specializing assumptions The |SSR| tactic: -.. coqdoc:: +.. rocqdoc:: move/(_ term1 … termn). is equivalent to the tactic: -.. coqdoc:: +.. rocqdoc:: intro top; generalize (top term1 … termn); clear top. @@ -5285,13 +5285,13 @@ If ``term`` is a double implication, then the view hint will be one of the defined view hints for implication. These hints are by default the ones present in the file ``ssreflect.v``: -.. coqdoc:: +.. rocqdoc:: Lemma iffLR : forall P Q, (P <-> Q) -> P -> Q. which transforms a double implication into the left-to-right one, or: -.. coqdoc:: +.. rocqdoc:: Lemma iffRL : forall P Q, (P <-> Q) -> Q -> P. @@ -5306,7 +5306,7 @@ but they also allow complex transformation, involving negations. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5314,11 +5314,11 @@ but they also allow complex transformation, involving negations. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Check introN. - .. coqtop:: all + .. rocqtop:: all Lemma test (a b : bool) (Ha : a) (Hb : b) : ~~ (a && b). apply/andP. @@ -5326,7 +5326,7 @@ but they also allow complex transformation, involving negations. In fact, this last script does not exactly use the hint ``introN``, but the more general hint: - .. coqtop:: all + .. rocqtop:: all Check introNTF. @@ -5339,7 +5339,7 @@ actually uses its propositional interpretation. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5347,7 +5347,7 @@ actually uses its propositional interpretation. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Lemma test (a b : bool) (pab : b && a) : b. have /andP [pa ->] : (a && b) by rewrite andbC. @@ -5396,13 +5396,13 @@ equality, while the second term is the one applied to the right-hand side. In this context, the identity view can be used when no view has to be applied: -.. coqdoc:: +.. rocqdoc:: Lemma idP : reflect b1 b1. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5410,7 +5410,7 @@ In this context, the identity view can be used when no view has to be applied: Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Lemma test (b1 b2 b3 : bool) : ~~ (b1 || b2) = b3. apply/idP/idP. @@ -5418,7 +5418,7 @@ In this context, the identity view can be used when no view has to be applied: The same goal can be decomposed in several ways, and the user may choose the most convenient interpretation. - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5426,7 +5426,7 @@ In this context, the identity view can be used when no view has to be applied: Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. rocqtop:: all Lemma test (b1 b2 b3 : bool) : ~~ (b1 || b2) = b3. apply/norP/idP. @@ -5471,7 +5471,7 @@ in sequence. Both ``move`` and ``apply`` can be followed by an arbitrary number of ``/term``. The main difference between the following two tactics -.. coqdoc:: +.. rocqdoc:: apply/v1/v2/v3. apply/v1; apply/v2; apply/v3. @@ -5483,7 +5483,7 @@ line would apply the view ``v2`` to all the goals generated by ``apply/v1``. Note that the NO-OP intro pattern ``-`` can be used to separate two views, making the two following examples equivalent: -.. coqdoc:: +.. rocqdoc:: move=> /v1; move=> /v2. move=> /v1 - /v2. @@ -5494,7 +5494,7 @@ pass a given hypothesis to a lemma. .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none From Corelib Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5503,7 +5503,7 @@ pass a given hypothesis to a lemma. Section Test. Variables P Q R : Prop. - .. coqtop:: all + .. rocqtop:: all Variable P2Q : P -> Q. Variable Q2R : Q -> R. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index afc538cc5a31..2a7cd8f99e31 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -301,7 +301,7 @@ These patterns can be used when the hypothesis is an equality: These are defined in ``theories/Init/Logic.v``. The "where" clauses define the infix notation for "or" and "and". - .. coqdoc:: + .. rocqdoc:: Inductive or (A B:Prop) : Prop := | or_introl : A -> A \/ B @@ -327,15 +327,15 @@ Examples: .. example:: intro pattern for /\\ - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall (A: Prop) (B: Prop), (A /\ B) -> True. - .. coqtop:: out + .. rocqtop:: out intros. - .. coqtop:: all + .. rocqtop:: all destruct H as (HA & HB). @@ -343,15 +343,15 @@ Examples: .. example:: intro pattern for \\/ - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall (A: Prop) (B: Prop), (A \/ B) -> True. - .. coqtop:: out + .. rocqtop:: out intros. - .. coqtop:: all + .. rocqtop:: all destruct H as [HA|HB]. all: swap 1 2. @@ -359,15 +359,15 @@ Examples: .. example:: -> intro pattern - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall (x:nat) (y:nat) (z:nat), (x = y) -> (y = z) -> (x = z). - .. coqtop:: out + .. rocqtop:: out intros * H. - .. coqtop:: all + .. rocqtop:: all intros ->. @@ -380,19 +380,19 @@ Examples: the contradiction :n:`1 = 2` (internally represented as :n:`(S O) = (S (S O))`) to complete the goal. - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall (n m:nat), (S n) = (S m) -> (S O)=(S (S O)) -> False. - .. coqtop:: out + .. rocqtop:: out intros *. - .. coqtop:: all + .. rocqtop:: all intros [= H]. - .. coqtop:: all + .. rocqtop:: all intros [=]. @@ -400,15 +400,15 @@ Examples: .. example:: (A & B & …) intro pattern - .. coqtop:: reset none + .. rocqtop:: reset none Parameters (A : Prop) (B: nat -> Prop) (C: Prop). - .. coqtop:: out + .. rocqtop:: out Goal A /\ (exists x:nat, B x /\ C) -> True. - .. coqtop:: all + .. rocqtop:: all intros (a & x & b & c). @@ -416,11 +416,11 @@ Examples: .. example:: * intro pattern - .. coqtop:: reset out + .. rocqtop:: reset out Goal forall (A: Prop) (B: Prop), A -> B. - .. coqtop:: all + .. rocqtop:: all intros *. @@ -428,21 +428,21 @@ Examples: .. example:: ** pattern ("intros \**" is equivalent to "intros") - .. coqtop:: reset out + .. rocqtop:: reset out Goal forall (A: Prop) (B: Prop), A -> B. - .. coqtop:: all + .. rocqtop:: all intros **. .. example:: compound intro pattern - .. coqtop:: reset out + .. rocqtop:: reset out Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. - .. coqtop:: all + .. rocqtop:: all intros * [a | (_,c)] f. all: swap 1 2. @@ -451,7 +451,7 @@ Examples: .. example:: combined intro pattern using [=] -> and % - .. coqtop:: reset none + .. rocqtop:: reset none Require Import ListDef. Section IntroPatterns. @@ -459,12 +459,12 @@ Examples: Axiom length_zero_iff_nil : forall [A] (l : list A), length l = 0 <-> l = nil. - .. coqtop:: out + .. rocqtop:: out Example ThreeIntroPatternsCombined : S (length ys) = 1 -> xs ++ ys = xs. - .. coqtop:: all + .. rocqtop:: all intros [=->%length_zero_iff_nil]. @@ -473,7 +473,7 @@ Examples: * `intros [=->%length_zero_iff_nil]` applies the theorem, making H the equality :g:`l=nil`, which is then applied as for :g:`->`. - .. coqdoc:: + .. rocqdoc:: Theorem length_zero_iff_nil (l : list A): length l = 0 <-> l=nil. @@ -652,7 +652,7 @@ Applying theorems .. example:: - .. coqtop:: reset all + .. rocqtop:: reset all Inductive Option : Set := | Fail : Option @@ -819,45 +819,45 @@ Applying theorems .. _apply_backward: .. example:: Backward reasoning in the goal with `apply` - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall A B C: Prop, (A -> B -> C) -> C. - .. coqtop:: out + .. rocqtop:: out intros A B C H. - .. coqtop:: all + .. rocqtop:: all apply H. (* replace goal with new goals for unmatched premises of H *) .. _apply_backward_w_premises: .. example:: Backward reasoning in the goal with `apply` including a premise - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall A B C: Prop, (A -> B -> C) -> (B -> C). - .. coqtop:: out + .. rocqtop:: out intros A B C H. - .. coqtop:: all + .. rocqtop:: all apply H. (* match on "B -> C", replace goal with "A" *) .. _apply_forward: .. example:: Forward reasoning in hypotheses with `apply` - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall A B C: Prop, B -> (A -> B -> C) -> True. - .. coqtop:: out + .. rocqtop:: out intros A B C H0 H1. - .. coqtop:: all + .. rocqtop:: all apply H1 in H0. (* change H0, create new goals for unmatched premises of H1 *) @@ -870,17 +870,17 @@ Applying theorems to, repectively, `n` and `p` in theorem (backward reasoning). The `with` clause provides the binding for `m`: - .. coqtop:: reset none + .. rocqtop:: reset none Axiom le_trans : forall n m p, n <= m -> m <= p -> n <= p. Goal forall (x y : nat), x <= y -> x * x <= y * y. - .. coqtop:: out + .. rocqtop:: out intros x y H0. - .. coqtop:: all + .. rocqtop:: all apply le_trans with (y * x). @@ -900,17 +900,17 @@ Applying theorems by name (as shown) or values for all the variables can be given positionally, i.e. `apply Nat.le_trans with (x * x) (y * y) (y * x) in H.` - .. coqtop:: reset none + .. rocqtop:: reset none Axiom le_trans : forall n m p, n <= m -> m <= p -> n <= p. Goal forall (x y : nat), x * x <= y * y -> x <= y. - .. coqtop:: out + .. rocqtop:: out intros x y H. - .. coqtop:: all + .. rocqtop:: all apply le_trans with (p := y * x) in H. @@ -928,15 +928,15 @@ Applying theorems Theorems that use :n:`<->` to state a logical equivalence behave consistently when applied to goals and hypotheses. - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall (A B: Prop) (H1: A <-> B) (H: A), A. - .. coqtop:: out + .. rocqtop:: out intros A B H1 H. - .. coqtop:: all + .. rocqtop:: all apply H1. apply H1 in H. @@ -949,15 +949,15 @@ Applying theorems Note that we usually use :tacn:`induction` rather than applying ``nat_ind`` directly. - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall x y, x + y = y + x. - .. coqtop:: out + .. rocqtop:: out intros. - .. coqtop:: all + .. rocqtop:: all Check nat_ind. @@ -1003,7 +1003,7 @@ Applying theorems .. _simple_apply_ex: .. example:: - .. coqtop:: reset all + .. rocqtop:: reset all Definition id (x : nat) := x. Parameter H : forall x y, id x = y. @@ -1031,7 +1031,7 @@ Applying theorems Assume we have a transitive relation ``R`` on ``nat``: - .. coqtop:: reset in + .. rocqtop:: reset in Parameter R : nat -> nat -> Prop. Axiom Rtrans : forall x y z:nat, R x y -> R y z -> R x z. @@ -1041,46 +1041,46 @@ Applying theorems Consider the goal ``(R n p)`` provable using the transitivity of ``R``: - .. coqtop:: in + .. rocqtop:: in Goal R n p. The direct application of ``Rtrans`` with ``apply`` fails because no value for ``y`` in ``Rtrans`` is found by ``apply``: - .. coqtop:: all fail + .. rocqtop:: all fail apply Rtrans. A solution is to ``apply (Rtrans n m p)`` or ``(Rtrans n m)``. - .. coqtop:: all + .. rocqtop:: all apply (Rtrans n m p). Note that ``n`` can be inferred from the goal, so the following would work too. - .. coqtop:: in restart + .. rocqtop:: in restart apply (Rtrans _ m). More elegantly, ``apply Rtrans with (y:=m)`` allows only mentioning the unknown m: - .. coqtop:: in restart + .. rocqtop:: in restart apply Rtrans with (y := m). Another solution is to mention the proof of ``(R x y)`` in ``Rtrans`` - .. coqtop:: all restart + .. rocqtop:: all restart apply Rtrans with (1 := Rnm). … or the proof of ``(R y z)``. - .. coqtop:: all restart + .. rocqtop:: all restart apply Rtrans with (2 := Rmp). @@ -1088,7 +1088,7 @@ Applying theorems finding ``m``. Then one can apply the hypotheses ``Rnm`` and ``Rmp``. This instantiates the existential variable and completes the proof. - .. coqtop:: all restart abort + .. rocqtop:: all restart abort eapply Rtrans. @@ -1166,11 +1166,11 @@ Managing the local context .. _intro_examples: .. example:: `intro` and `intros` - .. coqtop:: reset out + .. rocqtop:: reset out Goal forall m n, m < n -> (let x := 0 in True). - .. coqtop:: all + .. rocqtop:: all intro m. intro n. @@ -1179,11 +1179,11 @@ Managing the local context This single `intros` tactic is equivalent to the 4 preceding `intro` tactics: - .. coqtop:: reset out + .. rocqtop:: reset out Goal forall m n, m < n -> (let x := 0 in True). - .. coqtop:: all + .. rocqtop:: all intros m n H x. @@ -1213,21 +1213,21 @@ Managing the local context .. example:: intros until - .. coqtop:: reset out + .. rocqtop:: reset out Goal forall x y : nat, x = y -> y = x. - .. coqtop:: all + .. rocqtop:: all intros until y. Or: - .. coqtop:: reset out + .. rocqtop:: reset out Goal forall x y : nat, x = y -> y = x. - .. coqtop:: all + .. rocqtop:: all intros until 1. @@ -1340,15 +1340,15 @@ Managing the local context .. example:: move - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall x :nat, x = 0 -> forall y z:nat, y=y-> 0=x. - .. coqtop:: out + .. rocqtop:: out intros x Hx y z Hy. - .. coqtop:: in + .. rocqtop:: in (* x Hx y z Hy *) move y after z. (* x Hx z y Hy (z was left of y, intuitive case) *) @@ -1404,15 +1404,15 @@ Managing the local context :n:`set` does a simple syntactic replacement in the goal: - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall n, n = 0. - .. coqtop:: out + .. rocqtop:: out intros. - .. coqtop:: all + .. rocqtop:: all pattern n. (* without this, "set" won't replace anything in the goal *) set (f x := x = 0). @@ -1606,15 +1606,15 @@ Controlling the proof flow .. example:: partial application in :tacn:`specialize` - .. coqtop:: reset none + .. rocqtop:: reset none Goal (forall n m: nat, n + m = m + n) -> True. - .. coqtop:: out + .. rocqtop:: out intros. - .. coqtop:: all + .. rocqtop:: all specialize (H 1). (* equivalent to: specialize H with (n := 1) *) @@ -1624,16 +1624,16 @@ Controlling the proof flow :tacn:`apply`. :tacn:`specialize` won't introduce new goals as :tacn:`apply` can. - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall A B C: Prop, B -> (A -> B -> C) -> True. Proof. - .. coqtop:: out + .. rocqtop:: out intros A B C H0 H1. - .. coqtop:: all + .. rocqtop:: all specialize H1 with (2:=H0). @@ -1657,16 +1657,16 @@ Controlling the proof flow .. example:: - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall x y:nat, 0 <= x + y + y. Proof. intros *. - .. coqtop:: out + .. rocqtop:: out Show. - .. coqtop:: all abort + .. rocqtop:: all abort generalize (x + y + y). (* get a simpler goal that can be proven by induction *) @@ -1732,7 +1732,7 @@ Controlling the proof flow Advanced users may want to define and use an Ltac tactic to get more consistent behavior, such as: - .. coqdoc:: + .. rocqdoc:: Ltac instantiate_ltac_variable ev term := let H := fresh in @@ -1798,7 +1798,7 @@ Controlling the proof flow Simple examples. To see more detail, add `intros` after each `Goal`. - .. coqtop:: reset in + .. rocqtop:: reset in Inductive F :=. (* Another empty inductive type *) @@ -1816,15 +1816,15 @@ Controlling the proof flow Apply a fact from the standard library: - .. coqtop:: none + .. rocqtop:: none Axiom lt_irrefl : forall x, ~ (x < x). - .. coqtop:: in + .. rocqtop:: in Goal forall (A : Prop), 0 < 0 -> A. - .. coqtop:: all + .. rocqtop:: all intros. contradiction (lt_irrefl 0). @@ -1880,7 +1880,7 @@ Performance-oriented tactic variants .. example:: - .. coqtop:: all abort + .. rocqtop:: all abort Goal False. exact_no_check I. @@ -1894,7 +1894,7 @@ Performance-oriented tactic variants .. example:: - .. coqtop:: all abort + .. rocqtop:: all abort Goal False. vm_cast_no_check I. @@ -1908,7 +1908,7 @@ Performance-oriented tactic variants .. example:: - .. coqtop:: all abort + .. rocqtop:: all abort Goal False. native_cast_no_check I. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 6de1b98ad45f..efe4094cf911 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -219,7 +219,7 @@ described elsewhere .. example:: Searching for a pattern - .. coqtop:: none reset extra + .. rocqtop:: none reset extra From Stdlib Require Import PeanoNat. @@ -227,7 +227,7 @@ described elsewhere we are looking for commutativity lemmas. The following example requires the Stdlib library. - .. coqtop:: all + .. rocqtop:: all Search (_ ?n ?m = _ ?m ?n). @@ -235,7 +235,7 @@ described elsewhere .. example:: Searching for part of an identifier - .. coqtop:: all reset + .. rocqtop:: all reset Search "_assoc". @@ -243,7 +243,7 @@ described elsewhere .. example:: Searching for a reference by notation - .. coqtop:: all reset + .. rocqtop:: all reset Search "+". @@ -253,7 +253,7 @@ described elsewhere The following example requires the Stdlib library. - .. coqtop:: none reset extra + .. rocqtop:: none reset extra From Stdlib Require Import PeanoNat. @@ -261,7 +261,7 @@ described elsewhere objects whose type contains `Nat.modulo` but which do not contain the substring "mod". - .. coqtop:: all extra + .. rocqtop:: all extra Search "'mod'" -"mod". Search "mod"%nat -"mod". @@ -273,11 +273,11 @@ described elsewhere The following search shows the objects whose type contains `bool` in an hypothesis as a strict subterm only: - .. coqtop:: none reset + .. rocqtop:: none reset Add Search Blacklist "internal_". - .. coqtop:: all + .. rocqtop:: all Search hyp:bool -headhyp:bool. @@ -288,7 +288,7 @@ described elsewhere The following search shows the objects whose type contains `bool` in the conclusion as a strict subterm only: - .. coqtop:: all + .. rocqtop:: all Search concl:bool -headconcl:bool. @@ -299,25 +299,25 @@ described elsewhere The following search shows the definitions whose type is a `nat` or a function which returns a `nat` and the lemmas about `+`: - .. coqtop:: all reset + .. rocqtop:: all reset Search [ is:Definition headconcl:nat | is:Lemma (_ + _) ]. The following search shows the instances whose type includes the classes `Reflexive` or `Symmetric`: - .. coqtop:: none reset + .. rocqtop:: none reset Require Import Morphisms. - .. coqtop:: all + .. rocqtop:: all Search is:Instance [ Reflexive | Symmetric ]. The following search outputs operations on `nat` defined in the prelude either with the `Definition` or `Fixpoint` keyword: - .. coqtop:: all reset + .. rocqtop:: all reset Search (nat -> nat -> nat) -bool [ is:Definition | is:Fixpoint ]. @@ -334,17 +334,17 @@ described elsewhere The following example requires the Stdlib library. - .. coqtop:: in reset extra + .. rocqtop:: in reset extra From Stdlib Require Import Arith. - .. coqtop:: all extra + .. rocqtop:: all extra SearchPattern (_ + _ = _ + _). SearchPattern (nat -> bool). SearchPattern (forall l : list _, _ l l). - .. coqtop:: all extra + .. rocqtop:: all extra SearchPattern (?X1 + _ = _ + ?X1). @@ -361,11 +361,11 @@ described elsewhere The following example requires the Stdlib library. - .. coqtop:: in reset extra + .. rocqtop:: in reset extra From Stdlib Require Import Arith. - .. coqtop:: all extra + .. rocqtop:: all extra SearchRewrite (_ + _ + _). @@ -477,7 +477,7 @@ Requests to the environment .. example:: Locate examples - .. coqtop:: all + .. rocqtop:: all Locate nat. Locate Datatypes.O. @@ -1119,7 +1119,7 @@ Controlling Typing Flags .. example:: - .. coqtop:: all reset + .. rocqtop:: all reset Unset Guard Checking. @@ -1143,7 +1143,7 @@ Controlling Typing Flags Note that the proper way to define the Ackermann function is to use an inner fixpoint: - .. coqtop:: all reset + .. rocqtop:: all reset Fixpoint ack m := fix ackm n := @@ -1187,7 +1187,7 @@ Exposing constants to OCaml libraries This command supports attributes :attr:`local`, :attr:`export` and :attr:`global`. The default is :attr:`global`, even inside sections. - .. coqdoc:: + .. rocqdoc:: Register bool as kernel.ind_bool. diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index 19719b111704..17b39c29f473 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -113,7 +113,7 @@ Tactics .. example:: - .. coqtop:: all + .. rocqtop:: all Hint Resolve ex_intro : core. Goal forall P:nat -> Prop, P 0 -> exists n, P n. @@ -202,25 +202,25 @@ the optional tactic of the ``Hint Rewrite`` command. .. example:: Ackermann function - .. coqtop:: in reset + .. rocqtop:: in reset Parameter Ack : nat -> nat -> nat. - .. coqtop:: in + .. rocqtop:: in Axiom Ack0 : forall m:nat, Ack 0 m = S m. Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1. Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m). - .. coqtop:: in + .. rocqtop:: in Global Hint Rewrite Ack0 Ack1 Ack2 : base0. - .. coqtop:: all + .. rocqtop:: all Lemma ResAck0 : Ack 3 2 = 29. - .. coqtop:: all + .. rocqtop:: all autorewrite with base0 using try reflexivity. @@ -228,49 +228,49 @@ the optional tactic of the ``Hint Rewrite`` command. This example requires the Stdlib library. - .. coqtop:: in reset extra + .. rocqtop:: in reset extra From Stdlib Require Import Arith Lia. - .. coqtop:: in extra + .. rocqtop:: in extra Parameter g : nat -> nat -> nat. - .. coqtop:: in extra + .. rocqtop:: in extra 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 extra + .. rocqtop:: in extra Global Hint Rewrite g0 g1 g2 using lia : base1. - .. coqtop:: in extra + .. rocqtop:: in extra Lemma Resg0 : g 1 110 = 100. - .. coqtop:: out extra + .. rocqtop:: out extra Show. - .. coqtop:: all extra + .. rocqtop:: all extra autorewrite with base1 using reflexivity || simpl. - .. coqtop:: none extra + .. rocqtop:: none extra Qed. - .. coqtop:: all extra + .. rocqtop:: all extra Lemma Resg1 : g 1 95 = 91. - .. coqtop:: all extra + .. rocqtop:: all extra autorewrite with base1 using reflexivity || simpl. - .. coqtop:: none extra + .. rocqtop:: none extra Qed. @@ -526,7 +526,7 @@ Creating Hints .. example:: - .. coqtop:: in + .. rocqtop:: in Hint Extern 4 (~(_ = _)) => discriminate : core. @@ -540,7 +540,7 @@ Creating Hints .. example:: - .. coqtop:: reset all + .. rocqtop:: reset all Require Import ListDef. Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => @@ -638,13 +638,13 @@ Creating Hints This example illustrates the use of modes to control how resolutions can be triggered during proof search. - .. coqtop:: all reset + .. rocqtop:: all reset Parameter plus : nat -> nat -> nat -> Prop. Hint Mode plus ! - - : plus. Hint Mode plus - ! - : plus. - .. coqtop:: in + .. rocqtop:: in Axiom plus0l : forall m : nat, plus 0 m m. Axiom plus0r : forall n : nat, plus n 0 n. @@ -657,7 +657,7 @@ Creating Hints by a constructor or constant. The last argument of the predicate will be the inferred result. - .. coqtop:: all + .. rocqtop:: all Goal exists x y, plus x y 12. Proof. eexists ?[x], ?[y]. diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst index 17124eb5e13a..c33a0b096c7c 100644 --- a/doc/sphinx/proofs/automatic-tactics/logic.rst +++ b/doc/sphinx/proofs/automatic-tactics/logic.rst @@ -17,7 +17,7 @@ Solvers for logic and equality The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would fail: - .. coqtop:: reset all + .. rocqtop:: reset all Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x. intros. @@ -29,7 +29,7 @@ Solvers for logic and equality .. example:: - .. coqtop:: reset all + .. rocqtop:: reset all Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x. tauto. @@ -183,7 +183,7 @@ Solvers for logic and equality .. example:: - .. coqtop:: reset all + .. rocqtop:: 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. intros. diff --git a/doc/sphinx/proofs/writing-proofs/equality.rst b/doc/sphinx/proofs/writing-proofs/equality.rst index c8ecbc137fd1..007342e3d55d 100644 --- a/doc/sphinx/proofs/writing-proofs/equality.rst +++ b/doc/sphinx/proofs/writing-proofs/equality.rst @@ -10,7 +10,7 @@ There are multiple notions of :gdef:`equality` in Rocq: a `Prop`. The standard library defines `eq` similar to this: - .. coqdoc:: + .. rocqdoc:: Inductive eq {A : Type} (x : A) : A -> Prop := eq_refl : eq x x. @@ -187,24 +187,24 @@ Rewriting with Leibniz and setoid equality For instance, if we want to rewrite the right-hand side in the following goal, this will not work: - .. coqtop:: none + .. rocqtop:: none From Corelib Require Import Setoid. Axiom add_comm : forall n m, n + m = m + n. - .. coqtop:: out + .. rocqtop:: out Lemma example x y : x + y = y + x. - .. coqtop:: all fail + .. rocqtop:: all fail rewrite add_comm at 2. One can explicitly specify how some variables are bound to match a different subterm: - .. coqtop:: all abort + .. rocqtop:: all abort rewrite add_comm with (m := x). @@ -432,7 +432,7 @@ Rewriting with definitional equality .. example:: - .. coqtop:: all abort fail + .. rocqtop:: all abort fail Goal False. change_no_check True. @@ -441,7 +441,7 @@ Rewriting with definitional equality .. example:: - .. coqtop:: all abort fail + .. rocqtop:: all abort fail Goal True -> False. intro H. @@ -481,7 +481,7 @@ tactics change existential variables in a way similar to other conversions while also adding a single explicit cast to the proof term to tell the kernel which reduction engine to use. See :ref:`type-cast`.) For example: - .. coqtop:: all + .. rocqtop:: all Goal 3 + 4 = 7. Show Proof. @@ -490,7 +490,7 @@ which reduction engine to use. See :ref:`type-cast`.) For example: Show Proof. Show Existentials. - .. coqtop:: none + .. rocqtop:: none Abort. @@ -651,7 +651,7 @@ which reduction engine to use. See :ref:`type-cast`.) For example: Here are typical examples comparing :tacn:`cbn` and :tacn:`simpl`: - .. coqtop:: all + .. rocqtop:: all Definition add1 (n:nat) := n + 1. Eval simpl in add1 0. @@ -735,7 +735,7 @@ which reduction engine to use. See :ref:`type-cast`.) For example: .. example:: - .. coqtop:: abort all fail + .. rocqtop:: abort all fail Goal 0 <= 1. unfold le. @@ -747,7 +747,7 @@ which reduction engine to use. See :ref:`type-cast`.) For example: .. example:: - .. coqtop:: abort all fail + .. rocqtop:: abort all fail Opaque Nat.add. Goal 1 + 0 = 1. @@ -776,27 +776,27 @@ which reduction engine to use. See :ref:`type-cast`.) For example: .. example:: :tacn:`fold` doesn't always undo :tacn:`unfold` - .. coqtop:: all + .. rocqtop:: all Goal ~0=0. unfold not. This :tacn:`fold` doesn't undo the preceeding :tacn:`unfold` (it makes no change): - .. coqtop:: all + .. rocqtop:: all fold not. However, this :tacn:`pattern` followed by :tacn:`fold` does: - .. coqtop:: all abort + .. rocqtop:: all abort pattern (0 = 0). fold not. .. example:: Use :tacn:`fold` to reverse unfolding of `fold_right` - .. coqtop:: none + .. rocqtop:: none Require Import ListDef. Local Open Scope list_scope. @@ -807,7 +807,7 @@ which reduction engine to use. See :ref:`type-cast`.) For example: | b :: t => f b (fold_right t) end. - .. coqtop:: all abort + .. rocqtop:: all abort Goal forall x xs, fold_right and True (x::xs). red. @@ -1108,7 +1108,7 @@ which supports additional fine-tuning. .. example:: - .. coqtop:: all reset abort + .. rocqtop:: all reset abort Opaque id. Goal id 10 = 10. @@ -1130,7 +1130,7 @@ which supports additional fine-tuning. This can be illustrated with the following example involving the factorial function. - .. coqtop:: in reset + .. rocqtop:: in reset Fixpoint fact (n : nat) : nat := match n with @@ -1141,7 +1141,7 @@ which supports additional fine-tuning. Suppose now that, for whatever reason, we want in general to unfold the :g:`id` function very late during conversion: - .. coqtop:: in + .. rocqtop:: in Strategy 1000 [id]. @@ -1153,7 +1153,7 @@ which supports additional fine-tuning. :g:`nat`), which takes time :math:`n!`. We can see this cross the relevant threshold at around :math:`n = 9`: - .. coqtop:: all abort + .. rocqtop:: all abort Goal True. Time assert (id (fact 8) = fact 8) by reflexivity. @@ -1166,7 +1166,7 @@ which supports additional fine-tuning. We can get around this issue by using :tacn:`with_strategy`: - .. coqtop:: all + .. rocqtop:: all Goal True. Fail Timeout 1 assert (id (fact 100) = fact 100) by reflexivity. @@ -1176,14 +1176,14 @@ which supports additional fine-tuning. trouble, because the reduction strategy changes are local to the tactic passed to :tacn:`with_strategy`. - .. coqtop:: all abort fail + .. rocqtop:: all abort fail exact I. Timeout 1 Defined. We can fix this issue by using :tacn:`abstract`: - .. coqtop:: all + .. rocqtop:: all Goal True. Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] abstract reflexivity. diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst index 8a1eff03cc56..c1ec2be6710d 100644 --- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -57,11 +57,11 @@ When you begin proving a theorem, the proof state shows the statement of the theorem below the line and often nothing in the local context: -.. coqtop:: none +.. rocqtop:: none Parameter P: nat -> Prop. -.. coqtop:: out +.. rocqtop:: out Goal forall n m: nat, n > m -> P 1 /\ P 2. @@ -70,7 +70,7 @@ The names of variables (`n` and `m`) and hypotheses (`H`) appear before a colon, their type. The type doesn't have to be a provable statement. For example, `0 = 1` and `False` are both valid and useful types. -.. coqtop:: all +.. rocqtop:: all intros. @@ -79,7 +79,7 @@ be referred to as :gdef:`subgoals ` for clarity. Goals are numbered from 1 to N at each step of the proof to permit applying a tactic to specific goals. The local context is only shown for the first goal. -.. coqtop:: all +.. rocqtop:: all split. @@ -90,7 +90,7 @@ is `Set` or `Type`. :gdef:`"Hypotheses" ` refers to items that are for which the type of their type is `Prop` or `SProp`, but these terms are also used interchangeably. -.. coqtop:: out +.. rocqtop:: out let t_n := type of n in idtac "type of n :" t_n; let tt_n := type of t_n in idtac "type of" t_n ":" tt_n. @@ -111,7 +111,7 @@ The :cmd:`Show Proof` command displays the incomplete proof term before you've completed the proof. For example, here's the proof term after using the :tacn:`split` tactic above: -.. coqtop:: all +.. rocqtop:: all Show Proof. @@ -121,7 +121,7 @@ with names that begin with `?Goal`. (Note that some existential variables are not goals.) The :cmd:`Show Existentials` command shows each existential with the hypotheses and conclusion for the associated goal. -.. coqtop:: all +.. rocqtop:: all Show Existentials. @@ -145,7 +145,7 @@ After a proof is completed, :cmd:`Print` `` shows the proof term and its type. The type appears after the colon (`forall ...`), as for this theorem from Rocq's standard library: -.. coqtop:: all +.. rocqtop:: all Print proj1. @@ -351,7 +351,7 @@ When the proof is completed, you can exit proof mode with commands such as .. example:: - .. coqtop:: all reset + .. rocqtop:: all reset Section Test. Variable n : nat. @@ -360,7 +360,7 @@ When the proof is completed, you can exit proof mode with commands such as #[using="Hn"] Lemma example : 0 < n. - .. coqtop:: in + .. rocqtop:: in Abort. End Test. @@ -379,7 +379,7 @@ When the proof is completed, you can exit proof mode with commands such as Adding the unnecessary section variable `radixNotZero` changes how `foo'` can be applied. - .. coqtop :: in + .. rocqtop:: in Section bar. Variable radix : nat. @@ -391,7 +391,7 @@ When the proof is completed, you can exit proof mode with commands such as Lemma foo' : 0 = 0. Proof using radixNotZero. reflexivity. Qed. (* radixNotZero is not needed *) - .. coqtop :: all + .. rocqtop:: all Print foo'. (* Doesn't show radixNotZero yet *) End bar. @@ -399,15 +399,15 @@ When the proof is completed, you can exit proof mode with commands such as Print foo'. (* "End" added type radix (used by radixNotZero) and radixNotZero *) Goal 0 = 0. - .. coqtop :: in + .. rocqtop:: in Fail apply foo'. (* Fails because of the extra variable *) - .. coqtop :: all + .. rocqtop:: all apply (foo' 5). (* Can be used if the extra variable is provided explicitly *) - .. coqtop:: abort none + .. rocqtop:: abort none Proof using options ``````````````````` @@ -589,12 +589,12 @@ Curly braces .. example:: Working with named goals - .. coqtop:: in + .. rocqtop:: in Ltac name_goal name := refine ?[name]. (* for convenience *) Set Printing Goal Names. (* show goal names, e.g. "(?base)" and "(?step)" *) - .. coqtop:: all + .. rocqtop:: all Goal forall n, n + 0 = n. Proof. @@ -603,13 +603,13 @@ Curly braces [base]: { reflexivity. - .. coqtop:: in + .. rocqtop:: in } This can also be a way of focusing on a shelved goal, for instance: - .. coqtop:: all reset + .. rocqtop:: all reset Goal exists n : nat, n = n. eexists ?[x]. @@ -671,7 +671,7 @@ When a focused goal is proved, Rocq displays a message suggesting use of Note that the tactic following a bullet is frequently put on the same line with the bullet. Observe that this proof still works even if all the bullets in it are omitted. - .. coqtop:: in + .. rocqtop:: in Goal (1=1 /\ 2=2) /\ 3=3. Proof. @@ -766,7 +766,7 @@ tactic that unshelves goals by name. .. example:: shelve_unifiable - .. coqtop:: all abort + .. rocqtop:: all abort Goal exists n, n=0. refine (ex_intro _ _ _). @@ -807,11 +807,11 @@ Reordering goals .. example:: cycle - .. coqtop:: none reset + .. rocqtop:: none reset Parameter P : nat -> Prop. - .. coqtop:: in abort + .. rocqtop:: in abort Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. (* P 1, P 2, P 3, P 4, P 5 *) @@ -829,7 +829,7 @@ Reordering goals .. example:: swap - .. coqtop:: in abort + .. rocqtop:: in abort Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. (* P 1, P 2, P 3, P 4, P 5 *) @@ -844,7 +844,7 @@ Reordering goals .. example:: revgoals - .. coqtop:: in abort + .. rocqtop:: in abort Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. (* P 1, P 2, P 3, P 4, P 5 *) @@ -924,7 +924,7 @@ Requesting information .. example:: - .. coqtop:: all abort + .. rocqtop:: all abort Goal exists n, n = 0. eexists ?[n]. @@ -986,7 +986,7 @@ Requesting information .. example:: - .. coqtop:: all + .. rocqtop:: all Show Match nat. @@ -1141,33 +1141,33 @@ Notes: .. todo: Use this script and remove the screenshots when COQ_COLORS works for coqtop in sphinx - .. coqtop:: none + .. rocqtop:: none Set Diffs "on". Parameter P : nat -> Prop. Goal P 1 /\ P 2 /\ P 3. - .. coqtop:: out + .. rocqtop:: out split. - .. coqtop:: all abort + .. rocqtop:: all abort 2: split. .. - .. coqtop:: none + .. rocqtop:: none Set Diffs "on". Goal forall n m : nat, n + m = m + n. Set Diffs "on". - .. coqtop:: out + .. rocqtop:: out intros n. - .. coqtop:: all abort + .. rocqtop:: all abort intros m. diff --git a/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst b/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst index 9d97b205265f..44200b41f087 100644 --- a/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst +++ b/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst @@ -81,7 +81,7 @@ The tactics presented here specialize :tacn:`apply` and .. example:: :tacn:`constructor`, :tacn:`left` and :tacn:`right` - .. coqtop:: reset all + .. rocqtop:: reset all Print or. (* or, represented by \/, has two constructors, or_introl and or_intror *) Goal forall P1 P2 : Prop, P1 -> P1 \/ P2. @@ -90,21 +90,21 @@ The tactics presented here specialize :tacn:`apply` and In contrast, we won't be able to complete the proof if we select constructor 2: - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall P1 P2 : Prop, P1 -> P1 \/ P2. - .. coqtop:: all + .. rocqtop:: all constructor 2. (* equivalent to "right" *) You can also apply a constructor by name: - .. coqtop:: reset none + .. rocqtop:: reset none Goal forall P1 P2 : Prop, P1 -> P1 \/ P2. - .. coqtop:: all + .. rocqtop:: all intros; apply or_introl. (* equivalent to "left" *) @@ -196,11 +196,11 @@ analysis on inductive or coinductive objects (see :ref:`variants`). .. example:: Using :tacn:`destruct` on an argument with premises - .. coqtop:: reset in + .. rocqtop:: reset in Parameter A B C D : Prop. - .. coqtop:: all + .. rocqtop:: all Goal (A -> B \/ C) -> D. intros until 1. @@ -259,7 +259,7 @@ analysis on inductive or coinductive objects (see :ref:`variants`). .. example:: - .. coqtop:: reset all + .. rocqtop:: reset all Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C. intros A B C H; decompose [and or] H. @@ -337,7 +337,7 @@ Induction principle operates on. Note that it is not enough to be convertible, but you can work around that with :tacn:`change`: - .. coqtop:: reset all + .. rocqtop:: reset all Definition N := nat. Axiom strong : forall P, (forall n:N, (forall m:N, m < n -> P m) -> P n) @@ -358,7 +358,7 @@ Induction .. example:: - .. coqtop:: reset all + .. rocqtop:: reset all Lemma induction_test : forall n:nat, n = n -> n <= n. intros n H. @@ -367,7 +367,7 @@ Induction .. example:: :n:`induction` with :n:`@occurrences` - .. coqtop:: reset all + .. rocqtop:: reset all Lemma induction_test2 : forall n:nat, n = n -> n <= n. intros. @@ -435,7 +435,7 @@ Induction .. example:: - .. coqtop:: reset all extra + .. rocqtop:: reset all extra Lemma lt_1_r : forall n:nat, n < 1 -> n = 0. intros n H ; induction H. @@ -446,7 +446,7 @@ Induction argument is 1 here. Dependent induction solves this problem by adding the corresponding equality to the context. - .. coqtop:: reset all extra + .. rocqtop:: reset all extra Require Import Stdlib.Program.Equality. Lemma lt_1_r : forall n:nat, n < 1 -> n = 0. @@ -456,13 +456,13 @@ Induction simplify the subgoals with respect to the generated equalities. In this enriched context, it becomes possible to solve this subgoal. - .. coqtop:: all extra + .. rocqtop:: all extra reflexivity. Now we are in a contradictory context and the proof can be solved. - .. coqtop:: all abort extra + .. rocqtop:: all abort extra inversion H. @@ -592,7 +592,7 @@ This section describes some special purpose tactics to work with .. example:: Proving `1 <> 2` - .. coqtop:: reset in + .. rocqtop:: reset in Goal 1 <> 2. discriminate. @@ -601,21 +601,21 @@ This section describes some special purpose tactics to work with This works because `1 <> 2` is represented internally as `not (1 = 2)`, which is just `(1 = 2) -> False` from the definition of `not`: - .. coqtop:: all + .. rocqtop:: all Print not. You can see this better by doing the :n:`intro` explicitly: - .. coqtop:: in + .. rocqtop:: in Goal 1 <> 2. - .. coqtop:: all + .. rocqtop:: all intro. (* if omitted, "discriminate" does an intro *) - .. coqtop:: in + .. rocqtop:: in discriminate. Qed. @@ -624,19 +624,19 @@ This section describes some special purpose tactics to work with .. example:: :n:`discriminate` limitation: proving `n <> S n` - .. coqtop:: reset in + .. rocqtop:: reset in Goal forall n:nat, n <> S n. intro n. induction n. - .. coqtop:: all + .. rocqtop:: all - discriminate. (* works: O and (S O) start with different constructors *) - Fail discriminate. (* fails: discriminate doesn't handle this case *) injection. - .. coqtop:: in + .. rocqtop:: in assumption. Qed. @@ -695,7 +695,7 @@ This section describes some special purpose tactics to work with Consider the following goal: - .. coqtop:: in + .. rocqtop:: in Inductive list : Set := | nil : list @@ -703,7 +703,7 @@ This section describes some special purpose tactics to work with Parameter P : list -> Prop. Goal forall l n, P nil -> cons n l = cons 0 nil -> P l. - .. coqtop:: all + .. rocqtop:: all intros. injection H0. @@ -849,17 +849,17 @@ This section describes some special purpose tactics to work with .. example:: :tacn:`inversion` with :n:`as @or_and_intropattern` - .. coqtop:: reset all + .. rocqtop:: reset all Inductive contains0 : list nat -> Prop := | in_hd : forall l, contains0 (0 :: l) | in_tl : forall l b, contains0 l -> contains0 (b :: l). - .. coqtop:: in + .. rocqtop:: in Goal forall l:list nat, contains0 (1 :: l) -> contains0 l. - .. coqtop:: all + .. rocqtop:: all intros l H. inversion H as [ | l' p Hl' [Heqp Heql'] ]. @@ -919,7 +919,7 @@ This section describes some special purpose tactics to work with Let us consider the relation :g:`Le` over natural numbers: - .. coqtop:: reset in + .. rocqtop:: reset in Inductive Le : nat -> nat -> Set := | LeO : forall n:nat, Le 0 n @@ -928,14 +928,14 @@ This section describes some special purpose tactics to work with Let us consider the following goal: - .. coqtop:: none + .. rocqtop:: none Section Section. Variable P : nat -> nat -> Prop. Variable Q : forall n m:nat, Le n m -> Prop. Goal forall n m, Le (S n) m -> P n m. - .. coqtop:: out + .. rocqtop:: out intros. @@ -946,7 +946,7 @@ This section describes some special purpose tactics to work with the arrow in the type of :g:`LeS`. This inversion is possible because :g:`Le` is the smallest set closed by the constructors :g:`LeO` and :g:`LeS`. - .. coqtop:: all + .. rocqtop:: all inversion_clear H. @@ -957,11 +957,11 @@ This section describes some special purpose tactics to work with context to use it after. In that case we can use :tacn:`inversion` that does not clear the equalities: - .. coqtop:: none restart + .. rocqtop:: none restart intros. - .. coqtop:: all + .. rocqtop:: all inversion H. @@ -969,12 +969,12 @@ This section describes some special purpose tactics to work with Let us consider the following goal: - .. coqtop:: none + .. rocqtop:: none Abort. Goal forall n m (H:Le (S n) m), Q (S n) m H. - .. coqtop:: out + .. rocqtop:: out intros. @@ -984,7 +984,7 @@ This section describes some special purpose tactics to work with :tacn:`inversion_clear` do such a substitution. To have such a behavior we use the dependent inversion tactics: - .. coqtop:: all + .. rocqtop:: all dependent inversion_clear H. @@ -995,7 +995,7 @@ This section describes some special purpose tactics to work with Let us consider the following inductive type of length-indexed lists, and a lemma about inverting equality of cons: - .. coqtop:: reset all extra + .. rocqtop:: reset all extra Require Import Stdlib.Logic.Eqdep_dec. @@ -1012,20 +1012,20 @@ This section describes some special purpose tactics to work with After performing inversion, we are left with an equality of existTs: - .. coqtop:: all extra + .. rocqtop:: all extra inversion H. We can turn this equality into a usable form with inversion_sigma: - .. coqtop:: all extra + .. rocqtop:: all extra inversion_sigma. To finish cleaning up the proof, we will need to use the fact that that all proofs of n = n for n a nat are eq_refl: - .. coqtop:: all extra + .. rocqtop:: all extra let H := match goal with H : n = n |- _ => H end in pose proof (Eqdep_dec.UIP_refl_nat _ H); subst H. @@ -1033,7 +1033,7 @@ This section describes some special purpose tactics to work with Finally, we can finish the proof: - .. coqtop:: all extra + .. rocqtop:: all extra assumption. Qed. @@ -1052,18 +1052,18 @@ Helper tactics .. example:: Using :tacn:`decide` to rewrite the goal - .. coqtop:: in extra + .. rocqtop:: in extra Goal forall (P Q : Prop) (Hp : {P} + {~P}) (Hq : {Q} + {~Q}), P -> ~Q -> (if Hp then true else false) = (if Hq then false else true). - .. coqtop:: all extra + .. rocqtop:: all extra intros P Q Hp Hq p nq. decide Hp with p. decide Hq with nq. - .. coqtop:: in extra + .. rocqtop:: in extra reflexivity. Qed. @@ -1158,12 +1158,12 @@ Generation of induction principles with ``Scheme`` You can define a mutual induction principle for tree and forest in sort ``Set`` with the :cmd:`Scheme` command: - .. coqtop:: reset none + .. rocqtop:: reset none Axiom A : Set. Axiom B : Set. - .. coqtop:: in + .. rocqtop:: in Inductive tree : Set := | node : A -> forest -> tree @@ -1171,14 +1171,14 @@ Generation of induction principles with ``Scheme`` | leaf : B -> forest | cons : tree -> forest -> forest. - .. coqtop:: all + .. rocqtop:: all Scheme tree_forest_rec := Induction for tree Sort Set with forest_tree_rec := Induction for forest Sort Set. You may now look at the type of tree_forest_rec: - .. coqtop:: all + .. rocqtop:: all Check tree_forest_rec. @@ -1193,7 +1193,7 @@ Generation of induction principles with ``Scheme`` Let odd and even be inductively defined as: - .. coqtop:: in + .. rocqtop:: in Inductive odd : nat -> Prop := | oddS : forall n : nat, even n -> odd (S n) @@ -1203,14 +1203,14 @@ Generation of induction principles with ``Scheme`` The following command generates a powerful elimination principle: - .. coqtop:: all + .. rocqtop:: all Scheme odd_even := Minimality for odd Sort Prop with even_odd := Minimality for even Sort Prop. The type of odd_even for instance will be: - .. coqtop:: all + .. rocqtop:: all Check odd_even. @@ -1223,7 +1223,7 @@ Generation of induction principles with ``Scheme`` Let us demonstrate the difference between the Scheme commands. - .. coqtop:: all + .. rocqtop:: all Unset Elimination Schemes. @@ -1301,7 +1301,7 @@ Combined Scheme We can define the induction principles for trees and forests using: - .. coqtop:: all + .. rocqtop:: all Scheme tree_forest_ind := Induction for tree Sort Prop with forest_tree_ind := Induction for forest Sort Prop. @@ -1309,13 +1309,13 @@ Combined Scheme Then we can build the combined induction principle which gives the conjunction of the conclusions of each individual principle: - .. coqtop:: all + .. rocqtop:: all Combined Scheme tree_forest_mutind from tree_forest_ind,forest_tree_ind. The type of tree_forest_mutind will be: - .. coqtop:: all + .. rocqtop:: all Check tree_forest_mutind. @@ -1323,16 +1323,16 @@ Combined Scheme We can also combine schemes at sort ``Type``: - .. coqtop:: all + .. rocqtop:: all Scheme tree_forest_rect := Induction for tree Sort Type with forest_tree_rect := Induction for forest Sort Type. - .. coqtop:: all + .. rocqtop:: all Combined Scheme tree_forest_mutrect from tree_forest_rect, forest_tree_rect. - .. coqtop:: all + .. rocqtop:: all Check tree_forest_mutrect. @@ -1376,7 +1376,7 @@ Generation of inversion principles with ``Derive`` ``Inversion`` Consider the relation `Le` over natural numbers and the following parameter ``P``: - .. coqtop:: all + .. rocqtop:: all Inductive Le : nat -> nat -> Set := | LeO : forall n:nat, Le 0 n @@ -1387,19 +1387,19 @@ Generation of inversion principles with ``Derive`` ``Inversion`` To generate the inversion lemma for the instance :g:`(Le (S n) m)` and the sort :g:`Prop`, we do: - .. coqtop:: all + .. rocqtop:: all Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort Prop. Check leminv. Then we can use the proven inversion lemma: - .. coqtop:: none + .. rocqtop:: none Goal forall (n m : nat) (H : Le (S n) m), P n m. intros. - .. coqtop:: all + .. rocqtop:: all Show. @@ -1427,7 +1427,7 @@ argument a hypothesis to generalize. It uses the JMeq datatype defined in Stdlib.Logic.JMeq, hence we need to require it before. For example, revisiting the first example of the inversion documentation: -.. coqtop:: in reset extra +.. rocqtop:: in reset extra Require Import Stdlib.Logic.JMeq. @@ -1441,7 +1441,7 @@ example, revisiting the first example of the inversion documentation: intros n m H. -.. coqtop:: all extra +.. rocqtop:: all extra generalize_eqs H. @@ -1455,7 +1455,7 @@ rule of thumb, all the variables that appear inside constructors in the indices of the hypothesis should be generalized. This is exactly what the ``generalize_eqs_vars`` variant does: -.. coqtop:: all abort extra +.. rocqtop:: all abort extra generalize_eqs_vars H. induction H. @@ -1465,16 +1465,16 @@ 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 extra +.. rocqtop:: none extra Require Import Stdlib.Program.Equality. -.. coqtop:: in extra +.. rocqtop:: in extra Parameter Q : forall (n m : nat), Le n m -> Prop. Goal forall n m (p : Le (S n) m), Q (S n) m p. -.. coqtop:: all extra +.. rocqtop:: all extra intros n m p. generalize_eqs_vars p. @@ -1490,7 +1490,7 @@ automatically do such simplifications (which may involve the axiom K). This is what the ``simplify_dep_elim`` tactic from ``Stdlib.Program.Equality`` does. For example, we might simplify the previous goals considerably: -.. coqtop:: all abort extra +.. rocqtop:: all abort extra induction p ; simplify_dep_elim. @@ -1503,15 +1503,15 @@ are :tacn:`dependent induction` and :tacn:`dependent destruction` that do induct simply case analysis on the generalized hypothesis. For example we can redo what we've done manually with dependent destruction: -.. coqtop:: in extra +.. rocqtop:: in extra Lemma ex : forall n m:nat, Le (S n) m -> P n m. -.. coqtop:: in extra +.. rocqtop:: in extra intros n m H. -.. coqtop:: all abort extra +.. rocqtop:: all abort extra dependent destruction H. @@ -1520,30 +1520,30 @@ 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 extra +.. rocqtop:: in extra Set Implicit Arguments. -.. coqtop:: in extra +.. rocqtop:: in extra Parameter A : Set. -.. coqtop:: in extra +.. rocqtop:: in extra Inductive vector : nat -> Type := | vnil : vector 0 | vcons : A -> forall n, vector n -> vector (S n). -.. coqtop:: in extra +.. rocqtop:: in extra Goal forall n, forall v : vector (S n), exists v' : vector n, exists a : A, v = vcons a v'. -.. coqtop:: in extra +.. rocqtop:: in extra intros n v. -.. coqtop:: all extra +.. rocqtop:: all extra dependent destruction v. @@ -1561,27 +1561,27 @@ 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 reset extra +.. rocqtop:: in reset extra Inductive type : Type := | base : type | arrow : type -> type -> type. -.. coqtop:: in extra +.. rocqtop:: in extra Notation " t --> t' " := (arrow t t') (at level 20, t' at next level). -.. coqtop:: in extra +.. rocqtop:: in extra Inductive ctx : Type := | empty : ctx | snoc : ctx -> type -> ctx. -.. coqtop:: in extra +.. rocqtop:: in extra Notation " G , tau " := (snoc G tau) (at level 20, tau at next level). -.. coqtop:: in extra +.. rocqtop:: in extra Fixpoint conc (G D : ctx) : ctx := match D with @@ -1589,11 +1589,11 @@ dependently-typed style: | snoc D' x => snoc (conc G D') x end. -.. coqtop:: in extra +.. rocqtop:: in extra Notation " G ; D " := (conc G D) (at level 20). -.. coqtop:: in extra +.. rocqtop:: in extra Inductive term : ctx -> type -> Type := | ax : forall G tau, term (G, tau) tau @@ -1620,7 +1620,7 @@ name. A term is either an application of: Once we have this datatype we want to do proofs on it, like weakening: -.. coqtop:: in abort extra +.. rocqtop:: in abort extra Lemma weakening : forall G D tau, term (G ; D) tau -> forall tau', term (G , tau' ; D) tau. @@ -1629,7 +1629,7 @@ The problem here is that we can't just use induction on the typing derivation because it will forget about the ``G ; D`` constraint appearing in the instance. A solution would be to rewrite the goal as: -.. coqtop:: in abort extra +.. rocqtop:: in abort extra Lemma weakening' : forall G' tau, term G' tau -> forall G D, (G ; D) = G' -> @@ -1643,21 +1643,21 @@ more natural statement. The :tacn:`dependent induction` tactic alleviates this trouble by doing all of this plumbing of generalizing and substituting back automatically. Indeed we can simply write: -.. coqtop:: in extra +.. rocqtop:: in extra Require Import Stdlib.Program.Tactics. Require Import Stdlib.Program.Equality. -.. coqtop:: in extra +.. rocqtop:: in extra Lemma weakening : forall G D tau, term (G ; D) tau -> forall tau', term (G , tau' ; D) tau. -.. coqtop:: in extra +.. rocqtop:: in extra Proof with simpl in * ; simpl_depind ; auto. -.. coqtop:: in extra +.. rocqtop:: in extra intros G D tau H. dependent induction H generalizing G D ; intros. @@ -1669,7 +1669,7 @@ hypotheses. By default, all variables appearing inside constructors be generalized automatically but one can always give the list explicitly. -.. coqtop:: all extra +.. rocqtop:: all extra Show. @@ -1680,31 +1680,31 @@ cases where the equality is not between constructor forms though, one must help the automation by giving some arguments, using the ``specialize`` tactic for example. -.. coqtop:: in extra +.. rocqtop:: in extra destruct D... apply weak; apply ax. apply ax. -.. coqtop:: in extra +.. rocqtop:: in extra destruct D... -.. coqtop:: all extra +.. rocqtop:: all extra Show. -.. coqtop:: all extra +.. rocqtop:: all extra specialize (IHterm G0 empty eq_refl). Once the induction hypothesis has been narrowed to the right equality, it can be used directly. -.. coqtop:: all extra +.. rocqtop:: all extra apply weak, IHterm. Now concluding this subgoal is easy. -.. coqtop:: in extra +.. rocqtop:: in extra constructor; apply IHterm; reflexivity. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 46585e3ba62b..9b8e7320ff24 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -17,7 +17,7 @@ different contexts; to achieve this form of overloading, Rocq offers a notion of :ref:`notation scopes `. The main command to provide custom notations for tactics is :cmd:`Tactic Notation`. -.. coqtop:: none +.. rocqtop:: none Set Printing Depth 50. @@ -53,7 +53,7 @@ Basic notations For example, the following definition permits using the infix expression :g:`A /\ B` to represent :g:`(and A B)`: -.. coqtop:: in +.. rocqtop:: in Notation "A /\ B" := (and A B). @@ -71,7 +71,7 @@ literally when the notation is used. Identifiers enclosed in single quotes are treated as symbols and thus lose their role as parameters. For example: -.. coqtop:: in +.. rocqtop:: in Notation "'IF' c1 'then' c2 'else' c3" := (c1 /\ c2 \/ ~ c1 /\ c3) (at level 200, right associativity). @@ -129,7 +129,7 @@ precedence levels ranging from 0 to 100 (plus one extra level numbered Consider for example the new notation -.. coqtop:: in +.. rocqtop:: in Notation "A \/ B" := (or A B). @@ -157,7 +157,7 @@ right associativity (which is the choice of Rocq). Precedence levels and associativity rules of notations are specified with a list of parenthesized :n:`@syntax_modifier`\s. Here is how the previous examples refine: -.. coqtop:: in +.. rocqtop:: in Notation "A /\ B" := (and A B) (at level 80, right associativity). Notation "A \/ B" := (or A B) (at level 85, right associativity). @@ -177,14 +177,14 @@ Complex notations Notations can be made from arbitrarily complex symbols. One can for instance define prefix notations. -.. coqtop:: in +.. rocqtop:: in Notation "~ x" := (not x) (at level 75, right associativity). One can also define notations for incomplete terms, with the hole expected to be inferred during type checking. -.. coqtop:: in +.. rocqtop:: in Notation "x = y" := (@eq _ x y) (at level 70, no associativity). @@ -192,13 +192,13 @@ One can define *closed* notations whose both sides are symbols. In this case, the default precedence level for the inner sub-expression is 200, and the default level for the notation itself is 0. -.. coqtop:: in +.. rocqtop:: in Notation "( x , y )" := (@pair _ _ x y). One can also define notations for binders. -.. coqtop:: in +.. rocqtop:: in Notation "{ x : A | P }" := (sig A (fun x => P)). @@ -208,7 +208,7 @@ Grammar` `constr` is at level 100. To avoid ``x : A`` being parsed as a type cas it is necessary to put ``x`` at a level below 100, typically 99. Hence, a correct definition is the following: -.. coqtop:: reset all +.. rocqtop:: reset all Notation "{ x : A | P }" := (sig A (fun x => P)) (x at level 99). @@ -230,7 +230,7 @@ and ``y`` at level 69 would be broken by another rule that puts at level 200. To avoid such issues, you should left factorize rules, that is ensure that common prefixes use the samel levels. -.. coqtop:: all +.. rocqtop:: all Reserved Notation "x << y" (at level 70). Fail Reserved Notation "x << y << z" (at level 70, y at level 200). @@ -241,14 +241,14 @@ default behavior puts ``y`` at the next level below 70 in the first rule (``no associativity`` is the default). To fix this, we need to force the parsing level of ``y``, as follows. -.. coqtop:: reset all +.. rocqtop:: reset all Reserved Notation "x << y" (at level 70). Reserved Notation "x << y << z" (at level 70, y at next level). Or better yet, simply let the defaults ensure the best factorization. -.. coqtop:: reset all +.. rocqtop:: reset all Reserved Notation "x << y" (at level 70). Reserved Notation "x << y << z". @@ -277,7 +277,7 @@ Use of notations for printing The command :cmd:`Notation` has an effect both on the Rocq parser and on the Rocq printer. For example: -.. coqtop:: all +.. rocqtop:: all Check (and True True). @@ -301,27 +301,27 @@ separate the components) is interpreted as a space to be inserted by the printer. Here is an example showing how to add spaces next to the curly braces. -.. coqtop:: in +.. rocqtop:: in Notation "{{ x : A | P }}" := (sig (fun x : A => P)) (at level 0, x at level 99). -.. coqtop:: all +.. rocqtop:: all Check (sig (fun x : nat => x=x)). The second, more powerful control on printing is by using :n:`@syntax_modifier`\s. Here is an example -.. coqtop:: in +.. rocqtop:: in Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R. -.. coqtop:: all +.. rocqtop:: all Notation "'If' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3) (at level 200, right associativity, format "'[v ' 'If' c1 '/' '[' 'then' c2 ']' '/' '[' 'else' c3 ']' ']'"). -.. coqtop:: all +.. rocqtop:: all Check (IF_then_else (IF_then_else True False True) @@ -389,7 +389,7 @@ at the time of use of the notation. notations which capture the largest subterm of the term are used preferentially. Here is an example: - .. coqtop:: in + .. rocqtop:: in Notation "x < y" := (lt x y) (at level 70). Notation "x < y < z" := (lt x y /\ lt y z) (at level 70, y at next level). @@ -422,7 +422,7 @@ symbols. where ``x`` and ``y`` are fresh names and omitting the quotes around :n:`@string`. Here is an example: - .. coqtop:: in + .. rocqtop:: in Infix "/\" := and (at level 80, right associativity). @@ -440,7 +440,7 @@ Reserving notations without giving its interpretation. Here is an example from the initial state of Rocq. - .. coqtop:: in + .. rocqtop:: in Reserved Notation "x = y" (at level 70, no associativity). @@ -485,21 +485,21 @@ changing a parsing rule are accepted. Here are examples: -.. coqtop:: in +.. rocqtop:: in Reserved Notation "A & B" (at level 80). -.. coqtop:: in +.. rocqtop:: in Inductive and' (A B : Prop) : Prop := conj' : A -> B -> A & B where "A & B" := (and' A B). .. without this we get "not a truly recursive fixpoint" -.. coqtop:: none +.. rocqtop:: none Arguments S _ : clear scopes. -.. coqtop:: in +.. rocqtop:: in Fixpoint plus (n m : nat) {struct n} : nat := match n with @@ -618,7 +618,7 @@ Enabling and disabling notations .. example:: Enabling and disabling notations - .. coqtop:: all + .. rocqtop:: all Disable Notation "+" (all). Enable Notation "_ + _" (all) : type_scope. @@ -653,7 +653,7 @@ Displaying information about notations :token:`string`. :token:`ident`, if specified, is the name of the associated custom entry. See :cmd:`Declare Custom Entry`. - .. coqtop:: all + .. rocqtop:: all Reserved Notation "x # y" (at level 123, right associativity). Print Notation "_ # _". @@ -668,7 +668,7 @@ Displaying information about notations .. example:: :cmd:`Print Notation` - .. coqtop:: all + .. rocqtop:: all Reserved Notation "x 'mod' y" (at level 40, no associativity). Print Notation "_ mod _". @@ -821,7 +821,7 @@ To locate a particular notation, use a string where the variables of the notation are replaced by “``_``” and where possible single quotes inserted around identifiers or tokens starting with a single quote are dropped. -.. coqtop:: all +.. rocqtop:: all Locate "exists". Locate "exists _ .. _ , _". @@ -834,12 +834,12 @@ the notation inherits the implicit arguments (see :ref:`ImplicitArguments`) and notation scopes (see :ref:`Scopes`) of the constant. For instance: -.. coqtop:: in reset +.. rocqtop:: in reset Record R := {dom : Type; op : forall {A}, A -> dom}. Notation "# x" := (@op x) (at level 8). -.. coqtop:: all +.. rocqtop:: all Check fun x:R => # x 3. @@ -861,7 +861,7 @@ Binders bound in the notation and parsed as identifiers Here is the basic example of a notation using a binder: -.. coqtop:: in +.. rocqtop:: in Notation "'sigma' x : A , B" := (sigT (fun x : A => B)) (at level 200, x name, A at level 200, right associativity). @@ -873,7 +873,7 @@ parameters of the notation. This means that the term bound to :g:`B` can refer to the variable name bound to :g:`x` as shown in the following application of the notation: -.. coqtop:: all +.. rocqtop:: all Check sigma z : nat, z = 0. @@ -889,12 +889,12 @@ In the same way as patterns can be used as binders, as in defined so that any :n:`@pattern` can be used in place of the binder. Here is an example: -.. coqtop:: in reset +.. rocqtop:: in reset Notation "'subset' ' p , P " := (sig (fun p => P)) (at level 200, p pattern, format "'subset' ' p , P"). -.. coqtop:: all +.. rocqtop:: all Check subset '(x,y), x+y=0. @@ -902,7 +902,7 @@ The :n:`@syntax_modifier p pattern` in the declaration of the notation tells to :g:`p` as a pattern. Note that a single variable is both an identifier and a pattern, so, e.g., the following also works: -.. coqtop:: all +.. rocqtop:: all Check subset 'x, x=0. @@ -912,14 +912,14 @@ the :n:`@syntax_modifier p strict pattern`. For parsing, however, a ``strict pattern`` will continue to include the case of a variable. Here is an example showing the difference: -.. coqtop:: in +.. rocqtop:: in Notation "'subset_bis' ' p , P" := (sig (fun p => P)) (at level 200, p strict pattern). Notation "'subset_bis' p , P " := (sig (fun p => P)) (at level 200, p name). -.. coqtop:: all +.. rocqtop:: all Check subset_bis 'x, x=0. @@ -934,7 +934,7 @@ Sometimes, for the sake of factorization of rules, a binder has to be parsed as a term. This is typically the case for a notation such as the following: -.. coqdoc:: +.. rocqdoc:: Notation "{ x : A | P }" := (sig (fun x : A => P)) (at level 0, x at level 99 as name). @@ -953,14 +953,14 @@ library with the ``as name`` :n:`@syntax_modifier`. We cannot redefine it but one can define an alternative notation, say :g:`{ p such that P }`, using instead ``as pattern``. -.. coqtop:: in +.. rocqtop:: in Notation "{ p 'such' 'that' P }" := (sig (fun p => P)) (at level 0, p at level 99 as pattern). Then, the following works: -.. coqtop:: all +.. rocqtop:: all Check {(x,y) such that x+y=0}. @@ -978,7 +978,7 @@ Binders bound in the notation and parsed as general binders It is also possible to rely on Rocq's syntax of binders using the `binder` modifier as follows: -.. coqtop:: in +.. rocqtop:: in Notation "'myforall' p , [ P , Q ] " := (forall p, P -> Q) (at level 200, p binder). @@ -988,7 +988,7 @@ In this case, all of :n:`@ident`, :n:`{@ident}`, :n:`[@ident]`, :n:`@ident:@type the corresponding notation variable. In particular, the binder can declare implicit arguments: -.. coqtop:: all +.. rocqtop:: all Check fun (f : myforall {a}, [a=0, Prop]) => f eq_refl. Check myforall '((x,y):nat*nat), [ x = y, True ]. @@ -1006,17 +1006,17 @@ are not themselves bound in the notation. In this case, the binders are considered up to renaming of the internal binder. E.g., for the notation -.. coqtop:: in +.. rocqtop:: in Notation "'exists_different' n" := (exists p:nat, p<>n) (at level 200). the next command fails because p does not bind in the instance of n. -.. coqtop:: all +.. rocqtop:: all Fail Check (exists_different p). -.. coqtop:: in +.. rocqtop:: in Notation "[> a , .. , b <]" := (cons a .. (cons b nil) .., cons b .. (cons a nil) ..). @@ -1027,20 +1027,20 @@ Notations with expressions used both as binder and term It is possible to use parameters of the notation both in term and binding position. Here is an example: -.. coqtop:: in +.. rocqtop:: in Definition force n (P:nat -> Prop) := forall n', n' >= n -> P n'. Notation "▢_ n P" := (force n (fun n => P)) (at level 0, n name, P at level 9, format "▢_ n P"). -.. coqtop:: all +.. rocqtop:: all Check exists p, ▢_p (p >= 1). More generally, the parameter can be a pattern, as in the following variant: -.. coqtop:: in reset +.. rocqtop:: in reset Definition force2 q (P:nat*nat -> Prop) := (forall n', n' >= fst q -> forall p', p' >= snd q -> P q). @@ -1048,7 +1048,7 @@ variant: Notation "▢_ p P" := (force2 p (fun p => P)) (at level 0, p pattern at level 0, P at level 9, format "▢_ p P"). -.. coqtop:: all +.. rocqtop:: all Check exists x y, ▢_(x,y) (x >= 1 /\ y >= 2). @@ -1064,7 +1064,7 @@ Notations with recursive patterns A mechanism is provided for declaring elementary notations with recursive patterns. The basic example is: -.. coqtop:: all +.. rocqtop:: all Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..). @@ -1098,13 +1098,13 @@ and the terminating expression is ``nil``. Here is another example with the pattern associating on the left: -.. coqtop:: in +.. rocqtop:: in Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0). Here is an example with more involved recursive patterns: -.. coqtop:: in +.. rocqtop:: in Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c ) * u |]" := (pair (pair .. (pair (pair t x) (pair t y)) .. (pair t z)) @@ -1119,7 +1119,7 @@ beta-redexes are contracted, the notations stops to be used for printing. Support for notations defined in this way should be considered experimental. -.. coqtop:: in +.. rocqtop:: in Notation "x ⪯ y ⪯ .. ⪯ z ⪯ t" := ((fun b A a => a <= b /\ A b) y .. ((fun b A a => a <= b /\ A b) z (fun b => b <= t)) .. x) @@ -1137,7 +1137,7 @@ Notations with recursive patterns involving binders Recursive notations can also be used with binders. The basic example is: -.. coqtop:: in +.. rocqtop:: in Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) @@ -1170,7 +1170,7 @@ be of the more general form ``x s .. s y`` where ``s`` is an arbitrary sequence tokens. With open binders though, ``s`` has to be empty. Here is an example of recursive notation with closed binders: -.. coqtop:: in +.. rocqtop:: in Notation "'mylet' f x .. y := t 'in' u":= (let f := fun x => .. (fun y => t) .. in u) @@ -1179,7 +1179,7 @@ example of recursive notation with closed binders: A recursive pattern for binders can be used in position of a recursive pattern for terms. Here is an example: -.. coqtop:: in +.. rocqtop:: in Notation "'FUNAPP' x .. y , f" := (fun x => .. (fun y => (.. (f x) ..) y ) ..) @@ -1189,7 +1189,7 @@ If an occurrence of the :math:`[~]_E` is not in position of a binding variable but of a term, it is the name used in the binding which is used. Here is an example: -.. coqtop:: in +.. rocqtop:: in Notation "'exists_non_null' x .. y , P" := (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..)) @@ -1204,7 +1204,7 @@ to restrict the syntax of terms in a notation. For instance, the following notation will accept to parse only global reference in position of :g:`x`: -.. coqtop:: in +.. rocqtop:: in Notation "'apply' f a1 .. an" := (.. (f a1) .. an) (at level 10, f global, a1, an at level 9). @@ -1215,7 +1215,7 @@ already seen in :ref:`NotationsWithBinders`, even when the corresponding expression is not used as a binder in the right-hand side. E.g.: -.. coqtop:: in +.. rocqtop:: in Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an) (at level 10, f ident, a1, an at level 9). @@ -1242,7 +1242,7 @@ Custom entries For instance, we may want to define an ad hoc parser for arithmetical operations and proceed as follows: - .. coqtop:: reset all + .. rocqtop:: reset all Inductive Expr := | One : Expr @@ -1288,7 +1288,7 @@ associative and rules at level less or equal than ``n`` if the rule is declared right associative. This is what happens for instance in the rule -.. coqtop:: in +.. rocqtop:: in Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity). @@ -1301,7 +1301,7 @@ Rules associated with an entry can refer different sub-entries. The grammar entry name ``constr`` can be used to refer to the main grammar of term as in the rule -.. coqtop:: in +.. rocqtop:: in Notation "{ x }" := x (in custom expr at level 0, x constr). @@ -1315,14 +1315,14 @@ level``. Conversely, custom entries can be used to parse sub-expressions of the main grammar, or from another custom entry as is the case in -.. coqtop:: in +.. rocqtop:: in Notation "[ e ]" := e (e custom expr at level 2). to indicate that ``e`` has to be parsed at level ``2`` of the grammar associated with the custom entry ``expr``. The level can be omitted, as in -.. coqdoc:: +.. rocqdoc:: Notation "[ e ]" := e (e custom expr). @@ -1347,13 +1347,13 @@ side, i.e. that they are bound to an expression which is not reduced to a single variable. If the rule is not productive on the right-hand side, as it is the case above for -.. coqtop:: in +.. rocqtop:: in Notation "( x )" := x (in custom expr at level 0, x at level 2). and -.. coqtop:: in +.. rocqtop:: in Notation "{ x }" := x (in custom expr at level 0, x constr). @@ -1362,7 +1362,7 @@ print an expression which is not available in the current grammar at the current level of parsing or printing for this grammar but which is available in another grammar or in another level of the current grammar. For instance, -.. coqtop:: in +.. rocqtop:: in Notation "( x )" := x (in custom expr at level 0, x at level 2). @@ -1372,7 +1372,7 @@ expected to be used as a subterm at level 0 or 1. This allows for instance to parse and print :g:`Add x y` as a subterm of :g:`Mul (Add x y) z` using the syntax ``(x + y) z``. Similarly, -.. coqtop:: in +.. rocqtop:: in Notation "{ x }" := x (in custom expr at level 0, x constr). @@ -1384,22 +1384,22 @@ Another special situation is when parsing global references or identifiers. To indicate that a custom entry should parse identifiers, use the following form: -.. coqtop:: reset none +.. rocqtop:: reset none Declare Custom Entry expr. -.. coqtop:: in +.. rocqtop:: in Notation "x" := x (in custom expr at level 0, x ident). Similarly, to indicate that a custom entry should parse global references (i.e. qualified or unqualified identifiers), use the following form: -.. coqtop:: reset none +.. rocqtop:: reset none Declare Custom Entry expr. -.. coqtop:: in +.. rocqtop:: in Notation "x" := x (in custom expr at level 0, x global). @@ -1660,7 +1660,7 @@ Binding types or coercion classes to notation scopes Let's declare two scopes with a notation in each and an arbitrary function on type ``bool``. - .. coqtop:: in reset + .. rocqtop:: in reset Declare Scope T_scope. Declare Scope F_scope. @@ -1672,7 +1672,7 @@ Binding types or coercion classes to notation scopes By default, the argument of ``f`` is interpreted in the currently opened scopes. - .. coqtop:: all + .. rocqtop:: all Open Scope T_scope. Check f #. @@ -1681,7 +1681,7 @@ Binding types or coercion classes to notation scopes This can be changed by binding scopes to the type ``bool``. - .. coqtop:: all + .. rocqtop:: all Bind Scope T_scope with bool. Check f #. @@ -1690,7 +1690,7 @@ Binding types or coercion classes to notation scopes interpreted in the first scope containing them, from the top of the stack. - .. coqtop:: all + .. rocqtop:: all #[add_top] Bind Scope F_scope with bool. Check f #. @@ -1701,13 +1701,13 @@ Binding types or coercion classes to notation scopes Bindings for functions can be displayed with the :cmd:`About` command. - .. coqtop:: all + .. rocqtop:: all About f. Bindings are also used in casts. - .. coqtop:: all + .. rocqtop:: all Close Scope F_scope. Check #. @@ -1900,33 +1900,33 @@ Abbreviations An *abbreviation* is a name, possibly applied to arguments, that denotes a (presumably) more complex expression. Here are examples: - .. coqtop:: none + .. rocqtop:: none Require Import ListDef. Set Printing Notations. - .. coqtop:: in + .. rocqtop:: in Notation Nlist := (list nat). - .. coqtop:: all + .. rocqtop:: all Check 1 :: 2 :: 3 :: nil. - .. coqtop:: in + .. rocqtop:: in Notation reflexive R := (forall x, R x x). - .. coqtop:: all + .. rocqtop:: all Check forall A:Prop, A <-> A. Check reflexive iff. - .. coqtop:: in + .. rocqtop:: in Notation Plus1 B := (Nat.add B 1). - .. coqtop:: all + .. rocqtop:: all Compute (Plus1 3). @@ -1943,20 +1943,20 @@ Abbreviations abbreviation but at the time they are used. Especially, abbreviations can be bound to terms with holes (i.e. with “``_``”). For example: - .. coqtop:: none reset + .. rocqtop:: none reset Set Strict Implicit. Set Printing Depth 50. - .. coqtop:: in + .. rocqtop:: in Definition explicit_id (A:Set) (a:A) := a. - .. coqtop:: in + .. rocqtop:: in Notation id := (explicit_id _). - .. coqtop:: all + .. rocqtop:: all Check (id 0). @@ -1973,7 +1973,7 @@ Abbreviations Like for notations, it is possible to bind binders in abbreviations. Here is an example: - .. coqtop:: in reset + .. rocqtop:: in reset Definition force2 q (P:nat*nat -> Prop) := (forall n', n' >= fst q -> forall p', p' >= snd q -> P q). @@ -2343,7 +2343,7 @@ The following errors apply to both string and number notations: whose digits are :g:`0`, :g:`1` or :g:`2` as terms of the following inductive type encoding radix 3 numbers. - .. coqtop:: in reset + .. rocqtop:: in reset Inductive radix3 : Set := | x0 : radix3 @@ -2353,7 +2353,7 @@ The following errors apply to both string and number notations: We first define a parsing function - .. coqtop:: in + .. rocqtop:: in Definition of_uint_dec (u : Decimal.uint) : option radix3 := let fix f u := match u with @@ -2368,7 +2368,7 @@ The following errors apply to both string and number notations: and a printing function - .. coqtop:: in + .. rocqtop:: in Definition to_uint_dec (x : radix3) : Decimal.uint := let fix f x := match x with @@ -2381,7 +2381,7 @@ The following errors apply to both string and number notations: before declaring the notation - .. coqtop:: in + .. rocqtop:: in Declare Scope radix3_scope. Open Scope radix3_scope. @@ -2389,20 +2389,20 @@ The following errors apply to both string and number notations: We can check the printer - .. coqtop:: all + .. rocqtop:: all Check x3p2 (x3p1 x0). and the parser - .. coqtop:: all + .. rocqtop:: all Set Printing All. Check 120. Digits other than :g:`0`, :g:`1` and :g:`2` are rejected. - .. coqtop:: all fail + .. rocqtop:: all fail Check 3. @@ -2415,7 +2415,7 @@ The following errors apply to both string and number notations: parsing and printing of primitive integers are actually implemented in `PrimInt63.v`. - .. coqtop:: in reset + .. rocqtop:: in reset Require Import PrimInt63. Definition parser (x : pos_neg_int63) : option int := @@ -2432,13 +2432,13 @@ The following errors apply to both string and number notations: is encoded as :g:`3` while :g:`unit` is :g:`1` and :g:`0` stands for :g:`Empty_set`. The inductive :g:`I` will be used as :n:`@qualid__ind`. - .. coqtop:: in reset + .. rocqtop:: in reset Inductive I := Iempty : I | Iunit : I | Isum : I -> I -> I. We then define :n:`@qualid__parse` and :n:`@qualid__print` - .. coqtop:: in + .. rocqtop:: in Definition of_uint (x : Number.uint) : I := let fix f n := match n with @@ -2456,7 +2456,7 @@ The following errors apply to both string and number notations: the number notation itself - .. coqtop:: in + .. rocqtop:: in Notation nSet := Set (only parsing). Number Notation nSet of_uint to_uint (via I @@ -2464,14 +2464,14 @@ The following errors apply to both string and number notations: and check the printer - .. coqtop:: all + .. rocqtop:: all Local Open Scope type_scope. Check sum unit (sum unit unit). and the parser - .. coqtop:: all + .. rocqtop:: all Set Printing All. Check 3. @@ -2483,7 +2483,7 @@ The following errors apply to both string and number notations: The following example parses and prints natural numbers between :g:`0` and :g:`n-1` as terms of type :g:`Fin.t n`. - .. coqtop:: all reset warn + .. rocqtop:: all reset warn Module Fin. Inductive t : nat -> Set := F1 : forall n, t (S n) | FS : forall n, t n -> t (S n). @@ -2494,7 +2494,7 @@ The following errors apply to both string and number notations: Note the implicit arguments of :g:`Fin.F1` and :g:`Fin.FS`, which won't appear in the corresponding inductive type. - .. coqtop:: in + .. rocqtop:: in Inductive I := I1 : I | IS : I -> I. @@ -2515,19 +2515,19 @@ The following errors apply to both string and number notations: Now :g:`2` is parsed as :g:`Fin.FS (Fin.FS Fin.F1)`, that is :g:`@Fin.FS _ (@Fin.FS _ (@Fin.F1 _))`. - .. coqtop:: all + .. rocqtop:: all Check 2. which can be of type :g:`Fin.t 3` (numbers :g:`0`, :g:`1` and :g:`2`) - .. coqtop:: all + .. rocqtop:: all Check 2 : Fin.t 3. but cannot be of type :g:`Fin.t 2` (only :g:`0` and :g:`1`) - .. coqtop:: all fail + .. rocqtop:: all fail Check 2 : Fin.t 2. @@ -2538,14 +2538,14 @@ The following errors apply to both string and number notations: The parameter :g:`Byte.byte` for the parameterized inductive type :g:`list` is given through an :ref:`abbreviation `. - .. coqtop:: in reset + .. rocqtop:: in reset Notation string := (list Byte.byte) (only parsing). Definition id_string := @id string. String Notation string id_string id_string : list_scope. - .. coqtop:: all + .. rocqtop:: all Check "abc"%list. @@ -2607,7 +2607,7 @@ Tactic notations allow customizing the syntax of tactics. For example, the following command defines a notation with a single parameter `x`. - .. coqtop:: in + .. rocqtop:: in Tactic Notation "destruct_with_eqn" constr(x) := destruct x eqn:?. diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst index 150bf89130a2..373461aec79e 100644 --- a/doc/sphinx/using/libraries/funind.rst +++ b/doc/sphinx/using/libraries/funind.rst @@ -103,11 +103,11 @@ The following command is available when the ``FunInd`` library has been loaded v parameters of the function as first arguments. For example it is better to define plus like this: - .. coqtop:: reset none extra + .. rocqtop:: reset none extra From Stdlib Require Import FunInd. - .. coqtop:: all extra + .. rocqtop:: all extra Function plus (m n : nat) {struct n} : nat := match n with @@ -117,11 +117,11 @@ The following command is available when the ``FunInd`` library has been loaded v than like this: - .. coqtop:: reset none extra + .. rocqtop:: reset none extra From Stdlib Require Import FunInd. - .. coqtop:: all extra + .. rocqtop:: all extra Function plus (n m : nat) {struct n} : nat := match n with @@ -139,12 +139,12 @@ with applications only *at the end* of each branch. defined. Thus, the following example cannot be accepted due to the presence of partial application of :g:`wrong` in the body of :g:`wrong`: -.. coqtop:: none extra +.. rocqtop:: none extra From Stdlib Require List. Import List.ListNotations. -.. coqtop:: all fail extra +.. rocqtop:: all fail extra Function wrong (C:nat) : nat := List.hd 0 (List.map wrong (C::nil)). @@ -203,7 +203,7 @@ Tactics .. example:: - .. coqtop:: reset all extra + .. rocqtop:: reset all extra From Stdlib Require Import FunInd. Functional Scheme minus_ind := Induction for minus Sort Prop. @@ -298,7 +298,7 @@ Generation of induction principles with ``Functional`` ``Scheme`` We define the function div2 as follows: - .. coqtop:: all extra + .. rocqtop:: all extra From Stdlib Require Import FunInd. From Stdlib Require Import Arith. @@ -313,19 +313,19 @@ Generation of induction principles with ``Functional`` ``Scheme`` The definition of a principle of induction corresponding to the recursive structure of `div2` is defined by the command: - .. coqtop:: all extra + .. rocqtop:: all extra Functional Scheme div2_ind := Induction for div2 Sort Prop. You may now look at the type of div2_ind: - .. coqtop:: all extra + .. rocqtop:: all extra Check div2_ind. We can now prove the following lemma using this principle: - .. coqtop:: all extra + .. rocqtop:: all extra Lemma div2_le' : forall n:nat, div2 n <= n. intro n. @@ -339,7 +339,7 @@ Generation of induction principles with ``Functional`` ``Scheme`` We can use directly the functional induction (:tacn:`functional induction`) tactic instead of the pattern/apply trick: - .. coqtop:: all extra + .. rocqtop:: all extra Reset div2_le'. @@ -359,7 +359,7 @@ Generation of induction principles with ``Functional`` ``Scheme`` .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning - .. coqtop:: reset all extra + .. rocqtop:: reset all extra Axiom A : Set. @@ -373,7 +373,7 @@ Generation of induction principles with ``Functional`` ``Scheme`` forest. Note that we use ``Function`` which generally produces better principles. - .. coqtop:: all extra + .. rocqtop:: all extra From Stdlib Require Import FunInd. @@ -390,21 +390,21 @@ Generation of induction principles with ``Functional`` ``Scheme`` Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind`` generated by ``Function`` are not mutual. - .. coqtop:: all extra + .. rocqtop:: all extra Check tree_size_ind. Mutual induction principles following the recursive structure of ``tree_size`` and ``forest_size`` can be generated by the following command: - .. coqtop:: all extra + .. rocqtop:: all extra Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop with forest_size_ind2 := Induction for forest_size Sort Prop. You may now look at the type of `tree_size_ind2`: - .. coqtop:: all extra + .. rocqtop:: all extra Check tree_size_ind2. diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst index c5fbb0e71487..40f1430fa263 100644 --- a/doc/sphinx/using/libraries/writing.rst +++ b/doc/sphinx/using/libraries/writing.rst @@ -112,7 +112,7 @@ notation, definition, axiom, theorem or file. .. example:: Deprecating a tactic. - .. coqtop:: all abort warn + .. rocqtop:: all abort warn #[deprecated(since="mylib 0.9", note="Use idtac instead.")] Ltac foo := idtac. @@ -126,7 +126,7 @@ notation, definition, axiom, theorem or file. Let's say your library initially contained: - .. coqtop:: in + .. rocqtop:: in Definition foo x := S x. @@ -134,7 +134,7 @@ notation, definition, axiom, theorem or file. your users' code without advanced notice. To do so, replace the previous code by the following: - .. coqtop:: in reset + .. rocqtop:: in reset Definition bar x := S x. #[deprecated(since="mylib 1.2", note="Use bar instead.")] @@ -142,6 +142,6 @@ notation, definition, axiom, theorem or file. Then, the following code still works, but emits a warning: - .. coqtop:: all warn + .. rocqtop:: all warn Check (foo 0). diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 8a111dd98268..4775c575d374 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -685,13 +685,13 @@ class CoqtopDirective(Directive): Usage:: - .. coqtop:: options… + .. rocqtop:: options… Coq code to send to coqtop Example:: - .. coqtop:: in reset + .. rocqtop:: in reset Print nat. Definition a := 1. @@ -720,7 +720,7 @@ class CoqtopDirective(Directive): Be careful when using it to surround the code block with a sentence explaining what extra requirement is needed to compile it. - ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks + ``coqtop``\ 's state is preserved across consecutive ``.. rocqtop::`` blocks of the same document (``coqrst`` creates a single ``coqtop`` process per reST source file). Use the ``reset`` option to reset Coq's state. """ @@ -729,7 +729,7 @@ class CoqtopDirective(Directive): optional_arguments = 0 final_argument_whitespace = True option_spec = { 'name': directives.unchanged } - directive_name = "coqtop" + directive_name = "rocqtop" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable @@ -746,13 +746,13 @@ class CoqdocDirective(Directive): Usage:: - .. coqdoc:: + .. rocqdoc:: Coq code to highlight Example:: - .. coqdoc:: + .. rocqdoc:: Definition test := 1. """ @@ -762,7 +762,7 @@ class CoqdocDirective(Directive): optional_arguments = 0 final_argument_whitespace = True option_spec = { 'name': directives.unchanged } - directive_name = "coqdoc" + directive_name = "rocqdoc" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable @@ -789,7 +789,7 @@ class ExampleDirective(BaseAdmonition): The following adds ``plus_comm`` to the ``plu`` database: - .. coqdoc:: + .. rocqdoc:: Hint Resolve plus_comm : plu. """ @@ -1015,12 +1015,12 @@ def parse_options(node): unexpected_options = list(options - {'all', 'none', 'in', 'out'}) if unexpected_options: loc = os.path.basename(get_node_location(node)) - raise ExtensionError("{}: Unexpected options for .. coqtop:: {}".format(loc,unexpected_options)) + raise ExtensionError("{}: Unexpected options for .. rocqtop:: {}".format(loc,unexpected_options)) # Display options if len(options) != 1: loc = os.path.basename(get_node_location(node)) - raise ExtensionError("{}: Exactly one display option must be passed to .. coqtop::".format(loc)) + raise ExtensionError("{}: Exactly one display option must be passed to .. rocqtop::".format(loc)) opt_all = 'all' in options opt_input = 'in' in options diff --git a/stdlib/doc/sphinx/README.template.rst b/stdlib/doc/sphinx/README.template.rst index 9dd469d29d52..374f91c44542 100644 --- a/stdlib/doc/sphinx/README.template.rst +++ b/stdlib/doc/sphinx/README.template.rst @@ -190,7 +190,7 @@ DON'T .. tacv:: assert form as simple_intropattern -Using the ``.. coqtop::`` directive for syntax highlighting +Using the ``.. rocqtop::`` directive for syntax highlighting ----------------------------------------------------------- DO @@ -198,13 +198,13 @@ DO A tactic of the form: - .. coqdoc:: + .. rocqdoc:: do [ t1 | … | tn ]. is equivalent to the standard Ltac expression: - .. coqdoc:: + .. rocqdoc:: first [ t1 | … | tn ]. @@ -213,13 +213,13 @@ DON'T A tactic of the form: - .. coqtop:: in + .. rocqtop:: in do [ t1 | … | tn ]. is equivalent to the standard Ltac expression: - .. coqtop:: in + .. rocqtop:: in first [ t1 | … | tn ]. @@ -248,7 +248,7 @@ DO Here is a useful axiom: - .. coqdoc:: + .. rocqdoc:: Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. @@ -266,7 +266,7 @@ DON'T .. example:: - .. coqdoc:: + .. rocqdoc:: Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. @@ -276,13 +276,13 @@ Tips and tricks Nested lemmas ------------- -The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas (which by default results in a failure):: +The ``.. rocqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas (which by default results in a failure):: - .. coqtop:: all + .. rocqtop:: all Lemma l1: 1 + 1 = 2. - .. coqtop:: all + .. rocqtop:: all Lemma l2: 2 + 2 <> 1. diff --git a/stdlib/doc/sphinx/language/coq-library.rst b/stdlib/doc/sphinx/language/coq-library.rst index c21c11fe7e17..befc0502bbde 100644 --- a/stdlib/doc/sphinx/language/coq-library.rst +++ b/stdlib/doc/sphinx/language/coq-library.rst @@ -110,7 +110,7 @@ Notation Interpretation Precedence Associativity .. example:: - .. coqtop:: all reset + .. rocqtop:: all reset From Stdlib Require Import ZArith. Check (2 + 3)%Z. @@ -150,7 +150,7 @@ Notation Interpretation .. example:: - .. coqtop:: all reset + .. rocqtop:: all reset From Stdlib Require Import Reals. Check (2 + 3)%R. @@ -169,7 +169,7 @@ tactics (see Chapters ring and micromega), there are also: .. example:: - .. coqtop:: all reset + .. rocqtop:: all reset From Stdlib Require Import DiscrR. Open Scope R_scope. @@ -182,7 +182,7 @@ tactics (see Chapters ring and micromega), there are also: .. example:: - .. coqtop:: all reset + .. rocqtop:: all reset From Stdlib Require Import Reals. Open Scope R_scope. @@ -196,7 +196,7 @@ tactics (see Chapters ring and micromega), there are also: .. example:: - .. coqtop:: all reset + .. rocqtop:: all reset From Stdlib Require Import Reals. Open Scope R_scope. @@ -261,7 +261,7 @@ many such theorems. The library of primitive floating-point arithmetic can be loaded by requiring module ``Floats``: -.. coqtop:: in +.. rocqtop:: in From Stdlib Require Import Floats. @@ -270,7 +270,7 @@ named ``float``, defined in the kernel as well as two variant types ``float_comparison`` and ``float_class``: -.. coqtop:: all +.. rocqtop:: all Print float. Print float_comparison. @@ -340,7 +340,7 @@ decimal constants. This ensures that the composition .. example:: - .. coqtop:: all + .. rocqtop:: all Open Scope float_scope. Eval compute in 1 + 0.5. @@ -355,7 +355,7 @@ The primitive operators are specified with respect to their Gallina counterpart, using the variant type ``spec_float``, and the injection ``Prim2SF``: -.. coqtop:: all +.. rocqtop:: all Print spec_float. Check Prim2SF. diff --git a/stdlib/doc/tools/coqrst/coqdomain.py b/stdlib/doc/tools/coqrst/coqdomain.py index 5c6b7c317ced..278f5d35a27e 100644 --- a/stdlib/doc/tools/coqrst/coqdomain.py +++ b/stdlib/doc/tools/coqrst/coqdomain.py @@ -685,13 +685,13 @@ class CoqtopDirective(Directive): Usage:: - .. coqtop:: options… + .. rocqtop:: options… Coq code to send to coqtop Example:: - .. coqtop:: in reset + .. rocqtop:: in reset Print nat. Definition a := 1. @@ -716,7 +716,7 @@ class CoqtopDirective(Directive): - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode) - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any) - ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks + ``coqtop``\ 's state is preserved across consecutive ``.. rocqtop::`` blocks of the same document (``coqrst`` creates a single ``coqtop`` process per reST source file). Use the ``reset`` option to reset Coq's state. """ @@ -725,7 +725,7 @@ class CoqtopDirective(Directive): optional_arguments = 0 final_argument_whitespace = True option_spec = { 'name': directives.unchanged } - directive_name = "coqtop" + directive_name = "rocqtop" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable @@ -742,13 +742,13 @@ class CoqdocDirective(Directive): Usage:: - .. coqdoc:: + .. rocqdoc:: Coq code to highlight Example:: - .. coqdoc:: + .. rocqdoc:: Definition test := 1. """ @@ -758,7 +758,7 @@ class CoqdocDirective(Directive): optional_arguments = 0 final_argument_whitespace = True option_spec = { 'name': directives.unchanged } - directive_name = "coqdoc" + directive_name = "rocqdoc" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable @@ -785,7 +785,7 @@ class ExampleDirective(BaseAdmonition): The following adds ``plus_comm`` to the ``plu`` database: - .. coqdoc:: + .. rocqdoc:: Hint Resolve plus_comm : plu. """ @@ -1010,12 +1010,12 @@ def parse_options(node): unexpected_options = list(options - {'all', 'none', 'in', 'out'}) if unexpected_options: loc = os.path.basename(get_node_location(node)) - raise ExtensionError("{}: Unexpected options for .. coqtop:: {}".format(loc,unexpected_options)) + raise ExtensionError("{}: Unexpected options for .. rocqtop:: {}".format(loc,unexpected_options)) # Display options if len(options) != 1: loc = os.path.basename(get_node_location(node)) - raise ExtensionError("{}: Exactly one display option must be passed to .. coqtop::".format(loc)) + raise ExtensionError("{}: Exactly one display option must be passed to .. rocqtop::".format(loc)) opt_all = 'all' in options opt_input = 'in' in options