push_neg.use_distrib in bounded existential

Stream: mathlib4

[Patrick Massot]

I think that

import Mathlib.Tactic

example (h : ¬ (∃ x ∈ (Set.univ : Set ℕ), 0 < x)) : True := by
  set_option push_neg.use_distrib true in
  push_neg at h
  trivial

is an unintended corner case where the use_distrib option should not have any effect. This didn’t happen in Lean 3 because bounded existential were encoded differently. I suspect not many people care about this option. Maybe @Heather Macbeth? But I thought I would ask here before working on a fix anyway.

[Eric Wieser]

What would you expect the effect on ∃ x, x ∈ s ∧ x ∈ t to be? I think for the effect you want, we need the exists elaborator to record using Expr.mdata when an And was generated from a binder

[Eric Wieser]

... or revert to the lean 3 design that encoded this by using an inner Exists

[Patrick Massot]

Eric Wieser said:

What would you expect the effect on ∃ x, x ∈ s ∧ x ∈ t to be? I think for the effect you want, we need the exists elaborator to record using Expr.mdata when an And was generated from a binder

I’ll be happy with negating it to ∀ x ∈ s, x ∉ t. And really I’m not looking a super tight answer, this is purely for teaching purposes where the situation that arise are almost entirely under my control.

[Johan Commelin]

One thing I noticed again recently is how push_neg handles negations of And:

import Mathlib

example (P Q : Prop) (h : ¬ (P ∧ Q)) : P → ¬ Q := by
  push_neg at h -- `P → ¬ Q` instead of `¬ P ∨ ¬ Q`
  exact h

Which is not what my students were expecting after I taught them De Morgan.

@Patrick Massot Do you have a particular reason for moving to the implication (and breaking symmetry a bit)?

[Eric Wieser]

@Johan Commelin, that behavior is what set_option push_neg.use_distrib true changes

[Patrick Massot]

Yes, this is precisely the topic of this discussion. And I didn’t change that. I think Yury did, if I remember correctly.

[Patrick Massot]

push_neg started as a teaching tactic and was clearly implementing de Morgan laws. But then people started to find it useful for Mathlib itself and switched to the new behavior. Then I protested that it made it less useful for teaching and the option was introduced.

[Johan Commelin]

Aaah, I didn't realize that this was also in scope of use_distrib!
All the talk about existentials made me think it was only about that.

[Johan Commelin]

Do you think we could have push_neg +distrib?

[Patrick Massot]

It’s exactly the same thing. Negating ∃ x > 0, P x brings you to negating x > 0 ∧ P x.

[Patrick Massot]

Johan Commelin said:

Do you think we could have push_neg +distrib?

Yes, we could definitely have that. But I don’t really care because I want to take that decision on behalf of my students, and hide it (it’s obviously hidden in Verbose Lean, but you can also choose to hide it using almost vanilla tactics).