From f78d36363698f653ff8ff16389c58633579493eb Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 7 Feb 2019 11:45:10 +0100 Subject: Fix failing coqtops in extended-pattern-matching.rst --- doc/sphinx/addendum/extended-pattern-matching.rst | 28 +++++++++++++++-------- 1 file changed, 18 insertions(+), 10 deletions(-) (limited to 'doc/sphinx/addendum') diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 7b8a86d1ab..d77690458d 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. @@ -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 -- cgit v1.2.3 From d32a0db7b4d0775820b306badfe8072bd74cf62d Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 7 Feb 2019 11:51:08 +0100 Subject: Fix failing coqtops in generalized-rewriting.rst --- doc/sphinx/addendum/generalized-rewriting.rst | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) (limited to 'doc/sphinx/addendum') diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index b606fb4dd2..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). -- cgit v1.2.3 From e5fb9c5cbce5e7e7e8fcb3d82c45074f9c165158 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 7 Feb 2019 11:56:19 +0100 Subject: Fix failing coqtops in micromega.rst (the main one requires csdp) Maybe we should still let it run but let's disable it until we install csdp on the build server at least. --- doc/sphinx/addendum/micromega.rst | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'doc/sphinx/addendum') 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. -- cgit v1.2.3 From 75269e1b3fb98c8095b7f50e8ade2af87eb4061f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 7 Feb 2019 12:15:21 +0100 Subject: Fix failing coqtops in ring.rst --- doc/sphinx/addendum/ring.rst | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) (limited to 'doc/sphinx/addendum') 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 -- cgit v1.2.3 From 7104904f9f6e1a5e1b1590bd898ae20cb7178daf Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 7 Feb 2019 12:29:39 +0100 Subject: Fix failing coqtops universe-polymorphism.rst --- doc/sphinx/addendum/universe-polymorphism.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc/sphinx/addendum') 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 -- cgit v1.2.3