Canonical Structures in Lean

Stream: lean4

[Ivan Martinez Comas]

Hi, I am currently working in project of translation to Lean where I need to define a class Type’ and several instances of such, a minimal example of what I am doing would be:

class Type' where
type : Type
el : type

instance : CoeSort Type' Type where
coe A := A.type

instance nat' : Type' := { type := Nat, el := Nat.zero}

instance bool' : Type' := { type := Bool, el := true}

I am using coercion soLean identifies any A:Type’ as a A.Type when A is used as type, e.g, x:A  or A -> A.

Now what I need is these instances to acts as “canonical” in the sense that the following function type checks no matter the instance when applied to in this case true or Nat.zero.

 axiom TEST [A : Type'] (x : A) : Prop

However, this only works for the last instance defined in the code, that is, #check TEST true is correct while #check TEST Nat.zero is not. Is there a way to force Lean to look for the suited instance given the type param? (this one is inferred from x and using CoeSort) For instance, Rocq achieves this using the canonical structure mechanism.

[Robin Arnez]

You could make Type' a structure and setup unification hints like this:

unif_hint (A : Type') where A =?= nat' ⊢ A.type =?= Nat
unif_hint (A : Type') where A =?= bool' ⊢ A.type =?= Bool

but maybe the question is: why not

class Type' (type : Type) where
  el : type

instance nat' : Type' Nat := { el := Nat.zero }
instance bool' : Type' Bool := { el := true }

axiom TEST {A : Type} [Type' A] (x : A) : Prop

[Ivan Martinez Comas]

Oh thanks! The first approach is what i was looking for. I will look into the other one as well but I think it does not match my purposes. Thanks!

[Filippo A. E. Nuccio]

I think that this confusion might actually come from a difference between the bundling philosphy behind canonical structures and behind mathlib class inference system. If you compare MathComp's way of saying that $\mathbb{Z}$ is a group, namely

Canonical int_ZmodType := ZmodType int intZmod.Mixin

with Mathlib's Int.instAddCommGroup you see that

1. Rocq / MathComp approach is to say "int gives rise to a record of the formZmodType (which is defined as a record via Definition zmodType := Zmodule.Pack class., see Chap 8.3 of Mahboubi-Tassi's book), namely intZmod.Mixin: so, now, when Rocq needs (say) addition on int it can try to see whether there exists a mixin of the form ZmodType containing int as a field, and this is precisely the record int_ZmodType. In this view, ZmodType is a "pattern" of records, each containing a type, an addition, etc... In particular, one can define two terms in ZmodType, each with a different underlying type. What is "Canonical" is then the choice of a record whose underlying type would be, say, int.
2. Lean takes a different approach, and says that docs#AddCommGroup has a G : Type* parameter, but then AddCommGroup G consists of all add-comm-group structures on G and declaring an instance of AddCommGroup does not make any sense, you can only define an instace of a AddCommGroup ℤ, which will be "the unique add comm group structure on the integers".

To my eyes, writing class Type' where... is very much Rocq-idiomatic but not Leanidiomatic. In particular, writing instance nat ' : Type' basically declares that the only preferred term in Type' is nat', and when on the second line you type instance bool' : Type' you replace this prefered term in Type' with the new one (hence killing the previous one). Indeed, if you compare

class Type' where
type : Type
el : type
instance : CoeSort Type' Type where
  coe A := A.type
axiom TEST {A : Sort*} [A : Type'] (x : A) : Prop

instance nat' : Type' := { type := Nat, el := Nat.zero}
instance bool' : Type' := { type := Bool, el := true}
#check TEST Nat.zero
#check TEST true

with

class Type' where
type : Type
el : type
instance : CoeSort Type' Type where
  coe A := A.type
axiom TEST {A : Sort*} [A : Type'] (x : A) : Prop

instance bool' : Type' := { type := Bool, el := true}
instance nat' : Type' := { type := Nat, el := Nat.zero}
#check TEST Nat.zero
#check TEST true

(where I've swapped the instances), you see that what fails in both cases is the first instance, since it was forgotten by the second.

The usual Mathlib/Lean approach is to avoid bundling the type inside the structure, and this is exactly what @Robin Arnez is suggesting with the second option class Type' (type : Type): in that case, you would construct two different instances, one for Type' Bool and one for Type' Nat, that would not conflict with each other.

[Ivan Martinez Comas]

Hi, thaks for the explanation. I had more experience in Rocq and I was looking for something alike but after some testing and learning of Lean's type classes I realized that indeed, this second approach works much better, thanks!