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

Stream: new members

[Eduardo Cavazos]

Question posted to stackoverflow:

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

[Eduardo Cavazos]

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]

Thank you for any suggestions!

[Mario Carneiro]

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]

Try to prove ∃ x, p x by contradiction

[Eduardo Cavazos]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Eduardo Cavazos]

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]

Trying something...

[Eduardo Cavazos]

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]

As that gets me an x and p x.

[Eduardo Cavazos]

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

[Mario Carneiro]

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]

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

[Eduardo Cavazos]

@Mario Carneiro Ahhhhhhhhh!!!

[Eduardo Cavazos]

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

[Eduardo Cavazos]

Thank you!!!

[Johan Commelin]

@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]

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]

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

[Johan Commelin]

Sure...

[Johan Commelin]

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]

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]

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.

[Johan Commelin]

Fair enough

[Rob Lewis]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kenny Lau]

Kevin does not teach calculus :P

[Kevin Buzzard]

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]

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]

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]

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]

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

[Rob Lewis]

And you do that for a reason!

[Rob Lewis]

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

[Kevin Buzzard]

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]

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

[Rob Lewis]

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]

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

[Rob Lewis]

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]

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

[Kevin Buzzard]

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]

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

[Rob Lewis]

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]

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]

How about this version?

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

@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]

@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]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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

[Eduardo Cavazos]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Daniel Keys]

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),
        by_contradiction
            (λ 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]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Kenny Lau]

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

theorem T06_1 : ¬ (∀ x, ¬ p x) → (∃ x, p x) :=
assume hnAxnpx : ¬ (∀ x, ¬ p x),
  by_contradiction
    (λ 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,
  by_contradiction hnExpx,
  apply hnAxnpx,
  intro x,
  intro hpx,
  apply hnExpx,
  existsi x,
  exact hpx
end

[Patrick Massot]

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

[Daniel Keys]

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]

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]

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]

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

[Daniel Keys]

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]

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

[Daniel Keys]

Oh, absolutely!

[Patrick Massot]

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]

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

[Daniel Keys]

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]

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]

I definitely should have known this already! Thanks!