push_neg failure

Stream: general

[Kevin Buzzard]

import tactic

open function

example : ¬ (∀ (X Y Z : Type) (f : X → Y) (g : Y → Z),
  injective (g ∘ f) → injective g) :=
begin
  push_neg, -- error
end

I was hoping it would do _something_ (this is for teaching purposes). repeat {simp_rw not_forall} makes a lot of progress but also completely screws up all the variable names :-(

[Patrick Massot]

This looks like a bug in push_neg

[Kevin Buzzard]

My workaround for now is to just not teach the proof :-)

[Patrick Massot]

Another workaround it to remove the quantifier on X Y Z and replace them all by nat for instance.

[Patrick Massot]

The issue is only with this quantifier over X Y Z.

[Patrick Massot]

And this bug is above my pay grade. It seems to be a problem with the part that I blindly copied from @Jeremy Avigad 's finish tactic.

[Eric Wieser]

src#tactic.interactive.push_neg for those looking to debug

[Patrick Massot]

Patrick Massot said:

Another workaround it to remove the quantifier on X Y Z and replace them all by nat for instance.

I have an extremely evil example for you. I'll let you the pleasure of finishing the proof in three lines:

example: ¬ (∀  (f : ℕ → ℕ) (g : ℕ → ℕ),
  injective (g ∘ f) → injective g) :=
begin
  push_neg,
  refine ⟨λ x, x + 1, λ x, x - 1, _, _⟩,
  sorry
end

[Kevin Buzzard]

Crap, I accidentally finished it in two lines:

begin
  push_neg,
  refine ⟨λ x, x + 1, λ x, x - 1, _, _⟩,
    tauto,
  use [0, 1, rfl],
end

[Damiano Testa]

While we are with this, I found the solution below, but now I do not understand how use can simply finish the proof with rfl, while I need to tell refine explicitly about zero_ne_one. I thought that use and refine ⟨_, _⟩ we very similar...

example: ¬ (∀  (f : ℕ → ℕ) (g : ℕ → ℕ),
  injective (g ∘ f) → injective g) :=
begin
  push_neg,
  refine ⟨λ x, x + 1, λ x, x - 1, _, _⟩,
  exact λ x y xy, xy,
  exact ⟨0, 1, rfl, zero_ne_one⟩,
end

[Riccardo Brasca]

The doc for use says "Similar to existsi. use x will instantiate the first term of an ∃ or Σ goal with x. It will then try to close the new goal using triv, or try to simplify it by applying exists_prop". Indeed

example: ¬ (∀  (f : ℕ → ℕ) (g : ℕ → ℕ),
  function.injective (g ∘ f) → function.injective g) :=
begin
  push_neg,
  refine ⟨λ x, x + 1, λ x, x - 1, _, _⟩,
  exact λ x y xy, xy,
  use [0, 1],
  split,
  refl,
  triv,
end

works.

[Kevin Buzzard]

@Damiano Testa If reading the docstring of the tactic is not your style, you can right click on the tactic and look at the code defining it and actually see what it's doing! In the case of use (the user tactic, a.k.a. tactic.interactive.use) you can see that it first runs the more "primitive" tactic.use and then it tries triv.

[Patrick Massot]

tauto doing the injectivity on its own is a pleasant surprise. Riccardo and Damiano, you can also use exact ⟨0, 1, rfl, dec_trivial⟩ for the last line.

[Patrick Massot]

By really, the point of this example is that subtracting one is not injective :smiling_devil:

[Kevin Buzzard]

With goals like that I try hint nowadays, and it basically tries all the power tactics and tells you which ones work. The first one it suggests is ring_nf. I don't really understand why it suggests this because it doesn't seem to close the goal. It points out that finish also works though.

[Eric Rodriguez]

I was writing a thing earlier where I had functions to fin k and was incredibly confused why I couldn't find a proof that fin (k - 1 + 1) = fin k. It took me an embarrasingly long amount of time to realize...

[Eric Rodriguez]

Thankfully it's one of those things that bite you once and it shocks you so much, that you don't let it bite you again

[Riccardo Brasca]

I think the general principle is that to do math we should avoid to use functions that are only partially defined mathematically (except probably division in a field). If you need subtraction then go to Z.

[Damiano Testa]

Thank you all for the explanations! It is true that I never think of looking at the doc-strings for tactics. I also do not feel that I could understand the implementation: maybe the time has come to dive into that!

[Frédéric Le Roux]

(deleted)