Можно ли в Lean использовать decidable_linear_order с пользовательским отношением равенства?

Question

Lean поставляется с decidable_linear_order класс типов, содержащий полезные леммы об упорядочении и его отношении к равенству, такие как:

lemma eq_or_lt_of_not_lt [decidable_linear_order α] {a b : α} (h : ¬ a < b) : a = b ∨ b < a

Равенства в этих порядках выражаются в терминах =:

inductive eq {α : Sort u} (a : α) : α → Prop
| refl : eq a

Мне было интересно, можно ли как-то расширить этот класс (и его суперклассы) для работы с произвольно используемым определенным отношением равенства R: α → α → Prop это было рефлексивно, симметрично и транзитивно, или это было бы возможно только путем переписывания всех соответствующих лемм и их доказательств для использования R вместо eq?

Answer 1

Поскольку эти классы не параметризуются отношением равенства, вам действительно придется их переопределить (возможно, для этого может помочь метапрограммирование). В качестве альтернативы, поскольку у вас есть отношение эквивалентности, вы можете определить свой порядок по типу отношения и продолжать использовать eq,