Std simp-nf decide props

Stream: std4

[James Gallicchio]

while moving List.Pairwise to Std I got caught by this simp issue:

-- in current Std:
example {P} [Decidable P] : ¬ (decide ¬P) = true → P := by
  simp -- unsolved goal: ¬¬P → P

-- the simp set used in mathlib4:
example {P} [Decidable P] : ¬ (decide ¬P) = true → P := by
  simp only [decide_not, Bool.not_eq_true', decide_eq_false_iff_not, Classical.not_not, imp_self]

-- the constructive simp set:
example {P} [Decidable P] : ¬ (decide ¬P) = true → P := by
  simp only [decide_not, Bool.not_eq_true, Bool.not_eq_false', decide_eq_true_iff, imp_self]

would it be okay for us to add a simp lemma of the form [Decidable P] -> ¬¬P <-> P? or would that interfere with mathlib4 simp normal form?

[James Gallicchio]

Is the goal with Std simp-normal form to push everything into proposition world, and then rely on re-deriving Decidable (some complicated proposition) to apply classical simplifications like not_not?

[Mario Carneiro]

you should just use not_not as a local or file-local simp lemma

[James Gallicchio]

It feels doable for Std simp to generate constructive proofs of stuff like this. But I guess that would require a pretty broad rework of both Std and Mathlib simp lemmas.

[James Gallicchio]

& if we're not shooting for that, then I would probably suggest just marking not_not simp in Std. It feels very odd that this goal isn't closed by no-arg simp.

[Mario Carneiro]

Std is not optimizing for its own proofs

[Mario Carneiro]

it's not a global simp lemma because the mathlib simp lemma overrides it

[Mario Carneiro]

if there is a way to add this lemma without regressing mathlib simp, great

[Mario Carneiro]

but if the only issue is that it makes std proofs harder that's a non-goal