## Stream: new members

### Topic: example : ¬ (∀ x, ¬ p x) → (∃ x, p x)

#### Eduardo Cavazos (Nov 04 2019 at 08:40):

Question posted to stackoverflow:

https://stackoverflow.com/q/58689716/268581

#### Eduardo Cavazos (Nov 04 2019 at 08:43):

In a previous question about these exercises, Johan had suggested using import tactic to autogenerate a solution. However, I'd like to use that as a last resort as it will pretty much give me a direct answer (although perhaps somewhat obfuscated compared to what a reader of TPIL is expected to come up with).

I'd like to try a few approaches on my own before taking a look at what the autogenerated solution does.

#### Eduardo Cavazos (Nov 04 2019 at 08:43):

Thank you for any suggestions!

#### Mario Carneiro (Nov 04 2019 at 08:45):

You don't need the global variable a. It's a red herring here because you shadowed it with another variable called a leading to the confusion at the end

#### Mario Carneiro (Nov 04 2019 at 08:46):

Try to prove ∃ x, p x by contradiction

#### Eduardo Cavazos (Nov 04 2019 at 08:46):

@Mario Carneiro OK cool. So then I'll somehow need access to the 'x'?

#### Mario Carneiro (Nov 04 2019 at 08:47):

You need to produce a proof of false, and do as you did, applying the assumption ¬ (∀ x, ¬ p x)

#### Mario Carneiro (Nov 04 2019 at 08:47):

this gives you access to x and a proof that p x

#### Eduardo Cavazos (Nov 04 2019 at 08:51):

The only way I can see to create a false is to make a (∀ x, ¬ p x) for use with hnAxnpx, but that requires x so I'm back to square one. ;-)

#### Eduardo Cavazos (Nov 04 2019 at 09:06):

Trying something...

#### Eduardo Cavazos (Nov 04 2019 at 09:17):

Based on the above discussion, I tried the following:

example : ¬ (∀ x, ¬ p x) → (∃ x, p x) :=
(assume hnAxnpx : ¬ (∀ x, ¬ p x),
false.elim (hnAxnpx
(λ x,
(λ hpx : p x, _)))) -- Here we'll need a false.


#### Eduardo Cavazos (Nov 04 2019 at 09:17):

As that gets me an x and p x.

#### Eduardo Cavazos (Nov 04 2019 at 09:18):

However, at that point, it isn't clear to me how to get a false value at the point of the underscore.

#### Mario Carneiro (Nov 04 2019 at 09:36):

Don't use false.elim where you did; that's throwing away the information that we are trying to prove (∃ x, p x) and leads to an unsolvable state

#### Mario Carneiro (Nov 04 2019 at 09:37):

Use by_contradiction there instead, which gives you additionally the assumption that ¬ (∃ x, p x)

#### Eduardo Cavazos (Nov 04 2019 at 17:58):

@Mario Carneiro Ahhhhhhhhh!!!

#### Eduardo Cavazos (Nov 04 2019 at 17:59):

example : ¬ (∀ x, ¬ p x) → (∃ x, p x) :=
(assume hnAxnpx : ¬ (∀ x, ¬ p x),
(λ hnExpx : ¬ (∃ x, p x),
(hnAxnpx
(λ x, (λ hpx,
hnExpx (exists.intro x hpx))))))


Thank you!!!

#### Johan Commelin (Nov 04 2019 at 18:19):

@Eduardo Cavazos Here's a tactic mode proof that doesn't just kill it with automation.

import tactic
universe variable u
open_locale classical
variables {X : Type u} (p : X → Prop)

example : ¬ (∀ x, ¬ p x) → (∃ x, p x) :=
begin
contrapose!,
exact id,
end


#### Johan Commelin (Nov 04 2019 at 18:19):

https://leanprover-community.github.io/lean-web-editor/#code=import%20tactic%0A%0Auniverse%20variable%20u%0A%0Aopen_locale%20classical%0A%0Avariables%20%7BX%20%3A%20Type%20u%7D%20%28p%20%3A%20X%20%E2%86%92%20Prop%29%0A%0Aexample%20%3A%20%C2%AC%20%28%E2%88%80%20x%2C%20%C2%AC%20p%20x%29%20%E2%86%92%20%28%E2%88%83%20x%2C%20p%20x%29%20%3A%3D%0Abegin%0A%20%20contrapose!%2C%0A%20%20exact%20id%2C%0Aend%0A

#### Mario Carneiro (Nov 04 2019 at 18:24):

of course, contrapose is using a lemma that basically repeats this statement

Sure...

#### Johan Commelin (Nov 04 2019 at 18:29):

Isn't it wonderful that other people have taken care of this? So that we can just focus on the essential verb in this proof?

#### Johan Commelin (Nov 04 2019 at 18:30):

I like this version even better:

import tactic
universe variable u
open_locale classical
variables {X : Type u} (p : X → Prop)

example (h : ¬ (∀ x, ¬ p x)) : (∃ x, p x) :=
begin
contrapose! h,
assumption,
end


#### Rob Lewis (Nov 04 2019 at 18:39):

Isn't it wonderful that other people have taken care of this?

That depends what your goal is! If you're trying to learn how to "take care of" more things than just this, calling a bunch of tactics doesn't teach you anything. You're stuck as soon as you get to something that contrapose doesn't do and you're even more stuck if you want to write something like contrapose.

Fair enough

#### Rob Lewis (Nov 04 2019 at 18:44):

I get that sometimes it's pedagogically better to introduce the big (or medium) guns and avoid the details. That's fine, it has its place. But for little logic exercises like this, it's like telling a schoolkid to use a calculator when they're learning to add.

#### Kevin Buzzard (Nov 04 2019 at 18:47):

On the other hand Johan and I are both reflecting a mathematician's attitude here -- "who cares how it works, it's true, move on" and as a mathematician it is important to learn this attitude -- don't stress about the details.

#### Kevin Buzzard (Nov 04 2019 at 18:47):

The CS people just find this stuff more intrinsically beautiful I think.

#### Kevin Buzzard (Nov 04 2019 at 18:49):

I have written papers about objects whose definitions I do not know e.g. https://arxiv.org/abs/1009.0785 . I don't know the definition of an automorphic representation. But I know how they work.

#### Rob Lewis (Nov 04 2019 at 18:49):

Kevin, when you teach calculus, do you teach the chain rule, product rule, etc, or do you just point to the calculator?

#### Kenny Lau (Nov 04 2019 at 18:49):

Kevin does not teach calculus :P

#### Kevin Buzzard (Nov 04 2019 at 18:50):

I'm not sure a calculator would help, but when teaching it to people seeing the maths for the first time, I go through the proofs. Once. And then we expect the students to know that the proofs are there, and we don't ever revisit them.

#### Kevin Buzzard (Nov 04 2019 at 18:51):

And we spend the next 3 years just rewriting and not caring about how the proofs go -- indeed I am fairly confident that there will be 3rd year students who have forgotten how the proofs go and they are not at all bothered by this because they know it will not come up in the exam. Proofs are irrelevant.

#### Rob Lewis (Nov 04 2019 at 18:52):

I'm not talking about the proofs, I'm talking about computing a derivative. What's the derivative of sin^2(3*cos(x^4/5))? The TI83 will tell you, but at least in US high school calc courses (which I've taught), you spend time doing things like that by hand.

#### Kevin Buzzard (Nov 04 2019 at 18:52):

I think this is a genuine difference in our disciplines. You need to worry about what's going on because you don't want to create a term of size $10^{10}^{10}$. We don't have these problems so don't need to worry about what's holding it all together.

#### Kevin Buzzard (Nov 04 2019 at 18:53):

You only spend time doing it by hand in your first year at university.

#### Rob Lewis (Nov 04 2019 at 18:53):

And you do that for a reason!

#### Rob Lewis (Nov 04 2019 at 18:53):

Because if you didn't, the students would have less of a grasp on how derivatives work.

#### Kevin Buzzard (Nov 04 2019 at 18:54):

But what I'm saying is that after a while it doesn't matter how they work because nobody would ever actually ever be faced with a problem like yours

#### Kevin Buzzard (Nov 04 2019 at 18:54):

We reason, we don't compute, so leave the computing to the computers.

#### Rob Lewis (Nov 04 2019 at 18:57):

But you need to know what you're reasoning about. And computing derivatives by hand teaches students something about derivatives. It doesn't matter if they forget how to compute with them later, because indeed there are computers to do that. (Although if they learn well enough it's faster to do small ones by hand.) It's about learning the concept. Same thing here. I generally don't do little logic puzzles by hand, although occasionally it's faster than finding the right combo of tactics. And teaching people to just blast things away can be okay, depending on what you want them to do later -- maybe engineers can just use their calculator. But if you only learn black box tools then you're stuck as soon as you get somewhere those tools don't reach.

#### Kevin Buzzard (Nov 04 2019 at 18:57):

That's when I ask you to make more tools ;-)

#### Rob Lewis (Nov 04 2019 at 18:59):

Maybe @Eduardo Cavazos is the next person to make those tools. Using contrapose and tauto blindly on the exercises wouldn't be very helpful then.

#### Rob Lewis (Nov 04 2019 at 18:59):

And again, these are literally logic exercises we're talking about.

#### Kevin Buzzard (Nov 04 2019 at 19:00):

Perhaps it's different in CS than in maths. How do we find a question which is much more difficult than your derivative question. Well, we could just make it ten times longer and use more of the buttons on a calculator. But this is exactly the situation where one would want to use a tactic. But what about adding in other functions not on the calculator, or introducing some other layer of complexity...but actually I don't really see how to do this. On the other hand in CS it's really easy to see how to do this, just make a new type and make things a bit different and then the tools fail and you're going to have to know what you're doing again. Maybe the complexity somehow grows in a different way.

#### Kevin Buzzard (Nov 04 2019 at 19:00):

Maybe I am incorrectly interpolating a mathematician's attitude into a dangerous situation where you are convinced it does not apply.

#### Rob Lewis (Nov 04 2019 at 19:03):

I don't think this has anything to do with a CS/math attitude difference. Would you tell a 5 year old learning addition to just use a calculator? If you're going to insist that literally everything that can be computed is trivial and not worth learning, then yeah, let's call it an attitude difference. But somehow I doubt that.

#### Rob Lewis (Nov 04 2019 at 19:04):

Not everyone can ignore the fundamentals. Directing people away from fundamental techniques, when they're doing problems that are designed to teach the fundamentals, is just wrong.

#### Johan Commelin (Nov 04 2019 at 19:05):

example : (¬ (∀ x, ¬ p x)) → (∃ x, p x) :=
not_not.mp ∘ (not_iff_not.mpr not_exists).mpr


#### Kevin Buzzard (Nov 04 2019 at 19:06):

I don't think this has anything to do with a CS/math attitude difference. Would you tell a 5 year old learning addition to just use a calculator? If you're going to insist that literally everything that can be computed is trivial and not worth learning, then yeah, let's call it an attitude difference. But somehow I doubt that.

Do you know what Rob? I would seriously consider telling some 5 year olds learning addition to use a calculator. More and more I am questioning why we teach humans to do anything which tools can do. I had several miserable years of trying to teach my daughter her times tables and after a while I really started questioning what the whole point of it all was, given that she had a phone when she was 10 years old and the phone had a calculator on it and the calculator could do all the multiplications she was being asked. I am very confused about why society thinks it's a good idea to teach everyone how to do basic things which they have a tool in their pocket which does it better.

#### Rob Lewis (Nov 04 2019 at 19:06):

Equally illegible, but I bet the process of writing that is more enlightening than writing by contrapose!; assumption!

#### Kevin Buzzard (Nov 04 2019 at 19:08):

Humans which actively want to learn -- fair enough. But I don't care about the algorithm ring uses, all I know is that it works.

#### Eduardo Cavazos (Nov 04 2019 at 19:10):

I'm not talking about the proofs, I'm talking about computing a derivative. What's the derivative of sin^2(3*cos(x^4/5))? The TI83 will tell you, but at least in US high school calc courses (which I've taught), you spend time doing things like that by hand.

Not to go off on a tangent (ha!) but to compute it symbolically, I think you'd need a TI-89 which has CAS. (As far as I know, the TI-83 does not have a CAS).

#### Rob Lewis (Nov 04 2019 at 19:10):

That's totally fair. I'm not sure if I agree about multiplication, but I'd say the same thing about calculating derivatives, for some people. But not for everyone. And if someone came to me with a times table sheet I wouldn't hand them a calculator instead.

#### Rob Lewis (Nov 04 2019 at 19:11):

If someone came to me with an engineering problem set, I'd totally tell them to use a calculator. For both the multiplication and the derivatives.

#### Rob Lewis (Nov 04 2019 at 19:11):

Not to go off on a tangent (ha!) but to compute it symbolically, I think you'd need a TI-89 which has CAS. (As far as I know, the TI-83 does not have a CAS).

Hah, fair enough. It's been a long time!

#### Marc Huisinga (Nov 04 2019 at 19:12):

in my opinion, you at least need to make students believe that they understand the inner workings of things, to the degree that they are confident at the level of abstraction they work on. if they feel like something important is being hidden from them, they will not feel confident in their arguments and their work, and as far as i can tell building this confidence is very important.

touching on the inner workings of things is a good way to do this, but it is obviously not always necessary: you can educate math students in a way where they will be confident in their arguments without a class on ZFC. and perhaps more importantly, they will not always have to consider the inner workings - as with the calculus example, knowing that you verified them at some point in the past is good enough to build the necessary confidence.

but perhaps the level of abstraction that you work on when using a theorem prover is just inherently lower than doing math on paper right now. sure, the dream is that the theorem prover exactly models how a mathematician thinks, but we're certainly still far away from that goal.

that is not to say that stuff like the natural number game aren't great ways to get mathematicians interested in lean - i absolutely admire that approach!

#### Kevin Buzzard (Nov 04 2019 at 19:12):

The difference with our students is that they have actually chosen to learn this stuff. My daughter would definitely not have chosen to learn times tables, and I definitely choose not to learn the Gregoire-Mahboubi algorithm, however I will concede that it's supremely important that there are people around who know it!

#### Kevin Buzzard (Nov 04 2019 at 19:13):

@Marc Huisinga that's an interesting point. I don't care about the G-M algorithm but on the other hand I know how to use the axioms of a ring and am convinced that I could in theory prove anything which ring does using them.

#### Mario Carneiro (Nov 04 2019 at 19:14):

@Johan Commelin The library solution is this:

local attribute [instance] classical.dec

example : (¬ (∀ x, ¬ p x)) → (∃ x, p x) := not_forall_not.1


#### Kevin Buzzard (Nov 04 2019 at 19:14):

Aren't we supposed to put priority 10 or something?

#### Johan Commelin (Nov 04 2019 at 19:15):

@Mario Carneiro That shows how well I know this part of the library

#### Mario Carneiro (Nov 04 2019 at 19:16):

I contemplated writing

example : (¬ (∀ x, ¬ p x)) → (∃ x, p x) :=
by classical; exact not_forall_not.1


but this opens its own questions about tactic magic

#### Rob Lewis (Nov 04 2019 at 19:16):

For the times tables, I trust that the educational theorists who keep them in the curriculum know what they're doing. (Possibly misplaced trust there.) There's constant background noise about taking them out or changing the way they're taught or whatever. I dunno, when I taught high school my students knew how to multiply small numbers, so they weren't gone yet.

#### Marc Huisinga (Nov 04 2019 at 19:17):

i suppose that it's also easier to be convinced by experts when you've got lots of experience with doing maths yourself and have already seen many similar approaches. (i am reminded of https://terrytao.wordpress.com/career-advice/theres-more-to-mathematics-than-rigour-and-proofs/)

#### Mario Carneiro (Nov 04 2019 at 19:18):

There is obviously a place where you don't use ring, namely the class called "algebra 1" in US (7th - 8th grade)

#### Mario Carneiro (Nov 04 2019 at 19:19):

you make people work out Algebra with Letters and teach them about Distribution and teach them to simplify polynomial expressions

#### Eduardo Cavazos (Nov 04 2019 at 19:24):

In an undergraduate physics class (mechanics, newton's law, etc) and some engineering courses, often you'll have an exercise which will involve taking a set of equations and eliminating variables until it's in terms of values that you know. A CAS (TI-89, Mathematica, etc.) can help you with computing derivatives symbolically and even isolating some variables given an equation. What isn't quite there yet however is eliminating variables across a set of non-linear equations (i.e. they may involve trig functions, powers greater than one, etc).

Mathematica can kind of handle some of these cases with its Reduce function (which I heard uses cylindrical algebraic decomposition under the hood). But it gets pretty slow even on examples that would come up in an undergraduate course.

So for a physics class, how much calculator should be used? I think the critical piece is for the student to be able to identify which equations are applicable, based on the goal and the information they have. Moving the symbols around isn't important and so if they had a sufficiently powerful Reduce, it's OK for it to be used.

This is of course assuming that they've done a few examples by hand. Doing 100s of the same computation by hand is likely not helpful (and this is sometimes what happens in these courses!)

I've worked on a (very simple) computer algebra library for C#. Here's a simple physics problem solved in it using the above described approach (i.e. pick the right equations, but let the computer do the equation manipulation and variable elimination for you).

So on the one hand, I'm a big fan of using a calculator; but for my taste, it is to be used once you know what it's doing. That's for me personally. Everyone has their personal threshold of abstraction beyond which they don't need to descend.

#### Kevin Buzzard (Nov 04 2019 at 19:24):

I want to take the contentious position that if students don't want to learn how to do algebra with letters, you should just teach them to run ring. As Rob says though, the educational theorists don't seem to agree with me. Maybe you can't trust what people want :-/

#### Mario Carneiro (Nov 04 2019 at 19:33):

I think the time you teach people ring is when it stops being difficult and starts being tedious

#### Johan Commelin (Nov 04 2019 at 19:36):

Mathematicians think formalisation is tedious... physicists think mathematics is tedious...

#### Johan Commelin (Nov 04 2019 at 19:36):

Anyway... let's do some maths (-;

#### Daniel Keys (Feb 01 2020 at 16:12):

Still new to chapter 4 in TPiL, although I went through chapter 5. Trying to do this same proof in tactic mode, which is more intuitive for me, but I need some help. Here is the proof term built explicitly, together with my attempt at using tactic mode:

theorem T06_1 : ¬ (∀ x, ¬ p x) → (∃ x, p x) :=
(assume hnAxnpx : ¬ (∀ x, ¬ p x),
(λ hnExpx : ¬ (∃ x, p x),
(hnAxnpx
(λ x, (λ hpx,
hnExpx (exists.intro x hpx))))))
#check T06_1
-- it appears this is needed in tactic mode
local attribute [instance] classical.prop_decidable
theorem T06_2 : ¬ (∀ x, ¬ p x) → (∃ x, p x) :=
begin
intro hnAxnpx,
by_contradiction, -- introduces a_1 : ¬∃ (x : α), p x
-- but I don't find a way to use it (intro does not work)
end


At this point I'm not sure why I can't grab the extra hypothesis. How can this proof in T06_2 be completed?

#### Patrick Massot (Feb 01 2020 at 16:18):

There is nothing to intro, you are trying to prove false

#### Patrick Massot (Feb 01 2020 at 16:18):

You need to use something that produces false aka a negation.

#### Patrick Massot (Feb 01 2020 at 16:19):

You should have two of them in your context. One is created by by_contradiction, but applying it would be going back.

#### Kenny Lau (Feb 01 2020 at 16:20):

variables {α : Type*} {p : α → Prop}
open classical

theorem T06_1 : ¬ (∀ x, ¬ p x) → (∃ x, p x) :=
assume hnAxnpx : ¬ (∀ x, ¬ p x),
(λ hnExpx : ¬ (∃ x, p x),
(hnAxnpx
(λ x, (λ hpx,
hnExpx (exists.intro x hpx)))))

local attribute [instance] classical.prop_decidable
theorem T06_2 : ¬ (∀ x, ¬ p x) → (∃ x, p x) :=
begin
intro hnAxnpx,
apply hnAxnpx,
intro x,
intro hpx,
apply hnExpx,
existsi x,
exact hpx
end


#### Patrick Massot (Feb 01 2020 at 16:20):

Kenny... I was trying to lead him gently.

#### Daniel Keys (Feb 01 2020 at 16:22):

This would not have worked! I didn't know that I could have something like by_contradiction hnExpx. So that's the 'intro' I was looking for; after that you can use it. Thank you both Kenny, Patrick!

#### Patrick Massot (Feb 01 2020 at 16:23):

Let's try to comment a bit on efficiency then. Note that Kenny's two lines of intro can be merged in one intros x hpx. The last two lines can also be merged into use [x, hpx]. Of course you could also merge with the previous line, but this clearly going towards a proof term.

#### Patrick Massot (Feb 01 2020 at 16:24):

This would not have worked! I didn't know that I could have something like by_contradiction hnExpx. So that's the 'intro' I was looking for; after that you can use it. Thank you both Kenny, Patrick!

This variation is only providing an explicit name you didn't provide (you wrote Lean chose a_1 instead of hnExpx).

#### Patrick Massot (Feb 01 2020 at 16:25):

While you're learning tactics, note also that, if you are using mathlib, you can do the proof by push_neg, tauto.

#### Daniel Keys (Feb 01 2020 at 16:28):

The intros part I already knew from the natural number game. The use of a_1 was kind of cryptic, I tried to use it (probably in a wrong way) but Lean would not allow me to work with it at all. Or maybe I should say I didn't know how to! There are so many aspects to Lean proofs.

I don't want to go to the more automatic tools yet. Not until I understand how all these basics work. It is so simple in your head, and sometimes you need hours to figure it out in Lean. But things are getting better. Slowly.

#### Patrick Massot (Feb 01 2020 at 16:29):

I mean you should go back to the attempt you posted, and try to finish it using what you understood from our explanations.

Oh, absolutely!

#### Patrick Massot (Feb 01 2020 at 16:32):

The intros part I already knew from the natural number game. The use of a_1 was kind of cryptic, I tried to use it (probably in a wrong way) but Lean would not allow me to work with it at all. Or maybe I should say I didn't know how to! There are so many aspects to Lean proofs.

I don't want to go to the more automatic tools yet. Not until I understand how all these basics work. It is so simple in your head, and sometimes you need hours to figure it out in Lean. But things are getting better. Slowly.

I think your main issue is not about knowing Lean tactics. It's about really internalizing that negation of a statement P is P -> false.

#### Daniel Keys (Feb 01 2020 at 16:38):

Maybe, or maybe not. We don't need to believe everything we think either! -:)

#### Daniel Keys (Feb 01 2020 at 20:09):

Here's the other direction, where again I'm not sure how to proceed:

theorem T06R : (∃ x, p x) → ¬ (∀ x, ¬ p x) :=
begin
intros hExpx H,
end


At this point H and hExpx are so obviously in contradiction...but I don't know how to manipulate them. My idea would be to obtain an x for which p x holds, then to contrast the not p from H to obtain the needed false. Tried using match (sec. 4.4 in TPiL) with no success. Any hint on how to move forward?

#### Bryan Gin-ge Chen (Feb 01 2020 at 20:16):

You can use rintro / rcases on existential hypotheses:

import tactic

variables (α : Type) (x : α) (p : α → Prop)

theorem T06R : (∃ x, p x) → ¬ (∀ x, ¬ p x) :=
begin
rintro ⟨x, hpx⟩ h,
exact h x hpx
end


It's short for this (which doesn't need the import):

variables (α : Type) (x : α) (p : α → Prop)

theorem T06R : (∃ x, p x) → ¬ (∀ x, ¬ p x) :=
begin
intros hExpx H,
cases hExpx with x hpx,
exact H x hpx,
end


#### Daniel Keys (Feb 01 2020 at 20:33):

I definitely should have known this already! Thanks!

Last updated: May 17 2021 at 22:15 UTC