Different Instance on same structure

Stream: mathlib4

[Andrés Goens]

Sometimes a structure might have two plausible instances of a typeclass but one is obviously the canonical one, like PartialOrder Nat from Nat.lt when Dvd.dvd could also define one. Sometimes there's no obvious one like CommMonoid, and then people use different notions for the different instances like CommMonoid and AddCommMonoid e.g. in Nat too. But what if it's somewhere in-between?

We've been looking at Bitvector a bit and there there's different variants of a bunch of operations for both signed and unsigned bitvectors. Unsigned bitvectors seems to be a sensible default, for stuff typeclass instances like Preorder (for which there's already an instance, albeit a pretty old one), but also things like ShiftRight or even Div are different for signed or unsigned bitvectors. It probably doesn't make sense to define their own typeclasses for the signed variants, it's not like it's something that arises all over like AddCommMonoid. There seems to be four distinct options here:

• define no instances for anything and just prove stuff again if we need it
• define a new type (e.g. SignedBitvector) and prove everything twice for both types and have to deal with converting back and forth explicitly
• define 1 default instance (here, concretely, for unsigned bitvectors) and treat the other version like a less important one
• define 2 instances and put them away scoped under a namespace, in the same spirit of protected definitions.

I like the last one because if we do that, if we open that namespace, everything works seamlessly for that structure, and we can choose which structure we work with explicitly. @Chris Hughes pointed out that then sometimes say a rewrite might not work without passing an explicit typeclass instance, if the namespace is closed. I can see why this version of hiding things under a namespace might seem evil, but I wanted to hear other opinions, as none of the options seems clearly like the best here.

[James Gallicchio]

I'd definitely define a new type... would it really double the proofs? You already need to prove correctness for both signed and unsigned operations separately, no?

[Andrés Goens]

Sure, for things that are different. I guess for the ones that are the same the proofs would be fairly trivial by just unfolding the type alias. :thinking:

[James Gallicchio]

The proof might be defeq, even :)

[James Gallicchio]

You might even not have to copy the name into the new namespace, since I think the name resolution algorithm unfolds the head term if it can't find any matching names

[Andrés Goens]

James Gallicchio said:

You might even not have to copy the name into the new namespace, since I think the name resolution algorithm unfolds the head term if it can't find any matching names

that went a bit over my head :sweat_smile: meaning that MyType.someTheorem would be found if I just write someTheorem on an element of the alias? That'd be pretty cool indeed!

I guess I'm not sure what the best way is to define a type alias like that, as @abbrev will make the definition reducible for typeclass synthesis. Looking around in Mathlib/GroupTheory/GroupAction/ConjAct.lean there's a definition

/-- A type alias for a group `G`. `ConjAct G` acts on `G` by conjugation -/
def ConjAct : Type _ := G

But that doesn't seem to work e.g. if I try to copy ConjAct:

def MyNat : Type _ := Nat

instance : LT MyNat := ⟨LT Nat⟩
/-
application type mismatch
  { lt := LT Nat }
argument
  LT Nat
has type
  Type : Type 1
but is expected to have type
  MyNat → MyNat → Prop : Type
-/

[James Gallicchio]

Hm, I might be wrong. Let me search around zulip for a moment

[James Gallicchio]

def Foo := Unit
def Foo' := Foo

def Foo.bar (f : Foo) : Int := 0

def foo : Foo' := ()
#eval foo.bar

is what I was talking about

[James Gallicchio]

if you want to copy instances across defs, you generally have to do something like instance : Foo X := inferInstanceAs (FooDef X)

[Chris Hughes]

Try instance : LT MyNat := inferInstanceAs (LT Nat)