leaked `DecidableEq Prop`

Stream: mathlib4

[Thomas Zhu]

I have two related issues and I would like some advice on if/how it should be fixed:

(1) A LinearOrder Prop instance docs#Prop.linearOrder is defined in mathlib without scoping under Classical. As a result, because of docs#LinearOrder.toDecidableEq, we have DecidableEq Prop synthesizable without opening Classical. Informally, this is tantamount to saying that every Prop is decidable (because we have ∀ p, Decidable (p = True)).

We can define the following function without opening Classical. Although it is not idiomatic (it should be if p then 1 else 0), it can occur as an instantiation of a larger definition (e.g., counting True in a Multiset Prop).

import Mathlib
noncomputable def a (p : Prop) := if p = True then 1 else 0

(2) Regardless of whether it is scoped under Classical, this creates an instance diamond:

import Mathlib

-- I have a definition `a`
noncomputable def a (p : Prop) := if p = True then 1 else 0

-- suppose in a `classical` proof, or in a separate definition, I have
open Classical in
noncomputable def b (p : Prop) := if p = True then 1 else 0

example (p : Prop) : a p = b p := rfl  --fails

a and b are not definitionally equal because the first uses LinearOrder.toDecidableEq and the DecidableEq Prop instance is just Classical.propDecidable, while the second uses instDecidableEqOfIff on instDecidableIff with a non-Classical instDecidableTrue. (See Mathlib/RingTheory/Norm/Transitivity.lean for a real-world example).

My questions are:

• Is this an issue to be fixed?
• Should we make the instance scoped under Classical? Note that doing this works with open scoped Classical in ... but might not work with the classical tactic, in that writing classical might not make LinearOrder Prop available, because classical only adds docs#Classical.propDecidable which alone does not infer LinearOrder Prop because docs#Lattice.toLinearOrder is a non-instance.