decide vs Decidable.to_bool

Stream: mathlib4

[Chris B]

Is the motivation for having a separate Decidable.to_bool in addition to the prelude's Decide.decide something to do with the @[inlineIfReduce, nospecialize] attributes in core? Which one should users favor when writing lemmas and why?

[Chris B]

Also is there a downside to making decide_eq_true_iff and decide_eq_false_iff_not simp lemmas?

[David Renshaw]

It looks like I was the one who added Decidable.to_bool, in https://github.com/leanprover-community/mathlib4/pull/34

[David Renshaw]

The idea was to mechanically copy things over from the Lean3 prelude.

[David Renshaw]

https://github.com/leanprover-community/lean/blob/234e981cebe77b51f8dc8ffce281dd2819695243/library/init/logic.lean#L597

[Chris B]

I see. Do you know whether the plan is to eventually harmonize with changes in Lean 4 core (like removing to_bool in favor of the prelude's decide) or is that going to be subordinate to the desire to not have to change mathlib3 stuff?

[Mario Carneiro]

If there is a defeq matching, we should align to the lean 4 definition when possible

[Mario Carneiro]

which means that translated files will sometimes have some items omitted

[Chris B]

Ok thanks, I made a PR.