Why is not_and @[simp]?

Stream: new members

[Will Crichton]

It's quite annoying that ¬(a ∧ b) rewrites to a → ¬b automatically, since sometimes I want to rely on the commutativity of ∧ but that detail gets lost in this rewrite. Of course I can disable it with -not_and, but is there a more general rule governing which facts are marked as @[simp] or not?

[Richard Osborn]

One explanation for this would be when writing theorems, we write them curried:

variable {P Q R : Prop}

theorem foo (hp : P) (hq : Q) : ¬ R := by
  sorry

#check (foo : P → Q → ¬ R)

-- instead of
theorem bar : ¬ ((P ∧ Q) ∧ R) := by
  sorry

example : (P → Q → ¬ R) ↔ ¬ ((P ∧ Q) ∧ R) := by
  rw [not_and, and_imp] -- or just simp

This means most theorems will match the form a → ¬b over ¬(a ∧ b). As for why this is helpful see the documentation on simp-normal forms.

[Timo Carlin-Burns]

Does docs#imp_not_comm help here?

example (h : ¬ (P ∧ Q)) : ¬ (Q ∧ P) := by
  rw [not_and] at h ⊢
  rw [imp_not_comm]
  exact h