Decidable with structures

Stream: lean4

[Heather Macbeth]

I have a Prop structure for which I wrote a Decidable instance, but this instance doesn't seem to trigger. Is this expected behaviour? If so, how can I make decide work for my structure? MWE:

structure Nice (n : Nat) : Prop :=
  (large : 100 ≤ n)

theorem nice_iff (n : Nat) : Nice n ↔ 100 ≤ n := ⟨Nice.rec id, Nice.mk⟩

instance (n : Nat) : Decidable (Nice n) := by
  rw [nice_iff]
  infer_instance

example : Nice 102 := by decide -- fails
example : Nice 102 := by rw [nice_iff]; decide -- works

[Kyle Miller]

It fails because you used rw to define it. Here's the error message:

/-
tactic 'decide' failed for proposition
  Nice 102
since its 'Decidable' instance reduced to
  ⋯ ▸ inferInstance
rather than to the 'isTrue' constructor.
-/

What you should be getting from it is "it knows there's a Decidable instance, but something is wrong with it, and it gets stuck trying to evaluate it". The subst operator (the triangle) hints that it's a rewrite that made it get stuck.

[Kyle Miller]

This is one of the "right" ways to write the Decidable instance to circumvent this issue:

instance (n : Nat) : Decidable (Nice n) :=
  decidable_of_iff _ (nice_iff _).symm

example : Nice 102 := by decide

[Kyle Miller]

The key is that decidable_of_iff is defined using

def decidable_of_decidable_of_iff [Decidable p] (h : p ↔ q) : Decidable q :=
  if hp : p then
    isTrue (Iff.mp h hp)
  else
    isFalse fun hq => absurd (Iff.mpr h hq) hp

and it can reduce this (it's an honest if, and each case is just a constructor of Decidable).

[Kyle Miller]

Potentially someone could write a fancier decide that does a better job at diagnosing the issue. Right now, it just hands you what it sees after putting the instance into weak head normal form, which is simultaneously helpful and useless.

[Heather Macbeth]

Thanks! It's a bit reassuring to me that I have definitely never encountered this quirk before (can't use ▸ in decide) -- at least it's not something I should have figured out :)

[Heather Macbeth]

By the way, a related question: is there a derive handler which would generate the Decidable (Nice n) instance here?

[Kyle Miller]

Thinking about it now, it could easily detect that ▸ is there (that's Eq.rec by the way) and tell you more-or-less what I just told you. It could also tell you which definition(s) might be responsible.

[Kyle Miller]

Heather Macbeth said:

By the way, a related question: is there a derive handler which would generate the Decidable (Nice n) instance here?

I don't believe so, but it would be Nice

[Heather Macbeth]

Kyle Miller said:

I don't believe so, but it would be Nice

All the more so in my actual situation, in which I have a structure with five fields, so the nice_iff lemma is a real pain to write out:

theorem nice_iff (n : Nat) : Nice n ↔ stuff ∧ stuff ∧ stuff ∧ stuff ∧ stuff :=
  ⟨Nice.rec (fun h1 h2 h3 h4 h5 ↦ ⟨h1, h2, h3, h4, h5⟩),
    fun h ↦ Nice.mk h.1 h.2.1 h.2.2.1 h.2.2.2.1 h.2.2.2.2⟩

There's no better way, right?

[Kyle Miller]

Mathlib has the @[mk_iff] attribute:

@[mk_iff]
structure Nice (n : Nat) : Prop :=
  (large : 100 ≤ n)

#print nice_iff
/-
theorem nice_iff : ∀ (n : ℕ), Nice n ↔ 100 ≤ n :=
fun n ↦ { mp := fun a ↦ Nice.casesOn a fun large ↦ large, mpr := fun a ↦ { large := a } }
-/

Maybe we could have a mathlib Decidable deriving handler so that you can do

structure Nice (n : Nat) : Prop :=
  (large : 100 ≤ n)
  deriving Decidable

that makes use of the mk_iff machinery paired with decidable_of_iff.

[Heather Macbeth]

Oh, I didn't know about @[mk_iff], and it avoids almost all the pain. Thanks!

[Heather Macbeth]

(But indeed, the Decidable deriving handler would be even better.)

[Kyle Miller]

lean4#4674 is an experiment to make the decide tactic more informative.

structure Nice (n : Nat) : Prop :=
  (large : 100 ≤ n)

theorem nice_iff (n : Nat) : Nice n ↔ 100 ≤ n := ⟨Nice.rec id, Nice.mk⟩

instance (n : Nat) : Decidable (Nice n) := by
  rw [nice_iff]
  infer_instance

example : Nice 102 := by decide
/-
tactic 'decide' failed for proposition
  Nice 102
since its 'Decidable' instance did not reduce to 'isTrue' or 'isFalse'.

Instead, after unfolding the instance
  instDecidableNice
it reduced to
  ⋯ ▸ inferInstance

Hint: reduction got stuck on '▸' (Eq.rec), which indicates that one of the instances is
defined using tactics such as 'rw' or 'simp'. Use definitions such as 'inferInstanceAs'
or 'decidable_of_decidable_of_iff' to change or otherwise "rewrite" the type.
-/

To help with debugging, you can even hover over the names of unfolded instances to be able to do Go to Definition.
image.png