diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/canonical-structures.rst | 438 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 619 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 630 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 833 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 469 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 271 | ||||
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 58 | ||||
| -rw-r--r-- | doc/sphinx/addendum/nsatz.rst | 88 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 187 | ||||
| -rw-r--r-- | doc/sphinx/addendum/parallel-proof-processing.rst | 228 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 387 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 764 | ||||
| -rw-r--r-- | doc/sphinx/addendum/sprop.rst | 239 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 593 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 502 |
15 files changed, 6306 insertions, 0 deletions
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst new file mode 100644 index 0000000000..dd21ea09bd --- /dev/null +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -0,0 +1,438 @@ +.. _canonicalstructures: + +Canonical Structures +====================== + +:Authors: Assia Mahboubi and Enrico Tassi + +This chapter explains the basics of canonical structures and how they can be used +to overload notations and build a hierarchy of algebraic structures. The +examples are taken from :cite:`CSwcu`. We invite the interested reader to refer +to this paper for all the details that are omitted here for brevity. The +interested reader shall also find in :cite:`CSlessadhoc` a detailed description +of another, complementary, use of canonical structures: advanced proof search. +This latter papers also presents many techniques one can employ to tune the +inference of canonical structures. + + +Notation overloading +------------------------- + +We build an infix notation == for a comparison predicate. Such +notation will be overloaded, and its meaning will depend on the types +of the terms that are compared. + +.. coqtop:: all + + Module EQ. + Record class (T : Type) := Class { cmp : T -> T -> Prop }. + Structure type := Pack { obj : Type; class_of : class obj }. + Definition op (e : type) : obj e -> obj e -> Prop := + let 'Pack _ (Class _ the_cmp) := e in the_cmp. + Check op. + Arguments op {e} x y : simpl never. + Arguments Class {T} cmp. + Module theory. + Notation "x == y" := (op x y) (at level 70). + End theory. + End EQ. + +We use Coq modules as namespaces. This allows us to follow the same +pattern and naming convention for the rest of the chapter. The base +namespace contains the definitions of the algebraic structure. To +keep the example small, the algebraic structure ``EQ.type`` we are +defining is very simplistic, and characterizes terms on which a binary +relation is defined, without requiring such relation to validate any +property. The inner theory module contains the overloaded notation ``==`` +and will eventually contain lemmas holding all the instances of the +algebraic structure (in this case there are no lemmas). + +Note that in practice the user may want to declare ``EQ.obj`` as a +coercion, but we will not do that here. + +The following line tests that, when we assume a type ``e`` that is in +theEQ class, we can relate two of its objects with ``==``. + +.. coqtop:: all + + Import EQ.theory. + Check forall (e : EQ.type) (a b : EQ.obj e), a == b. + +Still, no concrete type is in the ``EQ`` class. + +.. coqtop:: all + + Fail Check 3 == 3. + +We amend that by equipping ``nat`` with a comparison relation. + +.. coqtop:: all + + Definition nat_eq (x y : nat) := Nat.compare x y = Eq. + Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq. + Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl. + Check 3 == 3. + Eval compute in 3 == 4. + +This last test shows that |Coq| is now not only able to type check ``3 == 3``, +but also that the infix relation was bound to the ``nat_eq`` relation. +This relation is selected whenever ``==`` is used on terms of type nat. +This can be read in the line declaring the canonical structure +``nat_EQty``, where the first argument to ``Pack`` is the key and its second +argument a group of canonical values associated to the key. In this +case we associate to nat only one canonical value (since its class, +``nat_EQcl`` has just one member). The use of the projection ``op`` requires +its argument to be in the class ``EQ``, and uses such a member (function) +to actually compare its arguments. + +Similarly, we could equip any other type with a comparison relation, +and use the ``==`` notation on terms of this type. + + +Derived Canonical Structures +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +We know how to use ``==`` on base types, like ``nat``, ``bool``, ``Z``. Here we show +how to deal with type constructors, i.e. how to make the following +example work: + + +.. coqtop:: all + + Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b). + +The error message is telling that |Coq| has no idea on how to compare +pairs of objects. The following construction is telling Coq exactly +how to do that. + +.. coqtop:: all + + Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) := + fst x == fst y /\ snd x == snd y. + + Definition pair_EQcl e1 e2 := EQ.Class (pair_eq e1 e2). + + Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type := + EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2). + + Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b). + + Check forall n m : nat, (3, 4) == (n, m). + +Thanks to the ``pair_EQty`` declaration, |Coq| is able to build a comparison +relation for pairs whenever it is able to build a comparison relation +for each component of the pair. The declaration associates to the key ``*`` +(the type constructor of pairs) the canonical comparison +relation ``pair_eq`` whenever the type constructor ``*`` is applied to two +types being themselves in the ``EQ`` class. + +Hierarchy of structures +---------------------------- + +To get to an interesting example we need another base class to be +available. We choose the class of types that are equipped with an +order relation, to which we associate the infix ``<=`` notation. + +.. coqtop:: all + + Module LE. + + Record class T := Class { cmp : T -> T -> Prop }. + + Structure type := Pack { obj : Type; class_of : class obj }. + + Definition op (e : type) : obj e -> obj e -> Prop := + let 'Pack _ (Class _ f) := e in f. + + Arguments op {_} x y : simpl never. + + Arguments Class {T} cmp. + + Module theory. + + Notation "x <= y" := (op x y) (at level 70). + + End theory. + + End LE. + +As before we register a canonical ``LE`` class for ``nat``. + +.. coqtop:: all + + Import LE.theory. + + Definition nat_le x y := Nat.compare x y <> Gt. + + Definition nat_LEcl : LE.class nat := LE.Class nat_le. + + Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl. + +And we enable |Coq| to relate pair of terms with ``<=``. + +.. coqtop:: all + + Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) := + fst x <= fst y /\ snd x <= snd y. + + Definition pair_LEcl e1 e2 := LE.Class (pair_le e1 e2). + + Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type := + LE.Pack (LE.obj e1 * LE.obj e2) (pair_LEcl e1 e2). + + Check (3,4,5) <= (3,4,5). + +At the current stage we can use ``==`` and ``<=`` on concrete types, like +tuples of natural numbers, but we can’t develop an algebraic theory +over the types that are equipped with both relations. + +.. coqtop:: all + + Check 2 <= 3 /\ 2 == 2. + + Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y. + + Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y. + +We need to define a new class that inherits from both ``EQ`` and ``LE``. + + +.. coqtop:: all + + Module LEQ. + + Record mixin (e : EQ.type) (le : EQ.obj e -> EQ.obj e -> Prop) := + Mixin { compat : forall x y : EQ.obj e, le x y /\ le y x <-> x == y }. + + Record class T := Class { + EQ_class : EQ.class T; + LE_class : LE.class T; + extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }. + + Structure type := _Pack { obj : Type; class_of : class obj }. + + Arguments Mixin {e le} _. + + Arguments Class {T} _ _ _. + +The mixin component of the ``LEQ`` class contains all the extra content we +are adding to ``EQ`` and ``LE``. In particular it contains the requirement +that the two relations we are combining are compatible. + +Unfortunately there is still an obstacle to developing the algebraic +theory of this new class. + +.. coqtop:: all + + Module theory. + + Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m. + + +The problem is that the two classes ``LE`` and ``LEQ`` are not yet related by +a subclass relation. In other words |Coq| does not see that an object of +the ``LEQ`` class is also an object of the ``LE`` class. + +The following two constructions tell |Coq| how to canonically build the +``LE.type`` and ``EQ.type`` structure given an ``LEQ.type`` structure on the same +type. + +.. coqtop:: all + + Definition to_EQ (e : type) : EQ.type := + EQ.Pack (obj e) (EQ_class _ (class_of e)). + + Canonical Structure to_EQ. + + Definition to_LE (e : type) : LE.type := + LE.Pack (obj e) (LE_class _ (class_of e)). + + Canonical Structure to_LE. + +We can now formulate out first theorem on the objects of the ``LEQ`` +structure. + +.. coqtop:: all + + Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y. + + now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. + + Qed. + + Arguments lele_eq {e} x y _ _. + + End theory. + + End LEQ. + + Import LEQ.theory. + + Check lele_eq. + +Of course one would like to apply results proved in the algebraic +setting to any concrete instate of the algebraic structure. + +.. coqtop:: all + + Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m. + + Fail apply (lele_eq n m). + + Abort. + + Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : + n <= m -> m <= n -> n == m. + + Fail apply (lele_eq n m). + + Abort. + +Again one has to tell |Coq| that the type ``nat`` is in the ``LEQ`` class, and +how the type constructor ``*`` interacts with the ``LEQ`` class. In the +following proofs are omitted for brevity. + +.. coqtop:: all + + Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m. + + Admitted. + + Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat. + + Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : + n <= m /\ m <= n <-> n == m. + + Admitted. + + Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2). + +The following script registers an ``LEQ`` class for ``nat`` and for the type +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. + +.. FIXME shouldn't warn + +.. coqtop:: all warn + + Module Add_instance_attempt. + + Canonical Structure nat_LEQty : LEQ.type := + LEQ._Pack nat (LEQ.Class nat_EQcl nat_LEcl nat_LEQmx). + + Canonical Structure pair_LEQty (l1 l2 : LEQ.type) : LEQ.type := + LEQ._Pack (LEQ.obj l1 * LEQ.obj l2) + (LEQ.Class + (EQ.class_of (pair_EQty (to_EQ l1) (to_EQ l2))) + (LE.class_of (pair_LEty (to_LE l1) (to_LE l2))) + (pair_LEQmx l1 l2)). + + Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m. + + now apply (lele_eq n m). + + Qed. + + Example test_algebraic2 (n m : nat * nat) : n <= m -> m <= n -> n == m. + + now apply (lele_eq n m). Qed. + + End Add_instance_attempt. + +Note that no direct proof of ``n <= m -> m <= n -> n == m`` is provided by +the user for ``n`` and m of type ``nat * nat``. What the user provides is a +proof of this statement for ``n`` and ``m`` of type ``nat`` and a proof that the +pair constructor preserves this property. The combination of these two +facts is a simple form of proof search that |Coq| performs automatically +while inferring canonical structures. + +Compact declaration of Canonical Structures +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +We need some infrastructure for that. + +.. coqtop:: all + + Require Import Strings.String. + + Module infrastructure. + + Inductive phantom {T : Type} (t : T) : Type := Phantom. + + Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := + phantom t1 -> phantom t2. + + Definition id {T} {t : T} (x : phantom t) := x. + + Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) + (at level 50, v ident, only parsing). + + Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) + (at level 50, v ident, only parsing). + + Notation "'Error : t : s" := (unify _ t (Some s)) + (at level 50, format "''Error' : t : s"). + + Open Scope string_scope. + + End infrastructure. + +To explain the notation ``[find v | t1 ~ t2]`` let us pick one of its +instances: ``[find e | EQ.obj e ~ T | "is not an EQ.type" ]``. It should be +read as: “find a class e such that its objects have type T or fail +with message "T is not an EQ.type"”. + +The other utilities are used to ask |Coq| to solve a specific unification +problem, that will in turn require the inference of some canonical structures. +They are explained in more details in :cite:`CSwcu`. + +We now have all we need to create a compact “packager” to declare +instances of the ``LEQ`` class. + +.. coqtop:: all + + Import infrastructure. + + Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) := + [find e | EQ.obj e ~ T | "is not an EQ.type" ] + [find o | LE.obj o ~ T | "is not an LE.type" ] + [find ce | EQ.class_of e ~ ce ] + [find co | LE.class_of o ~ co ] + [find m | m ~ m0 | "is not the right mixin" ] + LEQ._Pack T (LEQ.Class ce co m). + + Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id). + +The object ``Pack`` takes a type ``T`` (the key) and a mixin ``m``. It infers all +the other pieces of the class ``LEQ`` and declares them as canonical +values associated to the ``T`` key. All in all, the only new piece of +information we add in the ``LEQ`` class is the mixin, all the rest is +already canonical for ``T`` and hence can be inferred by |Coq|. + +``Pack`` is a notation, hence it is not type checked at the time of its +declaration. It will be type checked when it is used, an in that case ``T`` is +going to be a concrete type. The odd arguments ``_`` and ``id`` we pass to the +packager represent respectively the classes to be inferred (like ``e``, ``o``, +etc) and a token (``id``) to force their inference. Again, for all the details +the reader can refer to :cite:`CSwcu`. + +The declaration of canonical instances can now be way more compact: + +.. FIXME should not warn + +.. coqtop:: all warn + + Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. + + Canonical Structure pair_LEQty (l1 l2 : LEQ.type) := + Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2). + +Error messages are also quite intelligible (if one skips to the end of +the message). + +.. coqtop:: all + + Fail Canonical Structure err := Eval hnf in Pack bool nat_LEQmx. + diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst new file mode 100644 index 0000000000..e882ce6e88 --- /dev/null +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -0,0 +1,619 @@ +.. _extendedpatternmatching: + +Extended pattern matching +========================= + +:Authors: Cristina Cornes and Hugo Herbelin + +.. TODO links to figures + +This section describes the full form of pattern matching in |Coq| terms. + +.. |rhs| replace:: right hand sides + +Patterns +-------- + +The full syntax of match is presented in Figures 1.1 and 1.2. +Identifiers in patterns are either constructor names or variables. Any +identifier that is not the constructor of an inductive or co-inductive +type is considered to be a variable. A variable name cannot occur more +than once in a given pattern. It is recommended to start variable +names by a lowercase letter. + +If a pattern has the form ``(c x)`` where ``c`` is a constructor symbol and x +is a linear vector of (distinct) variables, it is called *simple*: it +is the kind of pattern recognized by the basic version of match. On +the opposite, if it is a variable ``x`` or has the form ``(c p)`` with ``p`` not +only made of variables, the pattern is called *nested*. + +A variable pattern matches any value, and the identifier is bound to +that value. The pattern “``_``” (called “don't care” or “wildcard” symbol) +also matches any value, but does not bind anything. It may occur an +arbitrary number of times in a pattern. Alias patterns written +:n:`(@pattern as @ident)` are also accepted. This pattern matches the +same values as :token:`pattern` does and :token:`ident` is bound to the matched +value. A pattern of the form :n:`@pattern | @pattern` is called disjunctive. A +list of patterns separated with commas is also considered as a pattern +and is called *multiple pattern*. However multiple patterns can only +occur at the root of pattern matching equations. Disjunctions of +*multiple patterns* are allowed though. + +Since extended ``match`` expressions are compiled into the primitive ones, +the expressiveness of the theory remains the same. Once parsing has finished +only simple patterns remain. The original nesting of the ``match`` expressions +is recovered at printing time. An easy way to see the result +of the expansion is to toggle off the nesting performed at printing +(use here :flag:`Printing Matching`), then by printing the term with :cmd:`Print` +if the term is a constant, or using the command :cmd:`Check`. + +The extended ``match`` still accepts an optional *elimination predicate* +given after the keyword ``return``. Given a pattern matching expression, +if all the right-hand-sides of ``=>`` have the same +type, then this type can be sometimes synthesized, and so we can omit +the return part. Otherwise the predicate after return has to be +provided, like for the basicmatch. + +Let us illustrate through examples the different aspects of extended +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 + + Fixpoint max (n m:nat) {struct m} : nat := + match n with + | O => m + | S n' => match m with + | O => S n' + | S m' => S (max n' m') + end + end. + +Multiple patterns +----------------- + +Using multiple patterns in the definition of ``max`` lets us write: + +.. coqtop:: in reset + + Fixpoint max (n m:nat) {struct m} : nat := + match n, m with + | O, _ => m + | S n', O => S n' + | S n', S m' => S (max n' m') + end. + +which will be compiled into the previous form. + +The pattern matching compilation strategy examines patterns from left +to right. A match expression is generated **only** when there is at least +one constructor in the column of patterns. E.g. the following example +does not build a match expression. + +.. coqtop:: all + + Check (fun x:nat => match x return nat with + | y => y + end). + + +Aliasing subpatterns +-------------------- + +We can also use :n:`as @ident` to associate a name to a sub-pattern: + +.. coqtop:: in reset + + Fixpoint max (n m:nat) {struct n} : nat := + match n, m with + | O, _ => m + | S n' as p, O => p + | S n', S m' => S (max n' m') + end. + +Nested patterns +--------------- + +Here is now an example of nested patterns: + +.. coqtop:: in + + Fixpoint even (n:nat) : bool := + match n with + | O => true + | S O => false + | S (S n') => even n' + end. + +This is compiled into: + +.. 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 + + Fixpoint lef (n m:nat) {struct m} : bool := + match n, m with + | O, x => true + | x, O => false + | S n, S m => lef n m + end. + +Note that the first and the second multiple pattern overlap because +the couple of values ``O O`` matches both. Thus, what is the result of the +function on those values? To eliminate ambiguity we use the *textual +priority rule:* we consider patterns to be ordered from top to bottom. A +value is matched by the pattern at the ith row if and only if it is +not matched by some pattern from a previous row. Thus in the example, ``O O`` +is matched by the first pattern, and so :g:`(lef O O)` yields true. + +Another way to write this function is: + +.. coqtop:: in reset + + Fixpoint lef (n m:nat) {struct m} : bool := + match n, m with + | O, x => true + | S n, S m => lef n m + | _, _ => false + end. + +Here the last pattern superposes with the first two. Because of the +priority rule, the last pattern will be used only for values that do +not match neither the first nor the second one. + +Terms with useless patterns are not accepted by the system. Here is an +example: + +.. coqtop:: all + + Fail Check (fun x:nat => + match x with + | O => true + | S _ => false + | x => true + end). + + +Disjunctive patterns +-------------------- + +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 reset + + Fixpoint max (n m:nat) {struct m} : nat := + match n, m with + | S n', S m' => S (max n' m') + | 0, p | p, 0 => p + end. + +Similarly, factorization of (not necessarily multiple) patterns that +share the same variables is possible by using the notation :n:`{+| @pattern}`. +Here is an example: + +.. coqtop:: in + + Definition filter_2_4 (n:nat) : nat := + match n with + | 2 as m | 4 as m => m + | _ => 0 + end. + + +Here is another example using disjunctive subpatterns. + +.. coqtop:: in + + Definition filter_some_square_corners (p:nat*nat) : nat*nat := + match p with + | ((2 as m | 4 as m), (3 as n | 5 as n)) => (m,n) + | _ => (0,0) + end. + +About patterns of parametric types +---------------------------------- + +Parameters in patterns +~~~~~~~~~~~~~~~~~~~~~~ + +When matching objects of a parametric type, parameters do not bind in +patterns. They must be substituted by “``_``”. Consider for example the +type of polymorphic lists: + +.. coqtop:: in + + Inductive List (A:Set) : Set := + | nil : List A + | cons : A -> List A -> List A. + +We can check the function *tail*: + +.. coqtop:: all + + Check + (fun l:List nat => + match l with + | nil _ => nil nat + | cons _ _ l' => l' + end). + +When we use parameters in patterns there is an error message: + +.. coqtop:: all + + Fail Check + (fun l:List nat => + match l with + | nil A => nil nat + | cons A _ l' => l' + end). + +.. flag:: Asymmetric Patterns + + This flag (off by default) removes parameters from constructors in patterns: + +.. coqtop:: all + + Set Asymmetric Patterns. + Check (fun l:List nat => + match l with + | nil => nil _ + | cons _ l' => l' + end). + Unset Asymmetric Patterns. + +Implicit arguments in patterns +------------------------------ + +By default, implicit arguments are omitted in patterns. So we write: + +.. coqtop:: all + + Arguments nil {A}. + Arguments cons [A] _ _. + Check + (fun l:List nat => + match l with + | nil => nil + | cons _ l' => l' + end). + +But the possibility to use all the arguments is given by “``@``” implicit +explicitations (as for terms, see :ref:`explicit-applications`). + +.. coqtop:: all + + Check + (fun l:List nat => + match l with + | @nil _ => @nil nat + | @cons _ _ l' => l' + end). + + +.. _matching-dependent: + +Matching objects of dependent types +----------------------------------- + +The previous examples illustrate pattern matching on objects of non- +dependent types, but we can also use the expansion strategy to +destructure objects of dependent types. Consider the type :g:`listn` of +lists of a certain length: + +.. coqtop:: in reset + + Inductive listn : nat -> Set := + | niln : listn 0 + | consn : forall n:nat, nat -> listn n -> listn (S n). + + +Understanding dependencies in patterns +-------------------------------------- + +We can define the function length over :g:`listn` by: + +.. coqdoc:: + + Definition length (n:nat) (l:listn n) := n. + +Just for illustrating pattern matching, we can define it by case +analysis: + +.. coqtop:: in + + Definition length (n:nat) (l:listn n) := + match l with + | niln => 0 + | consn n _ _ => S n + end. + +We can understand the meaning of this definition using the same +notions of usual pattern matching. + + +When the elimination predicate must be provided +----------------------------------------------- + +Dependent pattern matching +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The examples given so far do not need an explicit elimination +predicate because all the |rhs| have the same type and Coq +succeeds to synthesize it. Unfortunately when dealing with dependent +patterns it often happens that we need to write cases where the types +of the |rhs| are different instances of the elimination predicate. The +function :g:`concat` for :g:`listn` is an example where the branches have +different types and we need to provide the elimination predicate: + +.. coqtop:: in + + Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : + listn (n + m) := + match l in listn n return listn (n + m) with + | niln => l' + | 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`. + +In the concrete syntax, it should be written : +``match m as x in (I _ … _ y1 … ys) return Q with … end``. +The variables which appear in the ``in`` and ``as`` clause are new and bounded +in the property :g:`Q` in the return clause. The parameters of the +inductive definitions should not be mentioned and are replaced by ``_``. + +Multiple dependent pattern matching +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Recall that a list of patterns is also a pattern. So, when we +destructure several terms at the same time and the branches have +different types we need to provide the elimination predicate for this +multiple pattern. It is done using the same scheme: each term may be +associated to an ``as`` clause and an ``in`` clause in order to introduce +a dependent product. + +For example, an equivalent definition for :g:`concat` (even though the +matching on the second term is trivial) would have been: + +.. coqtop:: in + + Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : + listn (n + m) := + match l in listn n, l' return listn (n + m) with + | niln, x => x + | consn n' a y, x => consn (n' + m) a (concat n' y m x) + end. + +Even without real matching over the second term, this construction can +be used to keep types linked. If :g:`a` and :g:`b` are two :g:`listn` of the same +length, by writing + +.. coqtop:: in + + Check (fun n (a b: listn n) => + match a, b with + | niln, b0 => tt + | consn n' a y, bS => tt + end). + +we have a copy of :g:`b` in type :g:`listn 0` resp. :g:`listn (S n')`. + +.. _match-in-patterns: + +Patterns in ``in`` +~~~~~~~~~~~~~~~~~~ + +If the type of the matched term is more precise than an inductive +applied to variables, arguments of the inductive in the ``in`` branch can +be more complicated patterns than a variable. + +Moreover, constructors whose types do not follow the same pattern will +become impossible branches. In an impossible branch, you can answer +anything but False_rect unit has the advantage to be subterm of +anything. + +To be concrete: the ``tail`` function can be written: + +.. coqtop:: in + + Definition tail n (v: listn (S n)) := + match v in listn (S m) return listn m with + | niln => False_rect unit + | consn n' a y => y + end. + +and :g:`tail n v` will be subterm of :g:`v`. + +Using pattern matching to write proofs +-------------------------------------- + +In all the previous examples the elimination predicate does not depend +on the object(s) matched. But it may depend and the typical case is +when we write a proof by induction or a function that yields an object +of a dependent type. An example of a proof written using ``match`` is given +in the description of the tactic :tacn:`refine`. + +For example, we can write the function :g:`buildlist` that given a natural +number :g:`n` builds a list of length :g:`n` containing zeros as follows: + +.. coqtop:: in + + Fixpoint buildlist (n:nat) : listn n := + match n return listn n with + | O => niln + | S n => consn n 0 (buildlist n) + end. + +We can also use multiple patterns. Consider the following definition +of the predicate less-equal :g:`Le`: + +.. coqtop:: in + + Inductive LE : nat -> nat -> Prop := + | LEO : forall n:nat, LE 0 n + | LES : forall n m:nat, LE n m -> LE (S n) (S m). + +We can use multiple patterns to write the proof of the lemma +:g:`forall (n m:nat), (LE n m) \/ (LE m n)`: + +.. coqtop:: in + + Fixpoint dec (n m:nat) {struct n} : LE n m \/ LE m n := + match n, m return LE n m \/ LE m n with + | O, x => or_introl (LE x 0) (LEO x) + | x, O => or_intror (LE x 0) (LEO x) + | S n as n', S m as m' => + match dec n m with + | or_introl h => or_introl (LE m' n') (LES n m h) + | or_intror h => or_intror (LE n' m') (LES m n h) + end + end. + +In the example of :g:`dec`, the first match is dependent while the second +is not. + +The user can also use match in combination with the tactic :tacn:`refine` (see +Section 8.2.3) to build incomplete proofs beginning with a match +construction. + + +Pattern-matching on inductive objects involving local definitions +----------------------------------------------------------------- + +If local definitions occur in the type of a constructor, then there +are two ways to match on this constructor. Either the local +definitions are skipped and matching is done only on the true +arguments of the constructors, or the bindings for local definitions +can also be caught in the matching. + +.. example:: + + .. coqtop:: in reset + + Inductive list : nat -> Set := + | nil : list 0 + | cons : forall n:nat, let m := (2 * n) in list m -> list (S (S m)). + + In the next example, the local definition is not caught. + + .. coqtop:: in + + Fixpoint length n (l:list n) {struct l} : nat := + match l with + | nil => 0 + | cons n l0 => S (length (2 * n) l0) + end. + + But in this example, it is. + + .. coqtop:: in + + Fixpoint length' n (l:list n) {struct l} : nat := + match l with + | nil => 0 + | @cons _ m l0 => S (length' m l0) + end. + +.. note:: For a given matching clause, either none of the local + definitions or all of them can be caught. + +.. note:: You can only catch let bindings in mode where you bind all + variables and so you have to use ``@`` syntax. + +.. note:: this feature is incoherent with the fact that parameters + cannot be caught and consequently is somehow hidden. For example, + there is no mention of it in error messages. + +Pattern-matching and coercions +------------------------------ + +If a mismatch occurs between the expected type of a pattern and its +actual type, a coercion made from constructors is sought. If such a +coercion can be found, it is automatically inserted around the +pattern. + +.. example:: + + .. coqtop:: in + + Inductive I : Set := + | C1 : nat -> I + | C2 : I -> I. + + Coercion C1 : nat >-> I. + + .. coqtop:: all + + Check (fun x => match x with + | C2 O => 0 + | _ => 0 + end). + + +When does the expansion strategy fail? +-------------------------------------- + +The strategy works very like in ML languages when treating patterns of +non-dependent types. But there are new cases of failure that are due to +the presence of dependencies. + +The error messages of the current implementation may be sometimes +confusing. When the tactic fails because patterns are somehow +incorrect then error messages refer to the initial expression. But the +strategy may succeed to build an expression whose sub-expressions are +well typed when the whole expression is not. In this situation the +message makes reference to the expanded expression. We encourage +users, when they have patterns with the same outer constructor in +different equations, to name the variable patterns in the same +positions with the same name. E.g. to write ``(cons n O x) => e1`` and +``(cons n _ x) => e2`` instead of ``(cons n O x) => e1`` and +``(cons n' _ x') => e2``. This helps to maintain certain name correspondence between the +generated expression and the original. + +Here is a summary of the error messages corresponding to each +situation: + +.. exn:: The constructor @ident expects @num arguments. + + The variable ident is bound several times in pattern termFound a constructor + of inductive type term while a constructor of term is expectedPatterns are + incorrect (because constructors are not applied to the correct number of the + arguments, because they are not linear or they are wrongly typed). + +.. exn:: Non exhaustive pattern matching. + + The pattern matching is not exhaustive. + +.. exn:: The elimination predicate term should be of arity @num (for non \ + dependent case) or @num (for dependent case). + + The elimination predicate provided to match has not the expected arity. + +.. exn:: Unable to infer a match predicate + Either there is a type incompatibility or the problem involves dependencies. + + There is a type mismatch between the different branches. The user should + provide an elimination predicate. diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst new file mode 100644 index 0000000000..e93b01f14d --- /dev/null +++ b/doc/sphinx/addendum/extraction.rst @@ -0,0 +1,630 @@ +.. _extraction: + +Extraction of programs in |OCaml| and Haskell +============================================= + +:Authors: Jean-Christophe Filliâtre and Pierre Letouzey + +We present here the |Coq| extraction commands, used to build certified +and relatively efficient functional programs, extracting them from +either |Coq| functions or |Coq| proofs of specifications. The +functional languages available as output are currently |OCaml|, Haskell +and Scheme. In the following, "ML" will be used (abusively) to refer +to any of the three. + +Before using any of the commands or options described in this chapter, +the extraction framework should first be loaded explicitly +via ``Require Extraction``, or via the more robust +``From Coq Require Extraction``. +Note that in earlier versions of Coq, these commands and options were +directly available without any preliminary ``Require``. + +.. coqtop:: in + + Require Extraction. + +Generating ML Code +------------------- + +.. note:: + + In the following, a qualified identifier :token:`qualid` + can be used to refer to any kind of |Coq| global "object" : constant, + inductive type, inductive constructor or module name. + +The next two commands are meant to be used for rapid preview of +extraction. They both display extracted term(s) inside |Coq|. + +.. cmd:: Extraction @qualid + + Extraction of the mentioned object in the |Coq| toplevel. + +.. cmd:: Recursive Extraction {+ @qualid } + + Recursive extraction of all the mentioned objects and + all their dependencies in the |Coq| toplevel. + +All the following commands produce real ML files. User can choose to +produce one monolithic file or one file per |Coq| library. + +.. cmd:: Extraction @string {+ @qualid } + + Recursive extraction of all the mentioned objects and all + their dependencies in one monolithic file :token:`string`. + Global and local identifiers are renamed according to the chosen ML + language to fulfill its syntactic conventions, keeping original + names as much as possible. + +.. cmd:: Extraction Library @ident + + Extraction of the whole |Coq| library :n:`@ident.v` to an ML module + :n:`@ident.ml`. In case of name clash, identifiers are here renamed + using prefixes ``coq_`` or ``Coq_`` to ensure a session-independent + renaming. + +.. cmd:: Recursive Extraction Library @ident + + Extraction of the |Coq| library :n:`@ident.v` and all other modules + :n:`@ident.v` depends on. + +.. cmd:: Separate Extraction {+ @qualid } + + Recursive extraction of all the mentioned objects and all + their dependencies, just as :n:`Extraction @string {+ @qualid }`, + but instead of producing one monolithic file, this command splits + the produced code in separate ML files, one per corresponding Coq + ``.v`` file. This command is hence quite similar to + :cmd:`Recursive Extraction Library`, except that only the needed + parts of Coq libraries are extracted instead of the whole. + The naming convention in case of name clash is the same one as + :cmd:`Extraction Library`: identifiers are here renamed using prefixes + ``coq_`` or ``Coq_``. + +The following command is meant to help automatic testing of +the extraction, see for instance the ``test-suite`` directory +in the |Coq| sources. + +.. cmd:: Extraction TestCompile {+ @qualid } + + All the mentioned objects and all their dependencies are extracted + to a temporary |OCaml| file, just as in ``Extraction "file"``. Then + this temporary file and its signature are compiled with the same + |OCaml| compiler used to built |Coq|. This command succeeds only + if the extraction and the |OCaml| compilation succeed. It fails + if the current target language of the extraction is not |OCaml|. + +Extraction Options +------------------- + +Setting the target language +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Extraction Language ( OCaml | Haskell | Scheme ) + :name: Extraction Language + + The ability to fix target language is the first and more important + of the extraction options. Default is ``OCaml``. + + +Inlining and optimizations +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Since |OCaml| is a strict language, the extracted code has to +be optimized in order to be efficient (for instance, when using +induction principles we do not want to compute all the recursive calls +but only the needed ones). So the extraction mechanism provides an +automatic optimization routine that will be called each time the user +wants to generate an |OCaml| program. The optimizations can be split in two +groups: the type-preserving ones (essentially constant inlining and +reductions) and the non type-preserving ones (some function +abstractions of dummy types are removed when it is deemed safe in order +to have more elegant types). Therefore some constants may not appear in the +resulting monolithic |OCaml| program. In the case of modular extraction, +even if some inlining is done, the inlined constants are nevertheless +printed, to ensure session-independent programs. + +Concerning Haskell, type-preserving optimizations are less useful +because of laziness. We still make some optimizations, for example in +order to produce more readable code. + +The type-preserving optimizations are controlled by the following |Coq| options: + +.. flag:: Extraction Optimize + + Default is on. This controls all type-preserving optimizations made on + the ML terms (mostly reduction of dummy beta/iota redexes, but also + simplifications on Cases, etc). Turn this option off if you want a + ML term as close as possible to the Coq term. + +.. flag:: Extraction Conservative Types + + Default is off. This controls the non type-preserving optimizations + made on ML terms (which try to avoid function abstraction of dummy + types). Turn this option on to make sure that ``e:t`` + implies that ``e':t'`` where ``e'`` and ``t'`` are the extracted + code of ``e`` and ``t`` respectively. + +.. flag:: Extraction KeepSingleton + + Default is off. Normally, when the extraction of an inductive type + produces a singleton type (i.e. a type with only one constructor, and + only one argument to this constructor), the inductive structure is + removed and this type is seen as an alias to the inner type. + The typical example is ``sig``. This option allows disabling this + optimization when one wishes to preserve the inductive structure of types. + +.. flag:: Extraction AutoInline + + Default is on. The extraction mechanism inlines the bodies of + some defined constants, according to some heuristics + like size of bodies, uselessness of some arguments, etc. + Those heuristics are not always perfect; if you want to disable + this feature, turn this option off. + +.. cmd:: Extraction Inline {+ @qualid } + + In addition to the automatic inline feature, the constants + mentioned by this command will always be inlined during extraction. + +.. cmd:: Extraction NoInline {+ @qualid } + + Conversely, the constants mentionned by this command will + never be inlined during extraction. + +.. cmd:: Print Extraction Inline + + Prints the current state of the table recording the custom inlinings + declared by the two previous commands. + +.. cmd:: Reset Extraction Inline + + Empties the table recording the custom inlinings (see the + previous commands). + +**Inlining and printing of a constant declaration:** + +The user can explicitly ask for a constant to be extracted by two means: + + * by mentioning it on the extraction command line + + * by extracting the whole |Coq| module of this constant. + +In both cases, the declaration of this constant will be present in the +produced file. But this same constant may or may not be inlined in +the following terms, depending on the automatic/custom inlining mechanism. + +For the constants non-explicitly required but needed for dependency +reasons, there are two cases: + + * If an inlining decision is taken, whether automatically or not, + all occurrences of this constant are replaced by its extracted body, + and this constant is not declared in the generated file. + + * If no inlining decision is taken, the constant is normally + declared in the produced file. + +Extra elimination of useless arguments +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The following command provides some extra manual control on the +code elimination performed during extraction, in a way which +is independent but complementary to the main elimination +principles of extraction (logical parts and types). + +.. cmd:: Extraction Implicit @qualid [ {+ @ident } ] + + This experimental command allows declaring some arguments of + :token:`qualid` as implicit, i.e. useless in extracted code and hence to + be removed by extraction. Here :token:`qualid` can be any function or + inductive constructor, and the given :token:`ident` are the names of + the concerned arguments. In fact, an argument can also be referred + by a number indicating its position, starting from 1. + +When an actual extraction takes place, an error is normally raised if the +:cmd:`Extraction Implicit` declarations cannot be honored, that is +if any of the implicit arguments still occurs in the final code. +This behavior can be relaxed via the following option: + +.. flag:: Extraction SafeImplicits + + Default is on. When this option is off, a warning is emitted + instead of an error if some implicit arguments still occur in the + final code of an extraction. This way, the extracted code may be + obtained nonetheless and reviewed manually to locate the source of the issue + (in the code, some comments mark the location of these remaining implicit arguments). + Note that this extracted code might not compile or run properly, + depending of the use of these remaining implicit arguments. + +Realizing axioms +~~~~~~~~~~~~~~~~ + +Extraction will fail if it encounters an informative axiom not realized. +A warning will be issued if it encounters a logical axiom, to remind the +user that inconsistent logical axioms may lead to incorrect or +non-terminating extracted terms. + +It is possible to assume some axioms while developing a proof. Since +these axioms can be any kind of proposition or object or type, they may +perfectly well have some computational content. But a program must be +a closed term, and of course the system cannot guess the program which +realizes an axiom. Therefore, it is possible to tell the system +what ML term corresponds to a given axiom. + +.. cmd:: Extract Constant @qualid => @string + + Give an ML extraction for the given constant. + The :token:`string` may be an identifier or a quoted string. + +.. cmd:: Extract Inlined Constant @qualid => @string + + Same as the previous one, except that the given ML terms will + be inlined everywhere instead of being declared via a ``let``. + + .. note:: + This command is sugar for an :cmd:`Extract Constant` followed + by a :cmd:`Extraction Inline`. Hence a :cmd:`Reset Extraction Inline` + will have an effect on the realized and inlined axiom. + +.. caution:: It is the responsibility of the user to ensure that the ML + terms given to realize the axioms do have the expected types. In + fact, the strings containing realizing code are just copied to the + extracted files. The extraction recognizes whether the realized axiom + should become a ML type constant or a ML object declaration. For example: + +.. coqtop:: in + + Axiom X:Set. + Axiom x:X. + Extract Constant X => "int". + Extract Constant x => "0". + +Notice that in the case of type scheme axiom (i.e. whose type is an +arity, that is a sequence of product finished by a sort), then some type +variables have to be given (as quoted strings). The syntax is then: + +.. cmdv:: Extract Constant @qualid @string ... @string => @string + :undocumented: + +The number of type variables is checked by the system. For example: + +.. coqtop:: in + + Axiom Y : Set -> Set -> Set. + Extract Constant Y "'a" "'b" => " 'a * 'b ". + +Realizing an axiom via :cmd:`Extract Constant` is only useful in the +case of an informative axiom (of sort ``Type`` or ``Set``). A logical axiom +has no computational content and hence will not appear in extracted +terms. But a warning is nonetheless issued if extraction encounters a +logical axiom. This warning reminds user that inconsistent logical +axioms may lead to incorrect or non-terminating extracted terms. + +If an informative axiom has not been realized before an extraction, a +warning is also issued and the definition of the axiom is filled with +an exception labeled ``AXIOM TO BE REALIZED``. The user must then +search these exceptions inside the extracted file and replace them by +real code. + +Realizing inductive types +~~~~~~~~~~~~~~~~~~~~~~~~~ + +The system also provides a mechanism to specify ML terms for inductive +types and constructors. For instance, the user may want to use the ML +native boolean type instead of the |Coq| one. The syntax is the following: + +.. cmd:: Extract Inductive @qualid => @string [ {+ @string } ] + + Give an ML extraction for the given inductive type. You must specify + extractions for the type itself (first :token:`string`) and all its + constructors (all the :token:`string` between square brackets). In this form, + the ML extraction must be an ML inductive datatype, and the native + pattern matching of the language will be used. + +.. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string + + Same as before, with a final extra :token:`string` that indicates how to + perform pattern matching over this inductive type. In this form, + the ML extraction could be an arbitrary type. + For an inductive type with :math:`k` constructors, the function used to + emulate the pattern matching should expect :math:`k+1` arguments, first the :math:`k` + branches in functional form, and then the inductive element to + destruct. For instance, the match branch ``| S n => foo`` gives the + functional form ``(fun n -> foo)``. Note that a constructor with no + arguments is considered to have one unit argument, in order to block + early evaluation of the branch: ``| O => bar`` leads to the functional + form ``(fun () -> bar)``. For instance, when extracting :g:`nat` + into |OCaml| ``int``, the code to be provided has type: + ``(unit->'a)->(int->'a)->int->'a``. + +.. caution:: As for :cmd:`Extract Constant`, this command should be used with care: + + * The ML code provided by the user is currently **not** checked at all by + extraction, even for syntax errors. + + * Extracting an inductive type to a pre-existing ML inductive type + is quite sound. But extracting to a general type (by providing an + ad-hoc pattern matching) will often **not** be fully rigorously + correct. For instance, when extracting ``nat`` to |OCaml| ``int``, + it is theoretically possible to build ``nat`` values that are + larger than |OCaml| ``max_int``. It is the user's responsibility to + be sure that no overflow or other bad events occur in practice. + + * Translating an inductive type to an arbitrary ML type does **not** + magically improve the asymptotic complexity of functions, even if the + ML type is an efficient representation. For instance, when extracting + ``nat`` to |OCaml| ``int``, the function ``Nat.mul`` stays quadratic. + It might be interesting to associate this translation with + some specific :cmd:`Extract Constant` when primitive counterparts exist. + +Typical examples are the following: + +.. coqtop:: in + + Extract Inductive unit => "unit" [ "()" ]. + Extract Inductive bool => "bool" [ "true" "false" ]. + Extract Inductive sumbool => "bool" [ "true" "false" ]. + +.. note:: + + When extracting to |OCaml|, if an inductive constructor or type has arity 2 and + the corresponding string is enclosed by parentheses, and the string meets + |OCaml|'s lexical criteria for an infix symbol, then the rest of the string is + used as an infix constructor or type. + +.. coqtop:: in + + Extract Inductive list => "list" [ "[]" "(::)" ]. + Extract Inductive prod => "(*)" [ "(,)" ]. + +As an example of translation to a non-inductive datatype, let's turn +``nat`` into |OCaml| ``int`` (see caveat above): + +.. coqtop:: in + + Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))". + +Avoiding conflicts with existing filenames +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +When using :cmd:`Extraction Library`, the names of the extracted files +directly depend on the names of the |Coq| files. It may happen that +these filenames are in conflict with already existing files, +either in the standard library of the target language or in other +code that is meant to be linked with the extracted code. +For instance the module ``List`` exists both in |Coq| and in |OCaml|. +It is possible to instruct the extraction not to use particular filenames. + +.. cmd:: Extraction Blacklist {+ @ident } + + Instruct the extraction to avoid using these names as filenames + for extracted code. + +.. cmd:: Print Extraction Blacklist + + Show the current list of filenames the extraction should avoid. + +.. cmd:: Reset Extraction Blacklist + + Allow the extraction to use any filename. + +For |OCaml|, a typical use of these commands is +``Extraction Blacklist String List``. + +Additional settings +~~~~~~~~~~~~~~~~~~~ + +.. opt:: Extraction File Comment @string + :name: Extraction File Comment + + Provides a comment that is included at the beginning of the output files. + +.. opt:: Extraction Flag @num + :name: Extraction Flag + + Controls which optimizations are used during extraction, providing a finer-grained + control than :flag:`Extraction Optimize`. The bits of :token:`num` are used as a bit mask. + Keeping an option off keeps the extracted ML more similar to the Coq term. + Values are: + + +-----+-------+----------------------------------------------------------------+ + | Bit | Value | Optimization (default is on unless noted otherwise) | + +-----+-------+----------------------------------------------------------------+ + | 0 | 1 | Remove local dummy variables | + +-----+-------+----------------------------------------------------------------+ + | 1 | 2 | Use special treatment for fixpoints | + +-----+-------+----------------------------------------------------------------+ + | 2 | 4 | Simplify case with iota-redux | + +-----+-------+----------------------------------------------------------------+ + | 3 | 8 | Factor case branches as functions | + +-----+-------+----------------------------------------------------------------+ + | 4 | 16 | (not available, default false) | + +-----+-------+----------------------------------------------------------------+ + | 5 | 32 | Simplify case as function of one argument | + +-----+-------+----------------------------------------------------------------+ + | 6 | 64 | Simplify case by swapping case and lambda | + +-----+-------+----------------------------------------------------------------+ + | 7 | 128 | Some case optimization | + +-----+-------+----------------------------------------------------------------+ + | 8 | 256 | Push arguments inside a letin | + +-----+-------+----------------------------------------------------------------+ + | 9 | 512 | Use linear let reduction (default false) | + +-----+-------+----------------------------------------------------------------+ + | 10 | 1024 | Use linear beta reduction (default false) | + +-----+-------+----------------------------------------------------------------+ + +.. flag:: Extraction TypeExpand + + If set, fully expand Coq types in ML. See the Coq source code to learn more. + +Differences between |Coq| and ML type systems +---------------------------------------------- + +Due to differences between |Coq| and ML type systems, +some extracted programs are not directly typable in ML. +We now solve this problem (at least in |OCaml|) by adding +when needed some unsafe casting ``Obj.magic``, which give +a generic type ``'a`` to any term. + +First, if some part of the program is *very* polymorphic, there +may be no ML type for it. In that case the extraction to ML works +alright but the generated code may be refused by the ML +type checker. A very well known example is the ``distr-pair`` +function: + +.. coqtop:: in + + Definition dp {A B:Type}(x:A)(y:B)(f:forall C:Type, C->C) := (f A x, f B y). + +In |OCaml|, for instance, the direct extracted term would be:: + + let dp x y f = Pair((f () x),(f () y)) + +and would have type:: + + dp : 'a -> 'a -> (unit -> 'a -> 'b) -> ('b,'b) prod + +which is not its original type, but a restriction. + +We now produce the following correct version:: + + let dp x y f = Pair ((Obj.magic f () x), (Obj.magic f () y)) + +Secondly, some |Coq| definitions may have no counterpart in ML. This +happens when there is a quantification over types inside the type +of a constructor; for example: + +.. coqtop:: in + + Inductive anything : Type := dummy : forall A:Set, A -> anything. + +which corresponds to the definition of an ML dynamic type. +In |OCaml|, we must cast any argument of the constructor dummy +(no GADT are produced yet by the extraction). + +Even with those unsafe castings, you should never get error like +``segmentation fault``. In fact even if your program may seem +ill-typed to the |OCaml| type checker, it can't go wrong : it comes +from a Coq well-typed terms, so for example inductive types will always +have the correct number of arguments, etc. Of course, when launching +manually some extracted function, you should apply it to arguments +of the right shape (from the |Coq| point-of-view). + +More details about the correctness of the extracted programs can be +found in :cite:`Let02`. + +We have to say, though, that in most "realistic" programs, these problems do not +occur. For example all the programs of Coq library are accepted by the |OCaml| +type checker without any ``Obj.magic`` (see examples below). + +Some examples +------------- + +We present here two examples of extraction, taken from the +|Coq| Standard Library. We choose |OCaml| as the target language, +but everything, with slight modifications, can also be done in the +other languages supported by extraction. +We then indicate where to find other examples and tests of extraction. + +A detailed example: Euclidean division +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The file ``Euclid`` contains the proof of Euclidean division. +The natural numbers used here are unary, represented by the type``nat``, +which is defined by two constructors ``O`` and ``S``. +This module contains a theorem ``eucl_dev``, whose type is:: + + forall b:nat, b > 0 -> forall a:nat, diveucl a b + +where ``diveucl`` is a type for the pair of the quotient and the +modulo, plus some logical assertions that disappear during extraction. +We can now extract this program to |OCaml|: + +.. coqtop:: none + + Reset Initial. + +.. coqtop:: all + + Require Extraction. + Require Import Euclid Wf_nat. + Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2. + Recursive Extraction eucl_dev. + +The inlining of ``gt_wf_rec`` and others is not +mandatory. It only enhances readability of extracted code. +You can then copy-paste the output to a file ``euclid.ml`` or let +|Coq| do it for you with the following command:: + + Extraction "euclid" eucl_dev. + +Let us play the resulting program (in an |OCaml| toplevel):: + + #use "euclid.ml";; + type nat = O | S of nat + type sumbool = Left | Right + val sub : nat -> nat -> nat = <fun> + val le_lt_dec : nat -> nat -> sumbool = <fun> + val le_gt_dec : nat -> nat -> sumbool = <fun> + type diveucl = Divex of nat * nat + val eucl_dev : nat -> nat -> diveucl = <fun> + + # eucl_dev (S (S O)) (S (S (S (S (S O)))));; + - : diveucl = Divex (S (S O), S O) + +It is easier to test on |OCaml| integers:: + + # let rec nat_of_int = function 0 -> O | n -> S (nat_of_int (n-1));; + val nat_of_int : int -> nat = <fun> + + # let rec int_of_nat = function O -> 0 | S p -> 1+(int_of_nat p);; + val int_of_nat : nat -> int = <fun> + + # let div a b = + let Divex (q,r) = eucl_dev (nat_of_int b) (nat_of_int a) + in (int_of_nat q, int_of_nat r);; + val div : int -> int -> int * int = <fun> + + # div 173 15;; + - : int * int = (11, 8) + +Note that these ``nat_of_int`` and ``int_of_nat`` are now +available via a mere ``Require Import ExtrOcamlIntConv`` and then +adding these functions to the list of functions to extract. This file +``ExtrOcamlIntConv.v`` and some others in ``plugins/extraction/`` +are meant to help building concrete program via extraction. + +Extraction's horror museum +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Some pathological examples of extraction are grouped in the file +``test-suite/success/extraction.v`` of the sources of |Coq|. + +Users' Contributions +~~~~~~~~~~~~~~~~~~~~ + +Several of the |Coq| Users' Contributions use extraction to produce +certified programs. In particular the following ones have an automatic +extraction test: + + * ``additions`` : https://github.com/coq-contribs/additions + * ``bdds`` : https://github.com/coq-contribs/bdds + * ``canon-bdds`` : https://github.com/coq-contribs/canon-bdds + * ``chinese`` : https://github.com/coq-contribs/chinese + * ``continuations`` : https://github.com/coq-contribs/continuations + * ``coq-in-coq`` : https://github.com/coq-contribs/coq-in-coq + * ``exceptions`` : https://github.com/coq-contribs/exceptions + * ``firing-squad`` : https://github.com/coq-contribs/firing-squad + * ``founify`` : https://github.com/coq-contribs/founify + * ``graphs`` : https://github.com/coq-contribs/graphs + * ``higman-cf`` : https://github.com/coq-contribs/higman-cf + * ``higman-nw`` : https://github.com/coq-contribs/higman-nw + * ``hardware`` : https://github.com/coq-contribs/hardware + * ``multiplier`` : https://github.com/coq-contribs/multiplier + * ``search-trees`` : https://github.com/coq-contribs/search-trees + * ``stalmarck`` : https://github.com/coq-contribs/stalmarck + +Note that ``continuations`` and ``multiplier`` are a bit particular. They are +examples of developments where ``Obj.magic`` is needed. This is +probably due to a heavy use of impredicativity. After compilation, those +two examples run nonetheless, thanks to the correction of the +extraction :cite:`Let02`. diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst new file mode 100644 index 0000000000..b474c51f17 --- /dev/null +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -0,0 +1,833 @@ +.. _generalizedrewriting: + +Generalized rewriting +===================== + +:Author: Matthieu Sozeau + +This chapter presents the extension of several equality related +tactics to work over user-defined structures (called setoids) that are +equipped with ad-hoc equivalence relations meant to behave as +equalities. Actually, the tactics have also been generalized to +relations weaker then equivalences (e.g. rewriting systems). The +toolbox also extends the automatic rewriting capabilities of the +system, allowing the specification of custom strategies for rewriting. + +This documentation is adapted from the previous setoid documentation +by Claudio Sacerdoti Coen (based on previous work by Clément Renard). +The new implementation is a drop-in replacement for the old one +[#tabareau]_, hence most of the documentation still applies. + +The work is a complete rewrite of the previous implementation, based +on the typeclass infrastructure. It also improves on and generalizes +the previous implementation in several ways: + ++ User-extensible algorithm. The algorithm is separated into two parts: + generation of the rewriting constraints (written in ML) and solving + these constraints using typeclass resolution. As typeclass + resolution is extensible using tactics, this allows users to define + general ways to solve morphism constraints. ++ Subrelations. An example extension to the base algorithm is the + ability to define one relation as a subrelation of another so that + morphism declarations on one relation can be used automatically for + the other. This is done purely using tactics and typeclass search. ++ Rewriting under binders. It is possible to rewrite under binders in + the new implementation, if one provides the proper morphisms. Again, + most of the work is handled in the tactics. ++ First-class morphisms and signatures. Signatures and morphisms are + ordinary Coq terms, hence they can be manipulated inside Coq, put + inside structures and lemmas about them can be proved inside the + system. Higher-order morphisms are also allowed. ++ Performance. The implementation is based on a depth-first search for + the first solution to a set of constraints which can be as fast as + linear in the size of the term, and the size of the proof term is + linear in the size of the original term. Besides, the extensibility + allows the user to customize the proof search if necessary. + +.. [#tabareau] Nicolas Tabareau helped with the gluing. + +Introduction to generalized rewriting +------------------------------------- + + +Relations and morphisms +~~~~~~~~~~~~~~~~~~~~~~~ + +A parametric *relation* ``R`` is any term of type +``forall (x1 : T1) ... (xn : Tn), relation A``. +The expression ``A``, which depends on ``x1 ... xn`` , is called the *carrier* +of the relation and ``R`` is said to be a relation over ``A``; the list +``x1,...,xn`` is the (possibly empty) list of parameters of the relation. + +.. example:: Parametric relation + + It is possible to implement finite sets of elements of type ``A`` as + unordered lists of elements of type ``A``. + The function ``set_eq: forall (A : Type), relation (list A)`` + satisfied by two lists with the same elements is a parametric relation + over ``(list A)`` with one parameter ``A``. The type of ``set_eq`` + is convertible with ``forall (A : Type), list A -> list A -> Prop.`` + +An *instance* of a parametric relation ``R`` with n parameters is any term +``(R t1 ... tn)``. + +Let ``R`` be a relation over ``A`` with ``n`` parameters. A term is a parametric +proof of reflexivity for ``R`` if it has type +``forall (x1 : T1) ... (xn : Tn), reflexive (R x1 ... xn)``. +Similar definitions are given for parametric proofs of symmetry and transitivity. + +.. example:: Parametric relation (continued) + + The ``set_eq`` relation of the previous example can be proved to be + reflexive, symmetric and transitive. A parametric unary function ``f`` of type + ``forall (x1 : T1) ... (xn : Tn), A1 -> A2`` covariantly respects two parametric relation instances + ``R1`` and ``R2`` if, whenever ``x``, ``y`` satisfy ``R1 x y``, their images (``f x``) and (``f y``) + satisfy ``R2 (f x) (f y)``. An ``f`` that respects its input and output + relations will be called a unary covariant *morphism*. We can also say + that ``f`` is a monotone function with respect to ``R1`` and ``R2`` . The + sequence ``x1 ... xn`` represents the parameters of the morphism. + +Let ``R1`` and ``R2`` be two parametric relations. The *signature* of a +parametric morphism of type ``forall (x1 : T1) ... (xn : Tn), A1 -> A2`` +that covariantly respects two instances :math:`I_{R_1}` and :math:`I_{R_2}` of ``R1`` and ``R2`` +is written :math:`I_{R_1} ++> I_{R_2}`. Notice that the special arrow ++>, which +reminds the reader of covariance, is placed between the two relation +instances, not between the two carriers. The signature relation +instances and morphism will be typed in a context introducing +variables for the parameters. + +The previous definitions are extended straightforwardly to n-ary +morphisms, that are required to be simultaneously monotone on every +argument. + +Morphisms can also be contravariant in one or more of their arguments. +A morphism is contravariant on an argument associated to the relation +instance :math:`R` if it is covariant on the same argument when the inverse +relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->`` +is used in signatures for contravariant morphisms. + +Functions having arguments related by symmetric relations instances +are both covariant and contravariant in those arguments. The special +arrow ``==>`` is used in signatures for morphisms that are both +covariant and contravariant. + +An instance of a parametric morphism :math:`f` with :math:`n` +parameters is any term :math:`f \, t_1 \ldots t_n`. + +.. example:: Morphisms + + Continuing the previous example, let ``union: forall (A : Type), list A -> list A -> list A`` + perform the union of two sets by appending one list to the other. ``union` is a binary + morphism parametric over ``A`` that respects the relation instance + ``(set_eq A)``. The latter condition is proved by showing: + + .. coqdoc:: + + forall (A: Type) (S1 S1' S2 S2': list A), + set_eq A S1 S1' -> + set_eq A S2 S2' -> + set_eq A (union A S1 S2) (union A S1' S2'). + + The signature of the function ``union A`` is ``set_eq A ==> set_eq A ==> set_eq A`` + for all ``A``. + +.. example:: Contravariant morphisms + + The division function ``Rdiv : R -> R -> R`` is a morphism of signature + ``le ++> le --> le`` where ``le`` is the usual order relation over + real numbers. Notice that division is covariant in its first argument + and contravariant in its second argument. + +Leibniz equality is a relation and every function is a morphism that +respects Leibniz equality. Unfortunately, Leibniz equality is not +always the intended equality for a given structure. + +In the next section we will describe the commands to register terms as +parametric relations and morphisms. Several tactics that deal with +equality in Coq can also work with the registered relations. The exact +list of tactics will be given :ref:`in this section <tactics-enabled-on-user-provided-relations>`. +For instance, the tactic reflexivity can be used to solve a goal ``R n n`` whenever ``R`` +is an instance of a registered reflexive relation. However, the +tactics that replace in a context ``C[]`` one term with another one +related by ``R`` must verify that ``C[]`` is a morphism that respects the +intended relation. Currently the verification consists of checking +whether ``C[]`` is a syntactic composition of morphism instances that respects some obvious +compatibility constraints. + +.. example:: Rewriting + + Continuing the previous examples, suppose that the user must prove + ``set_eq int (union int (union int S1 S2) S2) (f S1 S2)`` under the + hypothesis ``H : set_eq int S2 (@nil int)``. It + is possible to use the ``rewrite`` tactic to replace the first two + occurrences of ``S2`` with ``@nil int`` in the goal since the + context ``set_eq int (union int (union int S1 nil) nil) (f S1 S2)``, + being a composition of morphisms instances, is a morphism. However the + tactic will fail replacing the third occurrence of ``S2`` unless ``f`` + has also been declared as a morphism. + + +Adding new relations and morphisms +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident + + This command declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`, + :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`. + + The :token:`ident` gives a unique name to the morphism and it is used + by the command to generate fresh names for automatically provided + lemmas used internally. + + Notice that the carrier and relation parameters may refer to the + context of variables introduced at the beginning of the declaration, + but the instances need not be made only of variables. Also notice that + ``A`` is *not* required to be a term having the same parameters as ``Aeq``, + although that is often the case in practice (this departs from the + previous implementation). + + To use this command, you need to first import the module ``Setoid`` using + the command ``Require Import Setoid``. + +.. cmd:: Add Relation + + In case the carrier and relations are not parametric, one can use this command + instead, whose syntax is the same except there is no local context. + + The proofs of reflexivity, symmetry and transitivity can be omitted if + the relation is not an equivalence relation. The proofs must be + instances of the corresponding relation definitions: e.g. the proof of + reflexivity must have a type convertible to + :g:`reflexive (A t1 ... tn) (Aeq t′ 1 …t′ n)`. + Each proof may refer to the introduced variables as well. + +.. example:: Parametric relation + + For Leibniz equality, we may declare: + + .. coqdoc:: + + Add Parametric Relation (A : Type) : A (@eq A) + [reflexivity proved by @refl_equal A] + ... + +Some tactics (:tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`transitivity`) work only on +relations that respect the expected properties. The remaining tactics +(:tacn:`replace`, :tacn:`rewrite` and derived tactics such as :tacn:`autorewrite`) do not +require any properties over the relation. However, they are able to +replace terms with related ones only in contexts that are syntactic +compositions of parametric morphism instances declared with the +following command. + +.. cmd:: Add Parametric Morphism (x1 : T1) ... (xk : Tk) : (f t1 ... tn) with signature sig as @ident + + This command declares ``f`` as a parametric morphism of signature ``sig``. The + identifier :token:`ident` gives a unique name to the morphism and it is used as + the base name of the typeclass instance definition and as the name of + the lemma that proves the well-definedness of the morphism. The + parameters of the morphism as well as the signature may refer to the + context of variables. The command asks the user to prove interactively + that ``f`` respects the relations identified from the signature. + +.. example:: + + We start the example by assuming a small theory over + homogeneous sets and we declare set equality as a parametric + equivalence relation and union of two sets as a parametric morphism. + + .. coqtop:: in + + Require Export Setoid. + Require Export Relation_Definitions. + + Set Implicit Arguments. + + Parameter set : Type -> Type. + Parameter empty : forall A, set A. + Parameter eq_set : forall A, set A -> set A -> Prop. + Parameter union : forall A, set A -> set A -> set A. + + Axiom eq_set_refl : forall A, reflexive _ (eq_set (A:=A)). + Axiom eq_set_sym : forall A, symmetric _ (eq_set (A:=A)). + Axiom eq_set_trans : forall A, transitive _ (eq_set (A:=A)). + Axiom empty_neutral : forall A (S : set A), eq_set (union S (empty A)) S. + + Axiom union_compat : + forall (A : Type), + forall x x' : set A, eq_set x x' -> + forall y y' : set A, eq_set y y' -> + eq_set (union x y) (union x' y'). + + Add Parametric Relation A : (set A) (@eq_set A) + reflexivity proved by (eq_set_refl (A:=A)) + symmetry proved by (eq_set_sym (A:=A)) + transitivity proved by (eq_set_trans (A:=A)) + as eq_set_rel. + + Add Parametric Morphism A : (@union A) + with signature (@eq_set A) ==> (@eq_set A) ==> (@eq_set A) as union_mor. + Proof. + exact (@union_compat A). + Qed. + + It is possible to reduce the burden of specifying parameters using + (maximally inserted) implicit arguments. If ``A`` is always set as + maximally implicit in the previous example, one can write: + + .. coqdoc:: + + Add Parametric Relation A : (set A) eq_set + reflexivity proved by eq_set_refl + symmetry proved by eq_set_sym + transitivity proved by eq_set_trans + as eq_set_rel. + + Add Parametric Morphism A : (@union A) with + signature eq_set ==> eq_set ==> eq_set as union_mor. + Proof. exact (@union_compat A). Qed. + + We proceed now by proving a simple lemma performing a rewrite step and + then applying reflexivity, as we would do working with Leibniz + equality. Both tactic applications are accepted since the required + properties over ``eq_set`` and ``union`` can be established from the two + declarations above. + + .. coqtop:: in + + Goal forall (S : set nat), + eq_set (union (union S (empty nat)) S) (union S S). + + .. coqtop:: in + + Proof. intros. rewrite empty_neutral. reflexivity. Qed. + + The tables of relations and morphisms are managed by the typeclass + instance mechanism. The behavior on section close is to generalize the + instances by the variables of the section (and possibly hypotheses + used in the proofs of instance declarations) but not to export them in + the rest of the development for proof search. One can use the + cmd:`Existing Instance` command to do so outside the section, using the name of the + declared morphism suffixed by ``_Morphism``, or use the ``Global`` modifier + for the corresponding class instance declaration + (see :ref:`First Class Setoids and Morphisms <first-class-setoids-and-morphisms>`) at + definition time. When loading a compiled file or importing a module, + all the declarations of this module will be loaded. + + +Rewriting and non reflexive relations +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +To replace only one argument of an n-ary morphism it is necessary to +prove that all the other arguments are related to themselves by the +respective relation instances. + +.. example:: + + To replace ``(union S empty)`` with ``S`` in ``(union (union S empty) S) (union S S)`` + the rewrite tactic must exploit the monotony of ``union`` (axiom ``union_compat`` + in the previous example). Applying ``union_compat`` by hand we are left with the + goal ``eq_set (union S S) (union S S)``. + +When the relations associated to some arguments are not reflexive, the +tactic cannot automatically prove the reflexivity goals, that are left +to the user. + +Setoids whose relations are partial equivalence relations (PER) are +useful for dealing with partial functions. Let ``R`` be a PER. We say that an +element ``x`` is defined if ``R x x``. A partial function whose domain +comprises all the defined elements is declared as a morphism that +respects ``R``. Every time a rewriting step is performed the user must +prove that the argument of the morphism is defined. + +.. example:: + + Let ``eqO`` be ``fun x y => x = y /\ x <> 0`` (the + smallest PER over nonzero elements). Division can be declared as a + morphism of signature ``eq ==> eq0 ==> eq``. Replacing ``x`` with + ``y`` in ``div x n = div y n`` opens an additional goal ``eq0 n n`` + which is equivalent to ``n = n /\ n <> 0``. + + +Rewriting and non symmetric relations +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +When the user works up to relations that are not symmetric, it is no +longer the case that any covariant morphism argument is also +contravariant. As a result it is no longer possible to replace a term +with a related one in every context, since the obtained goal implies +the previous one if and only if the replacement has been performed in +a contravariant position. In a similar way, replacement in an +hypothesis can be performed only if the replaced term occurs in a +covariant position. + +.. example:: Covariance and contravariance + + Suppose that division over real numbers has been defined as a morphism of signature + ``Z.div : Z.lt ++> Z.lt --> Z.lt`` (i.e. ``Z.div`` is increasing in + its first argument, but decreasing on the second one). Let ``<`` + denote ``Z.lt``. Under the hypothesis ``H : x < y`` we have + ``k < x / y -> k < x / x``, but not ``k < y / x -> k < x / x``. Dually, + under the same hypothesis ``k < x / y -> k < y / y`` holds, but + ``k < y / x -> k < y / y`` does not. Thus, if the current goal is + ``k < x / x``, it is possible to replace only the second occurrence of + ``x`` (in contravariant position) with ``y`` since the obtained goal + must imply the current one. On the contrary, if ``k < x / x`` is an + hypothesis, it is possible to replace only the first occurrence of + ``x`` (in covariant position) with ``y`` since the current + hypothesis must imply the obtained one. + + Contrary to the previous implementation, no specific error message + will be raised when trying to replace a term that occurs in the wrong + position. It will only fail because the rewriting constraints are not + satisfiable. However it is possible to use the at modifier to specify + which occurrences should be rewritten. + + As expected, composing morphisms together propagates the variance + annotations by switching the variance every time a contravariant + position is traversed. + +.. example:: + + Let us continue the previous example and let us consider + the goal ``x / (x / x) < k``. The first and third occurrences of + ``x`` are in a contravariant position, while the second one is in + covariant position. More in detail, the second occurrence of ``x`` + occurs covariantly in ``(x / x)`` (since division is covariant in + its first argument), and thus contravariantly in ``x / (x / x)`` + (since division is contravariant in its second argument), and finally + covariantly in ``x / (x / x) < k`` (since ``<``, as every + transitive relation, is contravariant in its first argument with + respect to the relation itself). + + +Rewriting in ambiguous setoid contexts +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +One function can respect several different relations and thus it can +be declared as a morphism having multiple signatures. + +.. example:: + + Union over homogeneous lists can be given all the + following signatures: ``eq ==> eq ==> eq`` (``eq`` being the + equality over ordered lists) ``set_eq ==> set_eq ==> set_eq`` + (``set_eq`` being the equality over unordered lists up to duplicates), + ``multiset_eq ==> multiset_eq ==> multiset_eq`` (``multiset_eq`` + being the equality over unordered lists). + +To declare multiple signatures for a morphism, repeat the :cmd:`Add Morphism` +command. + +When morphisms have multiple signatures it can be the case that a +rewrite request is ambiguous, since it is unclear what relations +should be used to perform the rewriting. Contrary to the previous +implementation, the tactic will always choose the first possible +solution to the set of constraints generated by a rewrite and will not +try to find *all* the possible solutions to warn the user about them. + + +Commands and tactics +-------------------- + + +.. _first-class-setoids-and-morphisms: + +First class setoids and morphisms +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + + + +The implementation is based on a first-class representation of +properties of relations and morphisms as typeclasses. That is, the +various combinations of properties on relations and morphisms are +represented as records and instances of theses classes are put in a +hint database. For example, the declaration: + +.. coqdoc:: + + Add Parametric Relation (x1 : T1) ... (xn : Tn) : (A t1 ... tn) (Aeq t′1 ... t′m) + [reflexivity proved by refl] + [symmetry proved by sym] + [transitivity proved by trans] + as id. + + +is equivalent to an instance declaration: + +.. coqdoc:: + + Instance (x1 : T1) ... (xn : Tn) => id : @Equivalence (A t1 ... tn) (Aeq t′1 ... t′m) := + [Equivalence_Reflexive := refl] + [Equivalence_Symmetric := sym] + [Equivalence_Transitive := trans]. + +The declaration itself amounts to the definition of an object of the +record type ``Coq.Classes.RelationClasses.Equivalence`` and a hint added +to the ``typeclass_instances`` hint database. Morphism declarations are +also instances of a typeclass defined in ``Classes.Morphisms``. See the +documentation on :ref:`typeclasses` and the theories files in Classes +for further explanations. + +One can inform the rewrite tactic about morphisms and relations just +by using the typeclass mechanism to declare them using Instance and +Context vernacular commands. Any object of type Proper (the type of +morphism declarations) in the local context will also be automatically +used by the rewriting tactic to solve constraints. + +Other representations of first class setoids and morphisms can also be +handled by encoding them as records. In the following example, the +projections of the setoid relation and of the morphism function can be +registered as parametric relations and morphisms. + +.. example:: First class setoids + + .. coqtop:: in reset + + Require Import Relation_Definitions Setoid. + + Record Setoid : Type := + { car: Type; + eq: car -> car -> Prop; + refl: reflexive _ eq; + sym: symmetric _ eq; + trans: transitive _ eq + }. + + Add Parametric Relation (s : Setoid) : (@car s) (@eq s) + reflexivity proved by (refl s) + symmetry proved by (sym s) + transitivity proved by (trans s) as eq_rel. + + Record Morphism (S1 S2 : Setoid) : Type := + { f: car S1 -> car S2; + compat: forall (x1 x2 : car S1), eq S1 x1 x2 -> eq S2 (f x1) (f x2) + }. + + Add Parametric Morphism (S1 S2 : Setoid) (M : Morphism S1 S2) : + (@f S1 S2 M) with signature (@eq S1 ==> @eq S2) as apply_mor. + Proof. apply (compat S1 S2 M). Qed. + + Lemma test : forall (S1 S2 : Setoid) (m : Morphism S1 S2) + (x y : car S1), eq S1 x y -> eq S2 (f _ _ m x) (f _ _ m y). + Proof. intros. rewrite H. reflexivity. Qed. + +.. _tactics-enabled-on-user-provided-relations: + +Tactics enabled on user provided relations +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The following tactics, all prefixed by ``setoid_``, deal with arbitrary +registered relations and morphisms. Moreover, all the corresponding +unprefixed tactics (i.e. :tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`transitivity`, +:tacn:`replace`, :tacn:`rewrite`) have been extended to fall back to their prefixed +counterparts when the relation involved is not Leibniz equality. +Notice, however, that using the prefixed tactics it is possible to +pass additional arguments such as ``using relation``. + +.. tacv:: setoid_reflexivity + setoid_symmetry {? in @ident} + setoid_transitivity + setoid_rewrite {? @orientation} @term {? at @occs} {? in @ident} + setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @tactic} + :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; setoid_replace + + The ``using relation`` arguments cannot be passed to the unprefixed form. + The latter argument tells the tactic what parametric relation should + be used to replace the first tactic argument with the second one. If + omitted, it defaults to the ``DefaultRelation`` instance on the type of + the objects. By default, it means the most recent ``Equivalence`` instance + in the environment, but it can be customized by declaring + new ``DefaultRelation`` instances. As Leibniz equality is a declared + equivalence, it will fall back to it if no other relation is declared + on a given type. + +Every derived tactic that is based on the unprefixed forms of the +tactics considered above will also work up to user defined relations. +For instance, it is possible to register hints for :tacn:`autorewrite` that +are not proofs of Leibniz equalities. In particular it is possible to +exploit :tacn:`autorewrite` to simulate normalization in a term rewriting +system up to user defined equalities. + + +Printing relations and morphisms +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Print Instances + + This command can be used to show the list of currently + registered ``Reflexive`` (using ``Print Instances Reflexive``), ``Symmetric`` + or ``Transitive`` relations, Equivalences, PreOrders, PERs, and Morphisms + (implemented as ``Proper`` instances). When the rewriting tactics refuse + to replace a term in a context because the latter is not a composition + of morphisms, the :cmd:`Print Instances` command can be useful to understand + what additional morphisms should be registered. + + +Deprecated syntax and backward incompatibilities +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Add Setoid @A @Aeq @ST as @ident + + This command for declaring setoids and morphisms is also accepted due + to backward compatibility reasons. + + Here ``Aeq`` is a congruence relation without parameters, ``A`` is its carrier + and ``ST`` is an object of type (``Setoid_Theory A Aeq``) (i.e. a record + packing together the reflexivity, symmetry and transitivity lemmas). + Notice that the syntax is not completely backward compatible since the + identifier was not required. + +.. cmd:: Add Morphism f : @ident + :name: Add Morphism + + This command is restricted to the declaration of morphisms + without parameters. It is not fully backward compatible since the + property the user is asked to prove is slightly different: for n-ary + morphisms the hypotheses of the property are permuted; moreover, when + the morphism returns a proposition, the property is now stated using a + bi-implication in place of a simple implication. In practice, porting + an old development to the new semantics is usually quite simple. + +Notice that several limitations of the old implementation have been +lifted. In particular, it is now possible to declare several relations +with the same carrier and several signatures for the same morphism. +Moreover, it is now also possible to declare several morphisms having +the same signature. Finally, the :tacn:`replace` and :tacn:`rewrite` tactics can be +used to replace terms in contexts that were refused by the old +implementation. As discussed in the next section, the semantics of the +new :tacn:`setoid_rewrite` tactic differs slightly from the old one and +:tacn:`rewrite`. + + +Extensions +---------- + + +Rewriting under binders +~~~~~~~~~~~~~~~~~~~~~~~ + +.. warning:: + Due to compatibility issues, this feature is enabled only + when calling the :tacn:`setoid_rewrite` tactic directly and not :tacn:`rewrite`. + +To be able to rewrite under binding constructs, one must declare +morphisms with respect to pointwise (setoid) equivalence of functions. +Example of such morphisms are the standard ``all`` and ``ex`` combinators for +universal and existential quantification respectively. They are +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 abort + + Proof. simpl_relation. + +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 +tactic each time we try to rewrite under an ``all`` application (products +in ``Prop`` are implicitly translated to such applications). + +Indeed, when rewriting under a lambda, binding variable ``x``, say from ``P x`` +to ``Q x`` using the relation iff, the tactic will generate a proof of +``pointwise_relation A iff (fun x => P x) (fun x => Q x)`` from the proof +of ``iff (P x) (Q x)`` and a constraint of the form ``Proper (pointwise_relation A iff ==> ?) m`` +will be generated for the surrounding morphism ``m``. + +Hence, one can add higher-order combinators as morphisms by providing +signatures using pointwise extension for the relations on the +functional arguments (or whatever subrelation of the pointwise +extension). For example, one could declare the ``map`` combinator on lists +as a morphism: + +.. coqdoc:: + + Instance map_morphism `{Equivalence A eqA, Equivalence B eqB} : + Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B). + +where ``list_equiv`` implements an equivalence on lists parameterized by +an equivalence on the elements. + +Note that when one does rewriting with a lemma under a binder using +:tacn:`setoid_rewrite`, the application of the lemma may capture the bound +variable, as the semantics are different from rewrite where the lemma +is first matched on the whole term. With the new :tacn:`setoid_rewrite`, +matching is done on each subterm separately and in its local +environment, and all matches are rewritten *simultaneously* by +default. The semantics of the previous :tacn:`setoid_rewrite` implementation +can almost be recovered using the ``at 1`` modifier. + + +Subrelations +~~~~~~~~~~~~~ + +Subrelations can be used to specify that one relation is included in +another, so that morphism signatures for one can be used for the +other. If a signature mentions a relation ``R`` on the left of an +arrow ``==>``, then the signature also applies for any relation ``S`` that is +smaller than ``R``, and the inverse applies on the right of an arrow. One +can then declare only a few morphisms instances that generate the +complete set of signatures for a particular constant. By default, the +only declared subrelation is ``iff``, which is a subrelation of ``impl`` and +``inverse impl`` (the dual of implication). That’s why we can declare only +two morphisms for conjunction: ``Proper (impl ==> impl ==> impl) and`` and +``Proper (iff ==> iff ==> iff) and``. This is sufficient to satisfy any +rewriting constraints arising from a rewrite using ``iff``, ``impl`` or +``inverse impl`` through ``and``. + +Subrelations are implemented in ``Classes.Morphisms`` and are a prime +example of a mostly user-space extension of the algorithm. + + +Constant unfolding +~~~~~~~~~~~~~~~~~~ + +The resolution tactic is based on typeclasses and hence regards user- +defined constants as transparent by default. This may slow down the +resolution due to a lot of unifications (all the declared ``Proper`` +instances are tried at each node of the search tree). To speed it up, +declare your constant as rigid for proof search using the command +:cmd:`Typeclasses Opaque`. + +Strategies for rewriting +------------------------ + +Definitions +~~~~~~~~~~~ + +The generalized rewriting tactic is based on a set of strategies that can be +combined to obtain custom rewriting procedures. Its set of strategies is based +on Elan’s rewriting strategies :cite:`Luttik97specificationof`. Rewriting +strategies are applied using the tactic ``rewrite_strat s`` where ``s`` is a +strategy expression. Strategies are defined inductively as described by the +following grammar: + +.. productionlist:: rewriting + s, t, u : `strategy` + : `lemma` + : `lemma_right_to_left` + : `failure` + : `identity` + : `reflexivity` + : `progress` + : `failure_catch` + : `composition` + : `left_biased_choice` + : `iteration_one_or_more` + : `iteration_zero_or_more` + : `one_subterm` + : `all_subterms` + : `innermost_first` + : `outermost_first` + : `bottom_up` + : `top_down` + : `apply_hint` + : `any_of_the_terms` + : `apply_reduction` + : `fold_expression` + +.. productionlist:: rewriting + strategy : ( `s` ) + lemma : `c` + lemma_right_to_left : <- `c` + failure : fail + identity : id + reflexivity : refl + progress : progress `s` + failure_catch : try `s` + composition : `s` ; `u` + left_biased_choice : choice `s` `t` + iteration_one_or_more : repeat `s` + iteration_zero_or_more : any `s` + one_subterm : subterm `s` + all_subterms : subterms `s` + innermost_first : innermost `s` + outermost_first : outermost `s` + bottom_up : bottomup `s` + top_down : topdown `s` + apply_hint : hints `hintdb` + any_of_the_terms : terms (`c`)+ + apply_reduction : eval `redexpr` + fold_expression : fold `c` + + +Actually a few of these are defined in term of the others using a +primitive fixpoint operator: + +.. productionlist:: rewriting + try `s` : choice `s` `id` + any `s` : fix `u`. try (`s` ; `u`) + repeat `s` : `s` ; any `s` + bottomup s : fix `bu`. (choice (progress (subterms bu)) s) ; try bu + topdown s : fix `td`. (choice s (progress (subterms td))) ; try td + innermost s : fix `i`. (choice (subterm i) s) + outermost s : fix `o`. (choice s (subterm o)) + +The basic control strategy semantics are straightforward: strategies +are applied to subterms of the term to rewrite, starting from the root +of the term. The lemma strategies unify the left-hand-side of the +lemma with the current subterm and on success rewrite it to the right- +hand-side. Composition can be used to continue rewriting on the +current subterm. The fail strategy always fails while the identity +strategy succeeds without making progress. The reflexivity strategy +succeeds, making progress using a reflexivity proof of rewriting. +Progress tests progress of the argument strategy and fails if no +progress was made, while ``try`` always succeeds, catching failures. +Choice is left-biased: it will launch the first strategy and fall back +on the second one in case of failure. One can iterate a strategy at +least 1 time using ``repeat`` and at least 0 times using ``any``. + +The ``subterm`` and ``subterms`` strategies apply their argument strategy ``s`` to +respectively one or all subterms of the current term under +consideration, left-to-right. ``subterm`` stops at the first subterm for +which ``s`` made progress. The composite strategies ``innermost`` and ``outermost`` +perform a single innermost or outermost rewrite using their argument +strategy. Their counterparts ``bottomup`` and ``topdown`` perform as many +rewritings as possible, starting from the bottom or the top of the +term. + +Hint databases created for :tacn:`autorewrite` can also be used +by :tacn:`rewrite_strat` using the ``hints`` strategy that applies any of the +lemmas at the current subterm. The ``terms`` strategy takes the lemma +names directly as arguments. The ``eval`` strategy expects a reduction +expression (see :ref:`performingcomputations`) and succeeds +if it reduces the subterm under consideration. The ``fold`` strategy takes +a term ``c`` and tries to *unify* it to the current subterm, converting it to ``c`` +on success, it is stronger than the tactic ``fold``. + + +Usage +~~~~~ + + +.. tacn:: rewrite_strat @s [in @ident] + :name: rewrite_strat + + Rewrite using the strategy s in hypothesis ident or the conclusion. + + .. exn:: Nothing to rewrite. + + If the strategy failed. + + .. exn:: No progress made. + + If the strategy succeeded but made no progress. + + .. exn:: Unable to satisfy the rewriting constraints. + + If the strategy succeeded and made progress but the + corresponding rewriting constraints are not satisfied. + + + The ``setoid_rewrite c`` tactic is basically equivalent to + ``rewrite_strat (outermost c)``. + diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst new file mode 100644 index 0000000000..d5523e8561 --- /dev/null +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -0,0 +1,469 @@ +.. _implicitcoercions: + +Implicit Coercions +==================== + +:Author: Amokrane Saïbi + +General Presentation +--------------------- + +This section describes the inheritance mechanism of |Coq|. In |Coq| with +inheritance, we are not interested in adding any expressive power to +our theory, but only convenience. Given a term, possibly not typable, +we are interested in the problem of determining if it can be well +typed modulo insertion of appropriate coercions. We allow to write: + + * :g:`f a` where :g:`f:(forall x:A,B)` and :g:`a:A'` when ``A'`` can + be seen in some sense as a subtype of ``A``. + * :g:`x:A` when ``A`` is not a type, but can be seen in + a certain sense as a type: set, group, category etc. + * :g:`f a` when ``f`` is not a function, but can be seen in a certain sense + as a function: bijection, functor, any structure morphism etc. + + +Classes +------- + +A class with :math:`n` parameters is any defined name with a type +:n:`forall (@ident__1 : @type__1)..(@ident__n:@type__n), @sort`. Thus a class with +parameters is considered as a single class and not as a family of +classes. An object of a class is any term of type :n:`@class @term__1 .. @term__n`. +In addition to these user-defined classes, we have two built-in classes: + + + * ``Sortclass``, the class of sorts; its objects are the terms whose type is a + sort (e.g. :g:`Prop` or :g:`Type`). + * ``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 classes is defined as: + +.. productionlist:: + class: `qualid` + : Sortclass + : Funclass + + +Coercions +--------- + +A name ``f`` can be declared as a coercion between a source user-defined class +``C`` with :math:`n` parameters and a target class ``D`` if one of these +conditions holds: + + * ``D`` is a user-defined class, then the type of ``f`` must have the form + :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), D u₁..uₘ` where :math:`m` + is the number of parameters of ``D``. + * ``D`` is ``Funclass``, then the type of ``f`` must have the form + :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ)(x:A), B`. + * ``D`` is ``Sortclass``, then the type of ``f`` must have the form + :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), s` with ``s`` a sort. + +We then write :g:`f : C >-> D`. The restriction on the type +of coercions is called *the uniform inheritance condition*. + +.. note:: The built-in class ``Sortclass`` can be used as a source class, but + the built-in class ``Funclass`` cannot. + +To coerce an object :g:`t:C t₁..tₙ` of ``C`` towards ``D``, we have to +apply the coercion ``f`` to it; the obtained term :g:`f t₁..tₙ t` is +then an object of ``D``. + + +Identity Coercions +------------------- + +Identity coercions are special cases of coercions used to go around +the uniform inheritance condition. Let ``C`` and ``D`` be two classes +with respectively `n` and `m` parameters and +:g:`f:forall (x₁:T₁)..(xₖ:Tₖ)(y:C u₁..uₙ), D v₁..vₘ` a function which +does not verify the uniform inheritance condition. To declare ``f`` as +coercion, one has first to declare a subclass ``C'`` of ``C``: + + :g:`C' := fun (x₁:T₁)..(xₖ:Tₖ) => C u₁..uₙ` + +We then define an *identity coercion* between ``C'`` and ``C``: + + :g:`Id_C'_C := fun (x₁:T₁)..(xₖ:Tₖ)(y:C' x₁..xₖ) => (y:C u₁..uₙ)` + +We can now declare ``f`` as coercion from ``C'`` to ``D``, since we can +"cast" its type as +:g:`forall (x₁:T₁)..(xₖ:Tₖ)(y:C' x₁..xₖ),D v₁..vₘ`. + +The identity coercions have a special status: to coerce an object +:g:`t:C' t₁..tₖ` +of ``C'`` towards ``C``, we do not have to insert explicitly ``Id_C'_C`` +since :g:`Id_C'_C t₁..tₖ t` is convertible with ``t``. However we +"rewrite" the type of ``t`` to become an object of ``C``; in this case, +it becomes :g:`C uₙ'..uₖ'` where each ``uᵢ'`` is the result of the +substitution in ``uᵢ`` of the variables ``xⱼ`` by ``tⱼ``. + +Inheritance Graph +------------------ + +Coercions form an inheritance graph with classes as nodes. We call +*coercion path* an ordered list of coercions between two nodes of +the graph. A class ``C`` is said to be a subclass of ``D`` if there is a +coercion path in the graph from ``C`` to ``D``; we also say that ``C`` +inherits from ``D``. Our mechanism supports multiple inheritance since a +class may inherit from several classes, contrary to simple inheritance +where a class inherits from at most one class. However there must be +at most one path between two classes. If this is not the case, only +the *oldest* one is valid and the others are ignored. So the order +of declaration of coercions is important. + +We extend notations for coercions to coercion paths. For instance +:g:`[f₁;..;fₖ] : C >-> D` is the coercion path composed +by the coercions ``f₁..fₖ``. The application of a coercion path to a +term consists of the successive application of its coercions. + + +Declaring Coercions +------------------------- + +.. cmd:: Coercion @qualid : @class >-> @class + + Declares the construction denoted by :token:`qualid` as a coercion between + the two given classes. + + .. exn:: @qualid not declared. + :undocumented: + + .. exn:: @qualid is already a coercion. + :undocumented: + + .. exn:: Funclass cannot be a source class. + :undocumented: + + .. exn:: @qualid is not a function. + :undocumented: + + .. exn:: Cannot find the source class of @qualid. + :undocumented: + + .. exn:: Cannot recognize @class as a source class of @qualid. + :undocumented: + + .. exn:: @qualid does not respect the uniform inheritance condition. + :undocumented: + + .. exn:: Found target class ... instead of ... + :undocumented: + + .. warn:: Ambiguous path. + + When the coercion :token:`qualid` is added to the inheritance graph, + invalid coercion paths are ignored. The :cmd:`Coercion` command tries to check + that they are convertible with existing ones on the same classes. + The paths for which this check fails are displayed by a warning in the form + :g:`[f₁;..;fₙ] : C >-> D`. + + .. cmdv:: Local Coercion @qualid : @class >-> @class + + Declares the construction denoted by :token:`qualid` as a coercion local to + the current section. + + .. cmdv:: Coercion @ident := @term {? @type } + + This defines :token:`ident` just like :n:`Definition @ident := term {? @type }`, + and then declares :token:`ident` as a coercion between it source and its target. + + .. cmdv:: Local Coercion @ident := @term {? @type } + + This defines :token:`ident` just like :n:`Let @ident := @term {? @type }`, + and then declares :token:`ident` as a coercion between it source and its target. + +Assumptions can be declared as coercions at declaration time. +This extends the grammar of assumptions from +Figure :ref:`vernacular` as follows: + +.. + FIXME: + \comindex{Variable \mbox{\rm (and coercions)}} + \comindex{Axiom \mbox{\rm (and coercions)}} + \comindex{Parameter \mbox{\rm (and coercions)}} + \comindex{Hypothesis \mbox{\rm (and coercions)}} + +.. productionlist:: + assumption : `assumption_keyword` `assums` . + assums : `simple_assums` + : (`simple_assums`) ... (`simple_assums`) + simple_assums : `ident` ... `ident` :[>] `term` + +If the extra ``>`` is present before the type of some assumptions, these +assumptions are declared as coercions. + +Similarly, constructors of inductive types can be declared as coercions at +definition time of the inductive type. This extends and modifies the +grammar of inductive types from Figure :ref:`vernacular` as follows: + +.. + FIXME: + \comindex{Inductive \mbox{\rm (and coercions)}} + \comindex{CoInductive \mbox{\rm (and coercions)}} + +.. productionlist:: + inductive : Inductive `ind_body` with ... with `ind_body` + : CoInductive `ind_body` with ... with `ind_body` + ind_body : `ident` [ `binders` ] : `term` := [[|] `constructor` | ... | `constructor` ] + constructor : `ident` [ `binders` ] [:[>] `term` ] + +Especially, if the extra ``>`` is present in a constructor +declaration, this constructor is declared as a coercion. + +.. cmd:: Identity Coercion @ident : @class >-> @class + + If ``C`` is the source `class` and ``D`` the destination, we check + that ``C`` is a constant with a body of the form + :g:`fun (x₁:T₁)..(xₙ:Tₙ) => D t₁..tₘ` where `m` is the + number of parameters of ``D``. Then we define an identity + function with type :g:`forall (x₁:T₁)..(xₙ:Tₙ)(y:C x₁..xₙ),D t₁..tₘ`, + and we declare it as an identity coercion between ``C`` and ``D``. + + .. exn:: @class must be a transparent constant. + :undocumented: + + .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident + + Same as :cmd:`Identity Coercion` but locally to the current section. + + .. cmdv:: SubClass @ident := @type + :name: SubClass + + If :n:`@type` is a class :n:`@ident'` applied to some arguments then + :n:`@ident` is defined and an identity coercion of name + :n:`Id_@ident_@ident'` is + declared. Otherwise said, this is an abbreviation for + + :n:`Definition @ident := @type.` + :n:`Identity Coercion Id_@ident_@ident' : @ident >-> @ident'`. + + .. cmdv:: Local SubClass @ident := @type + + Same as before but locally to the current section. + + +Displaying Available Coercions +------------------------------- + +.. cmd:: Print Classes + + Print the list of declared classes in the current context. + +.. cmd:: Print Coercions + + Print the list of declared coercions in the current context. + +.. cmd:: Print Graph + + Print the list of valid coercion paths in the current context. + +.. cmd:: Print Coercion Paths @class @class + + Print the list of valid coercion paths between the two given classes. + +Activating the Printing of Coercions +------------------------------------- + +.. flag:: Printing Coercions + + When on, this option forces all the coercions to be printed. + By default, coercions are not printed. + +.. table:: Printing Coercion @qualid + :name: Printing Coercion + + Specifies a set of qualids for which coercions are always displayed. Use the + :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. + +.. _coercions-classes-as-records: + +Classes as Records +------------------ + +.. index:: :> (coercion) + +We allow the definition of *Structures with Inheritance* (or classes as records) +by extending the existing :cmd:`Record` macro. Its new syntax is: + +.. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } } + + 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 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 + declared as a coercion from the record name to the class of this + field type. Note that the fields always verify the uniform + inheritance condition. If the optional ``>`` is given before the + record name, then the constructor name is automatically declared as + a coercion from the class of the last field type to the record name + (this may fail if the uniform inheritance condition is not + satisfied). + +.. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } } + :name: Structure + + This is a synonym of :cmd:`Record`. + + +Coercions and Sections +---------------------- + +The inheritance mechanism is compatible with the section +mechanism. The global classes and coercions defined inside a section +are redefined after its closing, using their new value and new +type. The classes and coercions which are local to the section are +simply forgotten. +Coercions with a local source class or a local target class, and +coercions which do not verify the uniform inheritance condition any longer +are also forgotten. + +Coercions and Modules +--------------------- + +The coercions present in a module are activated only when the module is +explicitly imported. + +Examples +-------- + +There are three situations: + +Coercion at function application +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +:g:`f a` is ill-typed where :g:`f:forall x:A,B` and :g:`a:A'`. If there is a +coercion path between ``A'`` and ``A``, then :g:`f a` is transformed into +:g:`f a'` where ``a'`` is the result of the application of this +coercion path to ``a``. + +We first give an example of coercion between atomic inductive types + +.. coqtop:: all + + Definition bool_in_nat (b:bool) := if b then 0 else 1. + Coercion bool_in_nat : bool >-> nat. + Check (0 = true). + Set Printing Coercions. + Check (0 = true). + Unset Printing Coercions. + + +.. warning:: + + 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. + +We give an example of coercion between classes with parameters. + +.. coqtop:: all + + Parameters (C : nat -> Set) (D : nat -> bool -> Set) (E : bool -> Set). + Parameter f : forall n:nat, C n -> D (S n) true. + Coercion f : C >-> D. + Parameter g : forall (n:nat) (b:bool), D n b -> E b. + Coercion g : D >-> E. + Parameter c : C 0. + Parameter T : E true -> nat. + Check (T c). + Set Printing Coercions. + Check (T c). + Unset Printing Coercions. + +We give now an example using identity coercions. + +.. coqtop:: all + + Definition D' (b:bool) := D 1 b. + Identity Coercion IdD'D : D' >-> D. + Print IdD'D. + Parameter d' : D' true. + Check (T d'). + Set Printing Coercions. + Check (T d'). + Unset Printing Coercions. + + +In the case of functional arguments, we use the monotonic rule of +sub-typing. To coerce :g:`t : forall x : A, B` towards +:g:`forall x : A', B'`, we have to coerce ``A'`` towards ``A`` and ``B`` +towards ``B'``. An example is given below: + +.. coqtop:: all + + Parameters (A B : Set) (h : A -> B). + Coercion h : A >-> B. + Parameter U : (A -> E true) -> nat. + Parameter t : B -> C 0. + Check (U t). + Set Printing Coercions. + Check (U t). + Unset Printing Coercions. + +Remark the changes in the result following the modification of the +previous example. + +.. coqtop:: all + + Parameter U' : (C 0 -> B) -> nat. + Parameter t' : E true -> A. + Check (U' t'). + Set Printing Coercions. + Check (U' t'). + Unset Printing Coercions. + + +Coercion to a type +~~~~~~~~~~~~~~~~~~ + +An assumption ``x:A`` when ``A`` is not a type, is ill-typed. It is +replaced by ``x:A'`` where ``A'`` is the result of the application to +``A`` of the coercion path between the class of ``A`` and +``Sortclass`` if it exists. This case occurs in the abstraction +:g:`fun x:A => t`, universal quantification :g:`forall x:A,B`, global +variables and parameters of (co-)inductive definitions and +functions. In :g:`forall x:A,B`, such a coercion path may also be applied +to ``B`` if necessary. + +.. coqtop:: all + + Parameter Graph : Type. + Parameter Node : Graph -> Type. + Coercion Node : Graph >-> Sortclass. + Parameter G : Graph. + Parameter Arrows : G -> G -> Type. + Check Arrows. + Parameter fg : G -> G. + Check fg. + Set Printing Coercions. + Check fg. + Unset Printing Coercions. + + +Coercion to a function +~~~~~~~~~~~~~~~~~~~~~~ + +``f a`` is ill-typed because ``f:A`` is not a function. The term +``f`` is replaced by the term obtained by applying to ``f`` the +coercion path between ``A`` and ``Funclass`` if it exists. + +.. coqtop:: all + + Parameter bij : Set -> Set -> Set. + Parameter ap : forall A B:Set, bij A B -> A -> B. + Coercion ap : bij >-> Funclass. + Parameter b : bij nat nat. + Check (b 0). + Set Printing Coercions. + Check (b 0). + Unset Printing Coercions. + +Let us see the resulting graph after all these examples. + +.. coqtop:: all + + Print Graph. diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst new file mode 100644 index 0000000000..e56b36caad --- /dev/null +++ b/doc/sphinx/addendum/micromega.rst @@ -0,0 +1,271 @@ +.. _ micromega: + +Micromega: tactics for solving arithmetic goals over ordered rings +================================================================== + +:Authors: Frédéric Besson and Evgeny Makarov + +Short description of the tactics +-------------------------------- + +The Psatz module (``Require Import Psatz.``) gives access to several +tactics for solving arithmetic goals over :math:`\mathbb{Z}`, :math:`\mathbb{Q}`, and :math:`\mathbb{R}` [#]_. +It also possible to get the tactics for integers by a ``Require Import Lia``, +rationals ``Require Import Lqa`` and reals ``Require Import Lra``. + ++ :tacn:`lia` is a decision procedure for linear integer arithmetic; ++ :tacn:`nia` is an incomplete proof procedure for integer non-linear + arithmetic; ++ :tacn:`lra` is a decision procedure for linear (real or rational) arithmetic; ++ :tacn:`nra` is an incomplete proof procedure for non-linear (real or + rational) arithmetic; ++ :tacn:`psatz` ``D n`` where ``D`` is :math:`\mathbb{Z}` or :math:`\mathbb{Q}` or :math:`\mathbb{R}`, and + ``n`` is an optional integer limiting the proof search depth, + is an incomplete proof procedure for non-linear arithmetic. + It is based on John Harrison’s HOL Light + driver to the external prover `csdp` [#]_. Note that the `csdp` driver is + generating a *proof cache* which makes it possible to rerun scripts + even without `csdp`. + +.. flag:: Simplex + + This option (set by default) instructs the decision procedures to + use the Simplex method for solving linear goals. If it is not set, + the decision procedures are using Fourier elimination. + + +The tactics solve propositional formulas parameterized by atomic +arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`. +The syntax of the formulas is the following: + + .. productionlist:: F + F : A ∣ P ∣ True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F + A : p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p + p : c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n + +where :math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the +operators :math:`−, +, ×` are respectively subtraction, addition, and product; +:math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition. +For :math:`\mathbb{Q}`, equality is not Leibniz equality ``=`` but the equality of +rationals ``==``. + +For :math:`\mathbb{Z}` (resp. :math:`\mathbb{Q}`), :math:`c` ranges over integer constants (resp. rational +constants). For :math:`\mathbb{R}`, the tactic recognizes as real constants the +following expressions: + +:: + + c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q | Rdiv(c,c) | Rinv c + +where :math:`z` is a constant in :math:`\mathbb{Z}` and :math:`q` is a constant in :math:`\mathbb{Q}`. +This includes integer constants written using the decimal notation, *i.e.*, ``c%R``. + + +*Positivstellensatz* refutations +-------------------------------- + +The name `psatz` is an abbreviation for *positivstellensatz* – literally +"positivity theorem" – which generalizes Hilbert’s *nullstellensatz*. It +relies on the notion of Cone. Given a (finite) set of polynomials :math:`S`, +:math:`\mathit{Cone}(S)` is inductively defined as the smallest set of polynomials +closed under the following rules: + +:math:`\begin{array}{l} +\dfrac{p \in S}{p \in \mathit{Cone}(S)} \quad +\dfrac{}{p^2 \in \mathit{Cone}(S)} \quad +\dfrac{p_1 \in \mathit{Cone}(S) \quad p_2 \in \mathit{Cone}(S) \quad +\Join \in \{+,*\}} {p_1 \Join p_2 \in \mathit{Cone}(S)}\\ +\end{array}` + +The following theorem provides a proof principle for checking that a +set of polynomial inequalities does not have solutions [#]_. + +.. _psatz_thm: + +**Theorem (Psatz)**. Let :math:`S` be a set of polynomials. +If :math:`-1` belongs to :math:`\mathit{Cone}(S)`, then the conjunction +:math:`\bigwedge_{p \in S} p\ge 0` is unsatisfiable. +A proof based on this theorem is called a *positivstellensatz* +refutation. The tactics work as follows. Formulas are normalized into +conjunctive normal form :math:`\bigwedge_i C_i` where :math:`C_i` has the +general form :math:`(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False}` and +:math:`\Join \in \{>,\ge,=\}` for :math:`D\in \{\mathbb{Q},\mathbb{R}\}` and +:math:`\Join \in \{\ge, =\}` for :math:`\mathbb{Z}`. + +For each conjunct :math:`C_i`, the tactic calls an oracle which searches for +:math:`-1` within the cone. Upon success, the oracle returns a *cone +expression* that is normalized by the :tacn:`ring` tactic (see :ref:`theringandfieldtacticfamilies`) +and checked to be :math:`-1`. + +`lra`: a decision procedure for linear real and rational arithmetic +------------------------------------------------------------------- + +.. tacn:: lra + :name: lra + + This tactic is searching for *linear* refutations. As a result, this tactic explores a subset of the *Cone* + defined as + + :math:`\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}` + + The deductive power of :tacn:`lra` overlaps with the one of :tacn:`field` + tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`. + + +`lia`: a tactic for linear integer arithmetic +--------------------------------------------- + +.. tacn:: lia + :name: lia + + This tactic offers an alternative to the :tacn:`omega` tactic. Roughly + speaking, the deductive power of lia is the combined deductive power of + :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear goals + that :tacn:`omega` does not solve, such as the following so-called *omega + nightmare* :cite:`TheOmegaPaper`. + +.. coqdoc:: + + Goal forall x y, + 27 <= 11 * x + 13 * y <= 45 -> + -10 <= 7 * x - 9 * y <= 4 -> False. + +The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` is under evaluation. + +High level view of `lia` +~~~~~~~~~~~~~~~~~~~~~~~~ + +Over :math:`\mathbb{R}`, *positivstellensatz* refutations are a complete proof +principle [#]_. However, this is not the case over :math:`\mathbb{Z}`. Actually, +*positivstellensatz* refutations are not even sufficient to decide +linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 -> \mathtt{False}` +which is a theorem of :math:`\mathbb{Z}` but not a theorem of :math:`{\mathbb{R}}`. To remedy this +weakness, the :tacn:`lia` tactic is using recursively a combination of: + ++ linear *positivstellensatz* refutations; ++ cutting plane proofs; ++ case split. + +Cutting plane proofs +~~~~~~~~~~~~~~~~~~~~~~ + +are a way to take into account the discreteness of :math:`\mathbb{Z}` by rounding up +(rational) constants up-to the closest integer. + +.. _ceil_thm: + +.. thm:: Bound on the ceiling function + + Let :math:`p` be an integer and :math:`c` a rational constant. Then + :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. + +For instance, from 2 x = 1 we can deduce + ++ :math:`x \ge 1/2` whose cut plane is :math:`x \ge \lceil{1/2}\rceil = 1`; ++ :math:`x \le 1/2` whose cut plane is :math:`x \le \lfloor{1/2}\rfloor = 0`. + +By combining these two facts (in normal form) :math:`x − 1 \ge 0` and +:math:`-x \ge 0`, we conclude by exhibiting a *positivstellensatz* refutation: +:math:`−1 \equiv x−1 + −x \in \mathit{Cone}({x−1,x})`. + +Cutting plane proofs and linear *positivstellensatz* refutations are a +complete proof principle for integer linear arithmetic. + +Case split +~~~~~~~~~~~ + +enumerates over the possible values of an expression. + +.. _casesplit_thm: + +**Theorem**. Let :math:`p` be an integer and :math:`c_1` and :math:`c_2` +integer constants. Then: + + :math:`c_1 \le p \le c_2 \Rightarrow \bigvee_{x \in [c_1,c_2]} p = x` + +Our current oracle tries to find an expression :math:`e` with a small range +:math:`[c_1,c_2]`. We generate :math:`c_2 − c_1` subgoals which contexts are enriched +with an equation :math:`e = i` for :math:`i \in [c_1,c_2]` and recursively search for +a proof. + +`nra`: a proof procedure for non-linear arithmetic +-------------------------------------------------- + +.. tacn:: nra + :name: nra + + This tactic is an *experimental* proof procedure for non-linear + arithmetic. The tactic performs a limited amount of non-linear + reasoning before running the linear prover of :tacn:`lra`. This pre-processing + does the following: + + ++ If the context contains an arithmetic expression of the form + :math:`e[x^2]` where :math:`x` is a monomial, the context is enriched with + :math:`x^2 \ge 0`; ++ For all pairs of hypotheses :math:`e_1 \ge 0`, :math:`e_2 \ge 0`, the context is + enriched with :math:`e_1 \times e_2 \ge 0`. + +After this pre-processing, the linear prover of :tacn:`lra` searches for a +proof by abstracting monomials by variables. + +`nia`: a proof procedure for non-linear integer arithmetic +---------------------------------------------------------- + +.. tacn:: nia + :name: nia + + This tactic is a proof procedure for non-linear integer arithmetic. + It performs a pre-processing similar to :tacn:`nra`. The obtained goal is + solved using the linear integer prover :tacn:`lia`. + +`psatz`: a proof procedure for non-linear arithmetic +---------------------------------------------------- + +.. tacn:: psatz + :name: psatz + + This tactic explores the *Cone* by increasing degrees – hence the + depth parameter *n*. In theory, such a proof search is complete – if the + goal is provable the search eventually stops. Unfortunately, the + external oracle is using numeric (approximate) optimization techniques + that might miss a refutation. + + To illustrate the working of the tactic, consider we wish to prove the + following Coq goal: + +.. needs csdp +.. coqdoc:: + + Require Import ZArith Psatz. + Open Scope Z_scope. + Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. + intro x. + psatz Z 2. + +As shown, such a goal is solved by ``intro x. psatz Z 2.``. The oracle returns the +cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + -x^2` +(polynomial hypotheses are printed in bold). By construction, this expression +belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running :tacn:`ring` we +obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. + +.. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with + the ``zify`` tactic. +.. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by + pre-processing the goal with the ``Z.div_mod_to_equations`` tactic (you may + need to manually run ``zify`` first). +.. [#] Support for :g:`Z.quot` and :g:`Z.rem` may be obtained by pre-processing + the goal with the ``Z.quot_rem_to_equations`` tactic (you may need to manually + run ``zify`` first). +.. [#] Note that support for :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and + :g:`Z.rem` may be simultaneously obtained by pre-processing the goal with the + ``Z.to_euclidean_division_equations`` tactic (you may need to manually run + ``zify`` first). +.. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp +.. [#] Variants deal with equalities and strict inequalities. +.. [#] In practice, the oracle might fail to produce such a refutation. + +.. comment in original TeX: +.. %% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a +.. %% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$. +.. %% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst new file mode 100644 index 0000000000..db8c09d88f --- /dev/null +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -0,0 +1,58 @@ +.. _miscellaneousextensions: + +Miscellaneous extensions +======================== + +Program derivation +------------------ + +|Coq| comes with an extension called ``Derive``, which supports program +derivation. Typically in the style of Bird and Meertens or derivations +of program refinements. To use the Derive extension it must first be +required with ``Require Coq.derive.Derive``. When the extension is loaded, +it provides the following command: + +.. cmd:: Derive @ident__1 SuchThat @type As @ident__2 + + :n:`@ident__1` can appear in :n:`@type`. This command opens a new proof + presenting the user with a goal for :n:`@type` in which the name :n:`@ident__1` is + bound to an existential variable :g:`?x` (formally, there are other goals + standing for the existential variables but they are shelved, as + described in :tacn:`shelve`). + + When the proof ends two constants are defined: + + + The first one is named :n:`@ident__1` and is defined as the proof of the + shelved goal (which is also the value of :g:`?x`). It is always + transparent. + + The second one is named :n:`@ident__2`. It has type :n:`@type`, and its body is + the proof of the initially visible goal. It is opaque if the proof + ends with :cmd:`Qed`, and transparent if the proof ends with :cmd:`Defined`. + +.. example:: + + .. coqtop:: all + + Require Coq.derive.Derive. + Require Import Coq.Numbers.Natural.Peano.NPeano. + + Section P. + + Variables (n m k:nat). + + Derive p SuchThat ((k*n)+(k*m) = p) As h. + Proof. + rewrite <- Nat.mul_add_distr_l. + subst p. + reflexivity. + Qed. + + End P. + + Print p. + Check h. + +Any property can be used as `term`, not only an equation. In particular, +it could be an order relation specifying some form of program +refinement or a non-executable property from which deriving a program +is convenient. diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst new file mode 100644 index 0000000000..ed2e1ea58c --- /dev/null +++ b/doc/sphinx/addendum/nsatz.rst @@ -0,0 +1,88 @@ +.. _nsatz_chapter: + +Nsatz: tactics for proving equalities in integral domains +=========================================================== + +:Author: Loïc Pottier + +.. tacn:: nsatz + :name: nsatz + + This tactic is for solving goals of the form + + :math:`\begin{array}{l} + \forall X_1, \ldots, X_n \in A, \\ + P_1(X_1, \ldots, X_n) = Q_1(X_1, \ldots, X_n), \ldots, P_s(X_1, \ldots, X_n) = Q_s(X_1, \ldots, X_n) \\ + \vdash P(X_1, \ldots, X_n) = Q(X_1, \ldots, X_n) \\ + \end{array}` + + where :math:`P, Q, P_1, Q_1, \ldots, P_s, Q_s` are polynomials and :math:`A` is an integral + domain, i.e. a commutative ring with no zero divisors. For example, :math:`A` + can be :math:`\mathbb{R}`, :math:`\mathbb{Z}`, or :math:`\mathbb{Q}`. + Note that the equality :math:`=` used in these goals can be + any setoid equality (see :ref:`tactics-enabled-on-user-provided-relations`) , not only Leibniz equality. + + It also proves formulas + + :math:`\begin{array}{l} + \forall X_1, \ldots, X_n \in A, \\ + P_1(X_1, \ldots, X_n) = Q_1(X_1, \ldots, X_n) \wedge \ldots \wedge P_s(X_1, \ldots, X_n) = Q_s(X_1, \ldots, X_n) \\ + \rightarrow P(X_1, \ldots, X_n) = Q(X_1, \ldots, X_n) \\ + \end{array}` + + doing automatic introductions. + + You can load the ``Nsatz`` module with the command ``Require Import Nsatz``. + +More about `nsatz` +--------------------- + +Hilbert’s Nullstellensatz theorem shows how to reduce proofs of +equalities on polynomials on a commutative ring :math:`A` with no zero divisors +to algebraic computations: it is easy to see that if a polynomial :math:`P` in +:math:`A[X_1,\ldots,X_n]` verifies :math:`c P^r = \sum_{i=1}^{s} S_i P_i`, with +:math:`c \in A`, :math:`c \not = 0`, +:math:`r` a positive integer, and the :math:`S_i` s in :math:`A[X_1,\ldots,X_n ]`, +then :math:`P` is zero whenever polynomials :math:`P_1,\ldots,P_s` are zero +(the converse is also true when :math:`A` is an algebraically closed field: the method is +complete). + +So, solving our initial problem reduces to finding :math:`S_1, \ldots, S_s`, +:math:`c` and :math:`r` such that :math:`c (P-Q)^r = \sum_{i} S_i (P_i-Q_i)`, +which will be proved by the tactic ring. + +This is achieved by the computation of a Gröbner basis of the ideal +generated by :math:`P_1-Q_1,...,P_s-Q_s`, with an adapted version of the +Buchberger algorithm. + +This computation is done after a step of *reification*, which is +performed using :ref:`typeclasses`. + +.. tacv:: nsatz with radicalmax:=@num%N strategy:=@num%Z parameters:=[{*, @ident}] variables:=[{*, @ident}] + + Most complete syntax for `nsatz`. + + * `radicalmax` is a bound when searching for r such that + :math:`c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)` + + * `strategy` gives the order on variables :math:`X_1,\ldots,X_n` and the strategy + used in Buchberger algorithm (see :cite:`sugar` for details): + + * strategy = 0: reverse lexicographic order and newest s-polynomial. + * strategy = 1: reverse lexicographic order and sugar strategy. + * strategy = 2: pure lexicographic order and newest s-polynomial. + * strategy = 3: pure lexicographic order and sugar strategy. + + * `parameters` is the list of variables :math:`X_{i_1},\ldots,X_{i_k}` among + :math:`X_1,\ldots,X_n` which are considered as parameters: computation will be performed with + rational fractions in these variables, i.e. polynomials are considered + with coefficients in :math:`R(X_{i_1},\ldots,X_{i_k})`. In this case, the coefficient + :math:`c` can be a non constant polynomial in :math:`X_{i_1},\ldots,X_{i_k}`, and the tactic + produces a goal which states that :math:`c` is not zero. + + * `variables` is the list of the variables in the decreasing order in + which they will be used in the Buchberger algorithm. If `variables` = :g:`(@nil R)`, + then `lvar` is replaced by all the variables which are not in + `parameters`. + +See the file `Nsatz.v` for many examples, especially in geometry. diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst new file mode 100644 index 0000000000..b008508bbc --- /dev/null +++ b/doc/sphinx/addendum/omega.rst @@ -0,0 +1,187 @@ +.. _omega: + +Omega: a solver for quantifier-free problems in Presburger Arithmetic +===================================================================== + +:Author: Pierre Crégut + +Description of ``omega`` +------------------------ + +.. tacn:: omega + + :tacn:`omega` is a tactic for solving goals in Presburger arithmetic, + i.e. for proving formulas made of equations and inequalities over the + type ``nat`` of natural numbers or the type ``Z`` of binary-encoded integers. + Formulas on ``nat`` are automatically injected into ``Z``. The procedure + may use any hypothesis of the current proof session to solve the goal. + + Multiplication is handled by :tacn:`omega` but only goals where at + least one of the two multiplicands of products is a constant are + solvable. This is the restriction meant by "Presburger arithmetic". + + If the tactic cannot solve the goal, it fails with an error message. + In any case, the computation eventually stops. + +Arithmetical goals recognized by ``omega`` +------------------------------------------ + +:tacn:`omega` applies only to quantifier-free formulas built from the connectives:: + + /\ \/ ~ -> + +on atomic formulas. Atomic formulas are built from the predicates:: + + = < <= > >= + +on ``nat`` or ``Z``. In expressions of type ``nat``, :tacn:`omega` recognizes:: + + + - * S O pred + +and in expressions of type ``Z``, :tacn:`omega` recognizes numeral constants and:: + + + - * Z.succ Z.pred + +All expressions of type ``nat`` or ``Z`` not built on these +operators are considered abstractly as if they +were arbitrary variables of type ``nat`` or ``Z``. + +Messages from ``omega`` +----------------------- + +When :tacn:`omega` does not solve the goal, one of the following errors +is generated: + +.. exn:: omega can't solve this system. + + This may happen if your goal is not quantifier-free (if it is + universally quantified, try :tacn:`intros` first; if it contains + existentials quantifiers too, :tacn:`omega` is not strong enough to solve your + goal). This may happen also if your goal contains arithmetical + operators not recognized by :tacn:`omega`. Finally, your goal may be simply + not true! + +.. exn:: omega: Not a quantifier-free goal. + + If your goal is universally quantified, you should first apply + :tacn:`intro` as many times as needed. + +.. exn:: omega: Unrecognized predicate or connective: @ident. + :undocumented: + +.. exn:: omega: Unrecognized atomic proposition: ... + :undocumented: + +.. exn:: omega: Can't solve a goal with proposition variables. + :undocumented: + +.. exn:: omega: Unrecognized proposition. + :undocumented: + +.. exn:: omega: Can't solve a goal with non-linear products. + :undocumented: + +.. exn:: omega: Can't solve a goal with equality on type ... + :undocumented: + + +Using ``omega`` +--------------- + +The ``omega`` tactic does not belong to the core system. It should be +loaded by + +.. coqtop:: in + + Require Import Omega. + +.. example:: + + .. coqtop:: all + + Require Import Omega. + + Open Scope Z_scope. + + Goal forall m n:Z, 1 + 2 * m <> 2 * n. + intros; omega. + Abort. + + Goal forall z:Z, z > 0 -> 2 * z + 1 > z. + intro; omega. + Abort. + + +Options +------- + +.. flag:: Stable Omega + + .. deprecated:: 8.5 + + This deprecated option (on by default) is for compatibility with Coq pre 8.5. It + resets internal name counters to make executions of :tacn:`omega` independent. + +.. flag:: Omega UseLocalDefs + + This option (on by default) allows :tacn:`omega` to use the bodies of local + variables. + +.. flag:: Omega System + + This option (off by default) activate the printing of debug information + +.. flag:: Omega Action + + This option (off by default) activate the printing of debug information + +Technical data +-------------- + +Overview of the tactic +~~~~~~~~~~~~~~~~~~~~~~ + + * The goal is negated twice and the first negation is introduced as a hypothesis. + * Hypotheses are decomposed in simple equations or inequalities. Multiple + goals may result from this phase. + * Equations and inequalities over ``nat`` are translated over + ``Z``, multiple goals may result from the translation of subtraction. + * Equations and inequalities are normalized. + * Goals are solved by the OMEGA decision procedure. + * The script of the solution is replayed. + +Overview of the OMEGA decision procedure +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The OMEGA decision procedure involved in the :tacn:`omega` tactic uses +a small subset of the decision procedure presented in :cite:`TheOmegaPaper` +Here is an overview, refer to the original paper for more information. + + * Equations and inequalities are normalized by division by the GCD of their + coefficients. + * Equations are eliminated, using the Banerjee test to get a coefficient + equal to one. + * Note that each inequality cuts the Euclidean space in half. + * Inequalities are solved by projecting on the hyperspace + defined by cancelling one of the variables. They are partitioned + according to the sign of the coefficient of the eliminated + variable. Pairs of inequalities from different classes define a + new edge in the projection. + * Redundant inequalities are eliminated or merged in new + equations that can be eliminated by the Banerjee test. + * The last two steps are iterated until a contradiction is reached + (success) or there is no more variable to eliminate (failure). + +It may happen that there is a real solution and no integer one. The last +steps of the Omega procedure are not implemented, so the +decision procedure is only partial. + +Bugs +---- + + * The simplification procedure is very dumb and this results in + many redundant cases to explore. + + * Much too slow. + + * Certainly other bugs! You can report them to https://coq.inria.fr/bugs/. diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst new file mode 100644 index 0000000000..903ee115c9 --- /dev/null +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -0,0 +1,228 @@ +.. _asynchronousandparallelproofprocessing: + +Asynchronous and Parallel Proof Processing +========================================== + +:Author: Enrico Tassi + +This chapter explains how proofs can be asynchronously processed by +|Coq|. This feature improves the reactivity of the system when used in +interactive mode via |CoqIDE|. In addition, it allows |Coq| to take +advantage of parallel hardware when used as a batch compiler by +decoupling the checking of statements and definitions from the +construction and checking of proofs objects. + +This feature is designed to help dealing with huge libraries of +theorems characterized by long proofs. In the current state, it may +not be beneficial on small sets of short files. + +This feature has some technical limitations that may make it +unsuitable for some use cases. + +For example, in interactive mode, some errors coming from the kernel +of |Coq| are signaled late. The type of errors belonging to this +category are universe inconsistencies. + +At the time of writing, only opaque proofs (ending with ``Qed`` or +``Admitted``) can be processed asynchronously. + +Finally, asynchronous processing is disabled when running |CoqIDE| in +Windows. The current implementation of the feature is not stable on +Windows. It can be enabled, as described below at :ref:`interactive-mode`, +though doing so is not recommended. + +Proof annotations +---------------------- + +To process a proof asynchronously |Coq| needs to know the precise +statement of the theorem without looking at the proof. This requires +some annotations if the theorem is proved inside a Section (see +Section :ref:`section-mechanism`). + +When a section ends, |Coq| looks at the proof object to decide which +section variables are actually used and hence have to be quantified in +the statement of the theorem. To avoid making the construction of +proofs mandatory when ending a section, one can start each proof with +the ``Proof using`` command (Section :ref:`proof-editing-mode`) that +declares which section variables the theorem uses. + +The presence of ``Proof`` using is needed to process proofs asynchronously +in interactive mode. + +It is not strictly mandatory in batch mode if it is not the first time +the file is compiled and if the file itself did not change. When the +proof does not begin with Proof using, the system records in an +auxiliary file, produced along with the ``.vo`` file, the list of section +variables used. + +Automatic suggestion of proof annotations +````````````````````````````````````````` + +The flag :flag:`Suggest Proof Using` makes |Coq| suggest, when a ``Qed`` +command is processed, a correct proof annotation. It is up to the user +to modify the proof script accordingly. + + +Proof blocks and error resilience +-------------------------------------- + +|Coq| 8.6 introduced a mechanism for error resilience: in interactive +mode |Coq| is able to completely check a document containing errors +instead of bailing out at the first failure. + +Two kind of errors are supported: errors occurring in vernacular +commands and errors occurring in proofs. + +To properly recover from a failing tactic, |Coq| needs to recognize the +structure of the proof in order to confine the error to a sub proof. +Proof block detection is performed by looking at the syntax of the +proof script (i.e. also looking at indentation). |Coq| comes with four +kind of proof blocks, and an ML API to add new ones. + +:curly: blocks are delimited by { and }, see Chapter :ref:`proofhandling` +:par: blocks are atomic, i.e. just one tactic introduced by the `par:` + goal selector +:indent: blocks end with a tactic indented less than the previous one +:bullet: blocks are delimited by two equal bullet signs at the same + indentation level + +Caveats +```````` + +When a vernacular command fails the subsequent error messages may be +bogus, i.e. caused by the first error. Error resilience for vernacular +commands can be switched off by passing ``-async-proofs-command-error-resilience off`` +to |CoqIDE|. + +An incorrect proof block detection can result into an incorrect error +recovery and hence in bogus errors. Proof block detection cannot be +precise for bullets or any other non well parenthesized proof +structure. Error resilience can be turned off or selectively activated +for any set of block kind passing to |CoqIDE| one of the following +options: + +- ``-async-proofs-tactic-error-resilience off`` +- ``-async-proofs-tactic-error-resilience all`` +- ``-async-proofs-tactic-error-resilience`` :n:`{*, blocktype}` + +Valid proof block types are: “curly”, “par”, “indent”, and “bullet”. + +.. _interactive-mode: + +Interactive mode +--------------------- + +At the time of writing the only user interface supporting asynchronous +proof processing is |CoqIDE|. + +When |CoqIDE| is started, two |Coq| processes are created. The master one +follows the user, giving feedback as soon as possible by skipping +proofs, which are delegated to the worker process. The worker process, +whose state can be seen by clicking on the button in the lower right +corner of the main |CoqIDE| window, asynchronously processes the proofs. +If a proof contains an error, it is reported in red in the label of +the very same button, that can also be used to see the list of errors +and jump to the corresponding line. + +If a proof is processed asynchronously the corresponding Qed command +is colored using a lighter color than usual. This signals that the +proof has been delegated to a worker process (or will be processed +lazily if the ``-async-proofs lazy`` option is used). Once finished, the +worker process will provide the proof object, but this will not be +automatically checked by the kernel of the main process. To force the +kernel to check all the proof objects, one has to click the button +with the gears (Fully check the document) on the top bar. +Only then all the universe constraints are checked. + +Caveats +``````` + +The number of worker processes can be increased by passing |CoqIDE| +the ``-async-proofs-j n`` flag. Note that the memory consumption increases too, +since each worker requires the same amount of memory as the master +process. Also note that increasing the number of workers may reduce +the reactivity of the master process to user commands. + +To disable this feature, one can pass the ``-async-proofs off`` flag to +|CoqIDE|. Conversely, on Windows, where the feature is disabled by +default, pass the ``-async-proofs on`` flag to enable it. + +Proofs that are known to take little time to process are not delegated +to a worker process. The threshold can be configured with +``-async-proofs-delegation-threshold``. Default is 0.03 seconds. + +Batch mode +--------------- + +When |Coq| is used as a batch compiler by running ``coqc``, it produces +a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other +things, theorem statements and proofs. Hence to produce a .vo |Coq| +need to process all the proofs of the ``.v`` file. + +The asynchronous processing of proofs can decouple the generation of a +compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the +generation and checking of the proof objects. The ``-quick`` flag can be +passed to ``coqc`` or ``coqtop`` to produce, quickly, ``.vio`` files. +Alternatively, when using a Makefile produced by ``coq_makefile``, +the ``quick`` target can be used to compile all files using the ``-quick`` flag. + +A ``.vio`` file can be loaded using ``Require`` exactly as a ``.vo`` file but +proofs will not be available (the Print command produces an error). +Moreover, some universe constraints might be missing, so universes +inconsistencies might go unnoticed. A ``.vio`` file does not contain proof +objects, but proof tasks, i.e. what a worker process can transform +into a proof object. + +Compiling a set of files with the ``-quick`` flag allows one to work, +interactively, on any file without waiting for all the proofs to be +checked. + +When working interactively, one can fully check all the ``.v`` files by +running ``coqc`` as usual. + +Alternatively one can turn each ``.vio`` into the corresponding ``.vo``. All +.vio files can be processed in parallel, hence this alternative might +be faster. The command ``coqtop -schedule-vio2vo 2 a b c`` can be used to +obtain a good scheduling for two workers to produce ``a.vo``, ``b.vo``, and +``c.vo``. When using a Makefile produced by ``coq_makefile``, the ``vio2vo`` target +can be used for that purpose. Variable ``J`` should be set to the number +of workers, e.g. ``make vio2vo J=2``. The only caveat is that, while the +.vo files obtained from ``.vio`` files are complete (they contain all proof +terms and universe constraints), the satisfiability of all universe +constraints has not been checked globally (they are checked to be +consistent for every single proof). Constraints will be checked when +these ``.vo`` files are (recursively) loaded with ``Require``. + +There is an extra, possibly even faster, alternative: just check the +proof tasks stored in ``.vio`` files without producing the ``.vo`` files. This +is possibly faster because all the proof tasks are independent, hence +one can further partition the job to be done between workers. The +``coqtop -schedule-vio-checking 6 a b c`` command can be used to obtain a +good scheduling for 6 workers to check all the proof tasks of ``a.vio``, +``b.vio``, and ``c.vio``. Auxiliary files are used to predict how long a proof +task will take, assuming it will take the same amount of time it took +last time. When using a Makefile produced by coq_makefile, the +``checkproofs`` target can be used to check all ``.vio`` files. Variable ``J`` +should be set to the number of workers, e.g. ``make checkproofs J=6``. As +when converting ``.vio`` files to ``.vo`` files, universe constraints are not +checked to be globally consistent. Hence this compilation mode is only +useful for quick regression testing and on developments not making +heavy use of the ``Type`` hierarchy. + +Limiting the number of parallel workers +-------------------------------------------- + +Many |Coq| processes may run on the same computer, and each of them may +start many additional worker processes. The ``coqworkmgr`` utility lets +one limit the number of workers, globally. + +The utility accepts the ``-j`` argument to specify the maximum number of +workers (defaults to 2). ``coqworkmgr`` automatically starts in the +background and prints an environment variable assignment +like ``COQWORKMGR_SOCKET=localhost:45634``. The user must set this variable +in all the shells from which |Coq| processes will be started. If one +uses just one terminal running the bash shell, then +``export ‘coqworkmgr -j 4‘`` will do the job. + +After that, all |Coq| processes, e.g. ``coqide`` and ``coqc``, will respect the +limit, globally. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst new file mode 100644 index 0000000000..b410833d25 --- /dev/null +++ b/doc/sphinx/addendum/program.rst @@ -0,0 +1,387 @@ +.. this should be just "_program", but refs to it don't work + +.. _programs: + +Program +======== + +:Author: Matthieu Sozeau + +We present here the |Program| tactic commands, used to build +certified |Coq| programs, elaborating them from their algorithmic +skeleton and a rich specification :cite:`sozeau06`. It can be thought of as a +dual of :ref:`Extraction <extraction>`. The goal of |Program| is to +program as in a regular functional programming language whilst using +as rich a specification as desired and proving that the code meets the +specification using the whole |Coq| proof apparatus. This is done using +a technique originating from the “Predicate subtyping” mechanism of +PVS :cite:`Rushby98`, which generates type checking conditions while typing a +term constrained to a particular type. Here we insert existential +variables in the term, which must be filled with proofs to get a +complete |Coq| term. |Program| replaces the |Program| tactic by Catherine +Parent :cite:`Parent95b` which had a similar goal but is no longer maintained. + +The languages available as input are currently restricted to |Coq|’s +term language, but may be extended to OCaml, Haskell and +others in the future. We use the same syntax as |Coq| and permit to use +implicit arguments and the existing coercion mechanism. Input terms +and types are typed in an extended system (Russell) and interpreted +into |Coq| terms. The interpretation process may produce some proof +obligations which need to be resolved to create the final term. + + +.. _elaborating-programs: + +Elaborating programs +--------------------- + +The main difference from |Coq| is that an object in a type :g:`T : Set` can +be considered as an object of type :g:`{x : T | P}` for any well-formed +:g:`P : Prop`. If we go from :g:`T` to the subset of :g:`T` verifying property +:g:`P`, we must prove that the object under consideration verifies it. Russell +will generate an obligation for every such coercion. In the other direction, +Russell will automatically insert a projection. + +Another distinction is the treatment of pattern matching. Apart from +the following differences, it is equivalent to the standard match +operation (see :ref:`extendedpatternmatching`). + + ++ Generation of equalities. A match expression is always generalized + by the corresponding equality. As an example, the expression: + + :: + + match x with + | 0 => t + | S n => u + end. + + will be first rewritten to: + + :: + + (match x as y return (x = y -> _) with + | 0 => fun H : x = 0 -> t + | S n => fun H : x = S n -> u + end) (eq_refl x). + + This permits to get the proper equalities in the context of proof + obligations inside clauses, without which reasoning is very limited. + ++ Generation of disequalities. If a pattern intersects with a previous + one, a disequality is added in the context of the second branch. See + for example the definition of div2 below, where the second branch is + typed in a context where :g:`∀ p, _ <> S (S p)`. ++ Coercion. If the object being matched is coercible to an inductive + type, the corresponding coercion will be automatically inserted. This + also works with the previous mechanism. + + +There are options to control the generation of equalities and +coercions. + +.. flag:: Program Cases + + This controls the special treatment of pattern matching generating equalities + and disequalities when using |Program| (it is on by default). All + pattern-matches and let-patterns are handled using the standard algorithm + of |Coq| (see :ref:`extendedpatternmatching`) when this option is + deactivated. + +.. flag:: Program Generalized Coercion + + This controls the coercion of general inductive types when using |Program| + (the option is on by default). Coercion of subset types and pairs is still + active in this case. + +.. flag:: Program Mode + + Enables the program mode, in which 1) typechecking allows subset coercions and + 2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and + :cmd:`Program Definition` act + like Program Fixpoint/Definition, generating obligations if there are + unresolved holes after typechecking. + +.. _syntactic_control: + +Syntactic control over equalities +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +To give more control over the generation of equalities, the +type checker will fall back directly to |Coq|’s usual typing of dependent +pattern matching if a ``return`` or ``in`` clause is specified. Likewise, the +if construct is not treated specially by |Program| so boolean tests in +the code are not automatically reflected in the obligations. One can +use the :g:`dec` combinator to get the correct hypotheses as in: + +.. coqtop:: in + + Require Import Program Arith. + +.. coqtop:: all + + Program Definition id (n : nat) : { x : nat | x = n } := + if dec (leb n 0) then 0 + else S (pred n). + +The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not +produce an equality, contrary to the let pattern construct +:g:`let '(x1,..., xn) := t in b`. +Also, :g:`term :>` explicitly asks the system to +coerce term to its support type. It can be useful in notations, for +example: + +.. coqtop:: all + + Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing). + +This notation denotes equality on subset types using equality on their +support types, avoiding uses of proof-irrelevance that would come up +when reasoning with equality on the subset types themselves. + +The next two commands are similar to their standard counterparts +:cmd:`Definition` and :cmd:`Fixpoint` +in that they define constants. However, they may require the user to +prove some goals to construct the final definitions. + + +.. _program_definition: + +Program Definition +~~~~~~~~~~~~~~~~~~ + +.. cmd:: Program Definition @ident := @term + + This command types the value term in Russell and generates proof + obligations. Once solved using the commands shown below, it binds the + final |Coq| term to the name ``ident`` in the environment. + + .. exn:: @ident already exists. + :name: @ident already exists. (Program Definition) + :undocumented: + + .. cmdv:: Program Definition @ident : @type := @term + + It interprets the type ``type``, potentially generating proof + obligations to be resolved. Once done with them, we have a |Coq| + type |type_0|. It then elaborates the preterm ``term`` into a |Coq| + term |term_0|, checking that the type of |term_0| is coercible to + |type_0|, and registers ``ident`` as being of type |type_0| once the + set of obligations generated during the interpretation of |term_0| + and the aforementioned coercion derivation are solved. + + .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ... + :undocumented: + + .. cmdv:: Program Definition @ident @binders : @type := @term + + This is equivalent to: + + :g:`Program Definition ident : forall binders, type := fun binders => term`. + + .. TODO refer to production in alias + +.. seealso:: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold` + +.. _program_fixpoint: + +Program Fixpoint +~~~~~~~~~~~~~~~~ + +.. cmd:: Program Fixpoint @ident @binders {? {@order}} : @type := @term + + The optional order annotation follows the grammar: + + .. productionlist:: orderannot + order : measure `term` [ `term` ] | wf `term` `ident` + + + :g:`measure f R` where :g:`f` is a value of type :g:`X` computed on + any subset of the arguments and the optional term + :g:`R` is a relation on :g:`X`. :g:`X` defaults to :g:`nat` and :g:`R` + to :g:`lt`. + + + :g:`wf R x` which is equivalent to :g:`measure x R`. + + The structural fixpoint operator behaves just like the one of |Coq| (see + :cmd:`Fixpoint`), except it may also generate obligations. It works + with mutually recursive definitions too. + +.. coqtop:: reset in + + Require Import Program Arith. + +.. coqtop:: all + + Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } := + match n with + | S (S p) => S (div2 p) + | _ => O + end. + +Here we have one obligation for each branch (branches for :g:`0` and +``(S 0)`` are automatically generated by the pattern matching +compilation algorithm). + +.. coqtop:: all + + Obligation 1. + +.. coqtop:: reset none + + Require Import Program Arith. + +One can use a well-founded order or a measure as termination orders +using the syntax: + +.. coqtop:: in + + Program Fixpoint div2 (n : nat) {measure n} : { x : nat | n = 2 * x \/ n = 2 * x + 1 } := + match n with + | S (S p) => S (div2 p) + | _ => O + end. + + + +.. caution:: When defining structurally recursive functions, the generated + obligations should have the prototype of the currently defined + functional in their context. In this case, the obligations should be + transparent (e.g. defined using :g:`Defined`) so that the guardedness + condition on recursive calls can be checked by the kernel’s type- + checker. There is an optimization in the generation of obligations + which gets rid of the hypothesis corresponding to the functional when + it is not necessary, so that the obligation can be declared opaque + (e.g. using :g:`Qed`). However, as soon as it appears in the context, the + proof of the obligation is *required* to be declared transparent. + + No such problems arise when using measures or well-founded recursion. + +.. _program_lemma: + +Program Lemma +~~~~~~~~~~~~~ + +.. cmd:: Program Lemma @ident : @type + + The Russell language can also be used to type statements of logical + properties. It will generate obligations, try to solve them + automatically and fail if some unsolved obligations remain. In this + case, one can first define the lemma’s statement using :g:`Program + Definition` and use it as the goal afterwards. Otherwise the proof + will be started with the elaborated version as a goal. The + :g:`Program` prefix can similarly be used as a prefix for + :g:`Variable`, :g:`Hypothesis`, :g:`Axiom` etc. + +.. _solving_obligations: + +Solving obligations +-------------------- + +The following commands are available to manipulate obligations. The +optional identifier is used when multiple functions have unsolved +obligations (e.g. when defining mutually recursive blocks). The +optional tactic is replaced by the default one if not specified. + +.. cmd:: {? Local|Global} Obligation Tactic := @tactic + :name: Obligation Tactic + + Sets the default obligation solving tactic applied to all obligations + automatically, whether to solve them or when starting to prove one, + e.g. using :g:`Next`. :g:`Local` makes the setting last only for the current + module. Inside sections, local is the default. + +.. cmd:: Show Obligation Tactic + + Displays the current default tactic. + +.. cmd:: Obligations {? of @ident} + + Displays all remaining obligations. + +.. cmd:: Obligation num {? of @ident} + + Start the proof of obligation num. + +.. cmd:: Next Obligation {? of @ident} + + Start the proof of the next unsolved obligation. + +.. cmd:: Solve Obligations {? {? of @ident} with @tactic} + + Tries to solve each obligation of ``ident`` using the given ``tactic`` or the default one. + +.. cmd:: Solve All Obligations {? with @tactic} + + Tries to solve each obligation of every program using the given + tactic or the default one (useful for mutually recursive definitions). + +.. cmd:: Admit Obligations {? of @ident} + + Admits all obligations (of ``ident``). + + .. note:: Does not work with structurally recursive programs. + +.. cmd:: Preterm {? of @ident} + + Shows the term that will be fed to the kernel once the obligations + are solved. Useful for debugging. + +.. flag:: Transparent Obligations + + Controls whether all obligations should be declared as transparent + (the default), or if the system should infer which obligations can be + declared opaque. + +.. flag:: Hide Obligations + + Controls whether obligations appearing in the + term should be hidden as implicit arguments of the special + constantProgram.Tactics.obligation. + +.. flag:: Shrink Obligations + + *Deprecated since 8.7* + + This option (on by default) controls whether obligations should have + their context minimized to the set of variables used in the proof of + the obligation, to avoid unnecessary dependencies. + +The module :g:`Coq.Program.Tactics` defines the default tactic for solving +obligations called :g:`program_simpl`. Importing :g:`Coq.Program.Program` also +adds some useful notations, as documented in the file itself. + +.. _program-faq: + +Frequently Asked Questions +--------------------------- + + +.. exn:: Ill-formed recursive definition. + + This error can happen when one tries to define a function by structural + recursion on a subset object, which means the |Coq| function looks like: + + :: + + Program Fixpoint f (x : A | P) := match x with A b => f b end. + + Supposing ``b : A``, the argument at the recursive call to ``f`` is not a + direct subterm of ``x`` as ``b`` is wrapped inside an ``exist`` constructor to + build an object of type ``{x : A | P}``. Hence the definition is + rejected by the guardedness condition checker. However one can use + wellfounded recursion on subset objects like this: + + :: + + Program Fixpoint f (x : A | P) { measure (size x) } := + match x with A b => f b end. + + One will then just have to prove that the measure decreases at each + recursive call. There are three drawbacks though: + + #. A measure function has to be defined; + #. The reduction is a little more involved, although it works well + using lazy evaluation; + #. Mutual recursion on the underlying inductive type isn’t possible + anymore, but nested mutual recursion is always possible. diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst new file mode 100644 index 0000000000..3b350d5dc0 --- /dev/null +++ b/doc/sphinx/addendum/ring.rst @@ -0,0 +1,764 @@ +.. |ra| replace:: :math:`\rightarrow_{\beta\delta\iota}` +.. |la| replace:: :math:`\leftarrow_{\beta\delta\iota}` +.. |eq| replace:: `=`:sub:`(by the main correctness theorem)` +.. |re| replace:: ``(PEeval`` `v` `ap`\ ``)`` +.. |le| replace:: ``(Pphi_dev`` `v` ``(norm`` `ap`\ ``))`` + +.. _theringandfieldtacticfamilies: + +The ring and field tactic families +==================================== + +:Author: Bruno Barras, Benjamin Grégoire, Assia Mahboubi, Laurent Théry [#f1]_ + +This chapter presents the tactics dedicated to dealing with ring and +field equations. + +What does this tactic do? +------------------------------ + +``ring`` does associative-commutative rewriting in ring and semiring +structures. Assume you have two binary functions :math:`\oplus` and +:math:`\otimes` that are associative and commutative, with :math:`\oplus` +distributive on :math:`\otimes`, and two constants 0 and 1 that are unities for +:math:`\oplus` and :math:`\otimes`. A polynomial is an expression built on +variables :math:`V_0`, :math:`V_1`, :math:`\dots` and constants by application +of :math:`\oplus` and :math:`\otimes`. + +Let an ordered product be a product of variables :math:`V_{i_1} \otimes \dots +\otimes V_{i_n}` verifying :math:`i_1 ≤ i_2 ≤ \dots ≤ i_n` . Let a monomial be +the product of a constant and an ordered product. We can order the monomials by +the lexicographic order on products of variables. Let a canonical sum be an +ordered sum of monomials that are all different, i.e. each monomial in the sum +is strictly less than the following monomial according to the lexicographic +order. It is an easy theorem to show that every polynomial is equivalent (modulo +the ring properties) to exactly one canonical sum. This canonical sum is called +the normal form of the polynomial. In fact, the actual representation shares +monomials with same prefixes. So what does the ``ring`` tactic do? It normalizes polynomials over +any ring or semiring structure. The basic use of ``ring`` is to simplify ring +expressions, so that the user does not have to deal manually with the theorems +of associativity and commutativity. + + +.. example:: + + In the ring of integers, the normal form of + :math:`x (3 + yx + 25(1 − z)) + zx` + is + :math:`28x + (−24)xz + xxy`. + + +``ring`` is also able to compute a normal form modulo monomial equalities. +For example, under the hypothesis that :math:`2x^2 = yz+1`, the normal form of +:math:`2(x + 1)x − x − zy` is :math:`x+1`. + +The variables map +---------------------- + +It is frequent to have an expression built with :math:`+` and :math:`\times`, +but rarely on variables only. Let us associate a number to each subterm of a +ring expression in the Gallina language. For example, consider this expression +in the semiring ``nat``: + +:: + + (plus (mult (plus (f (5)) x) x) + (mult (if b then (4) else (f (3))) (2))) + + +As a ring expression, it has 3 subterms. Give each subterm a number in +an arbitrary order: + +===== =============== ========================= +0 :math:`\mapsto` if b then (4) else (f (3)) +1 :math:`\mapsto` (f (5)) +2 :math:`\mapsto` x +===== =============== ========================= + +Then normalize the “abstract” polynomial +:math:`((V_1 \otimes V_2 ) \oplus V_2) \oplus (V_0 \otimes 2)` +In our example the normal form is: +:math:`(2 \otimes V_0 ) \oplus (V_1 \otimes V_2) \oplus (V_2 \otimes V_2 )`. +Then substitute the variables by their values in the variables map to +get the concrete normal polynomial: + +:: + + (plus (mult (2) (if b then (4) else (f (3)))) + (plus (mult (f (5)) x) (mult x x))) + + +Is it automatic? +--------------------- + +Yes, building the variables map and doing the substitution after +normalizing is automatically done by the tactic. So you can just +forget this paragraph and use the tactic according to your intuition. + +Concrete usage in Coq +-------------------------- + +.. tacn:: ring + + This tactic solves equations upon polynomial expressions of a ring + (or semiring) structure. It proceeds by normalizing both sides + of the equation (w.r.t. associativity, commutativity and + distributivity, constant propagation, rewriting of monomials) and + comparing syntactically the results. + +.. tacn:: ring_simplify + + This tactic applies the normalization procedure described above to + the given terms. The tactic then replaces all occurrences of the terms + given in the conclusion of the goal by their normal forms. If no term + is given, then the conclusion should be an equation and both + sides are normalized. The tactic can also be applied in a hypothesis. + + The tactic must be loaded by ``Require Import Ring``. The ring structures + must be declared with the ``Add Ring`` command (see below). The ring of + booleans is predefined; if one wants to use the tactic on |nat| one must + first require the module ``ArithRing`` exported by ``Arith``); for |Z|, do + ``Require Import ZArithRing`` or simply ``Require Import ZArith``; for |N|, do + ``Require Import NArithRing`` or ``Require Import NArith``. + + +.. example:: + + .. coqtop:: all + + Require Import ZArith. + Open Scope Z_scope. + Goal forall a b c:Z, + (a + b + c) ^ 2 = + a * a + b ^ 2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c. + intros; ring. + Abort. + Goal forall a b:Z, + 2 * a * b = 30 -> (a + b) ^ 2 = a ^ 2 + b ^ 2 + 30. + intros a b H; ring [H]. + Abort. + + +.. tacv:: ring [{* @term }] + + This tactic decides the equality of two terms modulo ring operations and + the equalities defined by the :token:`term`\ s. + Each :token:`term` has to be a proof of some equality :g:`m = p`, where :g:`m` + is a monomial (after “abstraction”), :g:`p` a polynomial and :g:`=` the + corresponding equality of the ring structure. + +.. tacv:: ring_simplify [{* @term }] {* @term } in @ident + + This tactic performs the simplification in the hypothesis named :token:`ident`. + + +.. note:: + + :n:`ring_simplify @term__1; ring_simplify @term__2` is not equivalent to + :n:`ring_simplify @term__1 @term__2`. + + In the latter case the variables map is shared between the two terms, and + common subterm :g:`t` of :n:`@term__1` and :n:`@term__2` + will have the same associated variable number. So the first + alternative should be avoided for terms belonging to the same ring + theory. + + +Error messages: + + +.. exn:: Not a valid ring equation. + + The conclusion of the goal is not provable in the corresponding ring theory. + +.. exn:: Arguments of ring_simplify do not have all the same type. + + :tacn:`ring_simplify` cannot simplify terms of several rings at the same + time. Invoke the tactic once per ring structure. + +.. exn:: Cannot find a declared ring structure over @term. + + No ring has been declared for the type of the terms to be simplified. + Use :cmd:`Add Ring` first. + +.. exn:: Cannot find a declared ring structure for equality @term. + + Same as above in the case of the :tacn:`ring` tactic. + + +Adding a ring structure +---------------------------- + +Declaring a new ring consists in proving that a ring signature (a +carrier set, an equality, and ring operations: ``Ring_theory.ring_theory`` +and ``Ring_theory.semi_ring_theory``) satisfies the ring axioms. Semi- +rings (rings without + inverse) are 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 definitions of ring and semiring (see module ``Ring_theory``) are: + +.. coqdoc:: + + Record ring_theory : Prop := mk_rt { + Radd_0_l : forall x, 0 + x == x; + Radd_sym : forall x y, x + y == y + x; + Radd_assoc : forall x y z, x + (y + z) == (x + y) + z; + Rmul_1_l : forall x, 1 * x == x; + Rmul_sym : forall x y, x * y == y * x; + Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z; + Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); + Rsub_def : forall x y, x - y == x + -y; + Ropp_def : forall x, x + (- x) == 0 + }. + + Record semi_ring_theory : Prop := mk_srt { + SRadd_0_l : forall n, 0 + n == n; + SRadd_sym : forall n m, n + m == m + n ; + SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p; + SRmul_1_l : forall n, 1*n == n; + SRmul_0_l : forall n, 0*n == 0; + SRmul_sym : forall n m, n*m == m*n; + SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p; + SRdistr_l : forall n m p, (n + m)*p == n*p + m*p + }. + + +This implementation of ``ring`` also features a notion of constant that +can be parameterized. This can be used to improve the handling of +closed expressions when operations are effective. It consists in +introducing a type of *coefficients* and an implementation of the ring +operations, and a morphism from the coefficient type to the ring +carrier type. The morphism needs not be injective, nor surjective. + +As an example, one can consider the real numbers. The set of +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: + +.. coqdoc:: + + Record ring_morph : Prop := mkmorph { + morph0 : [cO] == 0; + morph1 : [cI] == 1; + morph_add : forall x y, [x +! y] == [x]+[y]; + morph_sub : forall x y, [x -! y] == [x]-[y]; + morph_mul : forall x y, [x *! y] == [x]*[y]; + morph_opp : forall x, [-!x] == -[x]; + morph_eq : forall x y, x?=!y = true -> [x] == [y] + }. + + Record semi_morph : Prop := mkRmorph { + Smorph0 : [cO] == 0; + Smorph1 : [cI] == 1; + Smorph_add : forall x y, [x +! y] == [x]+[y]; + Smorph_mul : forall x y, [x *! y] == [x]*[y]; + Smorph_eq : forall x y, x?=!y = true -> [x] == [y] + }. + + +where ``c0`` and ``cI`` denote the 0 and 1 of the coefficient set, ``+!``, ``*!``, ``-!`` +are the implementations of the ring operations, ``==`` is the equality of +the coefficients, ``?+!`` is an implementation of this equality, and ``[x]`` +is a notation for the image of ``x`` by the ring morphism. + +Since |Z| is an initial ring (and |N| is an initial semiring), it can +always be considered as a set of coefficients. There are basically +three kinds of (semi-)rings: + +abstract rings + to be used when operations are not effective. The set + of coefficients is |Z| (or |N| for semirings). + +computational rings + to be used when operations are effective. The + set of coefficients is the ring itself. The user only has to provide + an implementation for the equality. + +customized ring + for other cases. The user has to provide the + coefficient set and the morphism. + + +This implementation of ring can also recognize simple power +expressions as ring expressions. A power function is specified by the +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, rpow r (Cp_phi n) = pow_N 1%R Rmult r n + }. + + End POWER. + + +The syntax for adding a new ring is + +.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )} + + The :token:`ident` is not relevant. It is used just for error messages. The + :token:`term` is a proof that the ring signature satisfies the (semi-)ring + axioms. The optional list of modifiers is used to tailor the behavior + of the tactic. The following list describes their syntax and effects: + + .. productionlist:: coq + ring_mod : abstract | decidable `term` | morphism `term` + : setoid `term` `term` + : constants [`ltac`] + : preprocess [`ltac`] + : postprocess [`ltac`] + : power_tac `term` [`ltac`] + : sign `term` + : div `term` + + abstract + declares the ring as abstract. This is the default. + + decidable :n:`@term` + declares the ring as computational. The expression + :n:`@term` is the correctness proof of an equality test ``?=!`` + (which should be evaluable). Its type should be of the form + ``forall x y, x ?=! y = true → x == y``. + + morphism :n:`@term` + declares the ring as a customized one. The expression + :n:`@term` is a proof that there exists a morphism between a set of + coefficient and the ring carrier (see ``Ring_theory.ring_morph`` and + ``Ring_theory.semi_morph``). + + setoid :n:`@term` :n:`@term` + forces the use of given setoid. The first + :n:`@term` is a proof that the equality is indeed a setoid (see + ``Setoid.Setoid_Theory``), and the second :n:`@term` a proof that the + ring operations are morphisms (see ``Ring_theory.ring_eq_ext`` and + ``Ring_theory.sring_eq_ext``). + This modifier needs not be used if the setoid and morphisms have been + declared. + + constants [ :n:`@ltac` ] + specifies a tactic expression :n:`@ltac` that, given a + term, returns either an object of the coefficient set that is mapped + to the expression via the morphism, or returns + ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1 + to their counterpart in the coefficient set. This is generally not + desirable for non trivial computational rings. + + preprocess [ :n:`@ltac` ] + specifies a tactic :n:`@ltac` that is applied as a + preliminary step for :tacn:`ring` and :tacn:`ring_simplify`. It can be used to + transform a goal so that it is better recognized. For instance, ``S n`` + can be changed to ``plus 1 n``. + + postprocess [ :n:`@ltac` ] + specifies a tactic :n:`@ltac` that is applied as a final + step for :tacn:`ring_simplify`. For instance, it can be used to undo + modifications of the preprocessor. + + power_tac :n:`@term` [ :n:`@ltac` ] + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize + power expressions with a constant positive integer exponent (example: + :math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies + the specification of a power function (term has to be a proof of + ``Ring_theory.power_theory``) and :n:`@ltac` specifies a tactic expression + that, given a term, “abstracts” it into an object of type |N| whose + interpretation via ``Cp_phi`` (the evaluation function of power + coefficient) is the original term, or returns ``InitialRing.NotConstant`` + if not a constant coefficient (i.e. |L_tac| is the inverse function of + ``Cp_phi``). See files ``plugins/setoid_ring/ZArithRing.v`` + and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic + does not recognize power expressions as ring expressions. + + sign :n:`@term` + allows :tacn:`ring_simplify` to use a minus operation when + outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The + term :token:`term` is a proof that a given sign function indicates expressions + that are signed (:token:`term` has to be a proof of ``Ring_theory.get_sign``). See + ``plugins/setoid_ring/InitialRing.v`` for examples of sign function. + + div :n:`@term` + allows :tacn:`ring` and :tacn:`ring_simplify` to use monomials with + coefficients other than 1 in the rewriting. The term :n:`@term` is a proof + that a given division function satisfies the specification of an + euclidean division function (:n:`@term` has to be a proof of + ``Ring_theory.div_theory``). For example, this function is called when + trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See + ``plugins/setoid_ring/InitialRing.v`` for examples of div function. + +Error messages: + +.. exn:: Bad ring structure. + + The proof of the ring structure provided is not + of the expected type. + +.. exn:: Bad lemma for decidability of equality. + + The equality function + provided in the case of a computational ring has not the expected + type. + +.. exn:: Ring operation should be declared as a morphism. + + A setoid associated to the carrier of the ring structure has been found, + but the ring operation should be declared as morphism. See :ref:`tactics-enabled-on-user-provided-relations`. + +How does it work? +---------------------- + +The code of ``ring`` is a good example of a tactic written using *reflection*. +What is reflection? Basically, using it means that a part of a tactic is written +in Gallina, Coq's language of terms, rather than |Ltac| or |OCaml|. From the +philosophical point of view, reflection is using the ability of the Calculus of +Constructions to speak and reason about itself. For the ``ring`` tactic we used +Coq as a programming language and also as a proof environment to build a tactic +and to prove its correctness. + +The interested reader is strongly advised to have a look at the +file ``Ring_polynom.v``. Here a type for polynomials is defined: + + +.. coqdoc:: + + Inductive PExpr : Type := + | PEc : C -> PExpr + | PEX : positive -> PExpr + | PEadd : PExpr -> PExpr -> PExpr + | PEsub : PExpr -> PExpr -> PExpr + | PEmul : PExpr -> PExpr -> PExpr + | PEopp : PExpr -> PExpr + | PEpow : PExpr -> N -> PExpr. + + +Polynomials in normal form are defined as: + + +.. coqdoc:: + + Inductive Pol : Type := + | Pc : C -> Pol + | Pinj : positive -> Pol -> Pol + | PX : Pol -> positive -> Pol -> Pol. + + +where ``Pinj n P`` denotes ``P`` in which :math:`V_i` is replaced by :math:`V_{i+n}` , +and ``PX P n Q`` denotes :math:`P \otimes V_1^n \oplus Q'`, `Q'` being `Q` where :math:`V_i` is replaced by :math:`V_{i+1}`. + +Variable maps are represented by lists of ring elements, and two +interpretation functions, one that maps a variables map and a +polynomial to an element of the concrete ring, and the second one that +does the same for normal forms: + + +.. coqdoc:: + + + Definition PEeval : list R -> PExpr -> R := [...]. + Definition Pphi_dev : list R -> Pol -> R := [...]. + + +A function to normalize polynomials is defined, and the big theorem is +its correctness w.r.t interpretation, that is: + + +.. coqdoc:: + + Definition norm : PExpr -> Pol := [...]. + Lemma Pphi_dev_ok : + forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe. + + +So now, what is the scheme for a normalization proof? Let p be the +polynomial expression that the user wants to normalize. First a little +piece of |ML| code guesses the type of `p`, the ring theory `T` to use, an +abstract polynomial `ap` and a variables map `v` such that `p` is |bdi|- +equivalent to `(PEeval v ap)`. Then we replace it by `(Pphi_dev v (norm ap))`, +using the main correctness theorem and we reduce it to a +concrete expression `p’`, which is the concrete normal form of `p`. This is summarized in this diagram: + +========= ====== ==== +`p` |ra| |re| +\ |eq| \ +`p’` |la| |le| +========= ====== ==== + +The user does not see the right part of the diagram. From outside, the +tactic behaves like a |bdi| simplification extended with rewriting rules +for associativity and commutativity. Basically, the proof is only the +application of the main correctness theorem to well-chosen arguments. + +Dealing with fields +------------------------ + +.. tacn:: field + + This tactic is an extension of the :tacn:`ring` tactic that deals with rational + expressions. Given a rational expression :math:`F = 0`. It first reduces the + expression `F` to a common denominator :math:`N/D = 0` where `N` and `D` + are two ring expressions. For example, if we take :math:`F = (1 − 1/x) x − x + 1`, this + gives :math:`N = (x − 1) x − x^2 + x` and :math:`D = x`. It then calls ring to solve + :math:`N = 0`. + + Note that :n:`field` also generates nonzero conditions for all the + denominators it encounters in the reduction. In our example, it + generates the condition :math:`x \neq 0`. These conditions appear as one subgoal + which is a conjunction if there are several denominators. Nonzero + conditions are always polynomial expressions. For example when + reducing the expression :math:`1/(1 + 1/x)`, two side conditions are + generated: :math:`x \neq 0` and :math:`x + 1 \neq 0`. Factorized expressions are broken since + a field is an integral domain, and when the equality test on + coefficients is complete w.r.t. the equality of the target field, + constants can be proven different from zero automatically. + + The tactic must be loaded by ``Require Import Field``. New field + structures can be declared to the system with the ``Add Field`` command + (see below). The field of real numbers is defined in module ``RealField`` + (in ``plugins/setoid_ring``). It is exported by module ``Rbase``, so + that requiring ``Rbase`` or ``Reals`` is enough to use the field tactics on + real numbers. Rational numbers in canonical form are also declared as + a field in the module ``Qcanon``. + + +.. example:: + + .. coqtop:: all + + Require Import Reals. + Open Scope R_scope. + Goal forall x, + x <> 0 -> (1 - 1 / x) * x - x + 1 = 0. + intros; field; auto. + Abort. + Goal forall x y, + y <> 0 -> y = x -> x / y = 1. + intros x y H H1; field [H1]; auto. + Abort. + +.. tacv:: field [{* @term}] + + This tactic decides the equality of two terms modulo + field operations and the equalities defined + by the :token:`term`\s. Each :token:`term` has to be a proof of some equality + :g:`m = p`, where :g:`m` is a monomial (after “abstraction”), :g:`p` a polynomial + and :g:`=` the corresponding equality of the field structure. + +.. note:: + + Rewriting works with the equality :g:`m = p` only if :g:`p` is a polynomial since + rewriting is handled by the underlying ring tactic. + +.. tacv:: field_simplify + + performs the simplification in the conclusion of the + goal, :math:`F_1 = F_2` becomes :math:`N_1 / D_1 = N_2 / D_2`. A normalization step + (the same as the one for rings) is then applied to :math:`N_1`, :math:`D_1`, + :math:`N_2` and :math:`D_2`. This way, polynomials remain in factorized form during + fraction simplification. This yields smaller expressions when + reducing to the same denominator since common factors can be canceled. + +.. tacv:: field_simplify [{* @term }] + + This variant performs the simplification in the conclusion of the goal using the equalities + defined by the :token:`term`\s. + +.. tacv:: field_simplify [{* @term }] {* @term } + + This variant performs the simplification in the terms :token:`term`\s of the conclusion of the goal + using the equalities defined by :token:`term`\s inside the brackets. + +.. tacv:: field_simplify in @ident + + This variant performs the simplification in the assumption :token:`ident`. + +.. tacv:: field_simplify [{* @term }] in @ident + + This variant performs the simplification + in the assumption :token:`ident` using the equalities defined by the :token:`term`\s. + +.. tacv:: field_simplify [{* @term }] {* @term } in @ident + + This variant performs the simplification in the :token:`term`\s of the + assumption :token:`ident` using the + equalities defined by the :token:`term`\s inside the brackets. + +.. tacv:: field_simplify_eq + + performs the simplification in the conclusion of + the goal removing the denominator. :math:`F_1 = F_2` becomes :math:`N_1 D_2 = N_2 D_1`. + +.. tacv:: field_simplify_eq [ {* @term }] + + This variant performs the simplification in + the conclusion of the goal using the equalities defined by :token:`term`\s. + +.. tacv:: field_simplify_eq in @ident + + This variant performs the simplification in the assumption :token:`ident`. + +.. tacv:: field_simplify_eq [{* @term}] in @ident + + This variant performs the simplification in the assumption :token:`ident` + using the equalities defined by :token:`term`\s and removing the denominator. + + +Adding a new field structure +--------------------------------- + +Declaring a new field consists in proving that a field signature (a +carrier set, an equality, and field operations: +``Field_theory.field_theory`` and ``Field_theory.semi_field_theory``) +satisfies the field axioms. Semi-fields (fields without + inverse) are +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: + +.. coqdoc:: + + Record field_theory : Prop := mk_field { + F_R : ring_theory rO rI radd rmul rsub ropp req; + F_1_neq_0 : ~ 1 == 0; + Fdiv_def : forall p q, p / q == p * / q; + Finv_l : forall p, ~ p == 0 -> / p * p == 1 + }. + + Record semi_field_theory : Prop := mk_sfield { + SF_SR : semi_ring_theory rO rI radd rmul req; + SF_1_neq_0 : ~ 1 == 0; + SFdiv_def : forall p q, p / q == p * / q; + SFinv_l : forall p, ~ p == 0 -> / p * p == 1 + }. + + +The result of the normalization process is a fraction represented by +the following type: + +.. coqdoc:: + + Record linear : Type := mk_linear { + num : PExpr C; + denum : PExpr C; + condition : list (PExpr C) + }. + + +where ``num`` and ``denum`` are the numerator and denominator; ``condition`` is a +list of expressions that have appeared as a denominator during the +normalization process. These expressions must be proven different from +zero for the correctness of the algorithm. + +The syntax for adding a new field is + +.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )} + + The :n:`@ident` is not relevant. It is used just for error + messages. :n:`@term` is a proof that the field signature satisfies the + (semi-)field axioms. The optional list of modifiers is used to tailor + the behavior of the tactic. + + .. productionlist:: coq + field_mod : `ring_mod` | completeness `term` + + Since field tactics are built upon ``ring`` + tactics, all modifiers of the ``Add Ring`` apply. There is only one + specific modifier: + + completeness :n:`@term` + allows the field tactic to prove automatically + that the image of nonzero coefficients are mapped to nonzero + elements of the field. :n:`@term` is a proof of + :g:`forall x y, [x] == [y] -> x ?=! y = true`, + which is the completeness of equality on coefficients + w.r.t. the field equality. + + +History of ring +-------------------- + +First Samuel Boutin designed the tactic ``ACDSimpl``. This tactic did lot +of rewriting. But the proofs terms generated by rewriting were too big +for |Coq|’s type checker. Let us see why: + +.. coqtop:: all + + Require Import ZArith. + Open Scope Z_scope. + Goal forall x y z : Z, + x + 3 + y + y * z = x + 3 + y + z * y. + intros; rewrite (Zmult_comm y z); reflexivity. + Save 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 +huge proof terms. Since ``ACDSimpl`` was too slow, Samuel Boutin rewrote +it using reflection (see :cite:`Bou97`). Later, it +was rewritten by Patrick Loiseleur: the new tactic does not any +more require ``ACDSimpl`` to compile and it makes use of |bdi|-reduction not +only to replace the rewriting steps, but also to achieve the +interleaving of computation and reasoning (see :ref:`discussion_reflection`). He also wrote +some |ML| code for the ``Add Ring`` command that allows registering new rings dynamically. + +Proofs terms generated by ring are quite small, they are linear in the +number of :math:`\oplus` and :math:`\otimes` operations in the normalized terms. Type checking +those terms requires some time because it makes a large use of the +conversion rule, but memory requirements are much smaller. + + +.. _discussion_reflection: + + +Discussion +---------------- + + +Efficiency is not the only motivation to use reflection here. ``ring`` +also deals with constants, it rewrites for example the expression +``34 + 2 * x − x + 12`` to the expected result ``x + 46``. +For the tactic ``ACDSimpl``, the only constants were 0 and 1. +So the expression ``34 + 2 * (x − 1) + 12`` +is interpreted as :math:`V_0 \oplus V_1 \otimes (V_2 \ominus 1) \oplus V_3`\ , +with the variables mapping +:math:`\{V_0 \mapsto 34; V_1 \mapsto 2; V_2 \mapsto x; V_3 \mapsto 12\}`\ . +Then it is rewritten to ``34 − x + 2 * x + 12``, very far from the expected result. +Here rewriting is not sufficient: you have to do some kind of reduction +(some kind of computation) to achieve the normalization. + +The tactic ``ring`` is not only faster than the old one: by using +reflection, we get for free the integration of computation and reasoning +that would be very difficult to implement without it. + +Is it the ultimate way to write tactics? The answer is: yes and no. +The ``ring`` tactic intensively uses the conversion rules of the Calculus of +Inductive Constructions, i.e. it replaces proofs by computations as much as possible. +It can be useful in all situations where a classical tactic generates huge proof +terms, like symbolic processing and tautologies. But there +are also tactics like ``auto`` or ``linear`` that do many complex computations, +using side-effects and backtracking, and generate a small proof term. +Clearly, it would be significantly less efficient to replace them by +tactics using reflection. + +Another idea suggested by Benjamin Werner: reflection could be used to +couple an external tool (a rewriting program or a model checker) +with |Coq|. We define (in |Coq|) a type of terms, a type of *traces*, and +prove a correctness theorem that states that *replaying traces* is safe +with respect to some interpretation. Then we let the external tool do every +computation (using side-effects, backtracking, exception, or others +features that are not available in pure lambda calculus) to produce +the trace. Now we can check in |Coq| that the trace has the expected +semantics by applying the correctness theorem. + + + + + + +.. rubric:: Footnotes +.. [#f1] based on previous work from Patrick Loiseleur and Samuel Boutin + + + diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst new file mode 100644 index 0000000000..c0c8c2d79c --- /dev/null +++ b/doc/sphinx/addendum/sprop.rst @@ -0,0 +1,239 @@ +.. _sprop: + +SProp (proof irrelevant propositions) +===================================== + +.. warning:: + + The status of strict propositions is experimental. + +This section describes the extension of |Coq| with definitionally +proof irrelevant propositions (types in the sort :math:`\SProp`, also +known as strict propositions). To use :math:`\SProp` you must pass +``-allow-sprop`` to the |Coq| program or use :opt:`Allow StrictProp`. + +.. opt:: Allow StrictProp + :name: Allow StrictProp + + Allows using :math:`\SProp` when set and forbids it when unset. The + initial value depends on whether you used the command line + ``-allow-sprop``. + +.. exn:: SProp not allowed, you need to Set Allow StrictProp or to use the -allow-sprop command-line-flag. + :undocumented: + +.. coqtop:: none + + Set Allow StrictProp. + +Some of the definitions described in this document are available +through ``Coq.Logic.StrictProp``, which see. + +Basic constructs +---------------- + +The purpose of :math:`\SProp` is to provide types where all elements +are convertible: + +.. coqdoc:: + + Definition irrelevance (A:SProp) (P:A -> Prop) (x:A) (v:P x) (y:A) : P y := v. + +Since we have definitional :ref:`eta-expansion` for +functions, the property of being a type of definitionally irrelevant +values is impredicative, and so is :math:`\SProp`: + +.. coqdoc:: + + Check fun (A:Type) (B:A -> SProp) => (forall x:A, B x) : SProp. + +.. warning:: + + Conversion checking through bytecode or native code compilation + currently does not understand proof irrelevance. + +In order to keep conversion tractable, cumulativity for :math:`\SProp` +is forbidden: + +.. coqtop:: all + + Fail Check (fun (A:SProp) => A : Type). + +We can explicitly lift strict propositions into the relevant world by +using a wrapping inductive type. The inductive stops definitional +proof irrelevance from escaping. + +.. coqtop:: in + + Inductive Box (A:SProp) : Prop := box : A -> Box A. + Arguments box {_} _. + +.. coqtop:: all + + Fail Check fun (A:SProp) (x y : Box A) => eq_refl : x = y. + +.. doesn't get merged with the above if coqdoc +.. coqtop:: in + + Definition box_irrelevant (A:SProp) (x y : Box A) : x = y + := match x, y with box x, box y => eq_refl end. + +In the other direction, we can use impredicativity to "squash" a +relevant type, making an irrelevant approximation. + +.. coqdoc:: + + Definition iSquash (A:Type) : SProp + := forall P : SProp, (A -> P) -> P. + Definition isquash A : A -> iSquash A + := fun a P f => f a. + Definition iSquash_sind A (P : iSquash A -> SProp) (H : forall x : A, P (isquash A x)) + : forall x : iSquash A, P x + := fun x => x (P x) (H : A -> P x). + +Or more conveniently (but equivalently) + +.. coqdoc:: + + Inductive Squash (A:Type) : SProp := squash : A -> Squash A. + +Most inductives types defined in :math:`\SProp` are squashed types, +i.e. they can only be eliminated to construct proofs of other strict +propositions. Empty types are the only exception. + +.. coqtop:: in + + Inductive sEmpty : SProp := . + +.. coqtop:: all + + Check sEmpty_rect. + +.. note:: + + Eliminators to strict propositions are called ``foo_sind``, in the + same way that eliminators to propositions are called ``foo_ind``. + +Primitive records in :math:`\SProp` are allowed when fields are strict +propositions, for instance: + +.. coqtop:: in + + Set Primitive Projections. + Record sProd (A B : SProp) : SProp := { sfst : A; ssnd : B }. + +On the other hand, to avoid having definitionally irrelevant types in +non-:math:`\SProp` sorts (through record η-extensionality), primitive +records in relevant sorts must have at least one relevant field. + +.. coqtop:: all + + Set Warnings "+non-primitive-record". + Fail Record rBox (A:SProp) : Prop := rbox { runbox : A }. + +.. coqdoc:: + + Record ssig (A:Type) (P:A -> SProp) : Type := { spr1 : A; spr2 : P spr1 }. + +Note that ``rBox`` works as an emulated record, which is equivalent to +the Box inductive. + +Encodings for strict propositions +--------------------------------- + +The elimination for unit types can be encoded by a trivial function +thanks to proof irrelevance: + +.. coqdoc:: + + Inductive sUnit : SProp := stt. + Definition sUnit_rect (P:sUnit->Type) (v:P stt) (x:sUnit) : P x := v. + +By using empty and unit types as base values, we can encode other +strict propositions. For instance: + +.. coqdoc:: + + Definition is_true (b:bool) : SProp := if b then sUnit else sEmpty. + + Definition is_true_eq_true b : is_true b -> true = b + := match b with + | true => fun _ => eq_refl + | false => sEmpty_ind _ + end. + + Definition eq_true_is_true b (H:true=b) : is_true b + := match H in _ = x return is_true x with eq_refl => stt end. + +Issues with non-cumulativity +---------------------------- + +During normal term elaboration, we don't always know that a type is a +strict proposition early enough. For instance: + +.. coqdoc:: + + Definition constant_0 : ?[T] -> nat := fun _ : sUnit => 0. + +While checking the type of the constant, we only know that ``?[T]`` +must inhabit some sort. Putting it in some floating universe ``u`` +would disallow instantiating it by ``sUnit : SProp``. + +In order to make the system usable without having to annotate every +instance of :math:`\SProp`, we consider :math:`\SProp` to be a subtype +of every universe during elaboration (i.e. outside the kernel). Then +once we have a fully elaborated term it is sent to the kernel which +will check that we didn't actually need cumulativity of :math:`\SProp` +(in the example above, ``u`` doesn't appear in the final term). + +This means that some errors will be delayed until ``Qed``: + +.. coqtop:: in + + Lemma foo : Prop. + Proof. pose (fun A : SProp => A : Type); exact True. + +.. coqtop:: all + + Fail Qed. + +.. coqtop:: in + + Abort. + +.. opt:: Elaboration StrictProp Cumulativity + :name: Elaboration StrictProp Cumulativity + + Unset this option (it's on by default) to be strict with regard to + :math:`\SProp` cumulativity during elaboration. + +The implementation of proof irrelevance uses inferred "relevance" +marks on binders to determine which variables are irrelevant. Together +with non-cumulativity this allows us to avoid retyping during +conversion. However during elaboration cumulativity is allowed and so +the algorithm may miss some irrelevance: + +.. coqtop:: all + + Fail Definition late_mark := fun (A:SProp) (P:A -> Prop) x y (v:P x) => v : P y. + +The binders for ``x`` and ``y`` are created before their type is known +to be ``A``, so they're not marked irrelevant. This can be avoided +with sufficient annotation of binders (see ``irrelevance`` at the +beginning of this chapter) or by bypassing the conversion check in +tactics. + +.. coqdoc:: + + Definition late_mark := fun (A:SProp) (P:A -> Prop) x y (v:P x) => + ltac:(exact_no_check v) : P y. + +The kernel will re-infer the marks on the fully elaborated term, and +so correctly converts ``x`` and ``y``. + +.. warn:: Bad relevance + + This is a developer warning, disabled by default. It is emitted by + the kernel when it is passed a term with incorrect relevance marks. + To avoid conversion issues as in ``late_mark`` you may wish to use + it to find when your tactics are producing incorrect marks. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst new file mode 100644 index 0000000000..b069cf27f4 --- /dev/null +++ b/doc/sphinx/addendum/type-classes.rst @@ -0,0 +1,593 @@ +.. _typeclasses: + +Typeclasses +=========== + +This chapter presents a quick reference of the commands related to type +classes. For an actual introduction to typeclasses, there is a +description of the system :cite:`sozeau08` and the literature on type +classes in Haskell which also applies. + + +Class and Instance declarations +------------------------------- + +The syntax for class and instance declarations is the same as the record +syntax of Coq: + +.. coqdoc:: + + Class classname (p1 : t1) ⋯ (pn : tn) [: sort] := { f1 : u1 ; ⋯ ; fm : um }. + + Instance instancename q1 ⋯ qm : classname p1 ⋯ pn := { f1 := t1 ; ⋯ ; fm := tm }. + +The ``pi : ti`` variables are called the *parameters* of the class and +the ``fi : ti`` are called the *methods*. Each class definition gives +rise to a corresponding record declaration and each instance is a +regular definition whose name is given by `instancename` and type is an +instantiation of the record type. + +We’ll use the following example class in the rest of the chapter: + +.. coqtop:: in + + Class EqDec (A : Type) := + { eqb : A -> A -> bool ; + eqb_leibniz : forall x y, eqb x y = true -> x = y }. + +This class implements a boolean equality test which is compatible with +Leibniz equality on some type. An example implementation is: + +.. coqtop:: in + + Instance unit_EqDec : EqDec unit := + { eqb x y := true ; + eqb_leibniz x y H := + match x, y return x = y with + | tt, tt => eq_refl tt + end }. + +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 + + Require Import Program.Tactics. + Program Instance eq_bool : EqDec bool := + { eqb x y := if x then y else negb y }. + +.. coqtop:: all + + Next Obligation. + destruct x ; destruct y ; (discriminate || reflexivity). + Defined. + +One has to take care that the transparency of every field is +determined by the transparency of the :cmd:`Instance` proof. One can use +alternatively the :cmd:`Program Instance` variant which has richer facilities +for dealing with obligations. + + +Binding classes +--------------- + +Once a typeclass is declared, one can use it in class binders: + +.. coqtop:: all + + Definition neqb {A} {eqa : EqDec A} (x y : A) := negb (eqb x y). + +When one calls a class method, a constraint is generated that is +satisfied only in contexts where the appropriate instances can be +found. In the example above, a constraint ``EqDec A`` is generated and +satisfied by ``eqa : EqDec A``. In case no satisfying constraint can be +found, an error is raised: + +.. coqtop:: all + + Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y). + +The algorithm used to solve constraints is a variant of the :tacn:`eauto` +tactic that does proof search with a set of lemmas (the instances). It +will use local hypotheses as well as declared lemmas in +the ``typeclass_instances`` database. Hence the example can also be +written: + +.. coqtop:: all + + Definition neqb' A (eqa : EqDec A) (x y : A) := negb (eqb x y). + +However, the generalizing binders should be used instead as they have +particular support for typeclasses: + ++ They automatically set the maximally implicit status for typeclass + arguments, making derived functions as easy to use as class methods. + In the example above, ``A`` and ``eqa`` should be set maximally implicit. ++ They support implicit quantification on partially applied type + classes (:ref:`implicit-generalization`). Any argument not given as part of a typeclass + binder will be automatically generalized. ++ They also support implicit quantification on :ref:`superclasses`. + + +Following the previous example, one can write: + +.. coqtop:: all + + Generalizable Variables A B C. + + Definition neqb_implicit `{eqa : EqDec A} (x y : A) := negb (eqb x y). + +Here ``A`` is implicitly generalized, and the resulting function is +equivalent to the one above. + +Parameterized Instances +----------------------- + +One can declare parameterized instances as in Haskell simply by giving +the constraints as a binding context before the instance, e.g.: + +.. coqtop:: in + + 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 + + Admit Obligations. + +These instances are used just as well as lemmas in the instance hint +database. + +.. _contexts: + +Sections and contexts +--------------------- + +To ease developments parameterized by many instances, one can use the +:cmd:`Context` command to introduce these parameters into section contexts, +it works similarly to the command :cmd:`Variable`, except it accepts any +binding context as an argument, so variables can be implicit, and +:ref:`implicit-generalization` can be used. +For example: + +.. coqtop:: all + + Section EqDec_defs. + + Context `{EA : EqDec A}. + +.. coqtop:: in + + 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 }. + Admit Obligations. + +.. coqtop:: all + + End EqDec_defs. + + About option_eqb. + +Here the :cmd:`Global` modifier redeclares the instance at the end of the +section, once it has been generalized by the context variables it +uses. + +.. seealso:: Section :ref:`section-mechanism` + +Building hierarchies +-------------------- + +.. _superclasses: + +Superclasses +~~~~~~~~~~~~ + +One can also parameterize classes by other classes, generating a +hierarchy of classes and superclasses. In the same way, we give the +superclasses as a binding context: + +.. coqtop:: all + + Class Ord `(E : EqDec A) := { le : A -> A -> bool }. + +Contrary to Haskell, we have no special syntax for superclasses, but +this declaration is equivalent to: + +.. coqdoc:: + + Class `(E : EqDec A) => Ord A := + { le : A -> A -> bool }. + + +This declaration means that any instance of the ``Ord`` class must have +an instance of ``EqDec``. The parameters of the subclass contain at +least all the parameters of its superclasses in their order of +appearance (here A is the only one). As we have seen, ``Ord`` is encoded +as a record type with two parameters: a type ``A`` and an ``E`` of type +``EqDec A``. However, one can still use it as if it had a single +parameter inside generalizing binders: the generalization of +superclasses will be done automatically. + +.. coqtop:: all + + Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x). + +In some cases, to be able to specify sharing of structures, one may +want to give explicitly the superclasses. It is is possible to do it +directly in regular binders, and using the ``!`` modifier in class +binders. For example: + +.. coqtop:: all + + Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y). + +The ``!`` modifier switches the way a binder is parsed back to the regular +interpretation of Coq. In particular, it uses the implicit arguments +mechanism if available, as shown in the example. + +Substructures +~~~~~~~~~~~~~ + +.. index:: :> (substructure) + +Substructures are components of a class which are instances of a class +themselves. They often arise when using classes for logical +properties, e.g.: + +.. coqtop:: none + + Require Import Relation_Definitions. + +.. coqtop:: in + + Class Reflexive (A : Type) (R : relation A) := + reflexivity : forall x, R x x. + + Class Transitive (A : Type) (R : relation A) := + transitivity : forall x y z, R x y -> R y z -> R x z. + +This declares singleton classes for reflexive and transitive relations, +(see the :ref:`singleton class <singleton-class>` variant for an +explanation). These may be used as parts of other classes: + +.. coqtop:: all + + Class PreOrder (A : Type) (R : relation A) := + { PreOrder_Reflexive :> Reflexive A R ; + PreOrder_Transitive :> Transitive A R }. + +The syntax ``:>`` indicates that each ``PreOrder`` can be seen as a +``Reflexive`` relation. So each time a reflexive relation is needed, a +preorder can be used instead. This is very similar to the coercion +mechanism of ``Structure`` declarations. The implementation simply +declares each projection as an instance. + +.. warn:: Ignored instance declaration for “@ident”: “@term” is not a class + + Using this ``:>`` syntax with a right-hand-side that is not itself a Class + has no effect (apart from emitting this warning). In particular, is does not + declare a coercion. + +One can also declare existing objects or structure projections using +the Existing Instance command to achieve the same effect. + + +Summary of the commands +----------------------- + +.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } } + + The :cmd:`Class` command is used to declare a typeclass with parameters + :token:`binders` and fields the declared record fields. + + .. _singleton-class: + + .. cmdv:: Class @ident {? @binders} : {? @sort} := @ident : @term + + This variant declares a *singleton* class with a single method. This + singleton class is a so-called definitional class, represented simply + as a definition ``ident binders := term`` and whose instances are + themselves objects of this type. Definitional classes are not wrapped + inside records, and the trivial projection of an instance of such a + class is convertible to the instance itself. This can be useful to + make instances of existing objects easily and to reduce proof size by + not inserting useless projections. The class constant itself is + declared rigid during resolution so that the class abstraction is + maintained. + + .. cmdv:: Existing Class @ident + + This variant declares a class a posteriori from a constant or + inductive definition. No methods or instances are defined. + + .. warn:: @ident is already declared as a typeclass + + This command has no effect when used on a typeclass. + +.. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } + + This command is used to declare a typeclass instance named + :token:`ident` of the class :token:`class` with parameters ``t1`` to ``tn`` and + fields ``b1`` to ``bi``, where each field must be a declared field of + the class. Missing fields must be filled in interactive proof mode. + + An arbitrary context of :token:`binders` can be put after the name of the + instance and before the colon to declare a parameterized instance. An + optional priority can be declared, 0 being the highest priority as for + :tacn:`auto` hints. If the priority is not specified, it defaults to the number + of non-dependent binders of the instance. + + .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term + + This syntax is used for declaration of singleton class instances or + for directly giving an explicit term of type :n:`forall @binders, @class + @term__1 … @term__n`. One need not even mention the unique field name for + singleton classes. + + .. cmdv:: Global Instance + :name: Global Instance + + One can use the :cmd:`Global` modifier on instances declared in a + section so that their generalization is automatically redeclared + after the section is closed. + + .. cmdv:: Program Instance + :name: Program Instance + + Switches the type checking to `Program` (chapter :ref:`programs`) and + uses the obligation mechanism to manage missing fields. + + .. cmdv:: Declare Instance + :name: Declare Instance + + In a :cmd:`Module Type`, this command states that a corresponding concrete + instance should exist in any implementation of this :cmd:`Module Type`. This + is similar to the distinction between :cmd:`Parameter` vs. :cmd:`Definition`, or + between :cmd:`Declare Module` and :cmd:`Module`. + + +Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a +few other commands related to typeclasses. + +.. cmd:: Existing Instance {+ @ident} [| priority] + + This command adds an arbitrary list of constants whose type ends with + an applied typeclass to the instance database with an optional + priority. It can be used for redeclaring instances at the end of + sections, or declaring structure projections as instances. This is + equivalent to ``Hint Resolve ident : typeclass_instances``, except it + registers instances for :cmd:`Print Instances`. + +.. tacn:: typeclasses eauto + :name: typeclasses eauto + + This tactic uses a different resolution engine than :tacn:`eauto` and + :tacn:`auto`. The main differences are the following: + + + Contrary to :tacn:`eauto` and :tacn:`auto`, the resolution is done entirely in + the new proof engine (as of Coq 8.6), meaning that backtracking is + available among dependent subgoals, and shelving goals is supported. + ``typeclasses eauto`` is a multi-goal tactic. It analyses the dependencies + between subgoals to avoid backtracking on subgoals that are entirely + independent. + + + When called with no arguments, ``typeclasses eauto`` uses + the ``typeclass_instances`` database by default (instead of core). + Dependent subgoals are automatically shelved, and shelved goals can + remain after resolution ends (following the behavior of Coq 8.5). + + .. note:: + As of Coq 8.6, ``all:once (typeclasses eauto)`` faithfully + mimicks what happens during typeclass resolution when it is called + during refinement/type inference, except that *only* declared class + subgoals are considered at the start of resolution during type + inference, while ``all`` can select non-class subgoals as well. It might + move to ``all:typeclasses eauto`` in future versions when the + refinement engine will be able to backtrack. + + + When called with specific databases (e.g. with), ``typeclasses eauto`` + allows shelved goals to remain at any point during search and treat + typeclass goals like any other. + + + The transparency information of databases is used consistently for + all hints declared in them. It is always used when calling the + unifier. When considering local hypotheses, we use the transparent + state of the first hint database given. Using an empty database + (created with :cmd:`Create HintDb` for example) with unfoldable variables and + constants as the first argument of ``typeclasses eauto`` hence makes + resolution with the local hypotheses use full conversion during + unification. + + + .. cmdv:: typeclasses eauto @num + + .. warning:: + The semantics for the limit :n:`@num` + is different than for auto. By default, if no limit is given, the + search is unbounded. Contrary to :tacn:`auto`, introduction steps are + counted, which might result in larger limits being necessary when + searching with ``typeclasses eauto`` than with :tacn:`auto`. + + .. cmdv:: typeclasses eauto with {+ @ident} + + This variant runs resolution with the given hint databases. It treats + typeclass subgoals the same as other subgoals (no shelving of + non-typeclass goals in particular). + +.. tacn:: autoapply @term with @ident + :name: autoapply + + The tactic ``autoapply`` applies a term using the transparency information + of the hint database ident, and does *no* typeclass resolution. This can + be used in :cmd:`Hint Extern`’s for typeclass instances (in the hint + database ``typeclass_instances``) to allow backtracking on the typeclass + subgoals created by the lemma application, rather than doing typeclass + resolution locally at the hint application time. + +.. _TypeclassesTransparent: + +Typeclasses Transparent, Typclasses Opaque +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Typeclasses Transparent {+ @ident} + + This command makes the identifiers transparent during typeclass + resolution. + +.. cmd:: Typeclasses Opaque {+ @ident} + + Make the identifiers opaque for typeclass search. It is useful when some + constants prevent some unifications and make resolution fail. It is also + useful to declare constants which should never be unfolded during + proof-search, like fixpoints or anything which does not look like an + abbreviation. This can additionally speed up proof search as the typeclass + map can be indexed by such rigid constants (see + :ref:`thehintsdatabasesforautoandeauto`). + +By default, all constants and local variables are considered transparent. One +should take care not to make opaque any constant that is used to abbreviate a +type, like: + +.. coqdoc:: + Definition relation A := A -> A -> Prop. + +This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. + + +Settings +~~~~~~~~ + +.. flag:: Typeclasses Dependency Order + + This flag (on by default since 8.6) respects the dependency order + between subgoals, meaning that subgoals on which other subgoals depend + come first, while the non-dependent subgoals were put before + the dependent ones previously (Coq 8.5 and below). This can result in + quite different performance behaviors of proof search. + + +.. flag:: Typeclasses Filtered Unification + + This flag, available since Coq 8.6 and off by default, switches the + hint application procedure to a filter-then-unify strategy. To apply a + hint, we first check that the goal *matches* syntactically the + inferred or specified pattern of the hint, and only then try to + *unify* the goal with the conclusion of the hint. This can drastically + improve performance by calling unification less often, matching + syntactic patterns being very quick. This also provides more control + on the triggering of instances. For example, forcing a constant to + explicitly appear in the pattern will make it never apply on a goal + where there is a hole in that place. + + +.. flag:: Typeclasses Limit Intros + + This flag (on by default) controls the ability to apply hints while + avoiding (functional) eta-expansions in the generated proof term. It + does so by allowing hints that conclude in a product to apply to a + goal with a matching product directly, avoiding an introduction. + + .. warning:: + + This can be expensive as it requires rebuilding hint + clauses dynamically, and does not benefit from the invertibility + status of the product introduction rule, resulting in potentially more + expensive proof-search (i.e. more useless backtracking). + +.. flag:: Typeclass Resolution For Conversion + + This flag (on by default) controls the use of typeclass resolution + when a unification problem cannot be solved during elaboration/type + inference. With this flag on, when a unification fails, typeclass + resolution is tried before launching unification once again. + + +.. flag:: Typeclasses Strict Resolution + + Typeclass declarations introduced when this flag is set have a + stricter resolution behavior (the flag is off by default). When + looking for unifications of a goal with an instance of this class, we + “freeze” all the existentials appearing in the goals, meaning that + they are considered rigid during unification and cannot be + instantiated. + + +.. flag:: Typeclasses Unique Solutions + + When a typeclass resolution is launched we ensure that it has a single + solution or fail. This ensures that the resolution is canonical, but + can make proof search much more expensive. + + +.. flag:: Typeclasses Unique Instances + + Typeclass declarations introduced when this flag is set have a more + efficient resolution behavior (the flag is off by default). When a + solution to the typeclass goal of this class is found, we never + backtrack on it, assuming that it is canonical. + +.. flag:: Typeclasses Iterative Deepening + + When this flag is set, the proof search strategy is breadth-first search. + Otherwise, the search strategy is depth-first search. The default is off. + :cmd:`Typeclasses eauto` is another way to set this flag. + +.. opt:: Typeclasses Depth @num + :name: Typeclasses Depth + + Sets the maximum proof search depth. The default is unbounded. + :cmd:`Typeclasses eauto` is another way to set this option. + +.. flag:: Typeclasses Debug + + Controls whether typeclass resolution steps are shown during search. Setting this flag + also sets :opt:`Typeclasses Debug Verbosity` to 1. :cmd:`Typeclasses eauto` + is another way to set this flag. + +.. opt:: Typeclasses Debug Verbosity @num + :name: Typeclasses Debug Verbosity + + Determines how much information is shown for typeclass resolution steps during search. + 1 is the default level. 2 shows additional information such as tried tactics and shelving + of goals. Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this + option to 0 turns that option off. + +.. flag:: Refine Instance Mode + + .. deprecated:: 8.10 + + This flag allows to switch the behavior of instance declarations made through + the Instance command. + + + 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. + +Typeclasses eauto `:=` +~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Typeclasses eauto := {? debug} {? (dfs) | (bfs) } @num + :name: Typeclasses eauto + + This command allows more global customization of the typeclass + resolution tactic. The semantics of the options are: + + + ``debug`` This sets the debug mode. In debug mode, the trace of + successfully applied tactics is printed. The debug mode can also + be set with :flag:`Typeclasses Debug`. + + + ``(dfs)``, ``(bfs)`` This sets the search strategy to depth-first + search (the default) or breadth-first search. The search strategy + can also be set with :flag:`Typeclasses Iterative Deepening`. + + + :token:`num` This sets the depth limit of the search. The depth + limit can also be set with :opt:`Typeclasses Depth`. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst new file mode 100644 index 0000000000..6b10b7c0b3 --- /dev/null +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -0,0 +1,502 @@ +.. _polymorphicuniverses: + +Polymorphic Universes +====================== + +:Author: Matthieu Sozeau + +General Presentation +--------------------- + +.. warning:: + + The status of Universe Polymorphism is experimental. + +This section describes the universe polymorphic extension of |Coq|. +Universe polymorphism makes it possible to write generic definitions +making use of universes and reuse them at different and sometimes +incompatible universe levels. + +A standard example of the difference between universe *polymorphic* +and *monomorphic* definitions is given by the identity function: + +.. coqtop:: in + + Definition identity {A : Type} (a : A) := a. + +By default, constant declarations are monomorphic, hence the identity +function declares a global universe (say ``Top.1``) for its domain. +Subsequently, if we try to self-apply the identity, we will get an +error: + +.. coqtop:: all + + Fail Definition selfid := identity (@identity). + +Indeed, the global level ``Top.1`` would have to be strictly smaller than +itself for this self-application to type check, as the type of +:g:`(@identity)` is :g:`forall (A : Type@{Top.1}), A -> A` whose type is itself +:g:`Type@{Top.1+1}`. + +A universe polymorphic identity function binds its domain universe +level at the definition level instead of making it global. + +.. coqtop:: in + + Polymorphic Definition pidentity {A : Type} (a : A) := a. + +.. coqtop:: all + + About pidentity. + +It is then possible to reuse the constant at different levels, like +so: + +.. coqtop:: in + + Definition selfpid := pidentity (@pidentity). + +Of course, the two instances of :g:`pidentity` in this definition are +different. This can be seen when the :flag:`Printing Universes` flag is on: + +.. coqtop:: none + + Set Printing Universes. + +.. coqtop:: all + + Print selfpid. + +Now :g:`pidentity` is used at two different levels: at the head of the +application it is instantiated at ``Top.3`` while in the argument position +it is instantiated at ``Top.4``. This definition is only valid as long as +``Top.4`` is strictly smaller than ``Top.3``, as shown by the constraints. Note +that this definition is monomorphic (not universe polymorphic), so the +two universes (in this case ``Top.3`` and ``Top.4``) are actually global +levels. + +When printing :g:`pidentity`, we can see the universes it binds in +the annotation :g:`@{Top.2}`. Additionally, when +:flag:`Printing Universes` is on we print the "universe context" of +:g:`pidentity` consisting of the bound universes and the +constraints they must verify (for :g:`pidentity` there are no constraints). + +Inductive types can also be declared universes polymorphic on +universes appearing in their parameters or fields. A typical example +is given by monoids: + +.. coqtop:: in + + Polymorphic Record Monoid := { mon_car :> Type; mon_unit : mon_car; + mon_op : mon_car -> mon_car -> mon_car }. + +.. coqtop:: in + + Print Monoid. + +The Monoid's carrier universe is polymorphic, hence it is possible to +instantiate it for example with :g:`Monoid` itself. First we build the +trivial unit monoid in :g:`Set`: + +.. coqtop:: in + + Definition unit_monoid : Monoid := + {| mon_car := unit; mon_unit := tt; mon_op x y := tt |}. + +From this we can build a definition for the monoid of :g:`Set`\-monoids +(where multiplication would be given by the product of monoids). + +.. coqtop:: in + + Polymorphic Definition monoid_monoid : Monoid. + refine (@Build_Monoid Monoid unit_monoid (fun x y => x)). + Defined. + +.. coqtop:: all + + Print monoid_monoid. + +As one can see from the constraints, this monoid is “large”, it lives +in a universe strictly higher than :g:`Set`. + +Polymorphic, Monomorphic +------------------------- + +.. cmd:: Polymorphic @definition + + As shown in the examples, polymorphic definitions and inductives can be + declared using the ``Polymorphic`` prefix. + +.. flag:: Universe Polymorphism + + Once enabled, this option will implicitly prepend ``Polymorphic`` to any + definition of the user. + +.. cmd:: Monomorphic @definition + + When the :flag:`Universe Polymorphism` option is set, to make a definition + producing global universe constraints, one can use the ``Monomorphic`` prefix. + +Many other commands support the ``Polymorphic`` flag, including: + +.. TODO add links on each of these? + +- ``Lemma``, ``Axiom``, and all the other “definition” keywords support + polymorphism. + +- ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support + polymorphism. This means that the universe variables (and associated + constraints) are discharged polymorphically over definitions that use + them. In other words, two definitions in the section sharing a common + variable will both get parameterized by the universes produced by the + variable declaration. This is in contrast to a “mononorphic” variable + which introduces global universes and constraints, making the two + definitions depend on the *same* global universes associated to the + variable. + +- :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint + polymorphically, not at a single instance. + +Cumulative, NonCumulative +------------------------- + +Polymorphic inductive types, coinductive types, variants and records can be +declared cumulative using the :g:`Cumulative` prefix. + +.. cmd:: Cumulative @inductive + + Declares the inductive as cumulative + +Alternatively, there is a flag :flag:`Polymorphic Inductive +Cumulativity` which when set, makes all subsequent *polymorphic* +inductive definitions cumulative. When set, inductive types and the +like can be enforced to be non-cumulative using the :g:`NonCumulative` +prefix. + +.. cmd:: NonCumulative @inductive + + Declares the inductive as non-cumulative + +.. flag:: Polymorphic Inductive Cumulativity + + When this option is on, it sets all following polymorphic inductive + types as cumulative (it is off by default). + +Consider the examples below. + +.. coqtop:: in + + Polymorphic Cumulative Inductive list {A : Type} := + | nil : list + | cons : A -> list -> list. + +.. coqtop:: all + + Print list. + +When printing :g:`list`, the universe context indicates the subtyping +constraints by prefixing the level names with symbols. + +Because inductive subtypings are only produced by comparing inductives +to themselves with universes changed, they amount to variance +information: each universe is either invariant, covariant or +irrelevant (there are no contravariant subtypings in Coq), +respectively represented by the symbols `=`, `+` and `*`. + +Here we see that :g:`list` binds an irrelevant universe, so any two +instances of :g:`list` are convertible: :math:`E[Γ] ⊢ \mathsf{list}@\{i\}~A +=_{βδιζη} \mathsf{list}@\{j\}~B` whenever :math:`E[Γ] ⊢ A =_{βδιζη} B` and +this applies also to their corresponding constructors, when +they are comparable at the same type. + +See :ref:`Conversion-rules` for more details on convertibility and subtyping. +The following is an example of a record with non-trivial subtyping relation: + +.. coqtop:: all + + Polymorphic Cumulative Record packType := {pk : Type}. + +:g:`packType` binds a covariant universe, i.e. + +.. math:: + + E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} + \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j + +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. +Notice that this is not the case for the option :flag:`Polymorphic Inductive Cumulativity`. +That is, this option, when set, makes all subsequent *polymorphic* +inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used) +but has no effect on *monomorphic* inductive declarations. + +Consider the following examples. + +.. coqtop:: all reset + + Fail Monomorphic Cumulative Inductive Unit := unit. + +.. coqtop:: all reset + + Fail Monomorphic NonCumulative Inductive Unit := unit. + +.. coqtop:: all reset + + Set Polymorphic Inductive Cumulativity. + Inductive Unit := unit. + +An example of a proof using cumulativity +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. coqtop:: in + + Set Universe Polymorphism. + Set Polymorphic Inductive Cumulativity. + + Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x. + + Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b}) + := forall f g : (forall a, B a), + (forall x, eq@{e} (f x) (g x)) + -> eq@{e} f g. + + Section down. + Universes a b e e'. + Constraint e' < e. + Lemma funext_down {A B} + (H : @funext_type@{a b e} A B) : @funext_type@{a b e'} A B. + Proof. + exact H. + Defined. + End down. + +Cumulativity Weak Constraints +----------------------------- + +.. flag:: Cumulativity Weak Constraints + + When set, which is the default, causes "weak" constraints to be produced + when comparing universes in an irrelevant position. Processing weak + constraints is delayed until minimization time. A weak constraint + between `u` and `v` when neither is smaller than the other and + one is flexible causes them to be unified. Otherwise the constraint is + silently discarded. + + This heuristic is experimental and may change in future versions. + Disabling weak constraints is more predictable but may produce + arbitrary numbers of universes. + + +Global and local universes +--------------------------- + +Each universe is declared in a global or local environment before it +can be used. To ensure compatibility, every *global* universe is set +to be strictly greater than :g:`Set` when it is introduced, while every +*local* (i.e. polymorphically quantified) universe is introduced as +greater or equal to :g:`Set`. + + +Conversion and unification +--------------------------- + +The semantics of conversion and unification have to be modified a +little to account for the new universe instance arguments to +polymorphic references. The semantics respect the fact that +definitions are transparent, so indistinguishable from their bodies +during conversion. + +This is accomplished by changing one rule of unification, the first- +order approximation rule, which applies when two applicative terms +with the same head are compared. It tries to short-cut unfolding by +comparing the arguments directly. In case the constant is universe +polymorphic, we allow this rule to fire only when unifying the +universes results in instantiating a so-called flexible universe +variables (not given by the user). Similarly for conversion, if such +an equation of applicative terms fail due to a universe comparison not +being satisfied, the terms are unfolded. This change implies that +conversion and unification can have different unfolding behaviors on +the same development with universe polymorphism switched on or off. + + +Minimization +------------- + +Universe polymorphism with cumulativity tends to generate many useless +inclusion constraints in general. Typically at each application of a +polymorphic constant :g:`f`, if an argument has expected type :g:`Type@{i}` +and is given a term of type :g:`Type@{j}`, a :math:`j ≤ i` constraint will be +generated. It is however often the case that an equation :math:`j = i` would +be more appropriate, when :g:`f`\'s universes are fresh for example. +Consider the following example: + +.. coqtop:: none + + Polymorphic Definition pidentity {A : Type} (a : A) := a. + Set Printing Universes. + +.. coqtop:: in + + Definition id0 := @pidentity nat 0. + +.. coqtop:: all + + Print id0. + +This definition is elaborated by minimizing the universe of :g:`id0` to +level :g:`Set` while the more general definition would keep the fresh level +:g:`i` generated at the application of :g:`id` and a constraint that :g:`Set` :math:`≤ i`. +This minimization process is applied only to fresh universe variables. +It simply adds an equation between the variable and its lower bound if +it is an atomic universe (i.e. not an algebraic max() universe). + +.. flag:: Universe Minimization ToSet + + Turning this flag off (it is on by default) disallows minimization + to the sort :g:`Set` and only collapses floating universes between + themselves. + + +Explicit Universes +------------------- + +The syntax has been extended to allow users to explicitly bind names +to universes and explicitly instantiate polymorphic definitions. + +.. cmd:: Universe @ident + + In the monorphic case, this command declares a new global universe + named :g:`ident`, which can be referred to using its qualified name + as well. Global universe names live in a separate namespace. The + command supports the polymorphic flag only in sections, meaning the + universe quantification will be discharged on each section definition + independently. One cannot mix polymorphic and monomorphic + declarations in the same section. + + +.. cmd:: Constraint @ident @ord @ident + + This command declares a new constraint between named universes. The + order relation :n:`@ord` can be one of :math:`<`, :math:`≤` or :math:`=`. If consistent, the constraint + is then enforced in the global environment. Like ``Universe``, it can be + used with the ``Polymorphic`` prefix in sections only to declare + constraints discharged at section closing time. One cannot declare a + global constraint on polymorphic universes. + + .. exn:: Undeclared universe @ident. + :undocumented: + + .. exn:: Universe inconsistency. + :undocumented: + + +Polymorphic definitions +~~~~~~~~~~~~~~~~~~~~~~~ + +For polymorphic definitions, the declaration of (all) universe levels +introduced by a definition uses the following syntax: + +.. coqtop:: in + + Polymorphic Definition le@{i j} (A : Type@{i}) : Type@{j} := A. + +.. coqtop:: all + + Print le. + +During refinement we find that :g:`j` must be larger or equal than :g:`i`, as we +are using :g:`A : Type@{i} <= Type@{j}`, hence the generated constraint. At the +end of a definition or proof, we check that the only remaining +universes are the ones declared. In the term and in general in proof +mode, introduced universe names can be referred to in terms. Note that +local universe names shadow global universe names. During a proof, one +can use :cmd:`Show Universes` to display the current context of universes. + +Definitions can also be instantiated explicitly, giving their full +instance: + +.. coqtop:: all + + Check (pidentity@{Set}). + Monomorphic Universes k l. + Check (le@{k l}). + +User-named universes and the anonymous universe implicitly attached to +an explicit :g:`Type` are considered rigid for unification and are never +minimized. Flexible anonymous universes can be produced with an +underscore or by omitting the annotation to a polymorphic definition. + +.. coqtop:: all + + Check (fun x => x) : Type -> Type. + Check (fun x => x) : Type -> Type@{_}. + + Check le@{k _}. + Check le. + +.. flag:: Strict Universe Declaration + + Turning this option off allows one to freely use + identifiers for universes without declaring them first, with the + semantics that the first use declares it. In this mode, the universe + names are not associated with the definition or proof once it has been + defined. This is meant mainly for debugging purposes. + +.. flag:: Private Polymorphic Universes + + This option, on by default, removes universes which appear only in + the body of an opaque polymorphic definition from the definition's + universe arguments. As such, no value needs to be provided for + these universes when instanciating the definition. Universe + constraints are automatically adjusted. + + Consider the following definition: + + .. coqtop:: all + + Lemma foo@{i} : Type@{i}. + Proof. exact Type. Qed. + Print foo. + + The universe :g:`Top.xxx` for the :g:`Type` in the body cannot be accessed, we + only care that one exists for any instantiation of the universes + appearing in the type of :g:`foo`. This is guaranteed when the + transitive constraint ``Set <= Top.xxx < i`` is verified. Then when + using the constant we don't need to put a value for the inner + universe: + + .. coqtop:: all + + Check foo@{_}. + + and when not looking at the body we don't mention the private + universe: + + .. coqtop:: all + + About foo. + + To recover the same behaviour with regard to universes as + :g:`Defined`, the option :flag:`Private Polymorphic Universes` may + be unset: + + .. coqtop:: all + + Unset Private Polymorphic Universes. + + Lemma bar : Type. Proof. exact Type. Qed. + About bar. + Fail Check bar@{_}. + Check bar@{_ _}. + + Note that named universes are always public. + + .. coqtop:: all + + Set Private Polymorphic Universes. + Unset Strict Universe Declaration. + + Lemma baz : Type@{outer}. Proof. exact Type@{inner}. Qed. + About baz. |