## Stream: new members

### Topic: Proofs involving negation

#### 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.

#### Kevin Buzzard (May 06 2020 at 14:31):

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

#### 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,
end


#### 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

#### 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


#### 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?

#### 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.

#### Marc Huisinga (May 06 2020 at 14:51):

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

#### 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.

#### 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.

#### 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

#### 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.

#### 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.

#### 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!

#### 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.

#### 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.

#### Filippo A. E. Nuccio (May 14 2020 at 14:58):

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

#### 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".

#### Filippo A. E. Nuccio (May 14 2020 at 14:59):

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

#### 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:

#### 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.

#### Johan Commelin (May 14 2020 at 15:04):

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

#### Reid Barton (May 14 2020 at 15:04):

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

Which is?

described here

#### 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?

#### Mario Carneiro (May 14 2020 at 16:34):

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

#### Jalex Stark (May 14 2020 at 16:35):

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

#### Reid Barton (May 14 2020 at 16:59):

Does ‽ count as one character?

#### Reid Barton (May 14 2020 at 16:59):

I've never used squeeze_simp

#### Johan Commelin (May 14 2020 at 17:03):

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

#### Reid Barton (May 14 2020 at 17:07):

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

#### Reid Barton (May 14 2020 at 17:07):

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

#### Mario Carneiro (May 14 2020 at 17:22):

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

#### 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

#### 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

#### Johan Commelin (May 14 2020 at 17:24):

Right, I use squeeze_simp for that

#### Johan Commelin (May 14 2020 at 17:24):

To figure out what should go in the rw

#### Reid Barton (May 14 2020 at 17:24):

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

#### Reid Barton (May 14 2020 at 17:24):

While the rewrite trace would just tell you the answer?

#### Johan Commelin (May 14 2020 at 17:24):

Sure, but at least I know what the pieces are

#### Mario Carneiro (May 14 2020 at 17:24):

I often convert squeeze_simp calls to rw as well

#### Reid Barton (May 14 2020 at 17:25):

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

#### Mario Carneiro (May 14 2020 at 17:25):

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

#### Johan Commelin (May 14 2020 at 17:25):

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

#### Mario Carneiro (May 14 2020 at 17:25):

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

#### Mario Carneiro (May 14 2020 at 17:26):

I think simp? could print both

#### 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?

#### 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

#### Mario Carneiro (May 14 2020 at 17:26):

so it's not always going to work

#### Mario Carneiro (May 14 2020 at 17:27):

but I think even the simp only proof fails sometimes

#### Johan Commelin (May 14 2020 at 17:28):

Yup, although it got a lot less rare

#### 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?

#### 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: Dec 20 2023 at 11:08 UTC