failed to synthesize Decidable (LT)

Stream: new members

[An Qi Zhang]

Hello, I'm trying to define a structure with 2 fields, and then show it implements an instance of DecidableLt.

I tried implementing DecidableLT for the structure, but that doesn't let me write
#eval t0 < t1 with the structure. Lean throws the error "failed to synthesize Decidable ( t0 < t1 )", but I don't know how to implement Decidable ( t0 < t1 ).

How do I implement Decidable (t0 < t1)? Or is this something Lean should be able to figure out, and I need to make a change to the definition?

Here's my MWE:

import Mathlib

namespace MWE

structure Ex where
  n : Nat
  b : Bool
deriving DecidableEq

def Ex.lt : Ex → Ex → Prop
| ex₁, ex₂ => (ex₁.n < ex₂.n ∨ ex₁.n = ex₂.n) ∧ (ex₁.b < ex₂.b ∨ ex₁.b = ex₂.b) ∧ ex₁ ≠ ex₂

instance Ex.instLT : (LT Ex) := {lt := Ex.lt}

instance Ex.instDecidableLt (_ _ : Ex) : (DecidableLT Ex)
| ⟨n₁,true⟩, ⟨n₂,false⟩ =>
  isFalse <| by
  simp[LT.lt]
  simp[Ex.lt] -- Lean complains about too many recusions if merged (simp[LT.lt, Ex.lt])
| ⟨n₁, false⟩, ⟨n₂, false⟩ | ⟨n₁,true⟩, ⟨n₂,true⟩ =>
  if h : n₁ < n₂ then isTrue <| by
    simp[LT.lt]
    simp[Ex.lt]
    apply And.intro
    case left =>
      simp[h] -- How to make this work with Ex.lt with ex₁.n ≤ ex₂.n, instead of ex₁.n < ex₂.n ∨ ex₁.n = ex₁.n?
    case right =>
      intro h₁
      aesop -- How to do this without aesop?
  else if n₁ = n₂ then isFalse <| by
    simp[LT.lt]
    simp[Ex.lt]
    intro h₁
    cases h₁
    case inl h₂ =>
      contradiction
    case inr h₂ =>
      apply h₂
  else isFalse <| by
    simp[LT.lt]
    simp[Ex.lt]
    intro h₁
    cases h₁
    case inl h₂ =>
      contradiction
    case inr h₂ =>
      apply h₂
| ⟨n₁,false⟩, ⟨n₂,true⟩ =>
  if h : n₁ < n₂ then isTrue <| by
    simp[LT.lt]
    simp[Ex.lt]
    apply Or.inl
    apply h
  else if h₁ : n₁ = n₂ then isTrue <| by
    simp[LT.lt]
    simp[Ex.lt]
    aesop
  else isFalse <| by
    simp[LT.lt]
    simp[Ex.lt]
    simp[h,h₁]
    aesop

def t0 : Ex := ⟨0,false⟩
def t1 : Ex := ⟨0,true⟩
-- DecidableLT Ex doesn't work?
#eval t0 < t1
-- Need to use Decidable (ex₁ < ex₂) instead of DecidableLT Ex?
instance (ex₁ ex₂ : Ex) : (Decidable (ex₁ < ex₂)) :=
  inferInstanceAs (Decidable (ex₁ < ex₂))   -- failed to synthesize Decidable (ex₁ < ex₂)

[Matt Diamond]

I changed Ex.lt to abbrev to allow typeclass search to see through the definition. (I also changed the definition to use ≤.) Lean knows how to figure out the rest.

import Mathlib

namespace MWE

structure Ex where
  n : Nat
  b : Bool
deriving DecidableEq

abbrev Ex.lt : Ex → Ex → Prop
| ex₁, ex₂ => ex₁.n ≤ ex₂.n ∧ ex₁.b ≤ ex₂.b ∧ ex₁ ≠ ex₂

instance Ex.instLT : LT Ex := {lt := Ex.lt}

instance Ex.instDecidableRel : DecidableRel Ex.lt := inferInstance

instance Ex.instDecidableLT : DecidableLT Ex := Ex.instDecidableRel

def t0 : Ex := ⟨0,false⟩
def t1 : Ex := ⟨0,true⟩

#eval t0 < t1

[Matt Diamond]

I think adding the explicit DecidableRel instance may have helped. inferInstance doesn't seem to suffice for proving DecidableLT Ex.

[Zhuanhao Z Wu]

For your particular case, you may just model Ex.lt as a function to Boolean, and it should be easy to lift it to Ex -> Ex -> Prop:

import Mathlib

namespace MWE

structure Ex where
  n : Nat
  b : Bool
deriving DecidableEq

def Ex.lt : Ex → Ex → Bool
| ex₁, ex₂ => (ex₁.n < ex₂.n ∨ ex₁.n = ex₂.n) ∧ (ex₁.b < ex₂.b ∨ ex₁.b = ex₂.b) ∧ ex₁ ≠ ex₂

instance Ex.instLT : (LT Ex) := {lt := λt0 t1 => Ex.lt t0 t1}

instance Ex.instDecidableLt : (DecidableLT Ex) := by
  unfold DecidableLT DecidableRel
  dsimp [· < ·]
  infer_instance

-- alternatively
instance (ex₁ ex₂ : Ex) : (Decidable (ex₁ < ex₂)) := by
  dsimp [· < ·]
  infer_instance

def t0 : Ex := ⟨0,false⟩
def t1 : Ex := ⟨0,true⟩
#eval t0 < t1

[Robin Arnez]

In the original example, the (_ _ : Ex) was the problem because they were not referenced anywhere and thus the instance synthesizer couldn't figure out what they should be.

[An Qi Zhang]

Thanks Matt and Zhuanhao! Your answers were very helpful, and also helped me with other LT instances!

@Robin Arnez Is (_ _ : Ex) the problem? If I write:

instance Ex.instDecidableLt (ex₁ ex₂ : Ex) : (DecidableLT Ex) :=
  inferInstanceAs (Decidable (ex₁ < ex₂))

in place of the original:

instance Ex.instDecidableLt (_ _ : Ex) : (DecidableLT Ex)

Then Lean isn't able to synthesize the Decidable (ex₁ < ex₂)

Is there something I'm missing here?

[Aaron Liu]

You want instance Ex.instDecidableLt : (DecidableLT Ex)

[Aaron Liu]

DecidableLT Ex is an abbrev for ∀ (a b : Ex), Decidable (a < b)