Variants and the match construct¶
Variants¶
-
Command
Variant variant_definition with variant_definition*¶ The
Variantcommand is similar to theInductivecommand, except that it disallows recursive definition of types (for instance, lists cannot be defined usingVariant). No induction scheme is generated for this variant, unless theNonrecursive Elimination Schemesflag is on.This command supports the
universes(polymorphic),universes(template),universes(cumulative), andprivate(matching)attributes.
Private (matching) inductive types¶
-
Attribute
private(matching)¶ This attribute can be used to forbid the use of the
matchconstruct on objects of this inductive type outside of the module where it is defined. There is also a legacy syntax using thePrivateprefix (cf.legacy_attr).The main use case of private (matching) inductive types is to emulate quotient types / higher-order inductive types in projects such as the HoTT library.
Example
- Module Foo.
- Interactive Module Foo started
- #[ private(matching) ] Inductive my_nat := my_O : my_nat | my_S : my_nat -> my_nat.
- my_nat is defined
- Check (fun x : my_nat => match x with my_O => true | my_S _ => false end).
- fun x : my_nat => match x with | my_O => true | my_S _ => false end : my_nat -> bool
- End Foo.
- Module Foo is defined
- Import Foo.
- Fail Check (fun x : my_nat => match x with my_O => true | my_S _ => false end).
- The command has indeed failed with message: case analysis on a private type.
Definition by cases: match¶
Objects of inductive types can be destructured by a case-analysis construction called pattern matching expression. A pattern matching expression is used to analyze the structure of an inductive object and to apply specific treatments accordingly.
Note that the pattern ::= pattern10 : term production
is not supported in match patterns. Trying to use it will give this error:
-
Error
Casts are not supported in this pattern.¶
This paragraph describes the basic form of pattern matching. See
Section Multiple and nested pattern matching and Chapter Extended pattern matching for the description
of the general form. The basic form of pattern matching is characterized
by a single case_item expression, an eqn restricted to a
single pattern and pattern restricted to the form
qualid ident*.
The expression
match term return term100? with patterni => termi+| end denotes a
pattern matching over the term term (expected to be
of an inductive type \(I\)). The termi
are the branches of the pattern matching
expression. Each patterni has the form qualid ident
where qualid must denote a constructor. There should be
exactly one branch for every constructor of \(I\).
The return term100 clause gives the type returned by the whole match
expression. There are several cases. In the non dependent case, all
branches have the same type, and the return term100 specifies that type.
In this case, return term100 can usually be omitted as it can be
inferred from the type of the branches 1.
In the dependent case, there are three subcases. In the first subcase,
the type in each branch may depend on the exact value being matched in
the branch. In this case, the whole pattern matching itself depends on
the term being matched. This dependency of the term being matched in the
return type is expressed with an ident clause where ident
is dependent in the return type. For instance, in the following example:
- Inductive bool : Type := true : bool | false : bool.
- bool is defined bool_rect is defined bool_ind is defined bool_rec is defined bool_sind is defined
- Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : eq A x x.
- eq is defined eq_rect is defined eq_ind is defined eq_rec is defined eq_sind is defined
- Inductive or (A:Prop) (B:Prop) : Prop := | or_introl : A -> or A B | or_intror : B -> or A B.
- or is defined or_ind is defined or_sind is defined
- Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := match b as x return or (eq bool x true) (eq bool x false) with | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true) | false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false) end.
- bool_case is defined
the branches have respective types "or (eq bool true true) (eq bool true false)"
and "or (eq bool false true) (eq bool false false)" while the whole
pattern matching expression has type "or (eq bool b true) (eq bool b false)",
the identifier b being used to represent the dependency.
Note
When the term being matched is a variable, the as clause can be
omitted and the term being matched can serve itself as binding name in
the return type. For instance, the following alternative definition is
accepted and has the same meaning as the previous one.
- Reset bool_case.
- Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := match b return or (eq bool b true) (eq bool b false) with | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true) | false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false) end.
- bool_case is defined
The second subcase is only relevant for annotated inductive types such
as the equality predicate (see Section Equality),
the order predicate on natural numbers or the type of lists of a given
length (see Section Matching objects of dependent types). In this configuration, the
type of each branch can depend on the type dependencies specific to the
branch and the whole pattern matching expression has a type determined
by the specific dependencies in the type of the term being matched. This
dependency of the return type in the annotations of the inductive type
is expressed with a clause in the form
in qualid _+ pattern+, where
qualidis the inductive type of the term being matched;the holes
_match the parameters of the inductive type: the return type is not dependent on them.each
patternmatches the annotations of the inductive type: the return type is dependent on themin the basic case which we describe below, each
patternis a nameident; see Patterns in in for the general case
For instance, in the following example:
- Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x := match H in eq _ _ z return eq A z x with | eq_refl _ _ => eq_refl A x end.
- eq_sym is defined
the type of the branch is eq A x x because the third argument of
eq is x in the type of the pattern eq_refl. On the contrary, the
type of the whole pattern matching expression has type eq A y x because the
third argument of eq is y in the type of H. This dependency of the case analysis
in the third argument of eq is expressed by the identifier z in the
return type.
Finally, the third subcase is a combination of the first and second
subcase. In particular, it only applies to pattern matching on terms in
a type with annotations. For this third subcase, both the clauses as and
in are available.
There are specific notations for case analysis on types with one or two
constructors: if … then … else … and let (…,…) := … in … (see
Sections Pattern-matching on boolean values: the if expression and Irrefutable patterns: the destructuring let variants).
- 1
Except if the inductive type is empty in which case there is no equation that can be used to infer the return type.