Is it possible to use equality where setoid is expected?

Stream: new members

[Ilmārs Cīrulis]

Something like this... but maybe there's simpler or more natural, better way?

import Mathlib

section S

variable {A : Type} [Setoid A] [DecidableRel (fun (x y : A) => x ≈ y)]
def check_if_same (x y : A) := if x ≈ y then true else false

end S

-- #eval check_if_same 4 5
-- fails

instance : Setoid ℕ where
  r := Eq
  iseqv := eq_equivalence

instance : DecidableRel (fun (x y : ℕ) => x ≈ y) := Nat.decEq

#eval check_if_same 4 5
-- works

[Aaron Liu]

import Mathlib

section S

variable {A : Type} [Setoid A] [DecidableRel (fun (x y : A) => x ≈ y)]
def check_if_same (x y : A) := if x ≈ y then true else false

end S

#eval @check_if_same Nat ⊥ Nat.decEq 4 5

[Ilmārs Cīrulis]

Thank you!

[Ilmārs Cīrulis]

I minimized somehow problem I had, but not sure if it's not my fault.

import Mathlib

section S

variable {A : Type} [s : Setoid A]

structure pair where
  x : A
  y : A
  x_eq_y : x ≈ y

end S

def test₀ A (x : A) : pair (A := A) (s := ⊥) := by
  use x, x; simp
-- works

def test₁ A (x : A) : pair (A := A) (s := ⊥) :=
  pair.mk x x (by simp)
-- failed to synthesize instance of type class Setoid A

def test₂ A (x : A) : pair (A := A) (s := ⊥) :=
  pair.mk (s := ⊥) x x (by simp)
-- works

def test₃ A (x : A) : pair (A := A) (s := ⊥) := by
  refine ⟨x, x, ?_⟩ -- same problem

[Jakub Nowak]

You can try:

import Mathlib

section S

structure pair {A : Type} [s : Setoid A] where
  x : A
  y : A
  x_eq_y : x ≈ y

end S

section f

variable {A : Type}
local instance : Setoid A := ⊥

def test₀ A (x : A) : pair (A := A) := by
  use x, x

def test₁ A (x : A) : pair (A := A) :=
  pair.mk x x (by simp)

def test₂ A (x : A) : pair (A := A) :=
  pair.mk (s := ⊥) x x (by simp)

def test₃ A (x : A) : pair (A := A) := by
  refine ⟨x, x, ?_⟩

end f

[Jakub Nowak]

You can also do this per-definition, instead of per-section, like this:

local instance : Setoid A := ⊥ in
def test₃ A (x : A) : pair (A := A) := by
  refine ⟨x, x, ?_⟩