# Zulip Chat Archive

## Stream: new members

### Topic: is `push_neg` classical?

#### Chris M (Jul 26 2020 at 11:31):

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 (Jul 26 2020 at 11:33):

yes

#### Patrick Massot (Jul 26 2020 at 11:59):

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

#### Anatole Dedecker (Jul 26 2020 at 12:07):

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 (Jul 26 2020 at 12:29):

Not so many. I think `choose`

, `contrapose`

, `push_neg`

, `apply_fun`

and `rename_var`

are the only ones.

#### Kevin Buzzard (Jul 26 2020 at 13:07):

`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 (Jul 26 2020 at 13:09):

@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 (Jul 26 2020 at 13:16):

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 (Jul 26 2020 at 13:26):

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 (Jul 26 2020 at 13:30):

Of course :laughing:

#### Chris M (Jul 26 2020 at 13:31):

Is there a tutorial that introduces `apply_fun`

? #mil doesn't seem to (based on a search through it).

#### Anatole Dedecker (Jul 26 2020 at 13:36):

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

#### Chris M (Jul 26 2020 at 13:37):

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

Last updated: Dec 20 2023 at 11:08 UTC