chore: DecidableRel allows a heterogeneous relation (#6341)

This PR generalizes `DecidableRel` to allow a heterogeneous relation.
leanprover · Dec 11, 2024 · 8709ca3 · 8709ca3
1 parent 19fb1fb
commit 8709ca3
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 7 deletions.
diff --git a/src/Init/Data/Nat/Dvd.lean b/src/Init/Data/Nat/Dvd.lean
@@ -77,7 +77,7 @@ theorem dvd_of_mod_eq_zero {m n : Nat} (H : n % m = 0) : m ∣ n := by
 theorem dvd_iff_mod_eq_zero {m n : Nat} : m ∣ n ↔ n % m = 0 :=
   ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩
 
-instance decidable_dvd : @DecidableRel Nat (·∣·) :=
+instance decidable_dvd : @DecidableRel Nat Nat (·∣·) :=
   fun _ _ => decidable_of_decidable_of_iff dvd_iff_mod_eq_zero.symm
 
 theorem emod_pos_of_not_dvd {a b : Nat} (h : ¬ a ∣ b) : 0 < b % a := by

diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean
@@ -96,12 +96,12 @@ This is similar to `<|>`/`orElse`, but it is strict in the second argument. -/
   | some a, _ => some a
   | none,   b => b
 
-@[inline] protected def lt (r : α → α → Prop) : Option α → Option α → Prop
+@[inline] protected def lt (r : α → β → Prop) : Option α → Option β → Prop
   | none, some _     => True
   | some x,   some y => r x y
   | _, _             => False
 
-instance (r : α → α → Prop) [s : DecidableRel r] : DecidableRel (Option.lt r)
+instance (r : α → β → Prop) [s : DecidableRel r] : DecidableRel (Option.lt r)
   | none,   some _ => isTrue  trivial
   | some x, some y => s x y
   | some _, none   => isFalse not_false

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
@@ -860,8 +860,8 @@ abbrev DecidablePred {α : Sort u} (r : α → Prop) :=
   (a : α) → Decidable (r a)
 
 /-- A decidable relation. See `Decidable`. -/
-abbrev DecidableRel {α : Sort u} (r : α → α → Prop) :=
-  (a b : α) → Decidable (r a b)
+abbrev DecidableRel {α : Sort u} {β : Sort v} (r : α → β → Prop) :=
+  (a : α) → (b : β) → Decidable (r a b)
 
 /--
 Asserts that `α` has decidable equality, that is, `a = b` is decidable

diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean
@@ -268,10 +268,10 @@ instance : OfNat Log.Pos (nat_lit 0) := ⟨⟨0⟩⟩
 instance : Ord Log.Pos := ⟨(compare ·.val ·.val)⟩
 instance : LT Log.Pos := ⟨(·.val < ·.val)⟩
 instance : DecidableRel (LT.lt (α := Log.Pos)) :=
-  inferInstanceAs (DecidableRel (α := Log.Pos) (·.val < ·.val))
+  inferInstanceAs (DecidableRel (α := Log.Pos) (β := Log.Pos) (·.val < ·.val))
 instance : LE Log.Pos := ⟨(·.val ≤ ·.val)⟩
 instance : DecidableRel (LE.le (α := Log.Pos)) :=
-  inferInstanceAs (DecidableRel (α := Log.Pos) (·.val ≤ ·.val))
+  inferInstanceAs (DecidableRel (α := Log.Pos) (β := Log.Pos) (·.val ≤ ·.val))
 instance : Min Log.Pos := minOfLe
 instance : Max Log.Pos := maxOfLe