push_neg is not confluent

Stream: general

[Johan Commelin]

This is probably a known issue.

import Mathlib

example (P Q : Prop) : ¬¬(P ∨ Q) ↔ ¬ (¬P ∧ ¬Q) := by
  push_neg
  fail_if_success rfl
  show P ∨ Q ↔ ¬P → Q
  tauto

This bit me because I tried to do

/--
error: Type mismatch
  h✝
has type
  a ≠ 0 → b = 0
but is expected to have type
  a = 0 ∨ b = 0
-/
example (a b : ℕ) : a ≠ 0 ∧ b ≠ 0 := by
  by_contra! (rfl | rfl) : a = 0 ∨ b = 0
  sorry

[Johan Commelin]

@Jovan Gerbscheid Do you have any ideas here?

[Johan Commelin]

Maybe, to #xy the by_contra! tactic shouldn't use push_neg but rather tauto?

[Jovan Gerbscheid]

This works:

import Mathlib

example (P Q : Prop) : ¬¬(P ∨ Q) ↔ ¬ (¬P ∧ ¬Q) := by
  set_option push_neg.use_distrib true in push_neg
  rfl

And once #31406 lands, you can write push_neg +distrib/by_contra! +distrib

[Yaël Dillies]

How would that make sense? It's not a closing tactic

[Jovan Gerbscheid]

It makes a little bit of sense for push_neg with a type annotation, for proving that the given type annotation matches the expected type. The current approach is to just push_neg in both and hope that they end up the same.

[Jovan Gerbscheid]

Do you think that by_contra! should use +distrib as the default?

[Johan Commelin]

What do you think of having it use tauto whenever the types don't line up?

[Jovan Gerbscheid]

Well I think that wouldn't really work because tauto is not aware of all push_neg theorems.

[Johan Commelin]

My question is rather why by_contra! should have anything to do with push_neg in the first place... :wink:

[Jovan Gerbscheid]

Well, by_contra! is the combination of by_contra and push_neg... Unless you want to put type annotations in every by_contra!, there is no other way.

[Johan Commelin]

Aah, so maybe I want tauto as a fall-back in the non-confluent cases?

[Johan Commelin]

Or maybe whenever the user gives a type annotation?

[Johan Commelin]

If the user gives a type annotation, there is an implicit claim that they have an idea of what the negation of the goal should look like. We should accomodate that, unless the claim is false.
tauto will do that, even when eg commutativity is needed.

[Jovan Gerbscheid]

Something like this should work

syntax "by_contra!_disch" ident : tactic
macro_rules | `(tactic| by_contra!_disch $h) => `(tactic| (try push_neg); exact $h)
macro_rules | `(tactic| by_contra!_disch $h) => `(tactic| tauto)

example (a b : ℕ) : a ≠ 0 ∧ b ≠ 0 := by
  by_contra h
  push_neg at h
  replace h : a = 0 ∨ b = 0 := by by_contra!_disch h

[Jovan Gerbscheid]

Oh wait, that will run tauto before running try push_neg); exact $h. But if we swap them, then we get the tauto error message instead of the error message that we want.

[Jovan Gerbscheid]

Ok, I think it would be reasonable to simply replace the exact h with tauto in the implementation of by_contra!. The only problem I see is that tauto gives a horribly useless error message: "tauto failed to solve some goals.". Instead, I'd like it to say that it couldn't solve the goal, and then print the goal.

[Johan Commelin]

Can that be solved by some try-catch?

[Jovan Gerbscheid]

If we just fix tauto to give a better error message, it should be fine, right?

[Johan Commelin]

That's the more principled approach :smiley:

[Patrick Massot]

Jovan Gerbscheid said:

It makes a little bit of sense for push_neg with a type annotation, for proving that the given type annotation matches the expected type. The current approach is to just push_neg in both and hope that they end up the same.

FYI, this is what I do in Verbose Lean as well.

[Bolton Bailey]

Perhaps this is related: I find it undesirable that docs#not_and is a simp lemma. Often this lemma turns a symmetrical expression into an unsymmetrical one and makes my InfoView harder to understand, I think I might prefer it more if docs#not_and_or were the lemma simp used here instead.

[Aaron Liu]

I definitely want ¬∃ x ∈ s, P x to be turned into ∀ x ∈ s, ¬P x instead of ∀ x, x ∉ s ∨ ¬P x

[Jovan Gerbscheid]

It is possible to add a push lemma ¬(∃ x, Q x ∧ P x) = ∀ x, Q x → ¬P x, and this would make your case still work as desired. (while also having not_and_or for bare conjunctions)