dependent-type - 在精益中，是否可以将 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.