diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/canonical-structures.rst | 435 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 611 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 586 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 845 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 469 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 252 | ||||
| -rw-r--r-- | doc/sphinx/addendum/nsatz.rst | 101 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 184 | ||||
| -rw-r--r-- | doc/sphinx/addendum/parallel-proof-processing.rst | 229 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 381 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 770 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 587 |
12 files changed, 5450 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..6843e9eaa1 --- /dev/null +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -0,0 +1,435 @@ +.. include:: ../replaces.rst +.. _canonicalstructures: + +Canonical Structures +====================== + +:Authors: Assia Mahboubi and Enrico Tassi + +This chapter explains the basics of Canonical Structure 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 name spaces. This allows us to follow the same +pattern and naming convention for the rest of the chapter. The base +name space 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 on 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, then we can relates 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 typecheck ``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 these declaration more compact. + +.. coqtop:: all + + 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 mode 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: + +.. coqtop:: all + + 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..64d4eddf04 --- /dev/null +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -0,0 +1,611 @@ +.. include:: ../replaces.rst + +.. _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 side + +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 @identifier)` are also accepted. This pattern matches the +same values as ``pattern`` does and ``identifier`` 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 pattern* are allowed though. + +Since extended ``match`` expressions are compiled into the primitive ones, +the expressiveness of the theory remains the same. Once the stage of +parsing has finished only simple patterns remain. Re-nesting of +pattern is performed at printing time. An easy way to see the result +of the expansion is to toggle off the nesting performed at printing +(use here :opt:`Set 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 undo + + 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 undo + + 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 undo + + 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 undo + + Unset Printing Matching. + Print even. + +In the previous examples patterns do not conflict with, but sometimes +it is comfortable to write patterns that admit a non trivial +superposition. Consider the boolean function :g:`lef` that given two +natural numbers yields :g:`true` if the first one is less or equal than the +second one and :g:`false` otherwise. We can write it as follows: + +.. coqtop:: in undo + + 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 superpose 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 ordered from top to bottom, then +a value is matched by the pattern at the ith row if and only if it is +not matched by some pattern of 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 + + 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 undo + + 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 (non necessary 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). + +.. opt:: Asymmetric Patterns + +This option (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 2.7.11). + +.. coqtop:: all + + Check + (fun l:List nat => + match l with + | @nil _ => @nil nat + | @cons _ _ l' => l' + end). + + +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 type. 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: + +.. coqtop:: in + + 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 the strategy +succeeds to synthesize it. Unfortunately when dealing with dependent +patterns it often happens that we need to write cases where the type +of the |rhs| are different instances of the elimination predicate. The +function concat for listn is an example where the branches have +different type 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. + +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 and 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 + + 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. + +I have a copy of :g:`b` in type :g:`listn 0` resp :g:`listn (S n')`. + + +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 type 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 dependent type. An example of proof using match in given in Section +8.2.3. + +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 + + 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 type. 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..d7f97edab1 --- /dev/null +++ b/doc/sphinx/addendum/extraction.rst @@ -0,0 +1,586 @@ +.. _extraction: + +.. include:: ../replaces.rst + +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 `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 ... @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 "@file" @qualid ... @qualid. + + Recursive extraction of all the mentioned objects and all + their dependencies in one monolithic `file`. + 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 ``ident.v`` to an ML module + ``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 ``ident.v`` and all other modules + ``ident.v`` depends on. + +.. cmd:: Separate Extraction @qualid ... @qualid. + + Recursive extraction of all the mentioned objects and all + their dependencies, just as ``Extraction "file"``, + 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 + ``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 + ``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 ... @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 +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The ability to fix target language is the first and more important +of the extraction options. Default is ``Ocaml``. + +.. cmd:: Extraction Language Ocaml. +.. cmd:: Extraction Language Haskell. +.. cmd:: Extraction Language Scheme. + +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 +want to generate OCaml programs. 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 constant 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: + +.. opt:: 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. + +.. opt:: 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. + +.. opt:: 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. + +.. opt:: 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 ... @qualid. + + In addition to the automatic inline feature, the constants + mentionned by this command will always be inlined during extraction. + +.. cmd:: Extraction NoInline @qualid ... @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:** + +A 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 ... @ident ]. + + This experimental command allows declaring some arguments of + `qualid` as implicit, i.e. useless in extracted code and hence to + be removed by extraction. Here `qualid` can be any function or + inductive constructor, and the given `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 +``Extraction Implicit`` declarations cannot be honored, that is +if any of the implicited variables still occurs in the final code. +This behavior can be relaxed via the following option: + +.. opt:: Extraction SafeImplicits. + + Default is on. When this option is off, a warning is emitted + instead of an error if some implicited variables 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 + implicited variables). + Note that this extracted code might not compile or run properly, + depending of the use of these remaining implicited variables. + +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 `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 ``Extract Constant`` followed + by a ``Extraction Inline``. Hence a ``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. + +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 ``Extract Constant`` is only useful in the +case of an informative axiom (of sort ``Type`` or ``Set``). A logical axiom +have no computational content and hence will not appears 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 |Coq| one. The syntax is the following: + +.. cmd:: Extract Inductive @qualid => @string [ @string ... @string ]. + + Give an ML extraction for the given inductive type. You must specify + extractions for the type itself (first `string`) and all its + constructors (all the `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 ] @string. + + Same as before, with a final extra `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 `k` constructors, the function used to + emulate the pattern-matching should expect `(k+1)` arguments, first the `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 + argument 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 ``nat`` + into OCaml ``int``, the code to provide has type: + ``(unit->'a)->(int->'a)->int->'a``. + +.. caution:: As for ``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 ``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 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 ``Extraction Library``, the names of the extracted files +directly depends from 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 ... @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``. + +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 extractions, taken from the +|Coq| Standard Library. We choose OCaml as target language, +but all can be done in the other dialects with slight modifications. +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 there are unary integers of type ``nat``, +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`` are needed. This is +probably due to an 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..da9e97e6fa --- /dev/null +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -0,0 +1,845 @@ +.. _generalizedrewriting: + +----------------------- + Generalized rewriting +----------------------- + +:Author: Matthieu Sozeau + +Generalized rewriting +===================== + + +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 type class infrastructure. It also improves on and generalizes +the previous implementation in several ways: + + ++ User-extensible algorithm. The algorithm is separated in two parts: + generations of the rewriting constraints (done in ML) and solving of + these constraints using type class resolution. As type class + resolution is extensible using tactics, this allows users to define + general ways to solve morphism constraints. ++ Sub-relations. 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 type class 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 1 (Parametric relation):** + +It is possible to implement finite sets of elements of type ``A`` as +unordered list 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 2 (Parametric relation (cont.)):** + +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 3 (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: + +.. coqtop:: in + + 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 4 (Contravariant morphism):** + +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 tactic will be given :ref:`in this section <tactics-enabled-on-user-provided-relations>`. +For instance, the tactic reflexivity can be used to close 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 in checking +whether ``C[]`` is a syntactic composition of morphism instances that respects some obvious +compatibility constraints. + + +**Example 5 (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 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +A parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm )`, +:g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)` can be +declared with the following command: + +.. 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. + +after having required the ``Setoid`` module with the ``Require Setoid`` +command. + +The :g:`@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). + + +.. 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 6 (Parametric relation):** + +For Leibniz equality, we may declare: + +.. coqtop:: in + + Add Parametric Relation (A : Type) : A (@eq A) + [reflexivity proved by @refl_equal A] + ... + +Some tactics (``reflexivity``, ``symmetry``, ``transitivity``) work only on +relations that respect the expected properties. The remaining tactics +(``replace``, ``rewrite`` and derived tactics such as ``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. + +The command declares ``f`` as a parametric morphism of signature ``sig``. The +identifier ``id`` gives a unique name to the morphism and it is used as +the base name of the type class 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 7:** + +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: + +.. coqtop:: in + + 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. + +.. coqtop:: in + + Add Parametric Morphism A : (@union A) with + signature eq_set ==> eq_set ==> eq_set as union_mor. + +.. coqtop:: in + + Proof. exact (@union_compat A). Qed. + +We proceed now by proving a simple lemma performing a rewrite step and +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) S) (union S S). + +.. coqtop:: in + + Proof. intros. rewrite empty_neutral. reflexivity. Qed. + +The tables of relations and morphisms are managed by the type class +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 +``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 8:** + +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 relation are partial equivalence relations (PER) are +useful to deal 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 only 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 9:** + +Let ``eqO`` be ``fun x y => x = y /\ x <> 0`` (the +smaller PER over non zero elements). Division can be declared as a +morphism of signature ``eq ==> eq0 ==> eq``. Replace ``x`` with +``y`` in ``div x n = div y n`` opens the additional goal ``eq0 n n`` +that 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 10 (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 ``<`` +denotes ``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 11:** + +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 12:** + + +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 ``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* possible solutions to warn the user about. + + +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 type classes. 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: + +.. coqtop:: in + + 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 id. + + +is equivalent to an instance declaration: + +.. coqtop:: in + + Instance (x1 : T1) ... (xn : Tk) => 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 type class defined in ``Classes.Morphisms``. See the +documentation on type classes :ref:`TODO-chapter-20-type-classes` +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 13 (First class setoids):** + +.. coqtop:: in + + 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. ``reflexivity``, ``symmetry``, ``transitivity``, +``replace``, ``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 + +.. tacv:: setoid_symmetry [in @ident] + +.. tacv:: setoid_transitivity + +.. tacv:: setoid_rewrite [@orientation] @term [at @occs] [in @ident] + +.. tacv:: setoid_replace @term with @term [in @ident] [using relation @term] [by @tactic] + + +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 ``autorewrite`` that +are not proof of Leibniz equalities. In particular it is possible to +exploit ``autorewrite`` to simulate normalization in a term rewriting +system up to user defined equalities. + + +Printing relations and morphisms +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The ``Print Instances`` 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 ``Print Instances`` commands can be useful to understand +what additional morphisms should be registered. + + +Deprecated syntax and backward incompatibilities +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Due to backward compatibility reasons, the following syntax for the +declaration of setoids and morphisms is also accepted. + +.. tacv:: Add Setoid @A @Aeq @ST as @ident + +where ``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. + +The latter command also 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 replace and 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 ``setoid_rewrite`` command differs slightly from the old one and +``rewrite``. + + +Extensions +---------- + + +Rewriting under binders +~~~~~~~~~~~~~~~~~~~~~~~ + +warning:: Due to compatibility issues, this feature is enabled only +when calling the ``setoid_rewrite`` tactics directly and not ``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:: in + + Instance all_iff_morphism (A : Type) : + Proper (pointwise_relation A iff ==> iff) (@all A). + +.. coqtop:: all + + 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: + +.. coqtop:: in + + 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 +``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 ``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 ``setoid_rewrite`` implementation +can almost be recovered using the ``at 1`` modifier. + + +Sub-relations +~~~~~~~~~~~~~ + +Sub-relations can be used to specify that one relation is included in +another, so that morphisms 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``. + +Sub-relations 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 type classes 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 +``Typeclasses Opaque`` (see :ref:`TODO-20.6.7-typeclasses-transparency`). + + +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 :ref:`TODO-102-biblio`. 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 ``autorewrite`` can also be used +by ``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:`TODO-8.7-performing-computations`) 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 +~~~~~ + + +.. tacv:: rewrite_strat @s [in @ident] + + 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..f5ca5be44a --- /dev/null +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -0,0 +1,469 @@ +.. _implicitcoercions: + +.. include:: ../replaces.rst + +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 `n` parameters is any defined name with a type +:g:`forall (x₁:A₁)..(xₙ:Aₙ),s` where ``s`` is a sort. Thus a class with +parameters is considered as a single class and not as a family of +classes. An object of a class ``C`` is any term of type :g:`C t₁ .. tₙ`. +In addition to these user-classes, we have two abstract 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 a classes is defined as: + +.. productionlist:: + class: qualid + : | `Sortclass` + : | `Funclass` + + +Coercions +--------- + +A name ``f`` can be declared as a coercion between a source user-class +``C`` with `n` parameters and a target class ``D`` if one of these +conditions holds: + + * ``D`` is a user-class, then the type of ``f`` must have the form + :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), D u₁..uₘ` where `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 abstract classe ``Sortclass`` can be used as a source class, but + the abstract 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 does 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. + + +Declaration of Coercions +------------------------- + +.. cmd:: Coercion @qualid : @class >-> @class. + + Declares the construction denoted by `qualid` as a coercion between + the two given classes. + + .. exn:: @qualid not declared + .. exn:: @qualid is already a coercion + .. exn:: Funclass cannot be a source class + .. exn:: @qualid is not a function + .. exn:: Cannot find the source class of @qualid + .. exn:: Cannot recognize @class as a source class of @qualid + .. exn:: @qualid does not respect the uniform inheritance condition + .. exn:: Found target class ... instead of ... + + .. warn:: Ambigous path: + + When the coercion `qualid` is added to the inheritance graph, non + valid coercion paths are ignored; they are signaled by a warning + displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. + + .. cmdv:: Local Coercion @qualid : @class >-> @class. + + Declares the construction denoted by `qualid` as a coercion local to + the current section. + + .. cmdv:: Coercion @ident := @term. + + This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. + + .. cmdv:: Coercion @ident := @term : @type. + + This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. + + .. cmdv:: Local Coercion @ident := @term. + + This defines `ident` just like ``Let`` `ident` ``:=`` `term`, + and then declares `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:`TODO-1.3-sentences-syntax` 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:`TODO-1.3-sentences-syntax` 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 + + .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident. + + Idem but locally to the current section. + + .. cmdv:: SubClass @ident := @type. + + If `type` is a class `ident'` applied to some arguments then + `ident` is defined and an identity coercion of name + `Id_ident_ident'` is + declared. Otherwise said, this is an abbreviation for + + ``Definition`` `ident` ``:=`` `type`. + + ``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 +------------------------------------- + +.. cmd:: Set Printing Coercions. + + This command forces all the coercions to be printed. + Conversely, to skip the printing of coercions, use + ``Unset Printing Coercions``. By default, coercions are not printed. + +.. cmd:: Add Printing Coercion @qualid. + + This command forces coercion denoted by `qualid` to be printed. + To skip the printing of coercion `qualid`, use + ``Remove Printing Coercion`` `qualid`. By default, a coercion is never printed. + + +Classes as Records +------------------ + +We allow the definition of *Structures with Inheritance* (or +classes as records) by extending the existing ``Record`` macro +(see Section :ref:`TODO-2.1-Record`). Its new syntax is: + +.. cmd:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }. + + The first identifier `ident` is the name of the defined record and + `sort` is its type. The optional identifier after ``:=`` is the name + of the constuctor (it will be ``Build_``\ `ident` if not given). + The other identifiers are the names of the fields, and the `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. Remark 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). + +.. note:: + + The keyword ``Structure`` is a synonym of ``Record``. + +.. + FIXME: \comindex{Structure} + + +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 +--------------------= + +From |Coq| version 8.3, the coercions present in a module are activated +only when the module is explicitly imported. Formerly, the coercions +were activated as soon as the module was required, whatever it was +imported or not. + +To recover the behavior of the versions of |Coq| prior to 8.3, use the +following command: + +.. cmd:: Set Automatic Coercions Import. + +To cancel the effect of the option, use instead ``Unset Automatic Coercions Import``. + + +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" behaviour 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. Approximatively, to coerce :g:`t:forall x:A,B` towards +:g:`forall x:A',B'`, one 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 be applied +to ``B`` also 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..e850587c8a --- /dev/null +++ b/doc/sphinx/addendum/micromega.rst @@ -0,0 +1,252 @@ +.. _ 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``. + ++ ``lia`` is a decision procedure for linear integer arithmetic (see Section :ref:`lia <lia>`); ++ ``nia`` is an incomplete proof procedure for integer non-linear + arithmetic (see Section :ref:`nia <nia>`); ++ ``lra`` is a decision procedure for linear (real or rational) arithmetic + (see Section :ref:`lra <lra>`); ++ ``nra`` is an incomplete proof procedure for non-linear (real or + rational) arithmetic (see Section :ref:`nra <nra>`); ++ ``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` (see Section :ref:`psatz <psatz>`). + +The tactics solve propositional formulas parameterized by atomic +arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}. +The syntax of the formulas is the following: + + .. productionlist:: `F` + F : A ∣ P ∣ True ∣ False ∣ F 1 ∧ F 2 ∣ F 1 ∨ F 2 ∣ F 1 ↔ F 2 ∣ F 1 → F 2 ∣ ¬ F + A : p 1 = p 2 ∣ p 1 > p 2 ∣ p 1 < p 2 ∣ p 1 ≥ p 2 ∣ p 1 ≤ p 2 + p : c ∣ x ∣ −p ∣ p 1 − p 2 ∣ p 1 + p 2 ∣ p 1 × p 2 ∣ 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 a oracle which searches for +:math:`-1` within the cone. Upon success, the oracle returns a *cone +expression* that is normalized by the ring tactic (see :ref:`theringandfieldtacticfamilies`) +and checked to be :math:`-1`. + +.. _lra: + +`lra`: a decision procedure for linear real and rational arithmetic +------------------------------------------------------------------- + +The `lra` tactic is searching for *linear* refutations using Fourier +elimination [#]_. 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 `lra` is the combined deductive power of +`ring_simplify` and `fourier`. There is also an overlap with the field +tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`. + + +.. _lia: + +`lia`: a tactic for linear integer arithmetic +--------------------------------------------- + +The tactic lia offers an alternative to the omega and romega tactic +(see :ref:`omega`). Roughly speaking, the deductive power of lia is +the combined deductive power of `ring_simplify` and `omega`. However, it +solves linear goals that `omega` and `romega` do not solve, such as the +following so-called *omega nightmare* :cite:`TheOmegaPaper`. + +.. coqtop:: in + + Goal forall x y, + 27 <= 11 * x + 13 * y <= 45 -> + -10 <= 7 * x - 9 * y <= 4 -> False. + +The estimation of the relative efficiency of `lia` *vs* `omega` and `romega` +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 `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: + +**Theorem**. 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: + +`nra`: a proof procedure for non-linear arithmetic +-------------------------------------------------- + +The `nra` 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 `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 `lra` searches for a +proof by abstracting monomials by variables. + +.. _nia: + +`nia`: a proof procedure for non-linear integer arithmetic +---------------------------------------------------------- + +The `nia` tactic is a proof procedure for non-linear integer arithmetic. +It performs a pre-processing similar to `nra`. The obtained goal is +solved using the linear integer prover `lia`. + +.. _psatz: + +`psatz`: a proof procedure for non-linear arithmetic +---------------------------------------------------- + +The `psatz` tactic explores the :math:`\mathit{Cone}` by increasing degrees – hence the +depth parameter :math:`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: + +.. coqtop:: all + + 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 `ring` we +obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. + +.. [#] Support for `nat` and :math:`\mathbb{N}` is obtained by pre-processing the goal with + the `zify` tactic. +.. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp +.. [#] Variants deal with equalities and strict inequalities. +.. [#] More efficient linear programming techniques could equally be employed. +.. [#] 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/nsatz.rst b/doc/sphinx/addendum/nsatz.rst new file mode 100644 index 0000000000..ef9b3505d4 --- /dev/null +++ b/doc/sphinx/addendum/nsatz.rst @@ -0,0 +1,101 @@ +.. include:: ../preamble.rst + +.. _nsatz: + +Nsatz: tactics for proving equalities in integral domains +=========================================================== + +:Author: Loïc Pottier + +The tactic `nsatz` proves 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₁,Q₁,\ldots,Pₛ, Qₛ` are polynomials and :math:`A` is an integral +domain, i.e. a commutative ring with no zero divisor. 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:`TODO-27.2.2`) , not only Leibnitz 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. + + +Using the basic tactic `nsatz` +------------------------------ + + +Load the Nsatz module: + +.. coqtop:: all + + Require Import Nsatz. + +and use the tactic `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 divisor +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 algebraic closed field: the method is +complete). + +So, proving our initial problem can reduce into 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`. + +The ``Nsatz`` module defines the tactic `nsatz`, which can be used without +arguments, or with the syntax: + +| nsatz with radicalmax:=num%N strategy:=num%Z parameters:= :n:`{* var}` variables:= :n:`{* var}` + +where: + +* `radicalmax` is a bound when for searching r s.t. + :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 Buchberger algorithm. If `variables` = `(@nil R)`, + then `lvar` is replaced by all the variables which are not in + `parameters`. + +See 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..20e40c5507 --- /dev/null +++ b/doc/sphinx/addendum/omega.rst @@ -0,0 +1,184 @@ +.. _omega: + +Omega: a solver for quantifier-free problems in Presburger Arithmetic +===================================================================== + +:Author: Pierre Crégut + +Description of ``omega`` +------------------------ + +This tactic does not need any parameter: + +.. tacn:: omega + +``omega`` solves a goal in Presburger arithmetic, i.e. a universally +quantified formula made of equations and inequations. Equations may +be specified either on the type ``nat`` of natural numbers or on +the type ``Z`` of binary-encoded integer numbers. 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 ``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`` +------------------------------------------ + +``omega`` applied only to quantifier-free formulas built from the +connectors:: + + /\ \/ ~ -> + +on atomic formulas. Atomic formulas are built from the predicates:: + + = < <= > >= + +on ``nat`` or ``Z``. In expressions of type ``nat``, ``omega`` recognizes:: + + + - * S O pred + +and in expressions of type ``Z``, ``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 ``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 ``intros`` first; if it contains + existentials quantifiers too, ``omega`` is not strong enough to solve your + goal). This may happen also if your goal contains arithmetical + operators unknown from ``omega``. Finally, your goal may be really + wrong! + +.. exn:: omega: Not a quantifier-free goal + + If your goal is universally quantified, you should first apply + ``intro`` as many time as needed. + +.. exn:: omega: Unrecognized predicate or connective: @ident + +.. exn:: omega: Unrecognized atomic proposition: ... + +.. exn:: omega: Can't solve a goal with proposition variables + +.. exn:: omega: Unrecognized proposition + +.. exn:: omega: Can't solve a goal with non-linear products + +.. exn:: omega: Can't solve a goal with equality on type ... + + +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 +------- + +.. opt:: Stable Omega + +This deprecated option (on by default) is for compatibility with Coq pre 8.5. It +resets internal name counters to make executions of ``omega`` independent. + +.. opt:: Omega UseLocalDefs + +This option (on by default) allows ``omega`` to use the bodies of local +variables. + +.. opt:: Omega System + +This option (off by default) activate the printing of debug information + +.. opt:: 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 an hypothesis. + * Hypothesis are decomposed in simple equations or inequations. Multiple + goals may result from this phase. + * Equations and inequations over ``nat`` are translated over + ``Z``, multiple goals may result from the translation of substraction. + * Equations and inequations 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 ``omega`` tactic uses +a small subset of the decision procedure presented in :cite:`TheOmegaPaper` +Here is an overview, look at the original paper for more information. + + * Equations and inequations 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 inequation defines a half space in the space of real value + of the variables. + * Inequations are solved by projecting on the hyperspace + defined by cancelling one of the variable. They are partitioned + according to the sign of the coefficient of the eliminated + variable. Pairs of inequations from different classes define a + new edge in the projection. + * Redundant inequations 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 (dark shadow) 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..8c1b9d152b --- /dev/null +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -0,0 +1,229 @@ +.. include:: ../replaces.rst + +.. _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:`TODO-2.4`). + +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:`TODO-7.1.5`) 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 command ``Set 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 resiliency: 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 resiliency 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 resiliency 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 that 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. Only then are all the universe constraints 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 configure with +``-async-proofs-delegation-threshold``. Default is 0.03 seconds. + +Batch mode +--------------- + +When |Coq| is used as a batch compiler by running `coqc` or `coqtop` +-compile, it produces a `.vo` file for each `.v` file. A `.vo` file contains, +among other things, theorems 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 honor the +limit, globally. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst new file mode 100644 index 0000000000..eb50e52dc7 --- /dev/null +++ b/doc/sphinx/addendum/program.rst @@ -0,0 +1,381 @@ +.. include:: ../preamble.rst +.. include:: ../replaces.rst + +.. 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 T : Set can +be considered as an object of type { x : T | P} for any wellformed P : +Prop. If we go from T to the subset of T verifying property 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 n). + + This permits to get the proper equalities in the context of proof + obligations inside clauses, without which reasoning is very limited. + ++ Generation of inequalities. If a pattern intersects with a previous + one, an inequality 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 ∀ 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. + +.. opt:: Program Cases + + This controls the special treatment of pattern-matching generating equalities + and inequalities when using |Program| (it is on by default). All + pattern-matchings and let-patterns are handled using the standard algorithm + of |Coq| (see :ref:`extendedpatternmatching`) when this option is + deactivated. + +.. opt:: 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. + +.. _syntactic_control: + +Syntactic control over equalities +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +To give more control over the generation of equalities, the +typechecker 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 dec combinator to get the correct hypotheses as in: + +.. coqtop:: none + + 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 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 +Definition (see Section `TODO-1.3.2-Definition`_) and Fixpoint (see Section `TODO-1.3.4-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 + + .. 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 ... + + + .. 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 + +See also: Sections `TODO-6.10.1-Opaque`_, `TODO-6.10.2-Transparent`_, `TODO-8.7.5-unfold`_ + +.. _program_fixpoint: + +Program Fixpoint +~~~~~~~~~~~~~~~~ + +.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term. + +The optional order annotation follows the grammar: + +.. productionlist:: orderannot + order : measure `term` (`term`)? | wf `term` `term` + ++ :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on + any subset of the arguments and the optional (parenthesised) term + ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R`` + to ``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 +Section `TODO-1.3.4-Fixpoint`_), except it may also generate obligations. It works +with mutually recursive definitions too. + +.. coqtop:: reset none + + 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 + + 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. + +.. opt:: Transparent Obligations + + Control whether all obligations should be declared as transparent + (the default), or if the system should infer which obligations can be + declared opaque. + +.. opt:: Hide Obligations + + Control whether obligations appearing in the + term should be hidden as implicit arguments of the special + constantProgram.Tactics.obligation. + +.. opt:: 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. + +.. bibliography:: ../biblio.bib + :keyprefix: p- diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst new file mode 100644 index 0000000000..b861892cbb --- /dev/null +++ b/doc/sphinx/addendum/ring.rst @@ -0,0 +1,770 @@ +.. include:: ../replaces.rst +.. |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 deal with ring and +field equations. + +What does this tactic do? +------------------------------ + +``ring`` does associative-commutative rewriting in ring and semi-ring +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 ring? It normalizes polynomials over +any ring or semi-ring 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 in the ring |nat|, consider +the expression: + + +:: + + (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 + +The ``ring`` tactic solves equations upon polynomial expressions of a ring +(or semi-ring) structure. It proceeds by normalizing both hand sides +of the equation (w.r.t. associativity, commutativity and +distributivity, constant propagation, rewriting of monomials) and +comparing syntactically the results. + +.. tacn:: ring_simplify + +``ring_simplify`` applies the normalization procedure described above to +the terms given. 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 hand +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 }] + +decides the equality of two terms modulo ring operations and +the equalities defined by the :n:`@term`\ s. +Each :n:`@term` has to be a proof of some equality `m = p`, where `m` is a monomial (after “abstraction”), `p` a polynomial and `=` the corresponding equality of the ring structure. + +.. tacv:: ring_simplify [{* @term }] {* @term } in @ident + +performs the simplification in the hypothesis named :n:`@ident`. + + +.. note:: + + .. tacn:: ring_simplify @term1; ring_simplify @term2 + + is not equivalent to + + .. tacn:: ring_simplify @term1 @term2 + + In the latter case the variables map + is shared between the two terms, and common subterm `t` of :n:`@term1` and :n:`@term2` + 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 + + ``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 ``Add Ring`` first. + +.. exn:: cannot find a declared ring structure for equality @term + + Same as above is the case of the ``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 definition of ring and semi-rings (see module +``Ring_theory``) is: + +.. coqtop:: in + + 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: + +.. coqtop:: in + + 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 semi-ring), 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 semi-rings). + +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 + + Section POWER. + Variable Cpow : Set. + Variable Cp_phi : N -> Cpow. + Variable rpow : R -> Cpow -> R. + + Record power_theory : Prop := mkpow_th { + rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n) + }. + + End POWER. + + +The syntax for adding a new ring is + +.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )}. + +The :n:`@ident` is not relevant. It is just used for error messages. The +:n:`@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: + +.. prodn:: + 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 hould 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 ``ring`` and ``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 ``ring_simplify``. For instance, it can be used to undo + modifications of the preprocessor. + +power_tac :n:`@term` [:n:`@ltac`] + allows ``ring`` and ``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 ``ring_simplify`` to use a minus operation when + outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The + term `:n:`@term` is a proof that a given sign function indicates expressions + that are signed (`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 ``ring`` and ``ring_simplify`` to use monomials with + coefficient 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 tactic written using *reflection*. +What is reflection? Basically, it is writing |Coq| tactics in |Coq|, rather +than in |OCaml|. From the philosophical point of view, it 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 it correctness. + +The interested reader is strongly advised to have a look at the +file ``Ring_polynom.v``. Here a type for polynomials is defined: + + +.. coqtop:: in + + 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: + + +.. coqtop:: in + + 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}`. + +Variables maps are represented by list 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: + + +.. coqtop:: in + + + 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: + + +.. coqtop:: in + + 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 do not see the right part of the diagram. From outside, the +tactic behaves like a |bdi| simplification extended with AC rewriting +rules. Basically, the proof is only the application of the main +correctness theorem to well-chosen arguments. + +Dealing with fields +------------------------ + +.. tacn:: field + +The ``field`` tactic is an extension of the ``ring`` to deal with rational +expression. 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 ``field`` also generates non-zero 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. Non-zero +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 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}] + + decides the equality of two terms modulo + field operations and the equalities defined + by the :n:`@term`\ s. Each :n:`@term` has to be a proof of some equality + `m` ``=`` `p`, where `m` is a monomial (after “abstraction”), `p` a polynomial + and ``=`` the corresponding equality of the field structure. + +.. note:: + + rewriting works with the equality `m` ``=`` `p` only if `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 the + fraction simplifications. This yields smaller expressions when + reducing to the same denominator since common factors can be canceled. + +.. tacv:: field_simplify [{* @term }] + + performs the simplification in the conclusion of the goal using the equalities + defined by the :n:`@term`\ s. + +.. tacv:: field_simplify [{* @term }] {* @term } + + performs the simplification in the terms :n:`@terms` of the conclusion of the goal + using the equalities defined by :n:`@term`\ s inside the brackets. + +.. tacv :: field_simplify in @ident + + performs the simplification in the assumption :n:`@ident`. + +.. tacv :: field_simplify [{* @term }] in @ident + + performs the simplification + in the assumption :n:`@ident` using the equalities defined by the :n:`@term`\ s. + +.. tacv:: field_simplify [{* @term }] {* @term } in @ident + + performs the simplification in the :n:`@term`\ s of the assumption :n:`@ident` using the + equalities defined by the :n:`@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 }] + + performs the simplification in + the conclusion of the goal using the equalities defined by + :n:`@term`\ s. + +.. tacv:: field_simplify_eq in @ident + + performs the simplification in the assumption :n:`@ident`. + +.. tacv:: field_simplify_eq [{* @term}] in @ident + + performs the simplification in the assumption :n:`@ident` using the equalities defined by + :n:`@terms`\ 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 semi-fields is: + +.. coqtop:: in + + 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: + +.. coqtop:: in + + 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 just used 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. + +.. prodn:: + 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 non-zero coefficients are mapped to non-zero + elements of the field. :n:`@term` is a proof of + + ``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 his article in TACS’97 [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 a +few |ML| code for the ``Add Ring`` command, that allow to register 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 a classical one: using +reflection, we get for free integration of computation and reasoning +that would be very complex to implement in the classic fashion. + +Is it the ultimate way to write tactics? The answer is: yes and no. +The ``ring`` tactic uses intensively the conversion rule of |Cic|, that is +replaces proof by computation the most as it is possible. It can be +useful in all situations where a classical tactic generates huge proof +terms. Symbolic Processing and Tautologies are in that case. 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 correction theorem that states that *replaying traces* is safe +w.r.t 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 +semantic by applying the correction lemma. + + + + + + +.. rubric:: Footnotes +.. [#f1] based on previous work from Patrick Loiseleur and Samuel Boutin + + + diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst new file mode 100644 index 0000000000..becebb421b --- /dev/null +++ b/doc/sphinx/addendum/type-classes.rst @@ -0,0 +1,587 @@ +.. include:: ../replaces.rst + +.. _typeclasses: + +Type Classes +============ + +:Source: https://coq.inria.fr/distrib/current/refman/type-classes.html +:Author: Matthieu Sozeau + +This chapter presents a quick reference of the commands related to type +classes. For an actual introduction to type classes, 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: + +``Class Id (`` |p_1| ``:`` |t_1| ``) ⋯ (`` |p_n| ``:`` |t_n| ``) [: +sort] := {`` |f_1| ``:`` |u_1| ``; ⋮`` |f_m| ``:`` |u_m| ``}.`` + +``Instance ident : Id`` |p_1| ``⋯`` |p_n| ``:= {`` |f_1| ``:=`` |t_1| ``; ⋮`` |f_m| ``:=`` |t_m| ``}.`` + +The |p_i| ``:`` |t_i| variables are called the *parameters* of the class and +the |f_i| ``:`` |t_i| 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 ident 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 }. + +If one does not give all the members in the Instance declaration, Coq +enters the proof-mode and the user is asked to build inhabitants of +the remaining fields, e.g.: + +.. coqtop:: in + + Instance eq_bool : EqDec bool := + { eqb x y := if x then y else negb y }. + +.. coqtop:: all + + Proof. intros x y H. + +.. coqtop:: all + + destruct x ; destruct y ; (discriminate || reflexivity). + +.. coqtop:: all + + Defined. + +One has to take care that the transparency of every field is +determined by the transparency of the ``Instance`` proof. One can use +alternatively the ``Program Instance`` variant which has richer facilities +for dealing with obligations. + + +Binding classes +--------------- + +Once a type class 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 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 type classes: + ++ They automatically set the maximally implicit status for type class + 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 type class + 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_impl `{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 + + 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 + + Abort. + +These instances are used just as well as lemmas in the instance hint +database. + +Sections and contexts +--------------------- + +To ease the parametrization of developments by type classes, we +provide a new way to introduce variables into section contexts, +compatible with the implicit argument mechanism. The new command works +similarly to the ``Variables`` vernacular (:ref:`TODO-1.3.2-Definitions`), except it +accepts any binding context as argument. For example: + +.. coqtop:: all + + Section EqDec_defs. + + Context `{EA : EqDec A}. + + Global 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 }. + Admitted. + + End EqDec_defs. + + About option_eqb. + +Here the Global modifier redeclares the instance at the end of the +section, once it has been generalized by the context variables it +uses. + + +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 morally equivalent to: + +:: + + 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 +~~~~~~~~~~~~~ + +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 part 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. + +One can also declare existing objects or structure projections using +the Existing Instance command to achieve the same effect. + + +Summary of the commands +----------------------- + + +.. _Class: + +.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } }. + + The ``Class`` command is used to declare a type class with parameters + ``binders`` and fields the declared record fields. + +Variants: + +.. _singleton-class: + +.. cmd:: 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. + +.. cmd:: Existing Class @ident + + This variant declares a class a posteriori from a constant or + inductive definition. No methods or instances are defined. + +.. _Instance: + +.. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } + +The ``Instance`` command is used to declare a type class instance named +``ident`` of the class ``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 ``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 +auto hints. If the priority is not specified, it defaults to the number +of non-dependent binders of the instance. + +Variants: + + +.. cmd:: Instance ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term + + This syntax is used for declaration of singleton class instances or + for directly giving an explicit term of type ``forall binders, Class + t1 … tn``. One need not even mention the unique field name for + singleton classes. + +.. cmd:: Global Instance + + One can use the ``Global`` modifier on instances declared in a + section so that their generalization is automatically redeclared + after the section is closed. + +.. cmd:: Program Instance + + Switches the type-checking to Program (chapter :ref:`program`) and + uses the obligation mechanism to manage missing fields. + +.. cmd:: Declare Instance + + In a Module Type, this command states that a corresponding concrete + instance should exist in any implementation of thisModule Type. This + is similar to the distinction betweenParameter vs. Definition, or + between Declare Module and Module. + + +Besides the ``Class`` and ``Instance`` vernacular commands, there are a +few other commands related to type classes. + +.. _ExistingInstance: + +Existing Instance +~~~~~~~~~~~~~~~~~ + +.. cmd:: Existing Instance {+ @ident} [| priority] + +This commands adds an arbitrary list of constants whose type ends with +an applied type class 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 ``Print Instances``. + +.. _Context: + +Context +~~~~~~~ + +.. cmd:: Context @binders + +Declares variables according to the given binding context, which might +use :ref:`implicit-generalization`. + + +.. _typeclasses-eauto: + +``typeclasses eauto`` +~~~~~~~~~~~~~~~~~~~~~ + +The ``typeclasses eauto`` tactic uses a different resolution engine than +eauto and auto. The main differences are the following: + ++ Contrary to ``eauto`` and ``auto``, the resolution is done entirely in + the new proof engine (as of Coq v8.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 + thetypeclass_instances database by default (instead of core). + Dependent subgoals are automatically shelved, and shelved goals can + remain after resolution ends (following the behavior ofCoq 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 + typeclasses 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 the local hypotheses, we use the transparent + state of the first hint database given. Using an empty database + (created with 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. + + +Variants: + +#. ``typeclasses eauto [num]`` + + *Warning:* The semantics for the limit num + is different than for auto. By default, if no limit is given the + search is unbounded. Contrary to auto, introduction steps (intro) are + counted, which might result in larger limits being necessary when + searching with typeclasses eauto than auto. + +#. ``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). + +.. _autoapply: + +``autoapply term with ident`` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +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 ``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 type class +resolution locally at the hint application time. + +.. _TypeclassesTransparent: + +Typeclasses Transparent, Typclasses Opaque +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Typeclasses { Transparent | Opaque } {+ @ident} + + This commands defines the transparency of the given identifiers + during type class resolution. 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: + +:: + + relation A := A -> A -> Prop. + +This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. + + +Set Typeclasses Dependency Order +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +This option (on by default since 8.6) respects the dependency order +between subgoals, meaning that subgoals which are depended on by other +subgoals come first, while the non-dependent subgoals were put before +the dependent ones previously (Coq v8.5 and below). This can result in +quite different performance behaviors of proof search. + + +Set Typeclasses Filtered Unification +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +This option, 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 +explicitely appear in the pattern will make it never apply on a goal +where there is a hole in that place. + + +Set Typeclasses Limit Intros +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + + +This option (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). + + +Set Typeclass Resolution For Conversion +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +This option (on by default) controls the use of typeclass resolution +when a unification problem cannot be solved during elaboration/type- +inference. With this option on, when a unification fails, typeclass +resolution is tried before launching unification once again. + + +Set Typeclasses Strict Resolution +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Typeclass declarations introduced when this option is set have a +stricter resolution behavior (the option 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. + + +Set 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. + + +Set Typeclasses Unique Instances +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Typeclass declarations introduced when this option is set have a more +efficient resolution behavior (the option 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. + + +Typeclasses eauto `:=` +~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Typeclasses eauto := {? debug} {? {dfs | bfs}} depth + + This command allows more global customization of the type class + resolution tactic. The semantics of the options are: + + + ``debug`` In debug mode, the trace of successfully applied tactics is + printed. + + + ``dfs, bfs`` This sets the search strategy to depth-first search (the + default) or breadth-first search. + + + ``depth`` This sets the depth limit of the search. + + +Set Typeclasses Debug +~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Set Typeclasses Debug {? Verbosity @num} + +These options allow to see the resolution steps of typeclasses that are +performed during search. The ``Debug`` option is synonymous to ``Debug +Verbosity 1``, and ``Debug Verbosity 2`` provides more information +(tried tactics, shelving of goals, etc…). + + +Set Refine Instance Mode +~~~~~~~~~~~~~~~~~~~~~~~~ + +The option Refine Instance Mode allows to switch the behavior of +instance declarations made through the Instance command. + ++ When it is on (the default), instances that have unsolved holes in + their proof-term silently open the proof mode with the remaining + obligations to prove. + ++ When it is off, they fail with an error instead. |