diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 42 | ||||
| -rw-r--r-- | doc/sphinx/language/core/variants.rst | 15 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/evars.rst | 32 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/implicit-arguments.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst | 2 |
5 files changed, 53 insertions, 42 deletions
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index f9d24fde0e..c27eb216e8 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -40,7 +40,7 @@ in the |Coq| root directory; this includes the modules ``Datatypes``, ``Specif``, ``Peano``, -``Wf`` and +``Wf`` and ``Tactics``. Module ``Logic_Type`` also makes it in the initial state. @@ -175,7 +175,7 @@ Quantifiers Then we find first-order quantifiers: .. coqtop:: in - + Definition all (A:Set) (P:A -> Prop) := forall x:A, P x. Inductive ex (A: Set) (P:A -> Prop) : Prop := ex_intro (x:A) (_:P x). @@ -256,12 +256,12 @@ Finally, a few easy lemmas are provided. single: f_equal2 ... f_equal5 (term) The theorem ``f_equal`` is extended to functions with two to five -arguments. The theorem are names ``f_equal2``, ``f_equal3``, +arguments. The theorem are names ``f_equal2``, ``f_equal3``, ``f_equal4`` and ``f_equal5``. For instance ``f_equal3`` is defined the following way. .. coqtop:: in abort - + Theorem f_equal3 : forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), @@ -324,7 +324,7 @@ Programming Note that zero is the letter ``O``, and *not* the numeral ``0``. -The predicate ``identity`` is logically +The predicate ``identity`` is logically equivalent to equality but it lives in sort ``Type``. It is mainly maintained for compatibility. @@ -367,7 +367,7 @@ infix notation ``||``), ``xorb``, ``implb`` and ``negb``. Specification ~~~~~~~~~~~~~ -The following notions defined in module ``Specif.v`` allow to build new data-types and specifications. +The following notions defined in module ``Specif.v`` allow to build new data-types and specifications. They are available with the syntax shown in the previous section :ref:`datatypes`. For instance, given :g:`A:Type` and :g:`P:A->Prop`, the construct @@ -393,11 +393,11 @@ provided. .. coqtop:: in Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x). - Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := + Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := exist2 (x:A) (_:P x) (_:Q x). A *strong (dependent) sum* :g:`{x:A & P x}` may be also defined, -when the predicate ``P`` is now defined as a +when the predicate ``P`` is now defined as a constructor of types in ``Type``. .. index:: @@ -556,7 +556,7 @@ section :tacn:`refine`). This scope is opened by default. Now comes the content of module ``Peano``: .. coqdoc:: - + Theorem eq_S : forall x y:nat, x = y -> S x = S y. Definition pred (n:nat) : nat := match n with @@ -628,7 +628,7 @@ induction principle. .. coqdoc:: Theorem nat_case : - forall (n:nat) (P:nat -> Prop), + forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. Theorem nat_double_ind : forall R:nat -> nat -> Prop, @@ -640,7 +640,7 @@ induction principle. Well-founded recursion ~~~~~~~~~~~~~~~~~~~~~~ -The basic library contains the basics of well-founded recursion and +The basic library contains the basics of well-founded recursion and well-founded induction, in module ``Wf.v``. .. index:: @@ -669,7 +669,7 @@ well-founded induction, in module ``Wf.v``. forall P:A -> Prop, (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a. -The automatically generated scheme ``Acc_rect`` +The automatically generated scheme ``Acc_rect`` can be used to define functions by fixpoints using well-founded relations to justify termination. Assuming extensionality of the functional used for the recursive call, the @@ -741,7 +741,7 @@ The standard library Survey ~~~~~~ -The rest of the standard library is structured into the following +The rest of the standard library is structured into the following subdirectories: * **Logic** : Classical logic and dependent equality @@ -751,8 +751,8 @@ subdirectories: * **ZArith** : Basic relative integer arithmetic * **Numbers** : Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2^31 binary words) * **Bool** : Booleans (basic functions and results) - * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types) - * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) + * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types) + * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) * **FSets** : Specification and implementations of finite sets and finite maps (by lists and by AVL trees) * **Reals** : Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...) * **Floats** : Machine implementation of floating-point arithmetic (for the binary64 format) @@ -903,7 +903,7 @@ tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: discrR :name: discrR - + Proves that two real integer constants are different. .. example:: @@ -931,7 +931,7 @@ tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: split_Rmult :name: split_Rmult - + Splits a condition that a product is non null into subgoals corresponding to the condition on each operand of the product. @@ -963,7 +963,7 @@ List library single: fold_left (term) single: fold_right (term) -Some elementary operations on polymorphic lists are defined here. +Some elementary operations on polymorphic lists are defined here. They can be accessed by requiring module ``List``. It defines the following notions: @@ -1052,9 +1052,9 @@ Notation Interpretation ``_ + _`` ``add`` ``_ * _`` ``mul`` ``_ / _`` ``div`` -``_ == _`` ``eqb`` -``_ < _`` ``ltb`` -``_ <= _`` ``leb`` +``_ =? _`` ``eqb`` +``_ <? _`` ``ltb`` +``_ <=? _`` ``leb`` ``_ ?= _`` ``compare`` =========== ============== diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index d00a2f4100..8e2bf32dd6 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -57,6 +57,11 @@ Private (matching) inductive types Definition by cases: match -------------------------- +Objects of inductive types can be destructured by a case-analysis +construction called *pattern matching* expression. A pattern matching +expression is used to analyze the structure of an inductive object and +to apply specific treatments accordingly. + .. insertprodn term_match pattern0 .. prodn:: @@ -77,10 +82,12 @@ Definition by cases: match | @numeral | @string -Objects of inductive types can be destructured by a case-analysis -construction called *pattern matching* expression. A pattern matching -expression is used to analyze the structure of an inductive object and -to apply specific treatments accordingly. +Note that the :n:`@pattern ::= @pattern10 : @term` production +is not supported in :n:`match` patterns. Trying to use it will give this error: + +.. exn:: Casts are not supported in this pattern. + :undocumented: + This paragraph describes the basic form of pattern matching. See Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst index 40e0898871..20f4310d13 100644 --- a/doc/sphinx/language/extensions/evars.rst +++ b/doc/sphinx/language/extensions/evars.rst @@ -13,13 +13,13 @@ Existential variables | ?[ ?@ident ] | ?@ident {? @%{ {+; @ident := @term } %} } -|Coq| terms can include existential variables which represents unknown -subterms to eventually be replaced by actual subterms. +|Coq| terms can include existential variables that represent unknown +subterms that are eventually replaced with actual subterms. -Existential variables are generated in place of unsolvable implicit +Existential variables are generated in place of unsolved implicit arguments or “_” placeholders when using commands such as ``Check`` (see Section :ref:`requests-to-the-environment`) or when using tactics such as -:tacn:`refine`, as well as in place of unsolvable instances when using +:tacn:`refine`, as well as in place of unsolved instances when using tactics such that :tacn:`eapply`. An existential variable is defined in a context, which is the context of variables of the placeholder which generated the existential variable, and a type, @@ -43,22 +43,18 @@ existential variable is represented by “?” followed by an identifier. Check identity _ (fun x => _). In the general case, when an existential variable :n:`?@ident` appears -outside of its context of definition, its instance, written under the -form :n:`{ {*; @ident := @term} }` is appending to its name, indicating +outside its context of definition, its instance, written in the +form :n:`{ {*; @ident := @term} }`, is appended to its name, indicating how the variables of its defining context are instantiated. -The variables of the context of the existential variables which are -instantiated by themselves are not written, unless the :flag:`Printing Existential Instances` flag -is on (see Section :ref:`explicit-display-existentials`), and this is why an -existential variable used in the same context as its context of definition is written with no instance. +Only the variables that are defined in another context are displayed: +this is why an existential variable used in the same context as its +context of definition is written with no instance. +This behaviour may be changed: see :ref:`explicit-display-existentials`. .. coqtop:: all Check (fun x y => _) 0 1. - Set Printing Existential Instances. - - Check (fun x y => _) 0 1. - Existential variables can be named by the user upon creation using the syntax :n:`?[@ident]`. This is useful when the existential variable needs to be explicitly handled later in the script (e.g. @@ -88,6 +84,14 @@ Explicit displaying of existential instances for pretty-printing context of an existential variable is instantiated at each of the occurrences of the existential variable. +.. coqtop:: all + + Check (fun x y => _) 0 1. + + Set Printing Existential Instances. + + Check (fun x y => _) 0 1. + .. _tactics-in-terms: Solving existential variables using tactics diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index bbd486e3ba..ca69072cb9 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -70,7 +70,7 @@ is said *contextual* if it can be inferred only from the knowledge of the type of the context of the current expression. For instance, the only argument of:: - nil : forall A:Set, list A` + nil : forall A:Set, list A is contextual. Similarly, both arguments of a term of type:: @@ -539,7 +539,7 @@ with free variables into a closed statement where these variables are quantified explicitly. Use the :cmd:`Generalizable` command to designate which variables should be generalized. -It is activated for a binder by prefixing a \`, and for terms by +It is activated within a binder by prefixing it with \`, and for terms by surrounding it with \`{ }, or \`[ ] or \`( ). Terms surrounded by \`{ } introduce their free variables as maximally diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index b4558ef07f..d6a828521f 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -94,7 +94,7 @@ The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1` performs case analysis on :n:`@term__0` whose type must be an inductive type with exactly one constructor. The number of variables :n:`@ident__i` must correspond to the number of arguments of this -contrustor. Then, in :n:`@term__1`, these variables are bound to the +constructor. Then, in :n:`@term__1`, these variables are bound to the arguments of the constructor in :n:`@term__0`. For instance, the definition |