push_neg doesn't simplify fully

Stream: mathlib4

[Gareth Ma]

In the lemma below, applying push_neg twice changes the goal, whereas I would assume that push_neg returns a canonical "pushed neg" form. Is my assumption false or is this a bug?

import Mathlib.Combinatorics.SimpleGraph.Hasse
import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Data.PNat.Prime

open SimpleGraph

def divisibilityGraph : SimpleGraph ℕ where
  Adj a b := (a ≠ b) ∧ ((a ∣ b) ∨ (b ∣ a))
  symm _ _ h := ⟨h.left.symm, h.right.symm⟩
  loopless a ha := ha.left $ refl a

example {p q : ℕ} (hp : p.Prime) (hq : q.Prime) : ¬ ⟦(p, q)⟧ ∈ divisibilityGraph.edgeSet := by
  rw [mem_edgeSet, divisibilityGraph]
  /- ⊢ ¬Adj (mk fun a b => a ≠ b ∧ (a ∣ b ∨ b ∣ a)) p q -/
  push_neg
  /- ⊢ ¬(p ≠ q ∧ (p ∣ q ∨ q ∣ p)) -/
  push_neg
  /- ⊢ p ≠ q → ¬p ∣ q ∧ ¬q ∣ p -/
  sorry

[Patrick Massot]

This is definitely a bug.

[Ruben Van de Velde]

Hmm, I'm surprised push_neg eliminates the Adj at all

[Gareth Ma]

I assume that wrapping the tactic core with repeat is not the correct fix, since this indicates something wrong with the algorithm?

[Gareth Ma]

Ruben Van de Velde said:

Hmm, I'm surprised push_neg eliminates the Adj at all

I don't know how the tactic works, but the source code indicates it uses simp to some degree, which can probably unfold the Adj - indeed simp only does unfold Adj

[Patrick Massot]

Unfolding Adj is definitely not part of the spec. The Lean 3 implementation was not using simp at all, but the Lean 4 port took a shortcut.

[Kyle Miller]

The existing simp configuration that push_neg uses probably should be reviewed more carefully, but setting it not not unfold projections was enough for this example: #7989