No decidability for structure

Stream: mathlib4

[Ian Jauslin]

I am having trouble manipulating structures (specifically, Finset's of structures). Here is an example:

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Real.Basic

structure Test where
  x : ℝ

def test_remove (t : Finset Test) (a : Test) :=
  Finset.erase t a

Fails with failed to synthesize instance DecidableEq Test. Why is this? I can actually prove DecidableEq Test and put it in by hand, but I wonder why this is not automatic.

[Alex J. Best]

How can you prove DecidableEq Test? Equality on the real numbers is not decidable. If your proof uses classical and you don't actually need computability of test_remove you can just put open Classical at the top of the file, below the imports

[Ian Jauslin]

Here's my proof:

lemma dd : DecidableEq Test := by
  dsimp [DecidableEq]
  intro a b
  by_cases a.x=b.x
  · right
    library_search
  · left
    library_search

(it's actually weird, the library_search's are not replaceable, but it concludes with goals accomplished. I assumed this means the proof worked, but maybe there's a bug somewhere?)

Anyways, I have the same issue if I replace R with N.

[Alex J. Best]

It should still say "declaration uses sorry" in the info view somewhere (but I do agree that library search can make you think that things succeed when they don't sometimes)

[Alex J. Best]

But once again unless you really want to evaluate this function (which you can't anyway if its defined on the reals), doing open Classical will provide decidable instances for you using classical logic.

[Alex J. Best]

You'll need to write noncomputable def also if you go that route

[Ian Jauslin]

I see. Anyways, it doesn't work with N either. This does not work:

structure Test where
  x : ℕ
def test_remove (t : Finset Test) (a : Test) :=
  Finset.erase t a

and this does:

def test_remove' (t : Finset ℕ) (a : ℕ) :=
  Finset.erase t a

I'm not actually using this for reals. I think the issue here is with structure

[Ian Jauslin]

The issue with noncomputable is I do need to evaluate the function (again, in my actual application, I'm not using reals).

[Alex J. Best]

I see. Well then you need to give an instance for decidable equality of your structure, the easiest way in this case is to write

structure Test where
  x : ℕ
deriving DecidableEq

and let a magic derive handler give the instance for you

[Alex J. Best]

Otherwise you can try and prove it as you did before with lemma dd (it should be provable now, though library search may have the same issues). What you need to do in that case is state it as instance : DecidableEq Test not as a lemma so that the typeclass mechanism finds it

[Ian Jauslin]

I see. I need to create it as an instance. This works for the simple example I posted above. Now I'll try to get this to work for my project, which uses an abstract notion of points and lines. We'll see... I already checkedc that deriving doesn't work in that case... (Maybe I don't actually have DecidableEq in that case).

Thank you so much!

[Alex J. Best]

You might also find the automatically generated ext lemmas useful

@[ext]
structure Test where
  x : ℕ

creates the basic lemmas

Test.ext : ∀ (x y : Test), x.x = y.x → x = y
Test.ext_iff : ∀ (x y : Test), x = y ↔ x.x = y.x

for you, which can be helpful with less trivial structures

[Ian Jauslin]

Yes, that might be useful! Thank you!

[Ian Jauslin]

In the end, I might just open Classical, as you suggested. It seems to work without headaches. What does Classical do? Is this documented somewhere?

[Alex J. Best]

Well if you use open Classical you won't be able to compute with the functions (i.e. produce runnable code that executes the function) . You can still reason about it fine.
There is some info (for lean 3 but the point is the same) at the end of tpil https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#the-law-of-the-excluded-middle. I don't know a better reference, maybe someone else does

[Eric Wieser]

If your structure is impossible to ever constructively decide equality (like the reals), then you may as well just add noncomputable instance : DecidableEq Test := Classical.dec_eq _

[Eric Wieser]

I think that might lead to less pain than using the Classical locale