Contextual simp with reducible definitions

Stream: lean4

[Bhavik Mehta]

Consider the following pair of simp calls:

def foo (a b : Nat) : Prop := Nat.gcd a b = 1
@[reducible] def bar (a b : Nat) : Prop := Nat.gcd a b = 1

theorem test_foo : ∀ a b : Nat, foo a b → ¬ a = 0 → foo a b := by
  simp +contextual

theorem test_bar : ∀ a b : Nat, bar a b → ¬ a = 0 → bar a b := by
  simp +contextual

The first succeeds, but the second fails. To me, this is unexpected because I'd expect both to behave the same, in particular that the second simp +contextual should succeed. Is this known behaviour?

[Sebastian Ullrich]

The problem is that your prop is an equality, so simp assumes you want it to be used to rewrite any occurrence of Nat.gcd a b to 1. But then when trying to prove bar a b, it doesn't try to reduce that def and prove the underlying property instead; if it did, I think that would have other unwanted side effects, we avoid such unconditional unfoldings unless directed to do so by the user. IOW, simp +contextual [bar] is one solution.