DecidableEq, LT, GT

Stream: lean4

[André Luiz Feijó dos Santos]

I've been struggling to define DecidableEq, LT, and LE instances for "non-direct" notions of equality — that is, equality different from the default, where, for example, in this post, monday = monday and wednesday = wednesday.

Suppose I want to define NumQ, which is rational -- like:

inductive NumQ where
| rat : Int -> Nat -> NumQ -- "rat num den"

where I want DecidableEq, LT and LE to consider the comparison by cross multiplication to say that, e.g.:

(rat 3 4 = rat 30 40) = true.

How should I define DecidableEq, LT, and LE for NumQ in this way?

[Aaron Liu]

for decidableeq you need to take a quotient

[André Luiz Feijó dos Santos]

Thanks for answering. Could you give me an example of how to implement it?

[Aaron Liu]

inductive NumQ : Type where
| rat : Int -> Nat -> NumQ -- "rat num den"

open NumQ

-- actually it doesn't work like that
example : rat 3 4 ≠ rat 30 40 := by simp

[Aaron Liu]

André Luiz Feijó dos Santos said:

Thanks for answering. Could you give me an example of how to implement it?

well Batteries does docs#Rat differently (it reduces the fractions) and usually we don't like to use Quotient if there's a way to efficiently pick a representative from each equivalence class

[Aaron Liu]

since it breaks canonicity

[Robin Arnez]

If you want to still know how quotients work:

inductive PreNumQ : Type where
  | rat : Int → Nat → PreNumQ -- "rat num den"

def PreNumQ.Eqv (x y : PreNumQ) : Prop :=
  match x, y with
  | .rat a b, .rat c d =>
    sorry -- what you want rat a b = rat c d to mean

instance PreNumQ.setoid : Setoid PreNumQ where
  r := PreNumQ.Eqv
  iseqv := { -- proof that it is an equivalence relation
    refl x := sorry
    symm {x y} h := sorry
    trans {x y z} h h' := sorry
  }

def NumQ := Quotient PreNumQ.setoid
def NumQ.rat (a : Int) (b : Nat) : NumQ := Quotient.mk _ (.rat a b)

theorem NumQ.rat_eq_rat_iff {a b c d} : rat a b = rat c d ↔ PreNumQ.Eqv (.rat a b) (.rat c d) :=
  ⟨Quotient.exact, Quotient.sound (s := PreNumQ.setoid)⟩

[Kenny Lau]

@André Luiz Feijó dos Santos the key concept here is that while < and <= are relations that can be defined arbitrarily, = is actually a core notion of Lean that cannot be changed

[François G. Dorais]

In addition to the previous responses, note that == (aka BEq) can be defined arbitrarily. It is, however, required to be decidable since its value is in Bool instead of Prop.

[Robert Maxton]

higher inductives when :(

[David Thrane Christiansen]

The reference manual explains quotient types and gives some related examples, in case that's useful.