diff options
Diffstat (limited to 'doc/sphinx/language/extensions')
| -rw-r--r-- | doc/sphinx/language/extensions/arguments-command.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/canonical.rst | 558 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/evars.rst | 112 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/implicit-arguments.rst | 121 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/index.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst | 898 |
6 files changed, 1572 insertions, 125 deletions
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index 34a48b368b..85481043b2 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -109,7 +109,7 @@ Setting properties of a function's arguments clears argument scopes of :n:`@smart_qualid` `extra scopes` defines extra argument scopes, to be used in case of coercion to ``Funclass`` - (see the :ref:`implicitcoercions` chapter) or with a computed type. + (see :ref:`coercions`) or with a computed type. `simpl nomatch` prevents performing a simplification step for :n:`@smart_qualid` that would expose a match construct in the head position. See :ref:`Args_effect_on_unfolding`. diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst new file mode 100644 index 0000000000..f55f3c5495 --- /dev/null +++ b/doc/sphinx/language/extensions/canonical.rst @@ -0,0 +1,558 @@ +.. _canonicalstructures: + +Canonical Structures +====================== + +:Authors: Assia Mahboubi and Enrico Tassi + +This chapter explains the basics of canonical structures and how they can be used +to overload notations and build a hierarchy of algebraic structures. The +examples are taken from :cite:`CSwcu`. We invite the interested reader to refer +to this paper for all the details that are omitted here for brevity. The +interested reader shall also find in :cite:`CSlessadhoc` a detailed description +of another, complementary, use of canonical structures: advanced proof search. +This latter papers also presents many techniques one can employ to tune the +inference of canonical structures. + + .. extracted from implicit arguments section + +.. _canonical-structure-declaration: + +Declaration of canonical structures +----------------------------------- + +A canonical structure is an instance of a record/structure type that +can be used to solve unification problems involving a projection +applied to an unknown structure instance (an implicit argument) and a +value. The complete documentation of canonical structures can be found +in :ref:`canonicalstructures`; here only a simple example is given. + +.. cmd:: Canonical {? Structure } @smart_qualid + Canonical {? Structure } @ident_decl @def_body + :name: Canonical Structure; _ + + The first form of this command declares an existing :n:`@smart_qualid` as a + canonical instance of a structure (a record). + + The second form defines a new constant as if the :cmd:`Definition` command + had been used, then declares it as a canonical instance as if the first + form had been used on the defined object. + + This command supports the :attr:`local` attribute. When used, the + structure is canonical only within the :cmd:`Section` containing it. + + Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the + structure :g:`struct` of which the fields are |x_1|, …, |x_n|. + Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be + solved during the type checking process, :token:`qualid` is used as a solution. + Otherwise said, :token:`qualid` is canonically used to extend the field |c_i| + into a complete structure built on |c_i|. + + Canonical structures are particularly useful when mixed with coercions + and strict implicit arguments. + + .. example:: + + Here is an example. + + .. coqtop:: all reset + + Require Import Relations. + + Require Import EqNat. + + Set Implicit Arguments. + + Unset Strict Implicit. + + Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier; + Prf_equiv : equivalence Carrier Equal}. + + Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y). + + Axiom eq_nat_equiv : equivalence nat eq_nat. + + Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. + + Canonical nat_setoid. + + Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A` + and :g:`B` can be synthesized in the next statement. + + .. coqtop:: all abort + + Lemma is_law_S : is_law S. + + .. note:: + If a same field occurs in several canonical structures, then + only the structure declared first as canonical is considered. + + .. attr:: canonical(false) + + To prevent a field from being involved in the inference of + canonical instances, its declaration can be annotated with the + :attr:`canonical(false)` attribute (cf. the syntax of + :n:`@record_field`). + + .. example:: + + For instance, when declaring the :g:`Setoid` structure above, the + :g:`Prf_equiv` field declaration could be written as follows. + + .. coqdoc:: + + #[canonical(false)] Prf_equiv : equivalence Carrier Equal + + See :ref:`canonicalstructures` for a more realistic example. + +.. attr:: canonical + + This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. + It is equivalent to having a :cmd:`Canonical Structure` declaration just + after the command. + +.. cmd:: Print Canonical Projections {* @smart_qualid } + + This displays the list of global names that are components of some + canonical structure. For each of them, the canonical structure of + which it is a projection is indicated. If constants are given as + its arguments, only the unification rules that involve or are + synthesized from simultaneously all given constants will be shown. + + .. example:: + + For instance, the above example gives the following output: + + .. coqtop:: all + + Print Canonical Projections. + + .. coqtop:: all + + Print Canonical Projections nat. + + .. note:: + + The last line in the first example would not show up if the + corresponding projection (namely :g:`Prf_equiv`) were annotated as not + canonical, as described above. + +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 reset + + Module EQ. + Record class (T : Type) := Class { cmp : T -> T -> Prop }. + Structure type := Pack { obj : Type; class_of : class obj }. + Definition op (e : type) : obj e -> obj e -> Prop := + let 'Pack _ (Class _ the_cmp) := e in the_cmp. + Check op. + Arguments op {e} x y : simpl never. + Arguments Class {T} cmp. + Module theory. + Notation "x == y" := (op x y) (at level 70). + End theory. + End EQ. + +We use Coq modules as namespaces. This allows us to follow the same +pattern and naming convention for the rest of the chapter. The base +namespace contains the definitions of the algebraic structure. To +keep the example small, the algebraic structure ``EQ.type`` we are +defining is very simplistic, and characterizes terms on which a binary +relation is defined, without requiring such relation to validate any +property. The inner theory module contains the overloaded notation ``==`` +and will eventually contain lemmas holding all the instances of the +algebraic structure (in this case there are no lemmas). + +Note that in practice the user may want to declare ``EQ.obj`` as a +coercion, but we will not do that here. + +The following line tests that, when we assume a type ``e`` that is in +theEQ class, we can relate two of its objects with ``==``. + +.. coqtop:: all + + Import EQ.theory. + Check forall (e : EQ.type) (a b : EQ.obj e), a == b. + +Still, no concrete type is in the ``EQ`` class. + +.. coqtop:: all + + Fail Check 3 == 3. + +We amend that by equipping ``nat`` with a comparison relation. + +.. coqtop:: all + + Definition nat_eq (x y : nat) := Nat.compare x y = Eq. + Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq. + Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl. + Check 3 == 3. + Eval compute in 3 == 4. + +This last test shows that |Coq| is now not only able to type check ``3 == 3``, +but also that the infix relation was bound to the ``nat_eq`` relation. +This relation is selected whenever ``==`` is used on terms of type nat. +This can be read in the line declaring the canonical structure +``nat_EQty``, where the first argument to ``Pack`` is the key and its second +argument a group of canonical values associated to the key. In this +case we associate to nat only one canonical value (since its class, +``nat_EQcl`` has just one member). The use of the projection ``op`` requires +its argument to be in the class ``EQ``, and uses such a member (function) +to actually compare its arguments. + +Similarly, we could equip any other type with a comparison relation, +and use the ``==`` notation on terms of this type. + + +Derived Canonical Structures +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +We know how to use ``==`` on base types, like ``nat``, ``bool``, ``Z``. Here we show +how to deal with type constructors, i.e. how to make the following +example work: + + +.. coqtop:: all + + Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b). + +The error message is telling that |Coq| has no idea on how to compare +pairs of objects. The following construction is telling Coq exactly +how to do that. + +.. coqtop:: all + + Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) := + fst x == fst y /\ snd x == snd y. + + Definition pair_EQcl e1 e2 := EQ.Class (pair_eq e1 e2). + + Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type := + EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2). + + Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b). + + Check forall n m : nat, (3, 4) == (n, m). + +Thanks to the ``pair_EQty`` declaration, |Coq| is able to build a comparison +relation for pairs whenever it is able to build a comparison relation +for each component of the pair. The declaration associates to the key ``*`` +(the type constructor of pairs) the canonical comparison +relation ``pair_eq`` whenever the type constructor ``*`` is applied to two +types being themselves in the ``EQ`` class. + +Hierarchy of structures +---------------------------- + +To get to an interesting example we need another base class to be +available. We choose the class of types that are equipped with an +order relation, to which we associate the infix ``<=`` notation. + +.. coqtop:: all + + Module LE. + + Record class T := Class { cmp : T -> T -> Prop }. + + Structure type := Pack { obj : Type; class_of : class obj }. + + Definition op (e : type) : obj e -> obj e -> Prop := + let 'Pack _ (Class _ f) := e in f. + + Arguments op {_} x y : simpl never. + + Arguments Class {T} cmp. + + Module theory. + + Notation "x <= y" := (op x y) (at level 70). + + End theory. + + End LE. + +As before we register a canonical ``LE`` class for ``nat``. + +.. coqtop:: all + + Import LE.theory. + + Definition nat_le x y := Nat.compare x y <> Gt. + + Definition nat_LEcl : LE.class nat := LE.Class nat_le. + + Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl. + +And we enable |Coq| to relate pair of terms with ``<=``. + +.. coqtop:: all + + Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) := + fst x <= fst y /\ snd x <= snd y. + + Definition pair_LEcl e1 e2 := LE.Class (pair_le e1 e2). + + Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type := + LE.Pack (LE.obj e1 * LE.obj e2) (pair_LEcl e1 e2). + + Check (3,4,5) <= (3,4,5). + +At the current stage we can use ``==`` and ``<=`` on concrete types, like +tuples of natural numbers, but we can’t develop an algebraic theory +over the types that are equipped with both relations. + +.. coqtop:: all + + Check 2 <= 3 /\ 2 == 2. + + Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y. + + Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y. + +We need to define a new class that inherits from both ``EQ`` and ``LE``. + + +.. coqtop:: all + + Module LEQ. + + Record mixin (e : EQ.type) (le : EQ.obj e -> EQ.obj e -> Prop) := + Mixin { compat : forall x y : EQ.obj e, le x y /\ le y x <-> x == y }. + + Record class T := Class { + EQ_class : EQ.class T; + LE_class : LE.class T; + extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }. + + Structure type := _Pack { obj : Type; #[canonical(false)] 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. + +The `class_of` projection of the `type` structure is annotated as *not canonical*; +it plays no role in the search for instances. + +Unfortunately there is still an obstacle to developing the algebraic +theory of this new class. + +.. coqtop:: all + + Module theory. + + Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m. + + +The problem is that the two classes ``LE`` and ``LEQ`` are not yet related by +a subclass relation. In other words |Coq| does not see that an object of +the ``LEQ`` class is also an object of the ``LE`` class. + +The following two constructions tell |Coq| how to canonically build the +``LE.type`` and ``EQ.type`` structure given an ``LEQ.type`` structure on the same +type. + +.. coqtop:: all + + Definition to_EQ (e : type) : EQ.type := + EQ.Pack (obj e) (EQ_class _ (class_of e)). + + Canonical Structure to_EQ. + + Definition to_LE (e : type) : LE.type := + LE.Pack (obj e) (LE_class _ (class_of e)). + + Canonical Structure to_LE. + +We can now formulate out first theorem on the objects of the ``LEQ`` +structure. + +.. coqtop:: all + + Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y. + + now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. + + Qed. + + Arguments lele_eq {e} x y _ _. + + End theory. + + End LEQ. + + Import LEQ.theory. + + Check lele_eq. + +Of course one would like to apply results proved in the algebraic +setting to any concrete instate of the algebraic structure. + +.. coqtop:: all + + Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m. + + Fail apply (lele_eq n m). + + Abort. + + Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : + n <= m -> m <= n -> n == m. + + Fail apply (lele_eq n m). + + Abort. + +Again one has to tell |Coq| that the type ``nat`` is in the ``LEQ`` class, and +how the type constructor ``*`` interacts with the ``LEQ`` class. In the +following proofs are omitted for brevity. + +.. coqtop:: all + + Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m. + + Admitted. + + Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat. + + Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : + n <= m /\ m <= n <-> n == m. + + Admitted. + + Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2). + +The following script registers an ``LEQ`` class for ``nat`` and for the type +constructor ``*``. It also tests that they work as expected. + +Unfortunately, these declarations are very verbose. In the following +subsection we show how to make them more compact. + +.. 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 more details in :cite:`CSwcu`. + +We now have all we need to create a compact “packager” to declare +instances of the ``LEQ`` class. + +.. coqtop:: all + + Import infrastructure. + + Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) := + [find e | EQ.obj e ~ T | "is not an EQ.type" ] + [find o | LE.obj o ~ T | "is not an LE.type" ] + [find ce | EQ.class_of e ~ ce ] + [find co | LE.class_of o ~ co ] + [find m | m ~ m0 | "is not the right mixin" ] + LEQ._Pack T (LEQ.Class ce co m). + + Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id). + +The object ``Pack`` takes a type ``T`` (the key) and a mixin ``m``. It infers all +the other pieces of the class ``LEQ`` and declares them as canonical +values associated to the ``T`` key. All in all, the only new piece of +information we add in the ``LEQ`` class is the mixin, all the rest is +already canonical for ``T`` and hence can be inferred by |Coq|. + +``Pack`` is a notation, hence it is not type checked at the time of its +declaration. It will be type checked when it is used, an in that case ``T`` is +going to be a concrete type. The odd arguments ``_`` and ``id`` we pass to the +packager represent respectively the classes to be inferred (like ``e``, ``o``, +etc) and a token (``id``) to force their inference. Again, for all the details +the reader can refer to :cite:`CSwcu`. + +The declaration of canonical instances can now be way more compact: + +.. 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/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst new file mode 100644 index 0000000000..40e0898871 --- /dev/null +++ b/doc/sphinx/language/extensions/evars.rst @@ -0,0 +1,112 @@ +.. extracted from Gallina extensions chapter + +.. _existential-variables: + +Existential variables +--------------------- + +.. insertprodn term_evar term_evar + +.. prodn:: + term_evar ::= _ + | ?[ @ident ] + | ?[ ?@ident ] + | ?@ident {? @%{ {+; @ident := @term } %} } + +|Coq| terms can include existential variables which represents unknown +subterms to eventually be replaced by actual subterms. + +Existential variables are generated in place of unsolvable implicit +arguments or “_” placeholders when using commands such as ``Check`` (see +Section :ref:`requests-to-the-environment`) or when using tactics such as +:tacn:`refine`, as well as in place of unsolvable instances when using +tactics such that :tacn:`eapply`. An existential +variable is defined in a context, which is the context of variables of +the placeholder which generated the existential variable, and a type, +which is the expected type of the placeholder. + +As a consequence of typing constraints, existential variables can be +duplicated in such a way that they possibly appear in different +contexts than their defining context. Thus, any occurrence of a given +existential variable comes with an instance of its original context. +In the simple case, when an existential variable denotes the +placeholder which generated it, or is used in the same context as the +one in which it was generated, the context is not displayed and the +existential variable is represented by “?” followed by an identifier. + +.. coqtop:: all + + Parameter identity : forall (X:Set), X -> X. + + Check identity _ _. + + Check identity _ (fun x => _). + +In the general case, when an existential variable :n:`?@ident` appears +outside of its context of definition, its instance, written under the +form :n:`{ {*; @ident := @term} }` is appending to its name, indicating +how the variables of its defining context are instantiated. +The variables of the context of the existential variables which are +instantiated by themselves are not written, unless the :flag:`Printing Existential Instances` flag +is on (see Section :ref:`explicit-display-existentials`), and this is why an +existential variable used in the same context as its context of definition is written with no instance. + +.. coqtop:: all + + Check (fun x y => _) 0 1. + + Set Printing Existential Instances. + + Check (fun x y => _) 0 1. + +Existential variables can be named by the user upon creation using +the syntax :n:`?[@ident]`. This is useful when the existential +variable needs to be explicitly handled later in the script (e.g. +with a named-goal selector, see :ref:`goal-selectors`). + +.. extracted from Gallina chapter + +.. index:: _ + +Inferable subterms +~~~~~~~~~~~~~~~~~~ + +Expressions often contain redundant pieces of information. Subterms that can be +automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will +guess the missing piece of information. + +.. extracted from Gallina extensions chapter + +.. _explicit-display-existentials: + +Explicit displaying of existential instances for pretty-printing +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. flag:: Printing Existential Instances + + This flag (off by default) activates the full display of how the + context of an existential variable is instantiated at each of the + occurrences of the existential variable. + +.. _tactics-in-terms: + +Solving existential variables using tactics +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Instead of letting the unification engine try to solve an existential +variable by itself, one can also provide an explicit hole together +with a tactic to solve it. Using the syntax ``ltac:(``\ `tacexpr`\ ``)``, the user +can put a tactic anywhere a term is expected. The order of resolution +is not specified and is implementation-dependent. The inner tactic may +use any variable defined in its scope, including repeated alternations +between variables introduced by term binding as well as those +introduced by tactic binding. The expression `tacexpr` can be any tactic +expression as described in :ref:`ltac`. + +.. coqtop:: all + + Definition foo (x : nat) : nat := ltac:(exact x). + +This construction is useful when one wants to define complicated terms +using highly automated tactics without resorting to writing the proof-term +by means of the interactive proof engine. diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index 73b1b65097..b4f7fe0846 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -466,127 +466,6 @@ function. Check (id 1). Check (id' nat 1). -.. _canonical-structure-declaration: - -Canonical structures -~~~~~~~~~~~~~~~~~~~~ - -A canonical structure is an instance of a record/structure type that -can be used to solve unification problems involving a projection -applied to an unknown structure instance (an implicit argument) and a -value. The complete documentation of canonical structures can be found -in :ref:`canonicalstructures`; here only a simple example is given. - -.. cmd:: Canonical {? Structure } @smart_qualid - Canonical {? Structure } @ident_decl @def_body - :name: Canonical Structure; _ - - The first form of this command declares an existing :n:`@smart_qualid` as a - canonical instance of a structure (a record). - - The second form defines a new constant as if the :cmd:`Definition` command - had been used, then declares it as a canonical instance as if the first - form had been used on the defined object. - - This command supports the :attr:`local` attribute. When used, the - structure is canonical only within the :cmd:`Section` containing it. - - Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the - structure :g:`struct` of which the fields are |x_1|, …, |x_n|. - Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be - solved during the type checking process, :token:`qualid` is used as a solution. - Otherwise said, :token:`qualid` is canonically used to extend the field |c_i| - into a complete structure built on |c_i|. - - Canonical structures are particularly useful when mixed with coercions - and strict implicit arguments. - - .. example:: - - Here is an example. - - .. coqtop:: all reset - - Require Import Relations. - - Require Import EqNat. - - Set Implicit Arguments. - - Unset Strict Implicit. - - Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier; - Prf_equiv : equivalence Carrier Equal}. - - Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y). - - Axiom eq_nat_equiv : equivalence nat eq_nat. - - Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. - - Canonical nat_setoid. - - Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A` - and :g:`B` can be synthesized in the next statement. - - .. coqtop:: all abort - - Lemma is_law_S : is_law S. - - .. note:: - If a same field occurs in several canonical structures, then - only the structure declared first as canonical is considered. - - .. attr:: canonical(false) - - To prevent a field from being involved in the inference of - canonical instances, its declaration can be annotated with the - :attr:`canonical(false)` attribute (cf. the syntax of - :n:`@record_field`). - - .. example:: - - For instance, when declaring the :g:`Setoid` structure above, the - :g:`Prf_equiv` field declaration could be written as follows. - - .. coqdoc:: - - #[canonical(false)] Prf_equiv : equivalence Carrier Equal - - See :ref:`canonicalstructures` for a more realistic example. - -.. attr:: canonical - - This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. - It is equivalent to having a :cmd:`Canonical Structure` declaration just - after the command. - -.. cmd:: Print Canonical Projections {* @smart_qualid } - - This displays the list of global names that are components of some - canonical structure. For each of them, the canonical structure of - which it is a projection is indicated. If constants are given as - its arguments, only the unification rules that involve or are - synthesized from simultaneously all given constants will be shown. - - .. example:: - - For instance, the above example gives the following output: - - .. coqtop:: all - - Print Canonical Projections. - - .. coqtop:: all - - Print Canonical Projections nat. - - .. note:: - - The last line in the first example would not show up if the - corresponding projection (namely :g:`Prf_equiv`) were annotated as not - canonical, as described above. - Implicit types of variables ~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst index fc2ce03093..ed207ca743 100644 --- a/doc/sphinx/language/extensions/index.rst +++ b/doc/sphinx/language/extensions/index.rst @@ -16,13 +16,13 @@ language presented in the :ref:`previous chapter <core-language>`. .. toctree:: :maxdepth: 1 - ../gallina-extensions + evars implicit-arguments - ../../addendum/extended-pattern-matching + match ../../user-extensions/syntax-extensions arguments-command ../../addendum/implicit-coercions ../../addendum/type-classes - ../../addendum/canonical-structures + canonical ../../addendum/program ../../proof-engine/vernacular-commands diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst new file mode 100644 index 0000000000..028d0aaf57 --- /dev/null +++ b/doc/sphinx/language/extensions/match.rst @@ -0,0 +1,898 @@ +.. _extendedpatternmatching: + +Extended pattern matching +========================= + +:Authors: Cristina Cornes and Hugo Herbelin + +This section describes the full form of pattern matching in |Coq| terms. + +.. |rhs| replace:: right hand sides + +.. extracted from Gallina extensions chapter + +Variants and extensions of :g:`match` +------------------------------------- + +.. _mult-match: + +Multiple and nested pattern matching +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The basic version of :g:`match` allows pattern matching on simple +patterns. As an extension, multiple nested patterns or disjunction of +patterns are allowed, as in ML-like languages +(cf. :ref:`multiple-patterns` and :ref:`nested-patterns`). + +The extension just acts as a macro that is expanded during parsing +into a sequence of match on simple patterns. Especially, a +construction defined using the extended match is generally printed +under its expanded form (see :flag:`Printing Matching`). + +.. _if-then-else: + +Pattern-matching on boolean values: the if expression +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. insertprodn term_if term_if + +.. prodn:: + term_if ::= if @term {? {? as @name } return @term100 } then @term else @term + +For inductive types with exactly two constructors and for pattern matching +expressions that do not depend on the arguments of the constructors, it is possible +to use a ``if … then … else`` notation. For instance, the definition + +.. coqtop:: all + + Definition not (b:bool) := + match b with + | true => false + | false => true + end. + +can be alternatively written + +.. coqtop:: reset all + + Definition not (b:bool) := if b then false else true. + +More generally, for an inductive type with constructors :n:`@ident__1` +and :n:`@ident__2`, the following terms are equal: + +:n:`if @term__0 {? {? as @name } return @term } then @term__1 else @term__2` + +:n:`match @term__0 {? {? as @name } return @term } with | @ident__1 {* _ } => @term__1 | @ident__2 {* _ } => @term__2 end` + +.. example:: + + .. coqtop:: all + + Check (fun x (H:{x=0}+{x<>0}) => + match H with + | left _ => true + | right _ => false + end). + +Notice that the printing uses the :g:`if` syntax because :g:`sumbool` is +declared as such (see :ref:`controlling-match-pp`). + +.. _irrefutable-patterns: + +Irrefutable patterns: the destructuring let variants +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Pattern-matching on terms inhabiting inductive type having only one +constructor can be alternatively written using :g:`let … in …` +constructions. There are two variants of them. + + +First destructuring let syntax +++++++++++++++++++++++++++++++ + +The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1` +performs case analysis on :n:`@term__0` whose type must be an +inductive type with exactly one constructor. The number of variables +:n:`@ident__i` must correspond to the number of arguments of this +contrustor. Then, in :n:`@term__1`, these variables are bound to the +arguments of the constructor in :n:`@term__0`. For instance, the +definition + +.. coqtop:: reset all + + Definition fst (A B:Set) (H:A * B) := match H with + | pair x y => x + end. + +can be alternatively written + +.. coqtop:: reset all + + Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x. + +Notice that reduction is different from regular :g:`let … in …` +construction since it happens only if :n:`@term__0` is in constructor form. +Otherwise, the reduction is blocked. + +The pretty-printing of a definition by matching on a irrefutable +pattern can either be done using :g:`match` or the :g:`let` construction +(see Section :ref:`controlling-match-pp`). + +If term inhabits an inductive type with one constructor `C`, we have an +equivalence between + +:: + + let (ident₁, …, identₙ) [dep_ret_type] := term in term' + +and + +:: + + match term [dep_ret_type] with + C ident₁ … identₙ => term' + end + + +Second destructuring let syntax ++++++++++++++++++++++++++++++++ + +Another destructuring let syntax is available for inductive types with +one constructor by giving an arbitrary pattern instead of just a tuple +for all the arguments. For example, the preceding example can be +written: + +.. coqtop:: reset all + + Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x. + +This is useful to match deeper inside tuples and also to use notations +for the pattern, as the syntax :g:`let ’p := t in b` allows arbitrary +patterns to do the deconstruction. For example: + +.. coqtop:: all + + Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A := + let '((a,b), (c, d)) := x in (a,b,c,d). + + Notation " x 'With' p " := (exist _ x p) (at level 20). + + Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A := + let 'x With p := t in x. + +When printing definitions which are written using this construct it +takes precedence over let printing directives for the datatype under +consideration (see Section :ref:`controlling-match-pp`). + + +.. _controlling-match-pp: + +Controlling pretty-printing of match expressions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The following commands give some control over the pretty-printing +of :g:`match` expressions. + +Printing nested patterns ++++++++++++++++++++++++++ + +.. flag:: Printing Matching + + The Calculus of Inductive Constructions knows pattern matching only + over simple patterns. It is however convenient to re-factorize nested + pattern matching into a single pattern matching over a nested + pattern. + + When this flag is on (default), |Coq|’s printer tries to do such + limited re-factorization. + Turning it off tells |Coq| to print only simple pattern matching problems + in the same way as the |Coq| kernel handles them. + + +Factorization of clauses with same right-hand side +++++++++++++++++++++++++++++++++++++++++++++++++++ + +.. flag:: Printing Factorizable Match Patterns + + When several patterns share the same right-hand side, it is additionally + possible to share the clauses using disjunctive patterns. Assuming that the + printing matching mode is on, this flag (on by default) tells |Coq|'s + printer to try to do this kind of factorization. + +Use of a default clause ++++++++++++++++++++++++ + +.. flag:: Printing Allow Match Default Clause + + When several patterns share the same right-hand side which do not depend on the + arguments of the patterns, yet an extra factorization is possible: the + disjunction of patterns can be replaced with a `_` default clause. Assuming that + the printing matching mode and the factorization mode are on, this flag (on by + default) tells |Coq|'s printer to use a default clause when relevant. + +Printing of wildcard patterns +++++++++++++++++++++++++++++++ + +.. flag:: Printing Wildcard + + Some variables in a pattern may not occur in the right-hand side of + the pattern matching clause. When this flag is on (default), the + variables having no occurrences in the right-hand side of the + pattern matching clause are just printed using the wildcard symbol + “_”. + + +Printing of the elimination predicate ++++++++++++++++++++++++++++++++++++++ + +.. flag:: Printing Synth + + In most of the cases, the type of the result of a matched term is + mechanically synthesizable. Especially, if the result type does not + depend of the matched term. When this flag is on (default), + the result type is not printed when |Coq| knows that it can re- + synthesize it. + + +Printing matching on irrefutable patterns +++++++++++++++++++++++++++++++++++++++++++ + +If an inductive type has just one constructor, pattern matching can be +written using the first destructuring let syntax. + +.. table:: Printing Let @qualid + :name: Printing Let + + Specifies a set of qualids for which pattern matching is displayed using a let expression. + Note that this only applies to pattern matching instances entered with :g:`match`. + It doesn't affect pattern matching explicitly entered with a destructuring + :g:`let`. + Use the :cmd:`Add` and :cmd:`Remove` commands to update this set. + + +Printing matching on booleans ++++++++++++++++++++++++++++++ + +If an inductive type is isomorphic to the boolean type, pattern matching +can be written using ``if`` … ``then`` … ``else`` …. This table controls +which types are written this way: + +.. table:: Printing If @qualid + :name: Printing If + + Specifies a set of qualids for which pattern matching is displayed using + ``if`` … ``then`` … ``else`` …. Use the :cmd:`Add` and :cmd:`Remove` + commands to update this set. + +This example emphasizes what the printing settings offer. + +.. example:: + + .. coqtop:: all + + Definition snd (A B:Set) (H:A * B) := match H with + | pair x y => y + end. + + Test Printing Let for prod. + + Print snd. + + Remove Printing Let prod. + + Unset Printing Synth. + + Unset Printing Wildcard. + + Print snd. + +Patterns +-------- + +The full syntax of `match` is presented in :ref:`match`. +Identifiers in patterns are either constructor names or variables. Any +identifier that is not the constructor of an inductive or co-inductive +type is considered to be a variable. A variable name cannot occur more +than once in a given pattern. It is recommended to start variable +names by a lowercase letter. + +If a pattern has the form ``c x`` where ``c`` is a constructor symbol and x +is a linear vector of (distinct) variables, it is called *simple*: it +is the kind of pattern recognized by the basic version of match. On +the opposite, if it is a variable ``x`` or has the form ``c p`` with ``p`` not +only made of variables, the pattern is called *nested*. + +A variable pattern matches any value, and the identifier is bound to +that value. The pattern “``_``” (called “don't care” or “wildcard” symbol) +also matches any value, but does not bind anything. It may occur an +arbitrary number of times in a pattern. Alias patterns written +:n:`(@pattern as @ident)` are also accepted. This pattern matches the +same values as :token:`pattern` does and :token:`ident` is bound to the matched +value. A pattern of the form :n:`@pattern | @pattern` is called disjunctive. A +list of patterns separated with commas is also considered as a pattern +and is called *multiple pattern*. However multiple patterns can only +occur at the root of pattern matching equations. Disjunctions of +*multiple patterns* are allowed though. + +Since extended ``match`` expressions are compiled into the primitive ones, +the expressiveness of the theory remains the same. Once parsing has finished +only simple patterns remain. The original nesting of the ``match`` expressions +is recovered at printing time. An easy way to see the result +of the expansion is to toggle off the nesting performed at printing +(use here :flag:`Printing Matching`), then by printing the term with :cmd:`Print` +if the term is a constant, or using the command :cmd:`Check`. + +The extended ``match`` still accepts an optional *elimination predicate* +given after the keyword ``return``. Given a pattern matching expression, +if all the right-hand-sides of ``=>`` have the same +type, then this type can be sometimes synthesized, and so we can omit +the return part. Otherwise the predicate after return has to be +provided, like for the basicmatch. + +Let us illustrate through examples the different aspects of extended +pattern matching. Consider for example the function that computes the +maximum of two natural numbers. We can write it in primitive syntax +by: + +.. coqtop:: in + + Fixpoint max (n m:nat) {struct m} : nat := + match n with + | O => m + | S n' => match m with + | O => S n' + | S m' => S (max n' m') + end + end. + +.. _multiple-patterns: + +Multiple patterns +----------------- + +Using multiple patterns in the definition of ``max`` lets us write: + +.. coqtop:: in reset + + Fixpoint max (n m:nat) {struct m} : nat := + match n, m with + | O, _ => m + | S n', O => S n' + | S n', S m' => S (max n' m') + end. + +which will be compiled into the previous form. + +The pattern matching compilation strategy examines patterns from left +to right. A match expression is generated **only** when there is at least +one constructor in the column of patterns. E.g. the following example +does not build a match expression. + +.. coqtop:: all + + Check (fun x:nat => match x return nat with + | y => y + end). + + +Aliasing subpatterns +-------------------- + +We can also use :n:`as @ident` to associate a name to a sub-pattern: + +.. coqtop:: in reset + + Fixpoint max (n m:nat) {struct n} : nat := + match n, m with + | O, _ => m + | S n' as p, O => p + | S n', S m' => S (max n' m') + end. + +.. _nested-patterns: + +Nested patterns +--------------- + +Here is now an example of nested patterns: + +.. coqtop:: in + + Fixpoint even (n:nat) : bool := + match n with + | O => true + | S O => false + | S (S n') => even n' + end. + +This is compiled into: + +.. coqtop:: all + + Unset Printing Matching. + Print even. + +.. coqtop:: none + + Set Printing Matching. + +In the previous examples patterns do not conflict with, but sometimes +it is comfortable to write patterns that admit a non trivial +superposition. Consider the boolean function :g:`lef` that given two +natural numbers yields :g:`true` if the first one is less or equal than the +second one and :g:`false` otherwise. We can write it as follows: + +.. coqtop:: in + + Fixpoint lef (n m:nat) {struct m} : bool := + match n, m with + | O, x => true + | x, O => false + | S n, S m => lef n m + end. + +Note that the first and the second multiple pattern overlap because +the couple of values ``O O`` matches both. Thus, what is the result of the +function on those values? To eliminate ambiguity we use the *textual +priority rule:* we consider patterns to be ordered from top to bottom. A +value is matched by the pattern at the ith row if and only if it is +not matched by some pattern from a previous row. Thus in the example, ``O O`` +is matched by the first pattern, and so :g:`(lef O O)` yields true. + +Another way to write this function is: + +.. coqtop:: in reset + + Fixpoint lef (n m:nat) {struct m} : bool := + match n, m with + | O, x => true + | S n, S m => lef n m + | _, _ => false + end. + +Here the last pattern superposes with the first two. Because of the +priority rule, the last pattern will be used only for values that do +not match neither the first nor the second one. + +Terms with useless patterns are not accepted by the system. Here is an +example: + +.. coqtop:: all + + Fail Check (fun x:nat => + match x with + | O => true + | S _ => false + | x => true + end). + + +Disjunctive patterns +-------------------- + +Multiple patterns that share the same right-hand-side can be +factorized using the notation :n:`{+| {+, @pattern } }`. For +instance, :g:`max` can be rewritten as follows: + +.. coqtop:: in reset + + Fixpoint max (n m:nat) {struct m} : nat := + match n, m with + | S n', S m' => S (max n' m') + | 0, p | p, 0 => p + end. + +Similarly, factorization of (not necessarily multiple) patterns that +share the same variables is possible by using the notation :n:`{+| @pattern}`. +Here is an example: + +.. coqtop:: in + + Definition filter_2_4 (n:nat) : nat := + match n with + | 2 as m | 4 as m => m + | _ => 0 + end. + + +Nested disjunctive patterns are allowed, inside parentheses, with the +notation :n:`({+| @pattern})`, as in: + +.. coqtop:: in + + Definition filter_some_square_corners (p:nat*nat) : nat*nat := + match p with + | ((2 as m | 4 as m), (3 as n | 5 as n)) => (m,n) + | _ => (0,0) + end. + +About patterns of parametric types +---------------------------------- + +Parameters in patterns +~~~~~~~~~~~~~~~~~~~~~~ + +When matching objects of a parametric type, parameters do not bind in +patterns. They must be substituted by “``_``”. Consider for example the +type of polymorphic lists: + +.. coqtop:: in + + Inductive List (A:Set) : Set := + | nil : List A + | cons : A -> List A -> List A. + +We can check the function *tail*: + +.. coqtop:: all + + Check + (fun l:List nat => + match l with + | nil _ => nil nat + | cons _ _ l' => l' + end). + +When we use parameters in patterns there is an error message: + +.. coqtop:: all + + Fail Check + (fun l:List nat => + match l with + | nil A => nil nat + | cons A _ l' => l' + end). + +.. flag:: Asymmetric Patterns + + This flag (off by default) removes parameters from constructors in patterns: + +.. coqtop:: all + + Set Asymmetric Patterns. + Check (fun l:List nat => + match l with + | nil => nil _ + | cons _ l' => l' + end). + Unset Asymmetric Patterns. + +Implicit arguments in patterns +------------------------------ + +By default, implicit arguments are omitted in patterns. So we write: + +.. coqtop:: all + + Arguments nil {A}. + Arguments cons [A] _ _. + Check + (fun l:List nat => + match l with + | nil => nil + | cons _ l' => l' + end). + +But the possibility to use all the arguments is given by “``@``” implicit +explicitations (as for terms, see :ref:`explicit-applications`). + +.. coqtop:: all + + Check + (fun l:List nat => + match l with + | @nil _ => @nil nat + | @cons _ _ l' => l' + end). + + +.. _matching-dependent: + +Matching objects of dependent types +----------------------------------- + +The previous examples illustrate pattern matching on objects of non- +dependent types, but we can also use the expansion strategy to +destructure objects of dependent types. Consider the type :g:`listn` of +lists of a certain length: + +.. coqtop:: in reset + + Inductive listn : nat -> Set := + | niln : listn 0 + | consn : forall n:nat, nat -> listn n -> listn (S n). + + +Understanding dependencies in patterns +-------------------------------------- + +We can define the function length over :g:`listn` by: + +.. coqdoc:: + + Definition length (n:nat) (l:listn n) := n. + +Just for illustrating pattern matching, we can define it by case +analysis: + +.. coqtop:: in + + Definition length (n:nat) (l:listn n) := + match l with + | niln => 0 + | consn n _ _ => S n + end. + +We can understand the meaning of this definition using the same +notions of usual pattern matching. + + +When the elimination predicate must be provided +----------------------------------------------- + +Dependent pattern matching +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The examples given so far do not need an explicit elimination +predicate because all the |rhs| have the same type and Coq +succeeds to synthesize it. Unfortunately when dealing with dependent +patterns it often happens that we need to write cases where the types +of the |rhs| are different instances of the elimination predicate. The +function :g:`concat` for :g:`listn` is an example where the branches have +different types and we need to provide the elimination predicate: + +.. coqtop:: in + + Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : + listn (n + m) := + match l in listn n return listn (n + m) with + | niln => l' + | consn n' a y => consn (n' + m) a (concat n' y m l') + end. + +.. coqtop:: none + + Reset concat. + +The elimination predicate is :g:`fun (n:nat) (l:listn n) => listn (n+m)`. +In general if :g:`m` has type :g:`(I q1 … qr t1 … ts)` where :g:`q1, …, qr` +are parameters, the elimination predicate should be of the form :g:`fun y1 … ys x : (I q1 … qr y1 … ys ) => Q`. + +In the concrete syntax, it should be written : +``match m as x in (I _ … _ y1 … ys) return Q with … end``. +The variables which appear in the ``in`` and ``as`` clause are new and bounded +in the property :g:`Q` in the return clause. The parameters of the +inductive definitions should not be mentioned and are replaced by ``_``. + +Multiple dependent pattern matching +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Recall that a list of patterns is also a pattern. So, when we +destructure several terms at the same time and the branches have +different types we need to provide the elimination predicate for this +multiple pattern. It is done using the same scheme: each term may be +associated to an ``as`` clause and an ``in`` clause in order to introduce +a dependent product. + +For example, an equivalent definition for :g:`concat` (even though the +matching on the second term is trivial) would have been: + +.. coqtop:: in + + Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : + listn (n + m) := + match l in listn n, l' return listn (n + m) with + | niln, x => x + | consn n' a y, x => consn (n' + m) a (concat n' y m x) + end. + +Even without real matching over the second term, this construction can +be used to keep types linked. If :g:`a` and :g:`b` are two :g:`listn` of the same +length, by writing + +.. coqtop:: in + + Check (fun n (a b: listn n) => + match a, b with + | niln, b0 => tt + | consn n' a y, bS => tt + end). + +we have a copy of :g:`b` in type :g:`listn 0` resp. :g:`listn (S n')`. + +.. _match-in-patterns: + +Patterns in ``in`` +~~~~~~~~~~~~~~~~~~ + +If the type of the matched term is more precise than an inductive +applied to variables, arguments of the inductive in the ``in`` branch can +be more complicated patterns than a variable. + +Moreover, constructors whose types do not follow the same pattern will +become impossible branches. In an impossible branch, you can answer +anything but False_rect unit has the advantage to be subterm of +anything. + +To be concrete: the ``tail`` function can be written: + +.. coqtop:: in + + Definition tail n (v: listn (S n)) := + match v in listn (S m) return listn m with + | niln => False_rect unit + | consn n' a y => y + end. + +and :g:`tail n v` will be subterm of :g:`v`. + +Using pattern matching to write proofs +-------------------------------------- + +In all the previous examples the elimination predicate does not depend +on the object(s) matched. But it may depend and the typical case is +when we write a proof by induction or a function that yields an object +of a dependent type. An example of a proof written using ``match`` is given +in the description of the tactic :tacn:`refine`. + +For example, we can write the function :g:`buildlist` that given a natural +number :g:`n` builds a list of length :g:`n` containing zeros as follows: + +.. coqtop:: in + + Fixpoint buildlist (n:nat) : listn n := + match n return listn n with + | O => niln + | S n => consn n 0 (buildlist n) + end. + +We can also use multiple patterns. Consider the following definition +of the predicate less-equal :g:`Le`: + +.. coqtop:: in + + Inductive LE : nat -> nat -> Prop := + | LEO : forall n:nat, LE 0 n + | LES : forall n m:nat, LE n m -> LE (S n) (S m). + +We can use multiple patterns to write the proof of the lemma +:g:`forall (n m:nat), (LE n m) \/ (LE m n)`: + +.. coqtop:: in + + Fixpoint dec (n m:nat) {struct n} : LE n m \/ LE m n := + match n, m return LE n m \/ LE m n with + | O, x => or_introl (LE x 0) (LEO x) + | x, O => or_intror (LE x 0) (LEO x) + | S n as n', S m as m' => + match dec n m with + | or_introl h => or_introl (LE m' n') (LES n m h) + | or_intror h => or_intror (LE n' m') (LES m n h) + end + end. + +In the example of :g:`dec`, the first match is dependent while the second +is not. + +The user can also use match in combination with the tactic :tacn:`refine` +to build incomplete proofs beginning with a :g:`match` construction. + + +Pattern-matching on inductive objects involving local definitions +----------------------------------------------------------------- + +If local definitions occur in the type of a constructor, then there +are two ways to match on this constructor. Either the local +definitions are skipped and matching is done only on the true +arguments of the constructors, or the bindings for local definitions +can also be caught in the matching. + +.. example:: + + .. coqtop:: in reset + + Inductive list : nat -> Set := + | nil : list 0 + | cons : forall n:nat, let m := (2 * n) in list m -> list (S (S m)). + + In the next example, the local definition is not caught. + + .. coqtop:: in + + Fixpoint length n (l:list n) {struct l} : nat := + match l with + | nil => 0 + | cons n l0 => S (length (2 * n) l0) + end. + + But in this example, it is. + + .. coqtop:: in + + Fixpoint length' n (l:list n) {struct l} : nat := + match l with + | nil => 0 + | @cons _ m l0 => S (length' m l0) + end. + +.. note:: For a given matching clause, either none of the local + definitions or all of them can be caught. + +.. note:: You can only catch let bindings in mode where you bind all + variables and so you have to use ``@`` syntax. + +.. note:: this feature is incoherent with the fact that parameters + cannot be caught and consequently is somehow hidden. For example, + there is no mention of it in error messages. + +Pattern-matching and coercions +------------------------------ + +If a mismatch occurs between the expected type of a pattern and its +actual type, a coercion made from constructors is sought. If such a +coercion can be found, it is automatically inserted around the +pattern. + +.. example:: + + .. coqtop:: in + + Inductive I : Set := + | C1 : nat -> I + | C2 : I -> I. + + Coercion C1 : nat >-> I. + + .. coqtop:: all + + Check (fun x => match x with + | C2 O => 0 + | _ => 0 + end). + + +When does the expansion strategy fail? +-------------------------------------- + +The strategy works very like in ML languages when treating patterns of +non-dependent types. But there are new cases of failure that are due to +the presence of dependencies. + +The error messages of the current implementation may be sometimes +confusing. When the tactic fails because patterns are somehow +incorrect then error messages refer to the initial expression. But the +strategy may succeed to build an expression whose sub-expressions are +well typed when the whole expression is not. In this situation the +message makes reference to the expanded expression. We encourage +users, when they have patterns with the same outer constructor in +different equations, to name the variable patterns in the same +positions with the same name. E.g. to write ``(cons n O x) => e1`` and +``(cons n _ x) => e2`` instead of ``(cons n O x) => e1`` and +``(cons n' _ x') => e2``. This helps to maintain certain name correspondence between the +generated expression and the original. + +Here is a summary of the error messages corresponding to each +situation: + +.. exn:: The constructor @ident expects @num arguments. + + The variable ident is bound several times in pattern termFound a constructor + of inductive type term while a constructor of term is expectedPatterns are + incorrect (because constructors are not applied to the correct number of the + arguments, because they are not linear or they are wrongly typed). + +.. exn:: Non exhaustive pattern matching. + + The pattern matching is not exhaustive. + +.. exn:: The elimination predicate term should be of arity @num (for non \ + dependent case) or @num (for dependent case). + + The elimination predicate provided to match has not the expected arity. + +.. exn:: Unable to infer a match predicate + Either there is a type incompatibility or the problem involves dependencies. + + There is a type mismatch between the different branches. The user should + provide an elimination predicate. |