instance cant be synthesized

Stream: mathlib4

[Shaojun Zhang]

Hello, i have a problem about instance mechanism. The problem can be summarized as when i want to define a order on some specific group, but the order is given by another property about the group, then < will be unavailable. Such as following test :

variable {A B : Type} [Group A]

structure foo (A : Type) (B : Type) where
  test : Prop

variable (hf : foo A B)

lemma fooo : Prop := hf.test

instance : LT A where
  lt := fun _ _ => fooo hf

#synth LT A -- failed to synthesize LT A

I have known the problem is that foo is used in this LT definition, but I don't know what the correct way to write it is. I tried to define foo as a class type, and encountered other problems. Such as following

class foo (A : Type) (B : Type) where
  test : Prop

variable [hf : foo A B]

lemma fooo : Prop := hf.test

instance : LT A where
  lt := fun _ _ => @fooo A B _
-- cannot find synthesization order for instance @instLT with type
  {A B : Type} → [hf : foo A B] → LT A
all remaining arguments have metavariables:
  foo A ?B

[Andrew Yang]

Can you un-#xy your self and describe what A and B and foo are? There are multiple ways to deal with this: outParams, type synonyms, explicit letIs, etc and it might not be easy to choose which to do.

[Shaojun Zhang]

Andrew Yang said:

Can you un-#xy your self and describe what A and B and foo are? There are multiple ways to deal with this: outParams, type synonyms, explicit letIs, etc and it might not be easy to choose which to do.

ok, i want to define Bruhat order on Coxeter group. The code is below

import Mathlib.GroupTheory.Coxeter.inversion

variable {B : Type*}
variable {W : Type} [Group W]
variable {M : CoxeterMatrix B} (cs : CoxeterSystem M W)
variable {u v : W}

def lt_adj  : W → W → Prop := fun u v =>
  (∃ t : cs.reflections, v = u * t) ∧ ℓ u < ℓ v

def lt := Relation.TransGen <| lt_adj cs

instance : LT W where
  lt := lt cs

The needed definition such as CoxeterSystem is in Mathlib.GroupTheory.Coxeter.Basic

[Shaojun Zhang]

Now i try to use [IsCoxeterGroup W] to write the definition of lt, i constructor the CoxeterSystem B W from [IsCoxeterGroup W]. The code is :

variable (G : Type) [Group G] [hG : IsCoxeterGroup G]

noncomputable def csOf := choice <| choose_spec <| (choose_spec hG.1)

noncomputable def indexOf := choose hG.1

def lt_adj  : W → W → Prop := fun u v =>
  (∃ t : (csOf W).reflections, v = u * t) ∧ ℓ u < ℓ v

def lt := Relation.TransGen <| lt_adj W

This works, but i dont think this is a good solution.

[Andrew Yang]

In that case I would suggest

def CoxeterSystem.Group (cs : CoxeterSystem M W) := W

instance : LT cs.Group where
  lt := lt cs

[Andrew Yang]

But someone more familiar with that part of the library might have a more informed suggestion.

[Shaojun Zhang]

Andrew Yang said:

But someone more familiar with that part of the library might have a more informed suggestion.

yeah, thank you! This is a good idea, i will try it :smiley: