Proofs involving negation

Stream: new members

[Noob]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

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]

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

[Noob]

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]

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

[Marc Huisinga]

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

[Noob]

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]

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

[Kevin Buzzard]

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

[Noob]

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]

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

[Noob]

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]

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

[Filippo A. E. Nuccio]

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.

[Patrick Massot]

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

[Filippo A. E. Nuccio]

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

[Johan Commelin]

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

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Reid Barton]

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

[Johan Commelin]

Which is?

[Reid Barton]

described here

[Mario Carneiro]

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]

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

[Jalex Stark]

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

[Reid Barton]

Does ‽ count as one character?

[Reid Barton]

I've never used squeeze_simp

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

Right, I use squeeze_simp for that

[Johan Commelin]

To figure out what should go in the rw

[Reid Barton]

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

[Reid Barton]

While the rewrite trace would just tell you the answer?

[Johan Commelin]

Sure, but at least I know what the pieces are

[Mario Carneiro]

I often convert squeeze_simp calls to rw as well

[Reid Barton]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

I think simp? could print both

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

so it's not always going to work

[Mario Carneiro]

but I think even the simp only proof fails sometimes

[Johan Commelin]

Yup, although it got a lot less rare

[Bryan Gin-ge Chen]

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

[Scott Morrison]

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.