diff options
| -rw-r--r-- | Makefile.doc | 1 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 28 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 25 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 6 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 26 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 26 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 192 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 14 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 5 |
17 files changed, 217 insertions, 168 deletions
diff --git a/Makefile.doc b/Makefile.doc index 7ac710b8c9..4b2dd8ed4d 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -54,6 +54,7 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex doc: refman stdlib +SPHINX_DEPS ?= ifndef QUICK SPHINX_DEPS := coq endif 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 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). 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/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 diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 39047f4f23..9d2afc080f 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -28,7 +28,7 @@ from shutil import copyfile import sphinx # Increase recursion limit for sphinx -sys.setrecursionlimit(1500) +sys.setrecursionlimit(3000) # If extensions (or modules to document with autodoc) are in another directory, # add these directories to sys.path here. If the directory is relative to the diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 962d2a94e3..a70cd4032d 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -782,7 +782,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` Inductive even : nat -> Prop := | even_O : even 0 | even_S : forall n, odd n -> even (S n) - with odd : nat -> prop := + with odd : nat -> Prop := | odd_S : forall n, even n -> odd (S n). @@ -929,7 +929,7 @@ condition* for a constant :math:`X` in the following cases: Inductive nattree (A:Type) : Type := | leaf : nattree A - | node : A -> (nat -> nattree A) -> nattree A. + | natnode : A -> (nat -> nattree A) -> nattree A. Then every instantiated constructor of ``nattree A`` satisfies the nested positivity condition for ``nattree``: @@ -939,7 +939,7 @@ condition* for a constant :math:`X` in the following cases: type of that constructor (primarily because ``nattree`` does not have any (real) arguments) ... (bullet 1) - + Type ``A → (nat → nattree A) → nattree A`` of constructor ``node`` satisfies the + + Type ``A → (nat → nattree A) → nattree A`` of constructor ``natnode`` satisfies the positivity condition for ``nattree`` because: - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 1) diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index b82b3b0e80..963242ea72 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -146,7 +146,7 @@ Propositional Connectives First, we find propositional calculus connectives: -.. coqtop:: in +.. coqdoc:: Inductive True : Prop := I. Inductive False : Prop := . @@ -236,7 +236,7 @@ Finally, a few easy lemmas are provided. single: eq_rect (term) single: eq_rect_r (term) -.. coqtop:: in +.. coqdoc:: Theorem absurd : forall A C:Prop, A -> ~ A -> C. Section equality. @@ -271,6 +271,10 @@ For instance ``f_equal3`` is defined the following way. (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3. +.. coqtop:: none + + Abort. + .. _datatypes: Datatypes @@ -465,7 +469,7 @@ Intuitionistic Type Theory. single: Choice2 (term) single: bool_choice (term) -.. coqtop:: in +.. coqdoc:: Lemma Choice : forall (S S':Set) (R:S -> S' -> Prop), @@ -506,7 +510,7 @@ realizability interpretation. single: absurd_set (term) single: and_rect (term) -.. coqtop:: in +.. coqdoc:: Definition except := False_rec. Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. @@ -531,7 +535,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 + .. coqtop:: in reset Fixpoint even (n:nat) : bool := match n with @@ -558,7 +562,7 @@ section :tacn:`refine`). This scope is opened by default. Now comes the content of module ``Peano``: -.. coqtop:: in +.. coqdoc:: Theorem eq_S : forall x y:nat, x = y -> S x = S y. Definition pred (n:nat) : nat := @@ -610,7 +614,7 @@ Finally, it gives the definition of the usual orderings ``le``, Inductive le (n:nat) : nat -> Prop := | le_n : le n n - | le_S : forall m:nat, n <= m -> n <= (S m). + | le_S : forall m:nat, n <= m -> n <= (S m) where "n <= m" := (le n m) : nat_scope. Definition lt (n m:nat) := S n <= m. Definition ge (n m:nat) := m <= n. @@ -625,7 +629,7 @@ induction principle. single: nat_case (term) single: nat_double_ind (term) -.. coqtop:: in +.. coqdoc:: Theorem nat_case : forall (n:nat) (P:nat -> Prop), @@ -652,7 +656,7 @@ well-founded induction, in module ``Wf.v``. single: Acc_rect (term) single: well_founded (term) -.. coqtop:: in +.. coqdoc:: Section Well_founded. Variable A : Type. @@ -681,7 +685,7 @@ fixpoint equation can be proved. single: Fix_F_inv (term) single: Fix_F_eq (term) -.. coqtop:: in +.. coqdoc:: Section FixPoint. Variable P : A -> Type. @@ -715,7 +719,7 @@ of equality: .. coqtop:: in Inductive identity (A:Type) (a:A) : A -> Type := - identity_refl : identity a a. + identity_refl : identity A a a. Some properties of ``identity`` are proved in the module ``Logic_Type``, which also provides the definition of ``Type`` level negation: diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 50a56f1d51..437b8e557e 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1970,6 +1970,10 @@ in :ref:`canonicalstructures`; here only a simple example is given. Lemma is_law_S : is_law S. + .. coqtop:: none + + Abort. + .. note:: If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. @@ -2019,10 +2023,10 @@ or :g:`m` to the type :g:`nat` of natural numbers). Implicit Types m n : nat. Lemma cons_inj_nat : forall m n l, n :: l = m :: l -> n = m. - - intros m n. + Proof. intros m n. Abort. Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m. + Abort. .. cmdv:: Implicit Type @ident : @type diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 5ecf007eff..9ab3f905e6 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -434,6 +434,10 @@ 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 + + Reset bool_case. + .. coqtop:: in Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := @@ -471,7 +475,7 @@ For instance, in the following example: 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 - | eq_refl _ => eq_refl A x + | eq_refl _ _ => eq_refl A x end. the type of the branch is :g:`eq A x x` because the third argument of @@ -826,6 +830,10 @@ Simple inductive types .. example:: + .. coqtop:: none + + Reset nat. + .. coqtop:: in Inductive nat : Set := O | S (_:nat). @@ -904,6 +912,10 @@ Parametrized inductive types Once again, it is possible to specify only the type of the arguments of the constructors, and to omit the type of the conclusion: + .. coqtop:: none + + Reset list. + .. coqtop:: in Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A). @@ -949,7 +961,7 @@ Parametrized inductive types inductive definitions are abstracted over their parameters before type checking constructors, allowing to write: - .. coqtop:: all undo + .. coqtop:: all Set Uniform Inductive Parameters. Inductive list3 (A:Set) : Set := @@ -960,7 +972,7 @@ Parametrized inductive types and using :cmd:`Context` to give the uniform parameters, like so (cf. :ref:`section-mechanism`): - .. coqtop:: all undo + .. coqtop:: all reset Section list3. Context (A:Set). @@ -1038,7 +1050,7 @@ Mutually defined inductive types two type variables :g:`A` and :g:`B`, the declaration should be done the following way: - .. coqtop:: in + .. coqdoc:: Inductive tree (A B:Set) : Set := node : A -> forest A B -> tree A B @@ -1130,6 +1142,10 @@ found in e.g. Agda, and preserves subject reduction. The above example can be rewritten in the following way. +.. coqtop:: none + + Reset Stream. + .. coqtop:: all Set Primitive Projections. @@ -1147,7 +1163,7 @@ axiom. .. coqtop:: all - Axiom Stream_eta : forall s: Stream, s = cons (hs s) (tl s). + Axiom Stream_eta : forall s: Stream, s = Seq (hd s) (tl s). More generally, as in the case of positive coinductive types, it is consistent to further identify extensional equality of coinductive types with propositional diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 9455228e7d..8b7fe20191 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -230,10 +230,12 @@ mathematical symbols ∀ and ∃, you may define: .. coqtop:: in - Notation "∀ x : T, P" := - (forall x : T, P) (at level 200, x ident). - Notation "∃ x : T, P" := - (exists x : T, P) (at level 200, x ident). + Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) + : type_scope. + Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..) + (at level 200, x binder, y binder, right associativity) + : type_scope. There exists a small set of such notations already defined, in the file `utf8.v` of Coq library, so you may enable them just by diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 442077616f..4f486a777d 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -859,6 +859,10 @@ We can carry out pattern matching on terms with: Goal True. f (3+4). + .. coqtop:: none + + Abort. + .. _ltac-match-goal: Pattern matching on goals @@ -1026,6 +1030,10 @@ Counting the goals all:pr_numgoals. + .. coqtop:: none + + Abort. + Testing boolean expressions ~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 483dbd311d..ec97377128 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -233,7 +233,7 @@ construct differs from the latter in that .. coqtop:: reset all - Definition f u := let (m, n) := u in m + n. + Fail Definition f u := let (m, n) := u in m + n. The ``let:`` construct is just (more legible) notation for the primitive @@ -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 undo + .. coqtop:: 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 - .. coqtop:: all undo + .. coqdoc:: Set Implicit Arguments. Unset Strict Implicit. @@ -505,7 +505,7 @@ Definitions |SSR| pose tactic supports *open syntax*: the body of the definition does not need surrounding parentheses. For instance: -.. coqtop:: in +.. coqdoc:: pose t := x + y. @@ -534,7 +534,7 @@ The |SSR| pose tactic also supports (co)fixpoints, by providing the local counterpart of the ``Fixpoint f := …`` and ``CoFixpoint f := …`` constructs. For instance, the following tactic: -.. coqtop:: in +.. coqdoc:: 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: -.. coqtop:: in +.. coqdoc:: 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: -.. coqtop:: in +.. coqdoc:: pose f := _ + 1. is shorthand for: -.. coqtop:: in +.. coqdoc:: 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: -.. coqtop:: in +.. coqdoc:: pose f x := x + _. is shorthand for: -.. coqtop:: in +.. coqdoc:: pose f n x := x + n. @@ -580,13 +580,13 @@ The interaction of the pose tactic with the interpretation of implicit arguments results in a powerful and concise syntax for local definitions involving dependent types. For instance, the tactic: -.. coqtop:: in +.. coqdoc:: pose f x y := (x, y). adds to the context the local definition: -.. coqtop:: in +.. coqdoc:: pose f (Tx Ty : Type) (x : Tx) (y : Ty) := (x, y). @@ -766,7 +766,7 @@ Moreover: .. coqtop:: all Lemma test : forall x : nat, x + 1 = 0. - set t := _ + 1. + Fail set t := _ + 1. + Typeclass inference should fill in any residual hole, but matching should never assign a value to a global existential variable. @@ -889,7 +889,7 @@ only one occurrence of the selected term. .. coqtop:: all Lemma test x y z : (x + y) + (z + z) = z + z. - set a := {2}(_ + _). + Fail set a := {2}(_ + _). .. _basic_localization_ssr: @@ -1079,7 +1079,7 @@ constants to the goal. Because they are tacticals, ``:`` and ``=>`` can be combined, as in -.. coqtop:: in +.. coqdoc:: move: m le_n_m => p le_n_p. @@ -1139,7 +1139,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 -.. coqtop:: in +.. coqdoc:: elim=> [|m IHm] n le_n. @@ -1150,7 +1150,7 @@ explained in terms of the goal stack:: is basically equivalent to -.. coqtop:: in +.. coqdoc:: move: a H1 H2; tactic => a H1 H2. @@ -1163,13 +1163,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 -.. coqtop:: in +.. coqdoc:: elim: n => [|n IHn] in m le_n_m *. instead of -.. coqtop:: in +.. coqdoc:: elim: n m le_n_m => [|n IHn] m le_n_m. @@ -1398,7 +1398,7 @@ Switches affect the discharging of a :token:`d_item` as follows: For example, the tactic: -.. coqtop:: in +.. coqdoc:: move: n {2}n (refl_equal n). @@ -1409,7 +1409,7 @@ For example, the tactic: Therefore this tactic changes any goal ``G`` into -.. coqtop:: +.. coqdoc:: forall n n0 : nat, n = n0 -> G. @@ -1843,7 +1843,7 @@ Generation of equations The generation of named equations option stores the definition of a new constant as an equation. The tactic: -.. coqtop:: in +.. coqdoc:: move En: (size l) => n. @@ -1851,7 +1851,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: -.. coqtop:: in +.. coqdoc:: pose n := (size l). @@ -1936,7 +1936,7 @@ be substituted. inferred looking at the type of the top assumption. This allows for the compact syntax: - .. coqtop:: in + .. coqdoc:: case: {2}_ / eqP. @@ -2112,7 +2112,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: -.. coqtop:: in +.. coqdoc:: by apply/eqP; rewrite -dvdn1. @@ -2147,13 +2147,13 @@ A natural and common way of closing a goal is to apply a lemma which is the exact one needed for the goal to be solved. The defective form of the tactic: -.. coqtop:: in +.. coqdoc:: exact. is equivalent to: -.. coqtop:: in +.. coqdoc:: do [done | by move=> top; apply top]. @@ -2161,13 +2161,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: -.. coqtop:: in +.. coqdoc:: exact: MyLemma. is equivalent to: -.. coqtop:: in +.. coqdoc:: by apply: MyLemma. @@ -2179,19 +2179,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: - .. coqtop:: in + .. coqdoc:: by rewrite my_lemma1. succeeds, then the tactic: - .. coqtop:: in + .. coqdoc:: by rewrite my_lemma1; apply my_lemma2. usually fails since it is equivalent to: - .. coqtop:: in + .. coqdoc:: by (rewrite my_lemma1; apply my_lemma2). @@ -2247,7 +2247,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 -.. coqtop:: in +.. coqdoc:: tactic ; last k [ tactic1 |…| tacticm ] || tacticn. @@ -2262,7 +2262,6 @@ to the others. .. coqtop:: reset - Abort. From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. @@ -2296,13 +2295,13 @@ Iteration A tactic of the form: -.. coqtop:: in +.. coqdoc:: do [ tactic 1 | … | tactic n ]. is equivalent to the standard Ltac expression: -.. coqtop:: in +.. coqdoc:: first [ tactic 1 | … | tactic n ]. @@ -2327,14 +2326,14 @@ Their meaning is: For instance, the tactic: -.. coqtop:: in +.. coqdoc:: 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: -.. coqtop:: in +.. coqdoc:: tactic; do 2! rewrite mult_comm. @@ -2518,7 +2517,7 @@ tactics of the form: which behave like: -.. coqtop:: in +.. coqdoc:: have: term ; first by tactic. move=> clear_switch i_item. @@ -2531,7 +2530,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: -.. coqtop:: in +.. coqdoc:: have H23 : 3 + 2 = 2 + 3 by rewrite addnC. @@ -2559,7 +2558,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): -.. coqtop:: in +.. coqdoc:: have {x} -> : x = y. @@ -2635,7 +2634,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:: in +.. coqdoc:: have (x) : 2 * x = x + x by omega. @@ -2816,7 +2815,7 @@ The + but the optional clear item is still performed in the *second* branch. This means that the tactic: - .. coqtop:: in + .. coqdoc:: suff {H} H : forall x : nat, x >= 0. @@ -2888,7 +2887,7 @@ name of the local definition with the ``@`` character. In the second subgoal, the tactic: -.. coqtop:: in +.. coqdoc:: move=> clear_switch i_item. @@ -2995,10 +2994,13 @@ illustrated in the following example. the pattern ``id (addx x)``, that would produce the following first subgoal - .. coqtop:: none + .. coqtop:: none reset + + From Coq Require Import ssreflect Omega. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. - Abort All. - From Coq Require Import Omega. Section Test. Variable x : nat. Definition addx z := z + x. @@ -3153,7 +3155,7 @@ An :token:`r_item` can be: Definition f := fun x y => x + y. Lemma test x y : x + y = f y x. - rewrite -[f y]/(y + _). + Fail rewrite -[f y]/(y + _). but the following script succeeds @@ -3192,7 +3194,7 @@ tactics. In a rewrite tactic of the form: -.. coqtop:: in +.. coqdoc:: rewrite occ_switch [term1]term2. @@ -3235,7 +3237,7 @@ Performing rewrite and simplification operations in a single tactic enhances significantly the concision of scripts. For instance the tactic: -.. coqtop:: in +.. coqdoc:: rewrite /my_def {2}[f _]/= my_eq //=. @@ -3316,7 +3318,7 @@ the equality. .. coqtop:: all Lemma test (H : forall t u, t + u * 0 = t) x y : x + y * 4 + 2 * 0 = x + 2 * 0. - rewrite [x + _]H. + Fail rewrite [x + _]H. Indeed the left hand side of ``H`` does not match the redex identified by the pattern ``x + y * 4``. @@ -3498,7 +3500,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: -.. coqtop:: in +.. coqdoc:: Lemma addE : add =2 addn. Lemma doubleE : double =1 doublen. @@ -3514,7 +3516,7 @@ hand side. In order to reason conveniently on expressions involving the efficient operations, we gather all these rules in the definition ``trecE``: -.. coqtop:: in +.. coqdoc:: Definition trecE := (addE, (doubleE, oddE), (mulE, add_mulE, (expE, mul_expE))). @@ -3572,14 +3574,14 @@ cases: + |SSR| never accepts to rewrite indeterminate patterns like: - .. coqtop:: in + .. coqdoc:: Lemma foo (x : unit) : x = tt. |SSR| will however accept the ηζ expansion of this rule: - .. coqtop:: in + .. coqdoc:: Lemma fubar (x : unit) : (let u := x in u) = tt. @@ -3617,7 +3619,7 @@ cases: .. coqtop:: all - rewrite H. + Fail rewrite H. Rewriting with ``H`` first requires unfolding the occurrences of ``f`` @@ -3729,7 +3731,7 @@ copy of any term t. However this copy is (on purpose) *not convertible* to t in the |Coq| system [#8]_. The job is done by the following construction: -.. coqtop:: in +.. coqdoc:: Lemma master_key : unit. Proof. exact tt. Qed. Definition locked A := let: tt := master_key in fun x : A => x. @@ -3793,14 +3795,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*: -.. coqtop:: in +.. coqdoc:: Notation "'nosimpl' t" := (let: tt := tt in t). The term ``(nosimpl t)`` simplifies to ``t`` *except* in a definition. More precisely, given: -.. coqtop:: in +.. coqdoc:: Definition foo := (nosimpl bar). @@ -3816,7 +3818,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: - .. coqtop:: in + .. coqdoc:: Definition foo x := nosimpl (bar x). @@ -3824,14 +3826,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: - .. coqtop:: in + .. coqdoc:: Definition foo x := nosimpl bar x. A standard example making this technique shine is the case of arithmetic operations. We define for instance: -.. coqtop:: in +.. coqdoc:: Definition addn := nosimpl plus. @@ -3851,7 +3853,7 @@ Congruence Because of the way matching interferes with parameters of type families, the tactic: -.. coqtop:: in +.. coqdoc:: apply: my_congr_property. @@ -4047,7 +4049,7 @@ For a quick glance at what can be expressed with the last :token:`r_pattern` consider the goal ``a = b`` and the tactic -.. coqtop:: in +.. coqdoc:: rewrite [in X in _ = X]rule. @@ -4148,14 +4150,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``. -.. coqtop:: in +.. coqdoc:: set t := ((a in A)). Contextual patterns can also be used as arguments of the ``:`` tactical. For example: -.. coqtop:: in +.. coqdoc:: elim: n (n in _ = n) (refl_equal n). @@ -4246,7 +4248,7 @@ context shortcuts. The following example is taken from ``ssreflect.v`` where the ``LHS`` and ``RHS`` shortcuts are defined. -.. coqtop:: in +.. coqdoc:: Notation RHS := (X in _ = X)%pattern. Notation LHS := (X in X = _)%pattern. @@ -4254,7 +4256,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: -.. coqtop:: in +.. coqdoc:: set rhs := RHS. rewrite [in RHS]rule. @@ -4287,13 +4289,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: -.. coqtop:: in +.. coqdoc:: elim/V. is a synonym for: -.. coqtop:: in +.. coqdoc:: intro top; elim top using V; clear top. @@ -4303,13 +4305,13 @@ Since an elimination view supports the two bookkeeping tacticals of discharge and introduction (see section :ref:`basic_tactics_ssr`), the |SSR| tactic: -.. coqtop:: in +.. coqdoc:: elim/V: x => y. is a synonym for: -.. coqtop:: in +.. coqdoc:: elim x using V; clear x; intro y. @@ -4367,13 +4369,13 @@ command) can be combined with the type family switches described in section :ref:`type_families_ssr`. Consider an eliminator ``foo_ind`` of type: -.. coqtop:: in +.. coqdoc:: foo_ind : forall …, forall x : T, P p1 … pm. and consider the tactic: -.. coqtop:: in +.. coqdoc:: elim/foo_ind: e1 … / en. @@ -4424,7 +4426,7 @@ Here is an example of a regular, but nontrivial, eliminator. The following tactics are all valid and perform the same elimination on this goal. - .. coqtop:: in + .. coqdoc:: elim/plus_ind: z / (plus _ z). elim/plus_ind: {z}(plus _ z). @@ -4473,7 +4475,7 @@ Here is an example of a regular, but nontrivial, eliminator. .. coqtop:: all - elim/plus_ind: y / _. + Fail elim/plus_ind: y / _. triggers an error: in the conclusion of the ``plus_ind`` eliminator, the first argument of the predicate @@ -4494,7 +4496,7 @@ Here is an example of a truncated eliminator: Unset Printing Implicit Defensive. Section Test. - .. coqtop:: in + .. coqdoc:: 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 -> @@ -4505,7 +4507,7 @@ Here is an example of a truncated eliminator: where the type of the ``big_prop`` eliminator is - .. coqtop:: in + .. coqdoc:: big_prop: forall (R : Type) (Pb : R -> Type) (idx : R) (op1 : R -> R -> R), Pb idx -> @@ -4518,7 +4520,7 @@ Here is an example of a truncated eliminator: inferred one is used instead: ``big[_/_]_(i <- _ | _ i) _ i``, and after the introductions, the following goals are generated: - .. coqtop:: in + .. coqdoc:: subgoal 1 is: p %| 1 -> exists2 x : nat * nat, x \in prime_decomp n & p = x.1 @@ -4624,7 +4626,7 @@ equation name generation mechanism (see section :ref:`generation_of_equations_ss This view tactic performs: - .. coqtop:: in + .. coqdoc:: move=> HQ; case: {HQ}(Q2P HQ) => [HPa | HPb]. @@ -4661,14 +4663,14 @@ relevant for the current goal. the double implication into the expected simple implication. The last script is in fact equivalent to: - .. coqtop:: in + .. coqdoc:: Lemma test a b : P (a || b) -> True. move/(iffLR (PQequiv _ _)). where: - .. coqtop:: in + .. coqdoc:: Lemma iffLR P Q : (P <-> Q) -> P -> Q. @@ -4810,7 +4812,7 @@ decidable predicate to its boolean version. First, booleans are injected into propositions using the coercion mechanism: -.. coqtop:: in +.. coqdoc:: Coercion is_true (b : bool) := b = true. @@ -4827,7 +4829,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: -.. coqtop:: in +.. coqdoc:: Inductive reflect (P: Prop): bool -> Type := | Reflect_true : P -> reflect P true @@ -4838,7 +4840,7 @@ logically equivalent propositions. For instance, the following lemma: -.. coqtop:: in +.. coqdoc:: Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2). @@ -4853,20 +4855,20 @@ to the case analysis of |Coq|’s inductive types. Since the equivalence predicate is defined in |Coq| as: -.. coqtop:: in +.. coqdoc:: Definition iff (A B:Prop) := (A -> B) /\ (B -> A). where ``/\`` is a notation for ``and``: -.. coqtop:: in +.. coqdoc:: Inductive and (A B:Prop) : Prop := conj : A -> B -> and A B. This make case analysis very different according to the way an equivalence property has been defined. -.. coqtop:: in +.. coqdoc:: Lemma andE (b1 b2 : bool) : (b1 /\ b2) <-> (b1 && b2). @@ -4950,13 +4952,13 @@ Specializing assumptions The |SSR| tactic: -.. coqtop:: in +.. coqdoc:: move/(_ term1 … termn). is equivalent to the tactic: -.. coqtop:: in +.. coqdoc:: intro top; generalize (top term1 … termn); clear top. @@ -5013,13 +5015,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``: -.. coqtop:: in +.. coqdoc:: Lemma iffLR : forall P Q, (P <-> Q) -> P -> Q. which transforms a double implication into the left-to-right one, or: -.. coqtop:: in +.. coqdoc:: Lemma iffRL : forall P Q, (P <-> Q) -> Q -> P. @@ -5123,7 +5125,7 @@ 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: -.. coqtop:: in +.. coqdoc:: Lemma idP : reflect b1 b1. @@ -5198,7 +5200,7 @@ in sequence. Both move and apply can be followed by an arbitrary number of ``/term``. The main difference between the following two tactics -.. coqtop:: in +.. coqdoc:: apply/v1/v2/v3. apply/v1; apply/v2; apply/v3. @@ -5210,7 +5212,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: -.. coqtop:: in +.. coqdoc:: move=> /v1; move=> /v2. move=> /v1 - /v2. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 66d510bc0e..0bcfce2322 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2493,7 +2493,7 @@ and an explanation of the underlying technique. Let us consider the relation Le over natural numbers and the following variables: - .. coqtop:: all + .. coqtop:: all reset Inductive Le : nat -> nat -> Set := | LeO : forall n:nat, Le 0 n diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 105b0445fd..4f46a80dcf 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -181,7 +181,7 @@ rules. Some simple left factorization work has to be done. Here is an example. .. coqtop:: all Notation "x < y" := (lt x y) (at level 70). - Notation "x < y < z" := (x < y /\ y < z) (at level 70). + Fail Notation "x < y < z" := (x < y /\ y < z) (at level 70). In order to factorize the left part of the rules, the subexpression referred to by ``y`` has to be at the same level in both rules. However the @@ -486,7 +486,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: -.. coqtop:: in +.. coqdoc:: Notation "{ x : A | P }" := (sig (fun x : A => P)) (at level 0, x at level 99 as ident). @@ -788,9 +788,9 @@ main grammar, or from another custom entry as is the case in to indicate that ``e`` has to be parsed at level ``2`` of the grammar associated to the custom entry ``expr``. The level can be omitted, as in -.. coqtop:: in +.. coqdoc:: - Notation "[ e ]" := e (e custom expr)`. + Notation "[ e ]" := e (e custom expr). in which case Coq tries to infer it. @@ -1058,7 +1058,7 @@ Binding arguments of a constant to an interpretation scope in the scope delimited by the key ``F`` (``Rfun_scope``) and the last argument in the scope delimited by the key ``R`` (``R_scope``). - .. coqtop:: in + .. coqdoc:: Arguments plus_fct (f1 f2)%F x%R. @@ -1066,7 +1066,7 @@ Binding arguments of a constant to an interpretation scope parentheses. In the following example arguments A and B are marked as maximally inserted implicit arguments and are put into the type_scope scope. - .. coqtop:: in + .. coqdoc:: Arguments respectful {A B}%type (R R')%signature _ _. @@ -1148,7 +1148,7 @@ Binding types of arguments to an interpretation scope can be bound to an interpretation scope. The command to do it is :n:`Bind Scope @scope with @class` - .. coqtop:: in + .. coqtop:: in reset Parameter U : Set. Bind Scope U_scope with U. diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 067af954ad..0dd9b3aa3e 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -560,7 +560,7 @@ class CoqtopDirective(Directive): Example:: - .. coqtop:: in reset undo + .. coqtop:: in undo Print nat. Definition a := 1. @@ -580,8 +580,7 @@ class CoqtopDirective(Directive): - Behavior options - ``reset``: Send a ``Reset Initial`` command before running this block - - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after - running all the commands in this block + - ``undo``: Reset state after executing. Not compatible with ``reset``. ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks of the same document (``coqrst`` creates a single ``coqtop`` process per |