In Lean, ist es möglich, Decidable_linear_order mit einer benutzerdefinierten Gleichheitsbeziehung zu verwenden?

Question

Lean kommt mit einem decidable_linear_order typeclass nützlich Lemmata über eine Ordnung und ihre Beziehung zur Gleichstellung enthalten, wie:

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

Die Gleichheiten in diesen Anordnungen in Bezug auf = alle ausgedrückt werden:

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

Ich frage mich, ob es irgendwie möglich wäre, diese Klasse (und ihre Oberklassen) zu erweitern, um mit einer beliebigen benutzten definierten Gleichheitsrelation zu arbeiten, die reflexiv, symmetrisch und transitiv, oder wäre dies nur möglich, indem alle relevanten Lemmas und ihre Beweise neu geschrieben werden, um R anstelle von eq zu verwenden?

Answer 1

Da diese Klassen nicht durch die Gleichheitsbeziehung parametrisiert sind, müssten Sie sie tatsächlich neu implementieren (vielleicht kann Metaprogrammierung dafür hilfreich sein). Alternativ können Sie, da Sie eine Äquivalenzbeziehung haben, Ihre Bestellung auf dem Quotienten-Typ definieren und so weiterhin eq verwenden.