Zulip Chat Archive

Stream: std4

Topic: Std simp-nf decide props


James Gallicchio (Jan 22 2023 at 16:51):

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 (Jan 22 2023 at 16:56):

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 (Jan 22 2023 at 17:00):

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

James Gallicchio (Jan 22 2023 at 17:03):

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 (Jan 22 2023 at 17:05):

& 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 (Jan 22 2023 at 17:24):

Std is not optimizing for its own proofs

Mario Carneiro (Jan 22 2023 at 17:25):

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

Mario Carneiro (Jan 22 2023 at 17:26):

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

Mario Carneiro (Jan 22 2023 at 17:26):

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


Last updated: Dec 20 2023 at 11:08 UTC