diff options
| -rw-r--r-- | doc/sphinx/language/core/primitive.rst | 107 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/evars.rst | 97 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst (renamed from doc/sphinx/addendum/extended-pattern-matching.rst) | 279 |
3 files changed, 483 insertions, 0 deletions
diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst new file mode 100644 index 0000000000..dc8f131209 --- /dev/null +++ b/doc/sphinx/language/core/primitive.rst @@ -0,0 +1,107 @@ +Primitive objects +================= + +.. _primitive-integers: + +Primitive Integers +------------------ + +The language of terms features 63-bit machine integers as values. The type of +such a value is *axiomatized*; it is declared through the following sentence +(excerpt from the :g:`Int63` module): + +.. coqdoc:: + + Primitive int := #int63_type. + +This type is equipped with a few operators, that must be similarly declared. +For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function, +declared and specified as follows: + +.. coqdoc:: + + Primitive eqb := #int63_eq. + Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. + + Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. + +The complete set of such operators can be obtained looking at the :g:`Int63` module. + +These primitive declarations are regular axioms. As such, they must be trusted and are listed by the +:g:`Print Assumptions` command, as in the following example. + +.. coqtop:: in reset + + From Coq Require Import Int63. + Lemma one_minus_one_is_zero : (1 - 1 = 0)%int63. + Proof. apply eqb_correct; vm_compute; reflexivity. Qed. + +.. coqtop:: all + + Print Assumptions one_minus_one_is_zero. + +The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement +dedicated, efficient, rules to reduce the applications of these primitive +operations. + +The extraction of these primitives can be customized similarly to the extraction +of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63` +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Uint63` module. Said OCaml module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq. + +Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values +wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on +64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the +function :g:`Uint63.compile` from the kernel). + +.. _primitive-floats: + +Primitive Floats +---------------- + +The language of terms features Binary64 floating-point numbers as values. +The type of such a value is *axiomatized*; it is declared through the +following sentence (excerpt from the :g:`PrimFloat` module): + +.. coqdoc:: + + Primitive float := #float64_type. + +This type is equipped with a few operators, that must be similarly declared. +For instance, the product of two primitive floats can be computed using the +:g:`PrimFloat.mul` function, declared and specified as follows: + +.. coqdoc:: + + Primitive mul := #float64_mul. + Notation "x * y" := (mul x y) : float_scope. + + Axiom mul_spec : forall x y, Prim2SF (x * y)%float = SF64mul (Prim2SF x) (Prim2SF y). + +where :g:`Prim2SF` is defined in the :g:`FloatOps` module. + +The set of such operators is described in section :ref:`floats_library`. + +These primitive declarations are regular axioms. As such, they must be trusted, and are listed by the +:g:`Print Assumptions` command. + +The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement +dedicated, efficient rules to reduce the applications of these primitive +operations, using the floating-point processor operators that are assumed +to comply with the IEEE 754 standard for floating-point arithmetic. + +The extraction of these primitives can be customized similarly to the extraction +of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlFloats` +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Float64` module. Said OCaml module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq. + +Literal values (of type :g:`Float64.t`) are extracted to literal OCaml +values (of type :g:`float`) written in hexadecimal notation and +wrapped into the :g:`Float64.of_float` constructor, e.g.: +:g:`Float64.of_float (0x1p+0)`. diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst new file mode 100644 index 0000000000..979a0a62e6 --- /dev/null +++ b/doc/sphinx/language/extensions/evars.rst @@ -0,0 +1,97 @@ +.. _existential-variables: + +Existential variables +--------------------- + +.. insertprodn term_evar term_evar + +.. prodn:: + term_evar ::= _ + | ?[ @ident ] + | ?[ ?@ident ] + | ?@ident {? @%{ {+; @ident := @term } %} } + +|Coq| terms can include existential variables which represents unknown +subterms to eventually be replaced by actual subterms. + +Existential variables are generated in place of unsolvable 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 +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, +which is the expected type of the placeholder. + +As a consequence of typing constraints, existential variables can be +duplicated in such a way that they possibly appear in different +contexts than their defining context. Thus, any occurrence of a given +existential variable comes with an instance of its original context. +In the simple case, when an existential variable denotes the +placeholder which generated it, or is used in the same context as the +one in which it was generated, the context is not displayed and the +existential variable is represented by “?” followed by an identifier. + +.. coqtop:: all + + Parameter identity : forall (X:Set), X -> X. + + Check identity _ _. + + 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 +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. + +.. 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. +with a named-goal selector, see :ref:`goal-selectors`). + +.. _explicit-display-existentials: + +Explicit displaying of existential instances for pretty-printing +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. flag:: Printing Existential Instances + + This flag (off by default) activates the full display of how the + context of an existential variable is instantiated at each of the + occurrences of the existential variable. + +.. _tactics-in-terms: + +Solving existential variables using tactics +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Instead of letting the unification engine try to solve an existential +variable by itself, one can also provide an explicit hole together +with a tactic to solve it. Using the syntax ``ltac:(``\ `tacexpr`\ ``)``, the user +can put a tactic anywhere a term is expected. The order of resolution +is not specified and is implementation-dependent. The inner tactic may +use any variable defined in its scope, including repeated alternations +between variables introduced by term binding as well as those +introduced by tactic binding. The expression `tacexpr` can be any tactic +expression as described in :ref:`ltac`. + +.. coqtop:: all + + Definition foo (x : nat) : nat := ltac:(exact x). + +This construction is useful when one wants to define complicated terms +using highly automated tactics without resorting to writing the proof-term +by means of the interactive proof engine. diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/language/extensions/match.rst index 8ec51e45ba..2aeace3cef 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -9,6 +9,281 @@ This section describes the full form of pattern matching in |Coq| terms. .. |rhs| replace:: right hand sides +Variants and extensions of :g:`match` +------------------------------------- + +.. _mult-match: + +Multiple and nested pattern matching +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The basic version of :g:`match` allows pattern matching on simple +patterns. As an extension, multiple nested patterns or disjunction of +patterns are allowed, as in ML-like languages +(cf. :ref:`multiple-patterns` and :ref:`nested-patterns`). + +The extension just acts as a macro that is expanded during parsing +into a sequence of match on simple patterns. Especially, a +construction defined using the extended match is generally printed +under its expanded form (see :flag:`Printing Matching`). + +.. _if-then-else: + +Pattern-matching on boolean values: the if expression +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. insertprodn term_if term_if + +.. prodn:: + term_if ::= if @term {? {? as @name } return @term100 } then @term else @term + +For inductive types with exactly two constructors and for pattern matching +expressions that do not depend on the arguments of the constructors, it is possible +to use a ``if … then … else`` notation. For instance, the definition + +.. coqtop:: all + + Definition not (b:bool) := + match b with + | true => false + | false => true + end. + +can be alternatively written + +.. coqtop:: reset all + + Definition not (b:bool) := if b then false else true. + +More generally, for an inductive type with constructors :n:`@ident__1` +and :n:`@ident__2`, the following terms are equal: + +:n:`if @term__0 {? {? as @name } return @term } then @term__1 else @term__2` + +:n:`match @term__0 {? {? as @name } return @term } with | @ident__1 {* _ } => @term__1 | @ident__2 {* _ } => @term__2 end` + +.. example:: + + .. coqtop:: all + + Check (fun x (H:{x=0}+{x<>0}) => + match H with + | left _ => true + | right _ => false + end). + +Notice that the printing uses the :g:`if` syntax because :g:`sumbool` is +declared as such (see :ref:`controlling-match-pp`). + +.. _irrefutable-patterns: + +Irrefutable patterns: the destructuring let variants +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Pattern-matching on terms inhabiting inductive type having only one +constructor can be alternatively written using :g:`let … in …` +constructions. There are two variants of them. + + +First destructuring let syntax +++++++++++++++++++++++++++++++ + +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 +arguments of the constructor in :n:`@term__0`. For instance, the +definition + +.. coqtop:: reset all + + Definition fst (A B:Set) (H:A * B) := match H with + | pair x y => x + end. + +can be alternatively written + +.. coqtop:: reset all + + Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x. + +Notice that reduction is different from regular :g:`let … in …` +construction since it happens only if :n:`@term__0` is in constructor form. +Otherwise, the reduction is blocked. + +The pretty-printing of a definition by matching on a irrefutable +pattern can either be done using :g:`match` or the :g:`let` construction +(see Section :ref:`controlling-match-pp`). + +If term inhabits an inductive type with one constructor `C`, we have an +equivalence between + +:: + + let (ident₁, …, identₙ) [dep_ret_type] := term in term' + +and + +:: + + match term [dep_ret_type] with + C ident₁ … identₙ => term' + end + + +Second destructuring let syntax ++++++++++++++++++++++++++++++++ + +Another destructuring let syntax is available for inductive types with +one constructor by giving an arbitrary pattern instead of just a tuple +for all the arguments. For example, the preceding example can be +written: + +.. coqtop:: reset all + + Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x. + +This is useful to match deeper inside tuples and also to use notations +for the pattern, as the syntax :g:`let ’p := t in b` allows arbitrary +patterns to do the deconstruction. For example: + +.. coqtop:: all + + Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A := + let '((a,b), (c, d)) := x in (a,b,c,d). + + Notation " x 'With' p " := (exist _ x p) (at level 20). + + Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A := + let 'x With p := t in x. + +When printing definitions which are written using this construct it +takes precedence over let printing directives for the datatype under +consideration (see Section :ref:`controlling-match-pp`). + + +.. _controlling-match-pp: + +Controlling pretty-printing of match expressions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The following commands give some control over the pretty-printing +of :g:`match` expressions. + +Printing nested patterns ++++++++++++++++++++++++++ + +.. flag:: Printing Matching + + The Calculus of Inductive Constructions knows pattern matching only + over simple patterns. It is however convenient to re-factorize nested + pattern matching into a single pattern matching over a nested + pattern. + + When this flag is on (default), |Coq|’s printer tries to do such + limited re-factorization. + Turning it off tells |Coq| to print only simple pattern matching problems + in the same way as the |Coq| kernel handles them. + + +Factorization of clauses with same right-hand side +++++++++++++++++++++++++++++++++++++++++++++++++++ + +.. flag:: Printing Factorizable Match Patterns + + When several patterns share the same right-hand side, it is additionally + possible to share the clauses using disjunctive patterns. Assuming that the + printing matching mode is on, this flag (on by default) tells |Coq|'s + printer to try to do this kind of factorization. + +Use of a default clause ++++++++++++++++++++++++ + +.. flag:: Printing Allow Match Default Clause + + When several patterns share the same right-hand side which do not depend on the + arguments of the patterns, yet an extra factorization is possible: the + disjunction of patterns can be replaced with a `_` default clause. Assuming that + the printing matching mode and the factorization mode are on, this flag (on by + default) tells |Coq|'s printer to use a default clause when relevant. + +Printing of wildcard patterns +++++++++++++++++++++++++++++++ + +.. flag:: Printing Wildcard + + Some variables in a pattern may not occur in the right-hand side of + the pattern matching clause. When this flag is on (default), the + variables having no occurrences in the right-hand side of the + pattern matching clause are just printed using the wildcard symbol + “_”. + + +Printing of the elimination predicate ++++++++++++++++++++++++++++++++++++++ + +.. flag:: Printing Synth + + In most of the cases, the type of the result of a matched term is + mechanically synthesizable. Especially, if the result type does not + depend of the matched term. When this flag is on (default), + the result type is not printed when |Coq| knows that it can re- + synthesize it. + + +Printing matching on irrefutable patterns +++++++++++++++++++++++++++++++++++++++++++ + +If an inductive type has just one constructor, pattern matching can be +written using the first destructuring let syntax. + +.. table:: Printing Let @qualid + :name: Printing Let + + Specifies a set of qualids for which pattern matching is displayed using a let expression. + Note that this only applies to pattern matching instances entered with :g:`match`. + It doesn't affect pattern matching explicitly entered with a destructuring + :g:`let`. + Use the :cmd:`Add` and :cmd:`Remove` commands to update this set. + + +Printing matching on booleans ++++++++++++++++++++++++++++++ + +If an inductive type is isomorphic to the boolean type, pattern matching +can be written using ``if`` … ``then`` … ``else`` …. This table controls +which types are written this way: + +.. table:: Printing If @qualid + :name: Printing If + + Specifies a set of qualids for which pattern matching is displayed using + ``if`` … ``then`` … ``else`` …. Use the :cmd:`Add` and :cmd:`Remove` + commands to update this set. + +This example emphasizes what the printing settings offer. + +.. example:: + + .. coqtop:: all + + Definition snd (A B:Set) (H:A * B) := match H with + | pair x y => y + end. + + Test Printing Let for prod. + + Print snd. + + Remove Printing Let prod. + + Unset Printing Synth. + + Unset Printing Wildcard. + + Print snd. + Patterns -------- @@ -68,6 +343,8 @@ by: end end. +.. _multiple-patterns: + Multiple patterns ----------------- @@ -110,6 +387,8 @@ We can also use :n:`as @ident` to associate a name to a sub-pattern: | S n', S m' => S (max n' m') end. +.. _nested-patterns: + Nested patterns --------------- |