diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 30 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 97 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 20 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 19 | ||||
| -rw-r--r-- | doc/sphinx/addendum/parallel-proof-processing.rst | 54 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 35 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 6 |
7 files changed, 142 insertions, 119 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 7b8a86d1ab..3ec6c118af 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -59,7 +59,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 undo +.. coqtop:: in Fixpoint max (n m:nat) {struct m} : nat := match n with @@ -75,7 +75,7 @@ Multiple patterns Using multiple patterns in the definition of ``max`` lets us write: -.. coqtop:: in undo +.. coqtop:: in reset Fixpoint max (n m:nat) {struct m} : nat := match n, m with @@ -103,7 +103,7 @@ Aliasing subpatterns We can also use :n:`as @ident` to associate a name to a sub-pattern: -.. coqtop:: in undo +.. coqtop:: in reset Fixpoint max (n m:nat) {struct n} : nat := match n, m with @@ -128,18 +128,22 @@ Here is now an example of nested patterns: This is compiled into: -.. coqtop:: all undo +.. coqtop:: all Unset Printing Matching. Print even. +.. coqtop:: none + + Set Printing Matching. + In the previous examples patterns do not conflict with, but sometimes it is comfortable to write patterns that admit a non trivial 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 undo +.. coqtop:: in Fixpoint lef (n m:nat) {struct m} : bool := match n, m with @@ -158,7 +162,7 @@ is matched by the first pattern, and so :g:`(lef O O)` yields true. Another way to write this function is: -.. coqtop:: in +.. coqtop:: in reset Fixpoint lef (n m:nat) {struct m} : bool := match n, m with @@ -191,7 +195,7 @@ Multiple patterns that share the same right-hand-side can be factorized using the notation :n:`{+| @mult_pattern}`. For instance, :g:`max` can be rewritten as follows: -.. coqtop:: in undo +.. coqtop:: in reset Fixpoint max (n m:nat) {struct m} : nat := match n, m with @@ -269,7 +273,7 @@ When we use parameters in patterns there is an error message: Set Asymmetric Patterns. Check (fun l:List nat => match l with - | nil => nil + | nil => nil _ | cons _ l' => l' end). Unset Asymmetric Patterns. @@ -291,7 +295,7 @@ By default, implicit arguments are omitted in patterns. So we write: end). But the possibility to use all the arguments is given by “``@``” implicit -explicitations (as for terms 2.7.11). +explicitations (as for terms, see :ref:`explicit-applications`). .. coqtop:: all @@ -325,7 +329,7 @@ Understanding dependencies in patterns We can define the function length over :g:`listn` by: -.. coqtop:: in +.. coqdoc:: Definition length (n:nat) (l:listn n) := n. @@ -367,6 +371,10 @@ 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 + + Reset concat. + The elimination predicate is :g:`fun (n:nat) (l:listn n) => listn (n+m)`. In general if :g:`m` has type :g:`(I q1 … qr t1 … ts)` where :g:`q1, …, qr` are parameters, the elimination predicate should be of the form :g:`fun y1 … ys x : (I q1 … qr y1 … ys ) => Q`. @@ -503,7 +511,7 @@ can also be caught in the matching. .. example:: - .. coqtop:: in + .. coqtop:: in reset Inductive list : nat -> Set := | nil : list 0 diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index e468cc63cd..cc788b3595 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: - .. coqtop:: in + .. coqdoc:: forall (A: Type) (S1 S1' S2 S2': list A), set_eq A S1 S1' -> @@ -205,7 +205,7 @@ Adding new relations and morphisms For Leibniz equality, we may declare: - .. coqtop:: in + .. coqdoc:: Add Parametric Relation (A : Type) : A (@eq A) [reflexivity proved by @refl_equal A] @@ -274,7 +274,7 @@ following command. (maximally inserted) implicit arguments. If ``A`` is always set as maximally implicit in the previous example, one can write: - .. coqtop:: in + .. coqdoc:: Add Parametric Relation A : (set A) eq_set reflexivity proved by eq_set_refl @@ -282,13 +282,8 @@ following command. transitivity proved by eq_set_trans as eq_set_rel. - .. coqtop:: in - Add Parametric Morphism A : (@union A) with signature eq_set ==> eq_set ==> eq_set as union_mor. - - .. coqtop:: in - Proof. exact (@union_compat A). Qed. We proceed now by proving a simple lemma performing a rewrite step and @@ -300,7 +295,7 @@ following command. .. coqtop:: in Goal forall (S : set nat), - eq_set (union (union S empty) S) (union S S). + eq_set (union (union S (empty nat)) S) (union S S). .. coqtop:: in @@ -486,7 +481,7 @@ registered as parametric relations and morphisms. .. example:: First class setoids - .. coqtop:: in + .. coqtop:: in reset Require Import Relation_Definitions Setoid. @@ -623,6 +618,10 @@ declared as morphisms in the ``Classes.Morphisms_Prop`` module. For example, to declare that universal quantification is a morphism for logical equivalence: +.. coqtop:: none + + Require Import Morphisms. + .. coqtop:: in Instance all_iff_morphism (A : Type) : @@ -632,6 +631,10 @@ logical equivalence: Proof. simpl_relation. +.. coqtop:: none + + Abort. + One then has to show that if two predicates are equivalent at every point, their universal quantifications are equivalent. Once we have declared such a morphism, it will be used by the setoid rewriting @@ -650,7 +653,7 @@ functional arguments (or whatever subrelation of the pointwise extension). For example, one could declare the ``map`` combinator on lists as a morphism: -.. coqtop:: in +.. coqdoc:: Instance map_morphism `{Equivalence A eqA, Equivalence B eqB} : Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B). @@ -714,47 +717,47 @@ following grammar: .. productionlist:: rewriting s, t, u : `strategy` - : | `lemma` - : | `lemma_right_to_left` - : | `failure` - : | `identity` - : | `reflexivity` - : | `progress` - : | `failure_catch` - : | `composition` - : | `left_biased_choice` - : | `iteration_one_or_more` - : | `iteration_zero_or_more` - : | `one_subterm` - : | `all_subterms` - : | `innermost_first` - : | `outermost_first` - : | `bottom_up` - : | `top_down` - : | `apply_hint` - : | `any_of_the_terms` - : | `apply_reduction` - : | `fold_expression` + : `lemma` + : `lemma_right_to_left` + : `failure` + : `identity` + : `reflexivity` + : `progress` + : `failure_catch` + : `composition` + : `left_biased_choice` + : `iteration_one_or_more` + : `iteration_zero_or_more` + : `one_subterm` + : `all_subterms` + : `innermost_first` + : `outermost_first` + : `bottom_up` + : `top_down` + : `apply_hint` + : `any_of_the_terms` + : `apply_reduction` + : `fold_expression` .. productionlist:: rewriting - strategy : "(" `s` ")" + strategy : ( `s` ) lemma : `c` - lemma_right_to_left : "<-" `c` - failure : `fail` - identity : `id` - reflexivity : `refl` - progress : `progress` `s` - failure_catch : `try` `s` - composition : `s` ";" `u` + lemma_right_to_left : <- `c` + failure : fail + identity : id + reflexivity : refl + progress : progress `s` + failure_catch : try `s` + composition : `s` ; `u` left_biased_choice : choice `s` `t` - iteration_one_or_more : `repeat` `s` - iteration_zero_or_more : `any` `s` + iteration_one_or_more : repeat `s` + iteration_zero_or_more : any `s` one_subterm : subterm `s` all_subterms : subterms `s` - innermost_first : `innermost` `s` - outermost_first : `outermost` `s` - bottom_up : `bottomup` `s` - top_down : `topdown` `s` + innermost_first : innermost `s` + outermost_first : outermost `s` + bottom_up : bottomup `s` + top_down : topdown `s` apply_hint : hints `hintdb` any_of_the_terms : terms (`c`)+ apply_reduction : eval `redexpr` @@ -767,7 +770,7 @@ primitive fixpoint operator: .. productionlist:: rewriting try `s` : choice `s` `id` any `s` : fix `u`. try (`s` ; `u`) - repeat `s` : `s` ; `any` `s` + repeat `s` : `s` ; any `s` bottomup s : fix `bu`. (choice (progress (subterms bu)) s) ; try bu topdown s : fix `td`. (choice s (progress (subterms td))) ; try td innermost s : fix `i`. (choice (subterm i) s) diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 64e2d7c4ab..d15aacad44 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -37,12 +37,12 @@ In addition to these user-defined classes, we have two built-in classes: * ``Funclass``, the class of functions; its objects are all the terms with a functional type, i.e. of form :g:`forall x:A,B`. -Formally, the syntax of a classes is defined as: +Formally, the syntax of classes is defined as: .. productionlist:: class: `qualid` - : | Sortclass - : | Funclass + : Sortclass + : Funclass Coercions @@ -184,10 +184,10 @@ Figure :ref:`vernacular` as follows: \comindex{Hypothesis \mbox{\rm (and coercions)}} .. productionlist:: - assumption : assumption_keyword assums . - assums : simple_assums - : | (simple_assums) ... (simple_assums) - simple_assums : ident ... ident :[>] term + assumption : `assumption_keyword` `assums` . + assums : `simple_assums` + : (`simple_assums`) ... (`simple_assums`) + simple_assums : `ident` ... `ident` :[>] `term` If the extra ``>`` is present before the type of some assumptions, these assumptions are declared as coercions. @@ -203,7 +203,7 @@ grammar of inductive types from Figure :ref:`vernacular` as follows: .. productionlist:: inductive : Inductive `ind_body` with ... with `ind_body` - : | CoInductive `ind_body` with ... with `ind_body` + : CoInductive `ind_body` with ... with `ind_body` ind_body : `ident` [ `binders` ] : `term` := [[|] `constructor` | ... | `constructor` ] constructor : `ident` [ `binders` ] [:[>] `term` ] @@ -289,7 +289,7 @@ by extending the existing :cmd:`Record` macro. Its new syntax is: The first identifier :token:`ident` is the name of the defined record and :token:`sort` is its type. The optional identifier after ``:=`` is the name - of the constuctor (it will be :n:`Build_@ident` if not given). + of the constructor (it will be :n:`Build_@ident` if not given). The other identifiers are the names of the fields, and :token:`term` are their respective types. If ``:>`` is used instead of ``:`` in the declaration of a field, then the name of this field is automatically @@ -365,7 +365,7 @@ We first give an example of coercion between atomic inductive types .. warning:: - Note that ``Check true=O`` would fail. This is "normal" behavior of + Note that ``Check (true = O)`` would fail. This is "normal" behavior of coercions. To validate ``true=O``, the coercion is searched from ``nat`` to ``bool``. There is none. diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index fd66de427c..e56b36caad 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -38,7 +38,7 @@ The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`. The syntax of the formulas is the following: - .. productionlist:: `F` + .. productionlist:: F F : A ∣ P ∣ True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F A : p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p p : c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n @@ -124,7 +124,7 @@ and checked to be :math:`-1`. that :tacn:`omega` does not solve, such as the following so-called *omega nightmare* :cite:`TheOmegaPaper`. -.. coqtop:: in +.. coqdoc:: Goal forall x y, 27 <= 11 * x + 13 * y <= 45 -> @@ -145,7 +145,7 @@ weakness, the :tacn:`lia` tactic is using recursively a combination of: + linear *positivstellensatz* refutations; + cutting plane proofs; + case split. - + Cutting plane proofs ~~~~~~~~~~~~~~~~~~~~~~ @@ -234,7 +234,8 @@ proof by abstracting monomials by variables. To illustrate the working of the tactic, consider we wish to prove the following Coq goal: -.. coqtop:: all +.. needs csdp +.. coqdoc:: Require Import ZArith Psatz. Open Scope Z_scope. @@ -250,6 +251,16 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. .. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with the ``zify`` tactic. +.. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by + pre-processing the goal with the ``Z.div_mod_to_equations`` tactic (you may + need to manually run ``zify`` first). +.. [#] Support for :g:`Z.quot` and :g:`Z.rem` may be obtained by pre-processing + the goal with the ``Z.quot_rem_to_equations`` tactic (you may need to manually + run ``zify`` first). +.. [#] Note that support for :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and + :g:`Z.rem` may be simultaneously obtained by pre-processing the goal with the + ``Z.to_euclidean_division_equations`` tactic (you may need to manually run + ``zify`` first). .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp .. [#] Variants deal with equalities and strict inequalities. .. [#] In practice, the oracle might fail to produce such a refutation. diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 8b7214e2ab..903ee115c9 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -52,7 +52,7 @@ in interactive mode. It is not strictly mandatory in batch mode if it is not the first time the file is compiled and if the file itself did not change. When the proof does not begin with Proof using, the system records in an -auxiliary file, produced along with the `.vo` file, the list of section +auxiliary file, produced along with the ``.vo`` file, the list of section variables used. Automatic suggestion of proof annotations @@ -154,22 +154,22 @@ to a worker process. The threshold can be configured with Batch mode --------------- -When |Coq| is used as a batch compiler by running `coqc` or `coqtop` --compile, it produces a `.vo` file for each `.v` file. A `.vo` file contains, -among other things, theorem statements and proofs. Hence to produce a -.vo |Coq| need to process all the proofs of the `.v` file. +When |Coq| is used as a batch compiler by running ``coqc``, it produces +a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other +things, theorem statements and proofs. Hence to produce a .vo |Coq| +need to process all the proofs of the ``.v`` file. The asynchronous processing of proofs can decouple the generation of a -compiled file (like the `.vo` one) that can be loaded by ``Require`` from the +compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the generation and checking of the proof objects. The ``-quick`` flag can be -passed to `coqc` or `coqtop` to produce, quickly, `.vio` files. -Alternatively, when using a Makefile produced by `coq_makefile`, +passed to ``coqc`` or ``coqtop`` to produce, quickly, ``.vio`` files. +Alternatively, when using a Makefile produced by ``coq_makefile``, the ``quick`` target can be used to compile all files using the ``-quick`` flag. -A `.vio` file can be loaded using ``Require`` exactly as a `.vo` file but +A ``.vio`` file can be loaded using ``Require`` exactly as a ``.vo`` file but proofs will not be available (the Print command produces an error). Moreover, some universe constraints might be missing, so universes -inconsistencies might go unnoticed. A `.vio` file does not contain proof +inconsistencies might go unnoticed. A ``.vio`` file does not contain proof objects, but proof tasks, i.e. what a worker process can transform into a proof object. @@ -177,52 +177,52 @@ Compiling a set of files with the ``-quick`` flag allows one to work, interactively, on any file without waiting for all the proofs to be checked. -When working interactively, one can fully check all the `.v` files by -running `coqc` as usual. +When working interactively, one can fully check all the ``.v`` files by +running ``coqc`` as usual. -Alternatively one can turn each `.vio` into the corresponding `.vo`. All +Alternatively one can turn each ``.vio`` into the corresponding ``.vo``. All .vio files can be processed in parallel, hence this alternative might be faster. The command ``coqtop -schedule-vio2vo 2 a b c`` can be used to -obtain a good scheduling for two workers to produce `a.vo`, `b.vo`, and -`c.vo`. When using a Makefile produced by `coq_makefile`, the ``vio2vo`` target -can be used for that purpose. Variable `J` should be set to the number +obtain a good scheduling for two workers to produce ``a.vo``, ``b.vo``, and +``c.vo``. When using a Makefile produced by ``coq_makefile``, the ``vio2vo`` target +can be used for that purpose. Variable ``J`` should be set to the number of workers, e.g. ``make vio2vo J=2``. The only caveat is that, while the -.vo files obtained from `.vio` files are complete (they contain all proof +.vo files obtained from ``.vio`` files are complete (they contain all proof terms and universe constraints), the satisfiability of all universe constraints has not been checked globally (they are checked to be consistent for every single proof). Constraints will be checked when -these `.vo` files are (recursively) loaded with ``Require``. +these ``.vo`` files are (recursively) loaded with ``Require``. There is an extra, possibly even faster, alternative: just check the -proof tasks stored in `.vio` files without producing the `.vo` files. This +proof tasks stored in ``.vio`` files without producing the ``.vo`` files. This is possibly faster because all the proof tasks are independent, hence one can further partition the job to be done between workers. The ``coqtop -schedule-vio-checking 6 a b c`` command can be used to obtain a -good scheduling for 6 workers to check all the proof tasks of `a.vio`, -`b.vio`, and `c.vio`. Auxiliary files are used to predict how long a proof +good scheduling for 6 workers to check all the proof tasks of ``a.vio``, +``b.vio``, and ``c.vio``. Auxiliary files are used to predict how long a proof task will take, assuming it will take the same amount of time it took last time. When using a Makefile produced by coq_makefile, the -``checkproofs`` target can be used to check all `.vio` files. Variable `J` +``checkproofs`` target can be used to check all ``.vio`` files. Variable ``J`` should be set to the number of workers, e.g. ``make checkproofs J=6``. As -when converting `.vio` files to `.vo` files, universe constraints are not +when converting ``.vio`` files to ``.vo`` files, universe constraints are not checked to be globally consistent. Hence this compilation mode is only useful for quick regression testing and on developments not making -heavy use of the `Type` hierarchy. +heavy use of the ``Type`` hierarchy. Limiting the number of parallel workers -------------------------------------------- Many |Coq| processes may run on the same computer, and each of them may -start many additional worker processes. The `coqworkmgr` utility lets +start many additional worker processes. The ``coqworkmgr`` utility lets one limit the number of workers, globally. The utility accepts the ``-j`` argument to specify the maximum number of -workers (defaults to 2). `coqworkmgr` automatically starts in the +workers (defaults to 2). ``coqworkmgr`` automatically starts in the background and prints an environment variable assignment like ``COQWORKMGR_SOCKET=localhost:45634``. The user must set this variable in all the shells from which |Coq| processes will be started. If one uses just one terminal running the bash shell, then ``export ‘coqworkmgr -j 4‘`` will do the job. -After that, all |Coq| processes, e.g. `coqide` and `coqc`, will respect the +After that, all |Coq| processes, e.g. ``coqide`` and ``coqc``, will respect the limit, globally. diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 99d689132d..20e4c6a3d6 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -197,7 +197,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: -.. coqtop:: in +.. coqdoc:: Record ring_theory : Prop := mk_rt { Radd_0_l : forall x, 0 + x == x; @@ -235,7 +235,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: -.. coqtop:: in +.. coqdoc:: Record ring_morph : Prop := mkmorph { morph0 : [cO] == 0; @@ -285,13 +285,14 @@ following property: .. coqtop:: in + Require Import Reals. Section POWER. Variable Cpow : Set. Variable Cp_phi : N -> Cpow. Variable rpow : R -> Cpow -> R. Record power_theory : Prop := mkpow_th { - rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n) + rpow_pow_N : forall r n, rpow r (Cp_phi n) = pow_N 1%R Rmult r n }. End POWER. @@ -308,13 +309,13 @@ The syntax for adding a new ring is .. productionlist:: coq ring_mod : abstract | decidable `term` | morphism `term` - : | setoid `term` `term` - : | constants [`ltac`] - : | preprocess [`ltac`] - : | postprocess [`ltac`] - : | power_tac `term` [`ltac`] - : | sign `term` - : | div `term` + : setoid `term` `term` + : constants [`ltac`] + : preprocess [`ltac`] + : postprocess [`ltac`] + : power_tac `term` [`ltac`] + : sign `term` + : div `term` abstract declares the ring as abstract. This is the default. @@ -422,7 +423,7 @@ The interested reader is strongly advised to have a look at the file ``Ring_polynom.v``. Here a type for polynomials is defined: -.. coqtop:: in +.. coqdoc:: Inductive PExpr : Type := | PEc : C -> PExpr @@ -437,7 +438,7 @@ file ``Ring_polynom.v``. Here a type for polynomials is defined: Polynomials in normal form are defined as: -.. coqtop:: in +.. coqdoc:: Inductive Pol : Type := | Pc : C -> Pol @@ -454,7 +455,7 @@ polynomial to an element of the concrete ring, and the second one that does the same for normal forms: -.. coqtop:: in +.. coqdoc:: Definition PEeval : list R -> PExpr -> R := [...]. @@ -465,7 +466,7 @@ A function to normalize polynomials is defined, and the big theorem is its correctness w.r.t interpretation, that is: -.. coqtop:: in +.. coqdoc:: Definition norm : PExpr -> Pol := [...]. Lemma Pphi_dev_ok : @@ -616,7 +617,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: -.. coqtop:: in +.. coqdoc:: Record field_theory : Prop := mk_field { F_R : ring_theory rO rI radd rmul rsub ropp req; @@ -636,7 +637,7 @@ fields and semifields is: The result of the normalization process is a fraction represented by the following type: -.. coqtop:: in +.. coqdoc:: Record linear : Type := mk_linear { num : PExpr C; @@ -690,7 +691,7 @@ for |Coq|’s type checker. Let us see why: x + 3 + y + y * z = x + 3 + y + z * y. intros; rewrite (Zmult_comm y z); reflexivity. Save foo. - Print foo. + Print foo. At each step of rewriting, the whole context is duplicated in the proof term. Then, a tactic that does hundreds of rewriting generates diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 04aedd0cf6..6b10b7c0b3 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -223,7 +223,7 @@ The following is an example of a record with non-trivial subtyping relation: E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j -Cumulative inductive types, coninductive types, variants and records +Cumulative inductive types, coinductive types, variants and records only make sense when they are universe polymorphic. Therefore, an error is issued whenever the user uses the :g:`Cumulative` or :g:`NonCumulative` prefix in a monomorphic context. @@ -236,11 +236,11 @@ Consider the following examples. .. coqtop:: all reset - Monomorphic Cumulative Inductive Unit := unit. + Fail Monomorphic Cumulative Inductive Unit := unit. .. coqtop:: all reset - Monomorphic NonCumulative Inductive Unit := unit. + Fail Monomorphic NonCumulative Inductive Unit := unit. .. coqtop:: all reset |