\[\begin{split}\newcommand{\alors}{\textsf{then}} \newcommand{\alter}{\textsf{alter}} \newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\bool}{\textsf{bool}} \newcommand{\case}{\kw{case}} \newcommand{\conc}{\textsf{conc}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\conshl}{\textsf{cons\_hl}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\EqSt}{\textsf{EqSt}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\false}{\textsf{false}} \newcommand{\filter}{\textsf{filter}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\from}{\textsf{from}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\haslength}{\textsf{has\_length}} \newcommand{\hd}{\textsf{hd}} \newcommand{\ident}{\textsf{ident}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\lb}{\lambda} \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{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\Nat}{\mathbb{N}} \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{\Prod}{\textsf{prod}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\si}{\textsf{if}} \newcommand{\sinon}{\textsf{else}} \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{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} \newcommand{\unfold}{\textsf{unfold}} \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}]} \newcommand{\zeros}{\textsf{zeros}} \end{split}\]

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.

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.
  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.
  
op
     : forall e : type, obj e -> obj e -> Prop

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

Import EQ.theory.

forall (e : EQ.type) (a b : EQ.obj e), a == b
     : Prop

Still, no concrete type is in the EQ class.

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.
Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq.
Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl.

3 == 3
     : Prop


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

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.

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


forall (e : EQ.type) (a b : EQ.obj e),
(a, b) == (a, b)
     : Prop



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.

  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.

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

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


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

2 <= 3 /\ 2 == 2
     : Prop



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



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.

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

Unfortunately there is still an obstacle to developing the algebraic theory of this new class.

Module theory.


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

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.

   
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.


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.

n, m:nat
n <= m -> m <= n -> 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".
n, m:nat
n <= m -> m <= n -> n == m


Abort.


l1, l2:LEQ.type
n, m:(LEQ.obj l1 * LEQ.obj l2)%type
n <= m -> m <= n -> 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".
l1, l2:LEQ.type
n, m:(LEQ.obj l1 * LEQ.obj l2)%type
n <= m -> m <= n -> 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.

n, m:nat
n <= m /\ m <= n <-> n == m


Admitted.

Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat.


l1, l2:LEQ.type
n, m:(LEQ.obj l1 * LEQ.obj l2)%type
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.

Module Add_instance_attempt.

  Canonical Structure nat_LEQty : LEQ.type :=
    LEQ._Pack nat (LEQ.Class nat_EQcl nat_LEcl nat_LEQmx).

  
Ignoring canonical projection to LEQ.Class by
LEQ.class_of in pair_LEQty: redundant with nat_LEQty
[redundant-canonical-projection,typechecker]


   
n, m:nat
n <= m -> m <= n -> n == m


   now apply (lele_eq n m).

   Qed.

   
n, m:(nat * nat)%type
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.

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 [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).

 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 [MT13].

The declaration of canonical instances can now be way more compact:

Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.


Ignoring canonical projection to LEQ.Class by
LEQ.class_of in pair_LEQty: redundant with nat_LEQty
[redundant-canonical-projection,typechecker]

Error messages are also quite intelligible (if one skips to the end of the message).

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