is `push_neg` classical?

Stream: new members

[Chris M]

Does push_neg tactic implicitly use the classical library? e.g. intuitionistically we can't prove \exists x, P x from neg \forall x, \neg P x, but this is what push_neg seems to do, is that right?

[Mario Carneiro]

yes

[Patrick Massot]

Of course it's classical! It was written for mathematics teaching.

[Anatole Dedecker]

Patrick Massot said:

Of course it's classical! It was written for mathematics teaching.

Now I'm wondering, how many of mathlib's tactics come from this course ?

[Patrick Massot]

Not so many. I think choose, contrapose, push_neg, apply_fun and rename_var are the only ones.

[Kevin Buzzard]

contrapose and push_neg allow mathematicians to do classical logic without having to learn logic.basic so they are really useful in practice, and choose allows them to apply the axiom of choice without having to deal with classical.some, so we can see a theme here: they're making an interface which mathematicians are familiar with. It was surprising how many mathematicians come here asking for apply_fun. Of course you can do it in Lean, but mathematicians can never work out why the apply command doesn't do it, because that's their mental model.

[Kevin Buzzard]

@Chris M you can check yourself that the axioms are being used:

import tactic

def test (P : ℕ → Prop) (h : ¬ ∀ x, ¬ P x) : ∃ x, P x :=
begin
  push_neg at h,
  exact h
end

#print axioms test
/-
propext
classical.choice
quot.sound
-/

[Anatole Dedecker]

Kevin Buzzard said:

It was surprising how many mathematicians come here asking for apply_fun. Of course you can do it in Lean, but mathematicians can never work out why the apply command doesn't do it, because that's their mental model.

Fun fact : in the exam, Patrick forgot to import apply_fun, and most people were stuck on an easy exercise about injectivity/surjectivity because they didn't know how to get x = y -> f x = f y without using it

[Patrick Massot]

In my defense, everything was doable without apply_fun or congr_whatever. But one of the main difficulties of teaching using Lean is that you never know which twisted path the students will try to explore (and get stuck because you didn't explain or didn't import something needed for this twisted path).

[Anatole Dedecker]

Of course :laughing:

[Chris M]

Is there a tutorial that introduces apply_fun? #mil doesn't seem to (based on a search through it).

[Anatole Dedecker]

https://leanprover-community.github.io/mathlib_docs/tactics.html#apply_fun

[Chris M]

Yes I have seen it, I was just wondering if there is a more extensive tutorial showing when people use it.