How to use "<" when definition using some other proposition

Stream: new members

[Shaojun Zhang]

For example, if i want to define order on a group using its conditions, i cant use the symbol '<' to express the order of the elements of the group. And i found define a new notation works, but this is not good solution. So how can i use the sign "<" under such conditions.

variable [Group W] (h : W ≃ ℤ)

def llt : W → W → Prop := fun x y => h x < h y

instance : LT W where
  lt := llt h

variable {u v : W}

local infix : 100 "<<" => llt h

#check u << v --llt h u v : Prop

#check u < v
--failed to synthesize LT W
--use `set_option diagnostics true` to get diagnostic information

#check llt h u v --llt h u v : Prop

[Edward van de Meent]

because the instance LT depends on an explicit variable, lean is unable to synthesise LT W, making the syntax < not work.

[Shaojun Zhang]

Edward van de Meent said:

because the instance LT depends on an explicit variable, lean is unable to synthesise LT W, making the syntax < not work.

Thanks for repley. yeah, that's the reason. So how can i write the definition if i want to use '<'

[Edward van de Meent]

i'd assume that LT W exists, and add a hypothesis that (. < .) <-> (e . < e .)

[Edward van de Meent]

basically, something like this:

variable {W : Type*} [Group W] (e : W ≃ ℤ)
-- name the equivalence `e` to avoid confusion, because it is not Prop-typed

variable [LT W]
-- you might want to upgrade this assumption if you want `<` to be transitive, antisymmetric, etc.
-- in that case, use `Preorder`, `PartialOrder`, or something even higher in the hierarchy

variable (h: (. < .) <-> (e . < e .))
-- assert/assume that `<` is lifted from `Int`

[Shaojun Zhang]

Thanks! This is a good solution, i will try this. (there may be some other questions this way because this example is more simple. Thank you anyway :smiley:

[Jireh Loreaux]

@Shaojun Zhang this seems a bit strange. For most choices of h : W ≃ ℤ this will make the group structure on W mostly unrelated to the order structure. Is that really what you want?