\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

# Typeclasses

Typeclasses are types whose values Rocq can automatically infer by using user declared instances. It allows for a form of programmatic proof or term search.

This chapter presents a quick reference of the commands related to typeclasses. Additional helpful information can be found in the paper introducing typeclasses to Coq [SO08] and the literature on type classes in Haskell.

## Typeclass and instance declarations

The syntax for typeclasses and instance declarations is the same as the record syntax:

Class classname (p1 : t1) ⋯ (pn : tn) [: sort] := { f1 : u1 ; ⋯ ; fm : um }. Instance instancename q1 ⋯ qm : classname p1 ⋯ pn := { f1 := e1 ; ⋯ ; fm := em }.

The `pi : ti` variables are called the parameters of the typeclass and the `fi : ui` are called the methods. Each typeclass definition gives rise to a corresponding record declaration and each instance is a regular definition whose name is given by `instancename` and type is an instantiation of the record type.

We’ll use the following example typeclass in the rest of the chapter:

Class EqDec (A : Type) := { eqb : A -> A -> bool ; eqb_leibniz : forall x y, eqb x y = true -> x = y }.
  EqDec is defined eqb is defined eqb_leibniz is defined

This typeclass implements a boolean equality test which is compatible with Leibniz equality on some type. An example implementation is:

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 }.
  unit_EqDec is defined

Using the `refine` attribute, if the term is not sufficient to finish the definition (e.g. due to a missing field or non-inferable hole) it must be finished in proof mode. If it is sufficient a trivial proof mode with no open goals is started.

#[refine] Instance unit_EqDec' : EqDec unit := { eqb x y := true }.
  1 goal ============================ forall x y : unit, true = true -> x = y
Proof. intros [] [];reflexivity. Defined.
  No more goals.

Note that if you finish the proof with `Qed` the entire instance will be opaque, including the fields given in the initial term.

Alternatively, in `Program Mode` if one does not give all the members in the Instance declaration, Rocq generates obligations for the remaining fields, e.g.:

Require Import Program.Tactics.
Program Instance eq_bool : EqDec bool := { eqb x y := if x then y else negb y }.
  eq_bool has type-checked, generating 1 obligation Solving obligations automatically... 1 obligation remaining Obligation 1 of eq_bool: (forall x y : bool, (fun x0 y0 : bool => if x0 then y0 else negb y0) x y = true -> x = y).

Next Obligation.
  1 goal x, y : bool H : (if x then y else negb y) = true ============================ x = y
destruct x ; destruct y ; (discriminate || reflexivity).
  No more goals.
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` attribute to get richer facilities for dealing with obligations.

## Binding typeclasses

Once a typeclass is declared, one can use it in typeclass binders:

Definition neqb {A} {eqa : EqDec A} (x y : A) := negb (eqb x y).
  neqb is defined

When one calls a typeclass 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:

Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
  The command has indeed failed with message: The following term contains unresolved implicit arguments: (fun (A : Type) (x y : A) => negb (eqb x y)) More precisely: - ?EqDec: Cannot infer the implicit parameter EqDec of eqb whose type is "EqDec A" (no type class instance found) in environment: A : Type x, y : A

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:

Definition neqb' A (eqa : EqDec A) (x y : A) := negb (eqb x y).
  neqb' is defined

However, the generalizing binders should be used instead as they have particular support for typeclasses:

- They automatically set the maximally implicit status for typeclass arguments, making derived functions as easy to use as typeclass methods. In the example above, `A` and `eqa` should be set maximally implicit.

- They support implicit quantification on partially applied typeclasses (Implicit generalization). Any argument not given as part of a typeclass binder will be automatically generalized.

- They also support implicit quantification on Superclasses.

Following the previous example, one can write:

Generalizable Variables A B C.
Definition neqb_implicit `{eqa : EqDec A} (x y : A) := negb (eqb x y).
  neqb_implicit is defined

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.:

Program Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := { eqb x y := match x, y with | (la, lb), (ra, rb) => andb (eqb la ra) (eqb lb rb) end }.
  prod_eqb has type-checked, generating 1 obligation Solving obligations automatically... 1 obligation remaining Obligation 1 of prod_eqb: (forall (A : Type) (EA : EqDec A) (B : Type) (EB : EqDec B) (x y : A * B), (fun x0 y0 : A * B => let program_branch_0 := fun (la : A) (lb : B) (ra : A) (rb : B) (_ : (la, lb) = x0) (_ : (ra, rb) = y0) => (eqb la ra && eqb lb rb)%bool in (let (la, lb) as x' return x' = x0 -> y0 = y0 -> bool := x0 in let (ra, rb) as y' return (la, lb) = x0 -> y' = y0 -> bool := y0 in program_branch_0 la lb ra rb) eq_refl eq_refl) x y = true -> x = y).

Admit Obligations.
  prod_eqb_obligation_1 is declared No more obligations remaining prod_eqb is defined

These instances are used just as well as lemmas in the instance hint database.

## Sections and contexts

To ease developments parameterized by many instances, one can use the `Context` command to introduce the parameters into the local context, which works similarly to the command `Variable`, except it accepts any binding context as an argument, so variables can be implicit, and Implicit generalization can be used. For example:

Section EqDec_defs.
Context `{EA : EqDec A}.
  A is declared EA is declared

#[ global, program ] Instance option_eqb : EqDec (option A) := { eqb x y := match x, y with | Some x, Some y => eqb x y | None, None => true | _, _ => false end }.
  option_eqb has type-checked, generating 3 obligations Solving obligations automatically... 3 obligations remaining Obligation 1 of option_eqb: (forall x y : option A, let program_branch_0 := fun (x0 y0 : A) (_ : Some x0 = x) (_ : Some y0 = y) => eqb x0 y0 in let program_branch_1 := fun (_ : None = x) (_ : None = y) => true in let program_branch_2 := fun (wildcard' wildcard'0 : option A) (_ : ~ (None = wildcard' /\ None = wildcard'0) /\ (forall x0 y0 : A, ~ (Some x0 = wildcard' /\ Some y0 = wildcard'0))) (_ : wildcard' = x) (_ : wildcard'0 = y) => false in forall a : A, let wildcard' := Some a in let wildcard'0 := None in ~ (None = wildcard' /\ None = wildcard'0) /\ (forall x0 y0 : A, ~ (Some x0 = wildcard' /\ Some y0 = wildcard'0))). Obligation 2 of option_eqb: (forall x y : option A, let program_branch_0 := fun (x0 y0 : A) (_ : Some x0 = x) (_ : Some y0 = y) => eqb x0 y0 in let program_branch_1 := fun (_ : None = x) (_ : None = y) => true in let program_branch_2 := fun (wildcard' wildcard'0 : option A) (_ : ~ (None = wildcard' /\ None = wildcard'0) /\ (forall x0 y0 : A, ~ (Some x0 = wildcard' /\ Some y0 = wildcard'0))) (_ : wildcard' = x) (_ : wildcard'0 = y) => false in let wildcard' := None in forall a : A, let wildcard'0 := Some a in ~ (None = wildcard' /\ None = wildcard'0) /\ (forall x0 y0 : A, ~ (Some x0 = wildcard' /\ Some y0 = wildcard'0))). Obligation 3 of option_eqb: (forall x y : option A, (fun x0 y0 : option A => let program_branch_0 := fun (x1 y1 : A) (_ : Some x1 = x0) (_ : Some y1 = y0) => eqb x1 y1 in let program_branch_1 := fun (_ : None = x0) (_ : None = y0) => true in let program_branch_2 := fun (wildcard' wildcard'0 : option A) (_ : ~ (None = wildcard' /\ None = wildcard'0) /\ (forall x1 y1 : A, ~ (Some x1 = wildcard' /\ Some y1 = wildcard'0))) (_ : wildcard' = x0) (_ : wildcard'0 = y0) => false in match x0 as x' return x' = x0 -> y0 = y0 -> bool with | Some x1 => match y0 as y' return Some x1 = x0 -> y' = y0 -> bool with | Some y1 => program_branch_0 x1 y1 | None => program_branch_2 (Some x1) None (option_eqb_obligation_1 x0 y0 x1) end | None => match y0 as y' return None = x0 -> y' = y0 -> bool with | Some a => program_branch_2 None (Some a) (option_eqb_obligation_2 x0 y0 a) | None => program_branch_1 end end eq_refl eq_refl) x y = true -> x = y).
Admit Obligations.
  option_eqb_obligation_1 is declared 2 obligations remaining Solving obligations automatically... 2 obligations remaining option_eqb_obligation_2 is declared 1 obligation remaining Solving obligations automatically... 1 obligation remaining option_eqb_obligation_3 is declared No more obligations remaining option_eqb is defined

End EqDec_defs.
About option_eqb.
  option_eqb : forall {A : Type}, EqDec A -> EqDec (option A) option_eqb is not universe polymorphic Arguments option_eqb {A}%_type_scope {EA} option_eqb is transparent Expands to: Constant Top.option_eqb Declared in toplevel input, characters 1213-1223

Here the `global` attribute redeclares the instance at the end of the section, once it has been generalized by the context variables it uses.

See also

Section Sections

## Building hierarchies

### Superclasses

One can also parameterize typeclasses by other typeclasses, generating a hierarchy of typeclasses and superclasses. In the same way, we give the superclasses as a binding context:

Class Ord `(E : EqDec A) := { le : A -> A -> bool }.
  Ord is defined le is defined

Contrary to Haskell, we have no special syntax for superclasses, but this declaration is equivalent to:

Class `(E : EqDec A) => Ord A := { le : A -> A -> bool }.

This declaration means that any instance of the `Ord` typeclass 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.

Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x).
  le_eqb is defined

To specify sharing of structures, you may want to explicitly specify the superclasses. You can do this directly in regular binders, and with the `!` modifier before typeclass binders. For example:

Definition lt `{eqa : EqDec A, !Ord eqa} (x y : A) := andb (le x y) (neqb x y).
  lt is defined

The `!` modifier switches how Rocq interprets a binder. In particular, it uses the implicit arguments mechanism if available, as shown in the example.

### Substructures

Substructures are components of a typeclass which are themselves instances of a typeclass. They often arise when using typeclasses for logical properties, e.g.:

Require Import Relation_Definitions.

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 typeclasses for reflexive and transitive relations, (see the singleton class variant for an explanation). These may be used as parts of other typeclasses:

Class PreOrder (A : Type) (R : relation A) := { PreOrder_Reflexive :: Reflexive A R ; PreOrder_Transitive :: Transitive A R }.
  PreOrder is defined PreOrder_Reflexive is defined PreOrder_Transitive is defined

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.

## Command summary

Command Class record_definition
Command Class ident_decl binder* : sort? := constructor

  The first form declares a record and makes the record a typeclass with parameters `binder*` and the listed record fields.

  The second form declares a singleton typeclass with a single projection. This singleton typeclass is a so-called definitional typeclass, represented simply as a definition `ident binders := term` and whose instances are themselves objects of this type.

  Definitional typeclasses are not wrapped inside records, and the trivial projection of an instance of such a typeclass 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 trivial projections. The typeclass constant itself is declared rigid during resolution so that the typeclass abstraction is maintained.

  Like any command declaring a record, this command supports the `universes(polymorphic)`, `universes(template)`, `universes(cumulative)` and `private(matching)` attributes.

  It also supports the `mode` attribute for setting a hint mode declaration for the class.

  Note

  Don't confuse typeclasses with "coercion classes", described in implicit coercions.

  When record syntax is used, this command also supports the `projections(primitive)` attribute.

  Attribute mode = string

    Sets the mode of resolution for queries on the class. The syntax to use in the quoted string is explained in `Hint Mode`.

  Command Existing Class qualid

    Declares a typeclass from a previously declared constant or inductive definition. No methods or instances are defined.

    Warning ident is already declared as a typeclass

      This command has no effect when used on a typeclass.

  Warning Ignored instance declaration for “ident”: “term” is not a class

    Using the `::` syntax in the `record_definition` or `constructor` with a right-hand-side that is not itself a Class has no effect (apart from emitting this warning).

Command Instance ident_decl binder*? : type hint_info? := { field_val* }​:= term?

  Declares a typeclass instance named `ident_decl` of the typeclass `type` with the specified parameters and with fields defined by `field_val`, where each field must be a declared field of the typeclass.

  Adds one or more `binder`s to declare a parameterized instance. `hint_info` may be used to specify the hint priority. If the priority is not specified, the default is the number of non-dependent binders of the instance. If `one_pattern` is given, terms matching that pattern will trigger use of the instance. Otherwise, use is triggered based on the conclusion of the type.

  This command supports the `local`, `global` and `export` locality attributes.

  Changed in version 8.18: The default value for instance locality outside sections is now `export`. It used to be `global`.

  Like `Definition`, it also supports the `program` attribute to switch the type checking to `Program` (chapter Program) and to use the obligation mechanism to manage missing fields.

  Finally, it supports the lighter `refine` attribute:

  Attribute refine

    This attribute can be used to leave holes or not provide all fields in the definition of an instance and open the tactic mode to fill them. It works exactly as if no body had been given and the `refine` tactic has been used first.

  Command Declare Instance ident_decl binder* : term hint_info?

    In a `Module Type`, declares that a corresponding concrete instance should exist in any implementation of this `Module Type`. This is similar to the distinction between `Parameter` vs. `Definition`, or between `Declare Module` and `Module`.

  Command Existing Instance qualid hint_info?
  Command Existing Instances qualid+ | natural?

    Adds a constant whose type ends with an applied typeclass to the instance database with an optional priority `natural`. 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`.

Command Print Instances reference

  Shows the list of instances associated with the typeclass `reference`.

Command Print Typeclasses

  Shows the list of declared typeclasses.

Tactic typeclasses eauto bfs​dfs​best_effort? nat_or_var? with ident+?

  This proof search tactic uses the resolution engine that is run implicitly during type checking, known as typeclass search. This tactic uses a different resolution engine than `eauto` and `auto`. The main differences are the following:

  - Unlike `eauto` and `auto`, the resolution is done entirely in the proof engine, 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.

  - The transparency information of databases is used consistently for all hints declared in them. It is always used when calling the unifier. When considering local hypotheses, we use the transparent state of the first hint database given. Using an empty database (created with `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.

  - The mode hints (see `Hint Mode`) associated with a typeclass are taken into account by `typeclasses eauto`. When a goal does not match any of the declared modes for its head (if any), instead of failing like `eauto`, the goal is suspended and resolution proceeds on the remaining goals. If after one run of resolution, there remain suspended goals, resolution is launched again on them, until it reaches a fixed point when the set of remaining suspended goals does not change. Using `solve [typeclasses eauto]` can be used to ensure that no suspended goals remain.

  - When considering local hypotheses, we use the union of all the modes declared in the given databases.

  - The tactic may produce more than one success when used in backtracking tactics such as `typeclasses eauto; ...`. See `ltac-seq`.

  - Use the `Typeclasses eauto` command to customize the behavior of this tactic.

  `bfs​dfs`

    Specifies whether to use breadth-first search or depth-first search. The default is depth-first search, which can be changed with the `Typeclasses Iterative Deepening` flag.

  `best_effort`

    If the `best_effort` option is given and resolution fails, `typeclasses eauto` returns the first partial solution in which all remaining subgoals fall into one of these categories:

    - Stuck goals: the head of the goal has at least one associated declared mode and the constraint does not match any mode declared for its head. These goals are shelved.

    - Mode failures: the head of the constraint has at least one matching declared mode, but the constraint couldn't be solved. These goals are left as subgoals of `typeclasses eauto best_effort`.

    During type inference, typeclass resolution always uses the `best_effort` option: in case of failure, it constructs a partial solution for the goals and gives a more informative error message. It can be used the same way in interactive proofs to check which instances/hints are missing for a typeclass resolution to succeed.

  `nat_or_var`

    Specifies the maximum depth of the search.

    > Warning

    > The semantics for the limit `nat_or_var` are different than for `auto`. By default, if no limit is given, the search is unbounded. Unlike `auto`, introduction steps count against the limit, which might result in larger limits being necessary when searching with `typeclasses eauto` than with `auto`.

  `with ident+`

    Runs resolution with the specified hint databases. It treats typeclass subgoals the same as other subgoals (no shelving of non-typeclass goals in particular), while allowing shelved goals to remain at any point during search.

    When `with` is not specified, `typeclasses eauto` uses the `typeclass_instances` database by default. (If `with` is provided, you must explicitly specify `typeclass_instances` to use it.) Unlike `auto` and `eauto`, `core` is not automatically included. Dependent subgoals are automatically shelved, and shelved goals can remain after resolution ends (following the behavior of Coq 8.5).

    Note

    `all:once (typeclasses eauto)` faithfully mimics what happens during typeclass resolution when it is called during refinement/type inference, except that only declared typeclass subgoals are considered at the start of resolution during type inference, while `all` can select non-typeclass subgoals as well. It might move to `all:typeclasses eauto` in future versions when the refinement engine will be able to backtrack.

Tactic autoapply one_term with ident

  The tactic `autoapply` applies `one_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 typeclass resolution locally at hint application time.

### Typeclasses Transparent, Typeclasses Opaque

Command Typeclasses Transparent qualid+

  Makes `qualid` transparent during typeclass resolution. A shortcut for `Hint Transparent` `qualid+ : typeclass_instances`

Command Typeclasses Opaque qualid+

  Make `qualid` opaque for typeclass search. A shortcut for `Hint Opaque` `qualid+ : typeclass_instances`.

  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 Hint databases).

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:

Definition relation A := A -> A -> Prop.

Added in version 8.15: `Typeclasses Transparent` and `Typeclasses Opaque` support locality attributes like `Hint` commands.

Deprecated since version 8.15: The default value for typeclass transparency hints will change in a future release. Hints added outside of sections without an explicit locality are now deprecated. We recommend using `export` where possible.

### Settings

Option Typeclasses Default Mode "+"​"-"​"!".

  Sets the default mode declaration associated with a `Class` or `Existing Class` declaration. It is set by default to "-", i.e. doing no mode filtering by default. Each class declaration uses this default mode for all its parameters, unless a `mode` attribute is used to set the mode explicitly.

  Warning Using inferred default mode: “mode” for “ident”

    Indicates that the `mode` for a `Class` declaration has been assigned automatically using the default mode. This warning is named `class-declaration-default-mode`. It is disabled by default. Enable it to find (and fix) any typeclasses that don't have explicit mode declarations.

Flag Typeclasses Dependency Order

  This flag (off by default) respects the dependency order between subgoals, meaning that subgoals on which other subgoals depend come first, while the non-dependent subgoals were put before the dependent ones previously (Coq 8.5 and below). This can result in quite different performance behaviors of proof search.

Flag Typeclasses Limit Intros

  This flag (on by default) controls the ability to apply hints while avoiding (functional) eta-expansions in the generated proof term. It does so by allowing hints that conclude in a product to apply to a goal with a matching product directly, avoiding an introduction.

  Warning

  This can be expensive as it requires rebuilding hint clauses dynamically, and does not benefit from the invertibility status of the product introduction rule, resulting in potentially more expensive proof search (i.e. more useless backtracking).

Flag Typeclass Resolution For Conversion

  This flag (on by default) controls the use of typeclass resolution when a unification problem cannot be solved during elaboration/type inference. With this flag on, when a unification fails, typeclass resolution is tried before launching unification once again.

Flag Typeclasses Strict Resolution

  Typeclass declarations introduced when this flag is set have a stricter resolution behavior (the flag is off by default). When looking for unifications of a goal with an instance of this typeclass, we “freeze” all the existentials appearing in the goals, meaning that they are considered rigid during unification and cannot be instantiated.

Flag Typeclasses Unique Solutions

  When a typeclass resolution is launched we ensure that it has a single solution or fail. This flag ensures that the resolution is canonical, but can make proof search much more expensive.

Flag Typeclasses Unique Instances

  Typeclass declarations introduced when this flag is set have a more efficient resolution behavior (the flag is off by default). When a solution to the typeclass goal of this typeclass is found, we never backtrack on it, assuming that it is canonical.

Flag Typeclasses Iterative Deepening

  When this flag is set, the proof search strategy is breadth-first search. Otherwise, the search strategy is depth-first search. The default is off. `Typeclasses eauto` is another way to set this flag.

Option Typeclasses Depth natural

  This option sets the maximum proof search depth. The default is unbounded. `Typeclasses eauto` is another way to set this option.

Flag Typeclasses Debug

  Controls whether typeclass resolution steps are shown during search. Setting this flag also sets `Typeclasses Debug Verbosity` to 1. `Typeclasses eauto` is another way to set this flag.

Option Typeclasses Debug Verbosity natural

  Determines how much information is shown for typeclass resolution steps during search. 1 is the default level. 2 shows additional information such as tried tactics and shelving of goals. Setting this option to 1 or 2 turns on the `Typeclasses Debug` flag; setting this option to 0 turns that flag off.

  Note that the tactics shown when `natural > 0`(after removing tactics that were backtracked) may not always work as a replacement for the proof search tactic. See :ref:`here <info_auto_not_exact>`.

### Typeclasses eauto

Command Typeclasses eauto := debug? ( bfs​dfs )? natural?

  Allows more global customization of the `typeclasses eauto` tactic. The options are:

  `debug`

    Sets debug mode. In debug mode, a trace of successfully applied tactics is printed. Debug mode can also be set with `Typeclasses Debug`.

  `bfs​dfs`

    Specifies whether to use breadth-first search or depth-first search. The default is depth-first search, which can be changed with the `Typeclasses Iterative Deepening` flag.

  `natural`

    Sets the depth limit for the search. The limit can also be set with `Typeclasses Depth`.

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF