push_neg without \not?

Stream: new members

[George Tsoukalas]

Hi,

I was experimenting with push_neg and I am a bit confused. If I give an example of the form

example : ¬ (∃ n : ℕ, n > 0) := by push_neg

Lean has no problem pushing the negation through towards the center of the statement. But if I instead write

example : (∃ n : ℕ, n > 0) → False := by push_neg

push_neg makes no progress. Even though, to my knowledge, the two statements are definitionally equivalent? How can I rewrite this example to include a negation symbol?

[Kyle Miller]

They're defeq, but just like simp and rw, it acts on the syntactical form of the expression. The definition docs#Not needs to be unfolded to see the defeq. We could modify push_neg to recognize -> False as being equivalent to Not (and have it normalize it to Not as well).

Barring that, you can use docs#imp_false