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 [MT13]. 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 [GZND11] 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.
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 Canonical Structures; here only a simple example is given.
- Command Canonical Structure? reference¶
- Command Canonical Structure? ident_decl def_body¶
The first form of this command declares an existing
reference
as a canonical instance of a structure (a record).The second form defines a new constant as if the
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
local
attribute. When used, the structure is canonical only within theSection
containing it.qualid
(inreference
) denotes an object(Build_struct c_{1} … c_{n})
in the structurestruct
for which the fields arex_{1}, …, x_{n}
. Then, each time an equation of the form(x_{i} _)
=
\(_{βδιζ}\)c_{i}
has to be solved during the type checking process,qualid
is used as a solution. Otherwise said,qualid
is canonically used to extend the fieldx_{i}
into a complete structure built onc_{i}
whenc_{i}
unifies with(x_{i} _)
.The following kinds of terms are supported for the fields
c_{i}
ofqualid
:Constants and section variables of an active section, applied to zero or more arguments.
sort
s.Literal functions:
fun … => …
.Literal, (possibly dependent) function types:
… -> …
andforall …, …
.Variables bound in
qualid
.
Only the head symbol of an existing instance's field
c_{i}
is considered when searching for a canonical extension. We call this head symbol the key and we say "qualid
keys the fieldx_{i}
tok
" whenc_{i}
's head symbol isk
. Keys are the only piece of information that is used for canonical extension. The keys corresponding to the kinds of terms listed above are:For constants and section variables, potentially applied to arguments: the constant or variable itself, disregarding any arguments.
For sorts: the sort itself.
For literal functions: skip the abstractions and use the key of the body.
For literal function types: a disembodied implication key denoted
forall _, _
, disregarding both its domain and codomain.For variables bound in
qualid
: a catch-all key denoted_
.
This means that, for example,
(some_constant x1)
and(some_constant (other_constant y1 y2) x2)
are not distinct keys.Variables bound in
qualid
match any term for the purpose of canonical extension. This has two major consequences for a fieldc_{i}
keyed to a variable ofqualid
:Unless another key—and, thus, instance—matches
c_{i}
, the instance will always be considered by unification.c_{i}
will be considered overlapping not distinct from any other canonical instance that keysx_{i}
to one of its own variables.
A record field
x_{i}
can only be keyed once to each key. Coq prints a warning whenqualid
keysx_{i}
to a term whose head symbol is already keyed by an existing canonical instance. In this case, Coq will not register thatqualid
as a canonical extension. (The remaining fields of the instance can still be used for canonical extension.)Canonical structures are particularly useful when mixed with coercions and strict implicit arguments.
Example
Here is an example.
- 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}.
- Setoid is defined Carrier is defined Equal is defined Prf_equiv is defined
- Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y).
- is_law is defined
- Axiom eq_nat_equiv : equivalence nat eq_nat.
- eq_nat_equiv is declared
- Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
- nat_setoid is defined
- Canonical nat_setoid.
Thanks to
nat_setoid
declared as canonical, the implicit argumentsA
andB
can be synthesized in the next statement.- Lemma is_law_S : is_law S.
- 1 goal ============================ is_law (A:=nat_setoid) (B:=nat_setoid) S
Note
If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered.
- Attribute canonical= yesno?¶
This boolean attribute can decorate a
Definition
orLet
command. It is equivalent to having aCanonical Structure
declaration just after the command.To prevent a field from being involved in the inference of canonical instances, its declaration can be annotated with
canonical=no
(cf. the syntax ofrecord_field
).Example
For instance, when declaring the
Setoid
structure above, thePrf_equiv
field declaration could be written as follows.#[canonical=no] Prf_equiv : equivalence Carrier EqualSee Hierarchy of structures for a more realistic example.
- Command Print Canonical Projections reference*¶
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:
- Print Canonical Projections.
- nat <- Carrier ( nat_setoid ) eq_nat <- Equal ( nat_setoid ) eq_nat_equiv <- Prf_equiv ( nat_setoid )
- Print Canonical Projections nat.
- nat <- Carrier ( nat_setoid )
Note
The last line in the first example would not show up if the corresponding projection (namely
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.
- Module EQ.
- Interactive Module EQ started
- Record class (T : Type) := Class { cmp : T -> T -> Prop }.
- class is defined cmp is defined
- Structure type := Pack { obj : Type; class_of : class obj }.
- type is defined obj is defined class_of is defined
- Definition op (e : type) : obj e -> obj e -> Prop := let 'Pack _ (Class _ the_cmp) := e in the_cmp.
- op is defined
- Check op.
- op : forall e : type, obj e -> obj e -> Prop
- Arguments op {e} x y : simpl never.
- Arguments Class {T} cmp.
- Module theory.
- Interactive Module theory started
- Notation "x == y" := (op x y) (at level 70).
- End theory.
- Module theory is defined
- End EQ.
- Module EQ is defined
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
the EQ
class, we can relate two of its objects with ==
.
- Import EQ.theory.
- Check forall (e : EQ.type) (a b : EQ.obj e), a == b.
- forall (e : EQ.type) (a b : EQ.obj e), a == b : Prop
Still, no concrete type is in the EQ
class.
- Fail Check 3 == 3.
- The command has indeed failed with message: The term "3" has type "nat" while it is expected to have type "EQ.obj ?e".
We amend that by equipping nat
with a comparison relation.
- Definition nat_eq (x y : nat) := Nat.compare x y = Eq.
- nat_eq is defined
- Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq.
- nat_EQcl is defined
- Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl.
- nat_EQty is defined
- Check 3 == 3.
- 3 == 3 : Prop
- Eval compute in 3 == 4.
- = Lt = Eq : Prop
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 with the key. In this
case we associate with 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:
- Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b).
- The command has indeed failed with message: In environment e : EQ.type a : EQ.obj e b : EQ.obj e The term "(a, b)" has type "(EQ.obj e * EQ.obj e)%type" while it is expected to have type "EQ.obj ?e".
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.
- Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) := fst x == fst y /\ snd x == snd y.
- pair_eq is defined
- Definition pair_EQcl e1 e2 := EQ.Class (pair_eq e1 e2).
- pair_EQcl is defined
- Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type := EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2).
- pair_EQty is defined
- Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b).
- forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b) : Prop
- Check forall n m : nat, (3, 4) == (n, m).
- forall n m : nat, (3, 4) == (n, m) : Prop
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.
- Module LE.
- Interactive Module LE started
- Record class T := Class { cmp : T -> T -> Prop }.
- class is defined cmp is defined
- Structure type := Pack { obj : Type; class_of : class obj }.
- type is defined obj is defined class_of is defined
- Definition op (e : type) : obj e -> obj e -> Prop := let 'Pack _ (Class _ f) := e in f.
- op is defined
- Arguments op {_} x y : simpl never.
- Arguments Class {T} cmp.
- Module theory.
- Interactive Module theory started
- Notation "x <= y" := (op x y) (at level 70).
- End theory.
- Module theory is defined
- End LE.
- Module LE is defined
As before we register a canonical LE
class for nat
.
- Import LE.theory.
- Definition nat_le x y := Nat.compare x y <> Gt.
- nat_le is defined
- Definition nat_LEcl : LE.class nat := LE.Class nat_le.
- nat_LEcl is defined
- Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl.
- nat_LEty is defined
And we enable Coq to relate pair of terms with <=
.
- Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) := fst x <= fst y /\ snd x <= snd y.
- pair_le is defined
- Definition pair_LEcl e1 e2 := LE.Class (pair_le e1 e2).
- pair_LEcl is defined
- Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type := LE.Pack (LE.obj e1 * LE.obj e2) (pair_LEcl e1 e2).
- pair_LEty is defined
- Check (3,4,5) <= (3,4,5).
- (3, 4, 5) <= (3, 4, 5) : Prop
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.
- Check 2 <= 3 /\ 2 == 2.
- 2 <= 3 /\ 2 == 2 : Prop
- Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y.
- The command has indeed failed with message: In environment e : EQ.type x : EQ.obj e y : EQ.obj e The term "x" has type "EQ.obj e" while it is expected to have type "LE.obj ?e".
- Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y.
- The command has indeed failed with message: In environment e : LE.type x : LE.obj e y : LE.obj e The term "x" has type "LE.obj e" while it is expected to have type "EQ.obj ?e".
We need to define a new class that inherits from both EQ
and LE
.
- Module LEQ.
- Interactive Module LEQ started
- 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 }.
- mixin is defined compat is defined
- 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) }.
- class is defined EQ_class is defined LE_class is defined extra is defined
- Structure type := _Pack { obj : Type; #[canonical=no] class_of : class obj }.
- type is defined obj is defined class_of is defined
- 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.
- Module theory.
- Interactive Module theory started
- Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m.
- The command has indeed failed with message: In environment le : type n : obj le m : obj le The term "n" has type "obj le" while it is expected to have type "LE.obj ?e".
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.
- Definition to_EQ (e : type) : EQ.type := EQ.Pack (obj e) (EQ_class _ (class_of e)).
- to_EQ is defined
- Canonical Structure to_EQ.
- Definition to_LE (e : type) : LE.type := LE.Pack (obj e) (LE_class _ (class_of e)).
- to_LE is defined
- Canonical Structure to_LE.
We can now formulate out first theorem on the objects of the LEQ
structure.
- Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y.
- 1 goal e : type x, y : obj e ============================ x <= y -> y <= x -> x == y
- now intros; apply (compat _ _ (extra _ (class_of e)) x y); split.
- No more goals.
- Qed.
- Arguments lele_eq {e} x y _ _.
- End theory.
- Module theory is defined
- End LEQ.
- Module LEQ is defined
- Import LEQ.theory.
- Check lele_eq.
- lele_eq : forall x y : LEQ.obj ?e, x <= y -> y <= x -> x == y where ?e : [ |- LEQ.type]
Of course one would like to apply results proved in the algebraic setting to any concrete instate of the algebraic structure.
- Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m.
- 1 goal n, m : nat ============================ n <= m -> m <= n -> n == m
- Fail apply (lele_eq n m).
- The command has indeed failed with message: In environment n, m : nat The term "n" has type "nat" while it is expected to have type "LEQ.obj ?e".
- Abort.
- Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : n <= m -> m <= n -> n == m.
- 1 goal l1, l2 : LEQ.type n, m : LEQ.obj l1 * LEQ.obj l2 ============================ n <= m -> m <= n -> n == m
- Fail apply (lele_eq n m).
- The command has indeed failed with message: In environment l1, l2 : LEQ.type n, m : LEQ.obj l1 * LEQ.obj l2 The term "n" has type "(LEQ.obj l1 * LEQ.obj l2)%type" while it is expected to have type "LEQ.obj ?e".
- 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.
- Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m.
- 1 goal n, m : nat ============================ n <= m /\ m <= n <-> n == m
- Admitted.
- nat_LEQ_compat is declared
- Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat.
- nat_LEQmx is defined
- Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : n <= m /\ m <= n <-> n == m.
- 1 goal l1, l2 : LEQ.type n, m : LEQ.obj l1 * LEQ.obj l2 ============================ n <= m /\ m <= n <-> n == m
- Admitted.
- pair_LEQ_compat is declared
- Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2).
- pair_LEQmx is defined
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.
- Module Add_instance_attempt.
- Interactive Module Add_instance_attempt started
- Canonical Structure nat_LEQty : LEQ.type := LEQ._Pack nat (LEQ.Class nat_EQcl nat_LEcl nat_LEQmx).
- nat_LEQty is defined
- 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)).
- pair_LEQty is defined
- Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m.
- 1 goal n, m : nat ============================ n <= m -> m <= n -> n == m
- now apply (lele_eq n m).
- No more goals.
- Qed.
- Example test_algebraic2 (n m : nat * nat) : n <= m -> m <= n -> n == m.
- 1 goal n, m : nat * nat ============================ n <= m -> m <= n -> n == m
- now apply (lele_eq n m). Qed.
- No more goals.
- End Add_instance_attempt.
- Module Add_instance_attempt is defined
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.
- Require Import Strings.String.
- [Loading ML file ring_plugin.cmxs (using legacy method) ... done]
- Module infrastructure.
- Interactive Module infrastructure started
- Inductive phantom {T : Type} (t : T) : Type := Phantom.
- phantom is defined phantom_rect is defined phantom_ind is defined phantom_rec is defined phantom_sind is defined
- Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := phantom t1 -> phantom t2.
- unify is defined
- Definition id {T} {t : T} (x : phantom t) := x.
- id is defined
- Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) (at level 50, v name, only parsing).
- Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) (at level 50, v name, only parsing).
- Notation "'Error : t : s" := (unify _ t (Some s)) (at level 50, format "''Error' : t : s").
- Open Scope string_scope.
- End infrastructure.
- Module infrastructure is defined
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 [MT13].
We now have all we need to create a compact “packager” to declare
instances of the LEQ
class.
- 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).
- packager is defined
- 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 with 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 [MT13].
The declaration of canonical instances can now be way more compact:
- Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.
- nat_LEQty is defined
- Canonical Structure pair_LEQty (l1 l2 : LEQ.type) := Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2).
- pair_LEQty is defined
Error messages are also quite intelligible (if one skips to the end of the message).
- Fail Canonical Structure err := Eval hnf in Pack bool nat_LEQmx.
- The command has indeed failed with message: The term "id" has type "phantom (EQ.obj ?e) -> phantom (EQ.obj ?e)" while it is expected to have type "'Error:bool:"is not an EQ.type"".