Zulip Chat Archive

Stream: new members

Topic: Proofs involving negation


view this post on Zulip Noob (May 06 2020 at 14:30):

Hi all,
I'm going through "Logic and Proof" and "Theorem Proving in Lean" exercises and got stuck on the ones that make use of negation.
Could someone outline the line of reasoning ivolved in proving something like

variables A B : Prop
example (h: ¬A  ¬B) : ¬(A  B) := sorry

?
With conjunction, disjunction and implication I usually start with a corresponding introduction rule and the rest follows naturally, but can't wrap my head around how to apply the same strategy to negation.

view this post on Zulip Kevin Buzzard (May 06 2020 at 14:31):

not X is just syntax sugar for X -> false if that helps

view this post on Zulip Kevin Buzzard (May 06 2020 at 14:32):

variables A B : Prop
example (h: ¬A  ¬B) : ¬(A  B) :=
begin
  cases h with hnA hnB,
  intro hAB,
  cases hAB with hA hB,
  { contradiction},
  { contradiction},
end

view this post on Zulip Patrick Massot (May 06 2020 at 14:32):

If you don't mind using tactics then you can follow the tutorials project. It has several files about negation, starting with https://github.com/leanprover-community/tutorials/blob/master/src/exercises/07_first_negations.lean

view this post on Zulip Kevin Buzzard (May 06 2020 at 14:33):

variables A B : Prop
example (h: ¬A  ¬B) : ¬(A  B) :=
h.elim $ λ hnA hnB hAB, hAB.elim hnA hnB

view this post on Zulip Noob (May 06 2020 at 14:47):

I'm not familiar with the cases and intro syntax yet, but I suppose it's equavalent to

  example (h: ¬A  ¬B) : ¬(A  B) :=
    have hnA : ¬A, from h.left,
    have hnB : ¬B, from h.right,
    λ hAB : A  B,

Is that correct?

view this post on Zulip Noob (May 06 2020 at 14:49):

I'd prefer not use tactics at this point, but do everything manually. Want to understand what is really going on.

view this post on Zulip Marc Huisinga (May 06 2020 at 14:51):

you probably meant λ hAB : A ∨ B,, but other than that you're right.

view this post on Zulip Noob (May 06 2020 at 15:04):

Correct. So here

  example (h: ¬A  ¬B) : ¬(A  B) :=
    have hnA : ¬A, from h.left,
    have hnB : ¬B, from h.right,
    λ hAB : A  B,

we have destructured our hypothesis such that each part can be referred to individually, we introduced a new hypothesis which is a negation of what needs to be proven.
Do we need the new hypothesis so we can arrive at a contradiction? I don't see how if so.

view this post on Zulip Marc Huisinga (May 06 2020 at 15:07):

try eliminating hAB and see if you can then derive false in both cases of the elimination.

view this post on Zulip Kevin Buzzard (May 06 2020 at 15:14):

I wrote hAB.elim but this is using some cunning dot notation. You can also write or.elim hAB

view this post on Zulip Noob (May 06 2020 at 15:38):

Thanks for the hints, I managed to prove it like this:

  example (h: ¬A  ¬B) : ¬(A  B) :=
    have hnA : ¬A, from h.left,
    have hnB : ¬B, from h.right,
    λ hAB : A  B,
      or.elim hAB
        (λ hA, absurd hA hnA)
        (λ hB, absurd hB hnB)

Still can't figure out why this

  example (h: ¬A  ¬B) : ¬(A  B) :=
    have hnA : ¬A, from h.left,
    have hnB : ¬B, from h.right,
    λ hAB : A  B,
      or.elim hAB
        (λ hA : A, false.elim (hnA hA))
        (λ hB : B, false.elim (hnB hB))

doesn't work - it looks the same to me.

view this post on Zulip Marc Huisinga (May 06 2020 at 15:52):

works for me. note that you don't actually need false.elim or absurd because you're trying to prove false itself.

view this post on Zulip Noob (May 06 2020 at 16:01):

Actually, it works for me too - VS Code got me confused.
With your latest suggestion the proof looks like this:

  example (h: ¬A  ¬B) : ¬(A  B) :=
    have hnA : ¬A, from h.left,
    have hnB : ¬B, from h.right,
    λ hAB : A  B,
      or.elim hAB
        (λ hA, hnA hA)
        (λ hB, hnB hB)

Thanks a lot for the help!

view this post on Zulip Marc Huisinga (May 06 2020 at 17:20):

another small trick: after using (λ hA, hnA hA) = hnA, your proof will look pretty similar to kevin's.

view this post on Zulip Filippo A. E. Nuccio (May 14 2020 at 14:52):

I am try to prove that 1 \ne 0. I can apply simp, and lean is happy. But I wanted to do it step-by-step.
To my knowledge, this should be an axiom (if these 1 and 0 were natural numbers, at least: but I believe that Lean has been taught that 0 : \R is the same as 0 : N; and likewise for 1). At any rate, I have tried
begin intro h,
and now should deduce from h: 1=0 that false
And I am stuck, both in performing the proof and in observing that if I try simp now, Lean is no longer happy.

view this post on Zulip Patrick Massot (May 14 2020 at 14:55):

https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/ may help

view this post on Zulip Filippo A. E. Nuccio (May 14 2020 at 14:58):

Seems a long read: I will try to digest the whole of it. Thanks.

view this post on Zulip Johan Commelin (May 14 2020 at 14:58):

@Filippo A. E. Nuccio That blogpost is good. But here is another approach, to figure things out yourself: you turn your first simp into squeeze_simp to see what it did. Then, you get that lemma name (probably nat.zero_ne_one) and write

#print nat.zero_ne_one

After that, you can right-click on it, and "Go to definition".

view this post on Zulip Filippo A. E. Nuccio (May 14 2020 at 14:59):

ah! the squeeze_simp is the gadget I was dreaming of! tnx

view this post on Zulip Johan Commelin (May 14 2020 at 14:59):

Then you can see how it's proven. And you'll find the no_confusion thing yourself. End result: you will ask a question here about no_confusion and still get pointed to the blogpost. :grinning_face_with_smiling_eyes:

view this post on Zulip Johan Commelin (May 14 2020 at 15:03):

@Filippo A. E. Nuccio Yup, squeeze_simp is amazing. There is also library_search, suggest, hint, and tidy? that are useful tools.

view this post on Zulip Johan Commelin (May 14 2020 at 15:04):

We should rename squeeze_simp to simp? now that we have forked lean.

view this post on Zulip Reid Barton (May 14 2020 at 15:04):

No, we should make simp? do the more useful thing

view this post on Zulip Johan Commelin (May 14 2020 at 15:04):

Which is?

view this post on Zulip Reid Barton (May 14 2020 at 15:05):

described here

view this post on Zulip Mario Carneiro (May 14 2020 at 16:34):

I disagree that this is the more useful thing. I find myself using squeeze_simp a lot more than actually trying to understand the list of rewrites. How about simp? for squeeze_simp and simp?? for simp with trace enabled?

view this post on Zulip Mario Carneiro (May 14 2020 at 16:34):

I really like the idea of a one character diff from simp to squeeze_simp

view this post on Zulip Jalex Stark (May 14 2020 at 16:35):

I would have broken my nonterminal simp habit faster if it were one character

view this post on Zulip Reid Barton (May 14 2020 at 16:59):

Does ‽ count as one character?

view this post on Zulip Reid Barton (May 14 2020 at 16:59):

I've never used squeeze_simp

view this post on Zulip Johan Commelin (May 14 2020 at 17:03):

@Reid Barton You do have sliced bread, do you?

view this post on Zulip Reid Barton (May 14 2020 at 17:07):

I guess I don't really understand what it's for

view this post on Zulip Reid Barton (May 14 2020 at 17:07):

aside from making proofs run faster, which I don't care terribly much about

view this post on Zulip Mario Carneiro (May 14 2020 at 17:22):

I care about making proofs faster even before I've finished writing them

view this post on Zulip Mario Carneiro (May 14 2020 at 17:23):

if I start off my proof with simp * then that call is going to slow down the entire interaction cycle for the rest of the proof

view this post on Zulip Reid Barton (May 14 2020 at 17:23):

I guess I also don't really use simp that much, or when I do use it experimentally I want to replace it with rw, not simp only

view this post on Zulip Johan Commelin (May 14 2020 at 17:24):

Right, I use squeeze_simp for that

view this post on Zulip Johan Commelin (May 14 2020 at 17:24):

To figure out what should go in the rw

view this post on Zulip Reid Barton (May 14 2020 at 17:24):

But then don't you still have to solve a puzzle?

view this post on Zulip Reid Barton (May 14 2020 at 17:24):

While the rewrite trace would just tell you the answer?

view this post on Zulip Johan Commelin (May 14 2020 at 17:24):

Sure, but at least I know what the pieces are

view this post on Zulip Mario Carneiro (May 14 2020 at 17:24):

I often convert squeeze_simp calls to rw as well

view this post on Zulip Reid Barton (May 14 2020 at 17:25):

I think maybe you are the one without sliced bread? :upside_down:

view this post on Zulip Mario Carneiro (May 14 2020 at 17:25):

I still want an auto-replace, not a tactic trace

view this post on Zulip Johan Commelin (May 14 2020 at 17:25):

A simp?? that outputs Try this: rw [foo, bar, bar, ← quux, foo] would be awesome.

view this post on Zulip Mario Carneiro (May 14 2020 at 17:25):

but it would be nice if the order that lemmas are printed matches the rewrite order

view this post on Zulip Mario Carneiro (May 14 2020 at 17:26):

I think simp? could print both

view this post on Zulip Johan Commelin (May 14 2020 at 17:26):

Of course simp only is more powerful than rw, so you can't always get what you want, right?

view this post on Zulip Mario Carneiro (May 14 2020 at 17:26):

also rw has to repeat lemmas and simp only doesn't, and simp only works under binders

view this post on Zulip Mario Carneiro (May 14 2020 at 17:26):

so it's not always going to work

view this post on Zulip Mario Carneiro (May 14 2020 at 17:27):

but I think even the simp only proof fails sometimes

view this post on Zulip Johan Commelin (May 14 2020 at 17:28):

Yup, although it got a lot less rare

view this post on Zulip Bryan Gin-ge Chen (May 14 2020 at 17:29):

simp? which offers both simp only and rw options would be lovely. What do we have to do to make it happen?

view this post on Zulip Scott Morrison (May 17 2020 at 04:22):

If we finish moving rewrite_search to mathlib, one possible mechanism for creating the rw suggestion would be to take the current output from squeeze_simp and pass that as the list of allowed lemmas to rewrite_search. That will automatically take care of generating the rw statement.


Last updated: May 09 2021 at 20:11 UTC