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?

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: May 08 2021 at 20:11 UTC