diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/canonical-structures.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 30 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 23 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 33 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 6 |
8 files changed, 70 insertions, 62 deletions
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 3e414a714c..a9d894cab5 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -313,7 +313,9 @@ 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 +.. FIXME shouldn't warn + +.. coqtop:: all warn Module Add_instance_attempt. @@ -418,7 +420,9 @@ the reader can refer to :cite:`CSwcu`. The declaration of canonical instances can now be way more compact: -.. coqtop:: all +.. FIXME should not warn + +.. coqtop:: all warn Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. 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 b606fb4dd2..b474c51f17 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,12 +618,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 + + Require Import Morphisms. + .. coqtop:: in Instance all_iff_morphism (A : Type) : Proper (pointwise_relation A iff ==> iff) (@all A). -.. coqtop:: all +.. coqtop:: all abort Proof. simpl_relation. @@ -650,7 +649,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). diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index e5b41be691..d15aacad44 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -37,7 +37,7 @@ 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` @@ -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 b076aac1ed..e56b36caad 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -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 -> @@ -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. diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 8204d93fa7..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. @@ -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/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 43d302114e..c7ea7e326f 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -44,25 +44,20 @@ Leibniz equality on some type. An example implementation is: eqb_leibniz x y H := match x, y return x = y with tt, tt => eq_refl tt end }. -If one does not give all the members in the Instance declaration, Coq -enters the proof-mode and the user is asked to build inhabitants of -the remaining fields, e.g.: +Using :cmd:`Program Instance`, if one does not give all the members in +the Instance declaration, Coq generates obligations for the remaining +fields, e.g.: .. coqtop:: in - Instance eq_bool : EqDec bool := + Require Import Program.Tactics. + Program Instance eq_bool : EqDec bool := { eqb x y := if x then y else negb y }. .. coqtop:: all - Proof. intros x y H. - -.. coqtop:: all - - destruct x ; destruct y ; (discriminate || reflexivity). - -.. coqtop:: all - + Next Obligation. + destruct x ; destruct y ; (discriminate || reflexivity). Defined. One has to take care that the transparency of every field is @@ -131,14 +126,14 @@ the constraints as a binding context before the instance, e.g.: .. coqtop:: in - Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := + 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 - Abort. + Admit Obligations. These instances are used just as well as lemmas in the instance hint database. @@ -157,13 +152,13 @@ vernacular, except it accepts any binding context as argument. For example: Context `{EA : EqDec A}. - Global Instance option_eqb : EqDec (option A) := + Global Program Instance option_eqb : EqDec (option A) := { eqb x y := match x, y with | Some x, Some y => eqb x y | None, None => true | _, _ => false end }. - Admitted. + Admit Obligations. End EqDec_defs. @@ -564,12 +559,12 @@ Settings This flag allows to switch the behavior of instance declarations made through the Instance command. - + When it is on (the default), instances that have unsolved holes in + + When it is off (the default), they fail with an error instead. + + + When it is on, instances that have unsolved holes in their proof-term silently open the proof mode with the remaining obligations to prove. - + When it is off, they fail with an error instead. - Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ 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 |