2.2 Variants and extensions of Cases
2.2.1 ML-style pattern-matching
The basic version ofCases allows pattern-matching on simple
patterns. As an extension, multiple and nested patterns are
allowed, as in ML-like languages.The extension just acts as a macro that is expanded during parsing into a sequence of Cases on simple patterns. Especially, a construction defined using the extended Cases is printed under its expanded form.
The syntax of the extended Cases is presented in figure 2.2. Note the annotation is mandatory when the sequence of equation is empty.
nested_pattern := ident | _ | ( ident nested_pattern ... nested_pattern ) | ( nested_pattern as ident ) | ( nested_pattern , nested_pattern ) | ( nested_pattern )
mult_pattern:= nested_pattern ... nested_pattern
ext_eqn:= mult_pattern => term
term:= [annotation] Cases term ... term of [ext_eqn | ... | ext_eqn] end
Figure 2.2:extended Cases syntax.
See also: chapter 13.
2.2.2 Pattern-matching on boolean values: the if expression
For inductive types isomorphic to the boolean types (i.e. two constructors without arguments), it is possible to use a if ... then ... else notation. This enriches the syntax of terms as follows:| term | := | [annotation] if term then term else term |
For instance, the definition
Coq < Definition not := [b:bool] Cases b of true => false | false => true end.not is defined
can be alternatively written
Coq < Definition not := [b:bool] if b then false else true.not is defined
2.2.3 Irrefutable patterns: the destructuring let
Terms in an inductive type having only one constructor, say foo, have necessarily the form (foo ...). In this case, the Cases construction can be replaced by a let ... in ... construction. This enriches the syntax of terms as follows:| | | [annotation] let ( ident , ... , ident ) = term in term |
For instance, the definition
Coq < Definition fst := [A,B:Set][H:A*B] Cases H of (pair x y) => x end.fst is defined
can be alternatively written
Coq < Definition fst := [A,B:Set][p:A*B] let (x,_) = p in x.fst is defined
The pretty-printing of a definition by cases on a irrefutable pattern can either be done using Cases or the let construction (see section 2.2.4).
2.2.4 Options for pretty-printing of Cases
There are three options controlling the pretty-printing of Cases expressions.Printing of wildcard pattern
Some variables in a pattern may not occur in the right-hand side of the pattern-matching clause. There are options to control the display of these variables.Set Printing Wildcard.
The variables having no occurrences in the right-hand side of the pattern-matching clause are just printed using the wildcard symbol ``_''.Unset Printing Wildcard.
The variables, even useless, are printed using their usual name. But some non dependent variables have no name. These ones are still printed using a ``_''.Print Printing Wildcard.
This tells if the wildcard printing mode is on or off. The default is to print wildcard for useless variables.Printing of the elimination predicate
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.Set Printing Synth.
The result type is not printed when it is easily synthesizable.Unset Printing Synth.
This forces the result type to be always printed (and then between angle brackets).Print Printing Synth.
This tells if the non-printing of synthesizable types is on or off. The default is to not print synthesizable types.Printing matching on irrefutable pattern
If an inductive type has just one constructor, pattern-matching can be written using let ... = ... in ...Add Printing Let ident.
This adds ident to the list of inductive types for which pattern-matching is written using a let expression.Remove Printing Let ident.
This removes ident from this list.Test Printing Let ident.
This tells if ident belongs to the list.Print Printing Let.
This prints the list of inductive types for which pattern-matching is written using a let expression.The table of inductive types for which pattern-matching is written using a let expression is managed synchronously. This means that it is sensible to the command Reset.
Printing matching on booleans
If an inductive type is isomorphic to the boolean type, pattern-matching can be written using if ... then ... else ...Add Printing If ident.
This adds ident to the list of inductive types for which pattern-matching is written using an if expression.Remove Printing If ident.
This removes ident from this list.Test Printing If ident.
This tells if ident belongs to the list.Print Printing If.
This prints the list of inductive types for which pattern-matching is written using an if expression.The table of inductive types for which pattern-matching is written using an if expression is managed synchronously. This means that it is sensible to the command Reset.
Example
This example emphasizes what the printing options offer.Coq < Test Printing Let prod.Cases on elements of prod are printed using a `let' form
Coq < Print fst.fst = [A,B:Set][p:A*B]let (x, _) = p in x
: (A,B:Set)A*B->A
Coq < Remove Printing Let prod.Coq < Unset Printing Synth.Coq < Unset Printing Wildcard.Coq < Print snd.snd =
[A:Set][B:Set][p:A*B]<B>Cases p of (pair x y) => y end
: (A,B:Set)A*B->B
2.2.5 Still not dead old notations
The following variant of Cases is inherited from older version of Coq.| term | ::= | annotation Match term with terms end |
This syntax is a macro generating a combination of Cases with Fix implementing a combinator for primitive recursion equivalent to the Match construction of Coq V5.8. It is provided only for sake of compatibility with Coq V5.8. It is recommended to avoid it. (see section 4.5.5).
There is also a notation Case that is the ancestor of Cases. Again, it is still in the code for compatibility with old versions but the user should not use it.