Zulip Chat Archive

Stream: new members

Topic: Proofs with negations


Arien Malec (Sep 25 2022 at 02:24):

Still working through TPIL and totally flummoxed by proofs of negations. For example, working through De Morgan's laws, and have gotten this to work by copying the very terse mathlib proof, but I don't understand how it works.

lemma not_or_dist_left {p q : Prop} : ¬(p  q)  ¬p :=
  assume hnpq: ¬(p  q),
  show ¬p, from (
    assume hp: p,
    hnpq (or.inl hp))

I've assumed p, provided that to ¬(p ∨ q) and demonstrated ¬p? It all feels very mindtwisty like there's a proof by contraction without stating by_contradiction or absurd.

Matt Diamond (Sep 25 2022 at 02:28):

keep in mind that ¬p is equivalent to p → false, so if you want to prove ¬p all you need to do is assume p and derive false somehow

Matt Diamond (Sep 25 2022 at 02:32):

also, since ¬p is equivalent to p → false, if you have a proof of ¬p and you apply p to it, you get false back (because what you're really doing is applying p to p → false)

Matt Diamond (Sep 25 2022 at 02:37):

what the above proof is doing is this:

1) we assume the premise, ¬(p ∨ q)
2) we want to prove ¬p which is actually proving p → false, so we assume p is true and our goal is to prove false
3) since p is true, we know that p ∨ q is true (this is what or.inl hp is doing)
4) now we know p ∨ q is true (represented by or.inl hp), and we also assumed ¬(p ∨ q) is true (represented by hnpq), so we combine those to get false in the final line and we're done

Arien Malec (Sep 25 2022 at 02:40):

Cool, so it's a sort of proof by contraction because we want false → p...?

Matt Diamond (Sep 25 2022 at 02:48):

not exactly... we don't want to derive p from false, but the other way around

Matt Diamond (Sep 25 2022 at 02:48):

though certainly, once you have false you can derive whatever you want

Matt Diamond (Sep 25 2022 at 02:50):

but the goal is to start with p and end up producing false somehow

¬p just is p → false within Lean... that's how it's represented

Matt Diamond (Sep 25 2022 at 02:51):

in other words, when you see ¬p you should think to yourself "that's a function from p to false"

Matt Diamond (Sep 25 2022 at 02:53):

(at least that's how I think of it, being a software engineer by trade... if you're a mathematician you can think of it as being equivalent to "if p, then false")

Matt Diamond (Sep 25 2022 at 02:56):

but yes, it's a proof by contradiction in the sense that you prove not p by assuming p and deriving false

Arien Malec (Sep 25 2022 at 02:58):

Thanks -- also software engineering by background and having a hard time reasoning over types here. I suppose like most things Lean I'll just get used to it.

Matt Diamond (Sep 25 2022 at 03:00):

yeah, it's a bit weird at first but eventually it starts to click

Arien Malec (Sep 25 2022 at 04:52):

So to check understanding, this bit:
assume hp: p is the premise to the function and we show false by hnpq (or.inl hp)

And in the other side of the double implication we do the same thing for ¬(p ∨ q) by assuming p ∨ q and showing each case leads to false...

Matt Diamond (Sep 25 2022 at 05:10):

We don't actually assume p v q. The statement we're trying to prove is "if ¬(p ∨ q), then ¬p". In other words, we need to produce a function that takes in a proof of ¬(p ∨ q) and returns a proof of ¬p.

Matt Diamond (Sep 25 2022 at 05:11):

So we assume ¬(p ∨ q) at the start, and our goal is to return ¬p (which is equivalent to saying that our goal is return a function from p to false).

Matt Diamond (Sep 25 2022 at 05:13):

At the point where we assumed p, we were able to derive p v q from that because it logically follows: "if P is true, then P or Q is true"

Matt Diamond (Sep 25 2022 at 05:17):

If assume is confusing, just remember that it's shorthand for λ a... it's just another way of declaring a function argument

Matt Diamond (Sep 25 2022 at 05:25):

Here's another way to write out the same proof:

lemma not_or_dist_left {p q : Prop} : ¬(p  q)  ¬p :=
λ not_p_or_q : ¬(p  q),
  -- we need a function from p to false
  λ proof_of_p : p,
    let p_or_q : p  q := or.inl proof_of_p in
    not_p_or_q p_or_q

Yaël Dillies (Sep 25 2022 at 08:10):

Does it make more sense if you write the goal as (p ∨ q → false) → (p → false)?

Damiano Testa (Sep 25 2022 at 08:28):

I also picture this proof in my mind as a proof by contradiction. Maybe, with the comments below, the argument makes more sense?

lemma not_or_dist_left {p q : Prop} : ¬(p  q)  ¬p :=
  assume hnpq: ¬(p  q),  -- Suppose that `p ∨ q` is false
  show ¬p, from (         -- We want to show that `p` itself must be false
    assume hp: p,         -- By contradiction, suppose that `p` is true instead
    hnpq (or.inl hp))     -- If `p` is true, then `p ∨ q` is true (this is the `or.inl` part),
                          -- contrary to the assumption `hnpq` that `p ∨ q` is false

Arien Malec (Sep 25 2022 at 14:32):

Thanks for all of this , and I think I'm understanding. At the type level, our function is really p ∨ q → false) → (p → false), inside the proof in the show, from step we are actually constructing a function p→ false, which, since it typechecks, constitutes proof, but the sugared logical flow in that step looks like a proof by contradiction (assuming p, showing that it leads to false.

Arien Malec (Sep 26 2022 at 20:57):

I am absurdly pleased by this, which took me far too much time to work out.

open classical

example {p r s : Prop}: (p  r  s)  ((p  r)  (p  s)) :=
  assume h: p  r  s,
  show (p  r)  (p  s), from (
    or.elim (em p)
    ( assume hp: p,
      have hrs: r  s, from h hp,
      hrs.elim
      ( assume hr: r,
        have hpr: p  r, from λ hp₂: p, hr,
        show (p  r)  (p  s), from or.inl hpr)
      ( assume hs: s,
        have hps: p  s, from λ hp₂, hs,
        show (p  r)  (p  s), from or.inr hps)
    )
    ( assume hnp: ¬p,
      have hpr: p  r, from λ hp: p, absurd hp hnp,
      show (p  r)  (p  s), from or.inl hpr)
  )

It seems that Lean knows that the three lambda expressions here occur in a context where it is already known that p is true or false as the case may be??

Kyle Miller (Sep 26 2022 at 22:07):

Lean doesn't consider propositions to be true or false per se -- we consider a proposition to be "true" if we have a proof of it in context.

Matt Diamond (Sep 26 2022 at 22:08):

@Arien Malec What programming language are you the most familiar with? I ask because there isn't really any magic going on in the above code (Lean doesn't have to "know" anything), and perhaps I can rewrite it in a way that demonstrates that

Kyle Miller (Sep 26 2022 at 22:08):

It might be helpful to see the proof with a bunch of the syntactic sugar removed:

open classical

example {p r s : Prop} : (p  r  s)  ((p  r)  (p  s)) :=
  λ (h : p  r  s),
    or.elim (em p)
    (λ (hp : p),
      have hrs: r  s, from h hp,
      hrs.elim
      (λ (hr : r),
        have hpr: p  r, from λ hp₂ : p, hr,
        or.inl hpr)
      (λ (hs : s),
        have hps: p  s, from λ hp₂, hs,
        or.inr hps))
    (λ (hnp : ¬p),
      have hpr : p  r, from λ hp : p, absurd hp hnp,
      or.inl hpr)

Kyle Miller (Sep 26 2022 at 22:08):

I still left the have clauses, which are yet another way to write lambda expressions

Kyle Miller (Sep 26 2022 at 22:10):

The show clauses weren't completely necessary since you can get the goal from the goal view in VS Code or Emacs. There's no harm in keeping them, and I removed them just to illustrate that they're not doing any magic.

Arien Malec (Sep 26 2022 at 22:11):

Most relevant, Rust, enough Haskell to do stuff, but not be typesystem dangerous.

λ hp₂ : p, hr is an anonymous lambda, which can be called with any value? It could be called in a context where p is false, yeah? But we know that we are are calling in in a context where p is true...

Kyle Miller (Sep 26 2022 at 22:12):

Here's it with all the have's removed too:

open classical

example {p r s : Prop} : (p  r  s)  ((p  r)  (p  s)) :=
  λ (h : p  r  s),
    or.elim (em p)
    (λ (hp : p),
      or.elim (h hp)
      (λ (hr : r), or.inl (λ (hp₂ : p), hr))
      (λ (hs : s), or.inr (λ (hp₂ : p), hs)))
    (λ (hnp : ¬p),
      or.inl (λ (hp : p), absurd hp hnp))

Kyle Miller (Sep 26 2022 at 22:12):

Yes, λ hp₂ : p, hr can be called with any proof hp₂ of p. It can only be called when p is "true" for that reason.

Kyle Miller (Sep 26 2022 at 22:13):

It can only be called in a context when p is "false" when p is also "true" (i.e., when there's a logical contradiction)

Matt Diamond (Sep 26 2022 at 22:14):

it's also true that λ hp₂ : p, hr by itself is a valid proof of p → r in a context where you already have a proof of r in a variable hr

Matt Diamond (Sep 26 2022 at 22:18):

we are calling it in a context where p is true

maybe there's a misunderstanding because we're not "calling " (hp₂ : p), hr anywhere (I think)

Matt Diamond (Sep 26 2022 at 22:19):

we're writing it out as a proof of the proposition (p → r), and then using it to prove (p → r) ∨ (p → s)

Kyle Miller (Sep 26 2022 at 22:19):

(I'll mention that it's a Lean theorem that if you have h : p (i.e., p is "true" since we have a proof of it) then you can conclude that p = true. But Lean generally won't replace p with docs#true on its own.)

Matt Diamond (Sep 26 2022 at 22:48):

@Arien Malec I'm curious why you said we were "calling" λ hp₂ : p, hr... are you imagining that the function has to be "called" to create a proof of p → r? Because it doesn't... the function is the proof.

Arien Malec (Sep 26 2022 at 22:48):

In the H-M type system languages I've used in anger (Ocaml, Rust, Swift, Haskell), if I define, say |p: bool| -> bool {r}, r in the lambda body is bound and captured, but p is free, and I'm saying "whatever p is, return the bound value of r", which is a stronger proof than we want, yeah? It's a function from ¬p to r as well. I have to know that p as well?

Put it another way, out of context that p, how could λ h : p, hr constitute a proof (p → r)?

Matt Diamond (Sep 26 2022 at 22:51):

p → r means "if you give me a proof of p, I'll give you a proof of r"... in other words, a function that takes in a proof of p and returns a proof of r

Matt Diamond (Sep 26 2022 at 22:51):

in this case, it so happens that we already have a proof of r in the variable hr

Matt Diamond (Sep 26 2022 at 22:53):

it doesn't matter that we might not have a proof of p... an implication is just a hypothetical, saying if this is the case, then that is the case

Arien Malec (Sep 26 2022 at 22:54):

Matt Diamond said:

Arien Malec I'm curious why you said we were "calling" λ hp₂ : p, hr... are you imagining that the function has to be "called" to create a proof of p → r? Because it doesn't... the function is the proof.

I think I've got that (or it's getting grokked slowly). But it's only a proof when we already know that p, right?

If I dropped the same function in to the other branch of the elim, it would constitute a proof of the opposite, right?

(λ (hnp : ¬p), (λ (hr : r), or.inl (λ (hp₂ : p), hr)) in that context would be a proof that ¬p → r?

Arien Malec (Sep 26 2022 at 22:55):

Or…would that fail to typecheck, because p and ¬p aren't values of a bool, they are totally different types…

Matt Diamond (Sep 26 2022 at 22:55):

the thing is that the implication doesn't require p to be true

Matt Diamond (Sep 26 2022 at 22:56):

in fact, you could replace the exact same function in the same place with (hp₂ : ¬p), hr and you would have a proof of ¬p → r

Matt Diamond (Sep 26 2022 at 22:57):

but Lean would be confused because the goal at that point is to prove p → r

Arien Malec (Sep 26 2022 at 22:57):

I think the lighbulb moment here is "p and ¬p aren't values of a bool, they are totally different types"

Matt Diamond (Sep 26 2022 at 22:59):

(λ (hnp : ¬p), (λ (hr : r), or.inl (λ (hp₂ : p), hr)) would be a proof of ¬p → r → p ∨ r

Matt Diamond (Sep 26 2022 at 23:00):

which is just true in any context

Matt Diamond (Sep 26 2022 at 23:01):

it's like we need to prove "if aliens are real, then your name is Arien Malec" and we have a proof that your name is Arien Malec

Arien Malec (Sep 26 2022 at 23:02):

I'm walking around with a mental model of Prop being like bool, when p: Prop is already an assertion that p.

Matt Diamond (Sep 26 2022 at 23:02):

p : Prop is a proposition named p, it doesn't assert anything. However, hp : p is a proof of p.

Matt Diamond (Sep 26 2022 at 23:05):

the "propositions are types and proofs are terms of them" model can be a bit tricky to wrap your mind around, for sure

Matt Diamond (Sep 26 2022 at 23:06):

it's a bit confusing because the proposition is the type, while Prop is the type of propositions

Matt Diamond (Sep 26 2022 at 23:08):

so if you had a variable h whose type was ∃ n, n > 0, then it would be a proof that there's a number greater than 0

Kyle Miller (Sep 26 2022 at 23:08):

Mathlib has that there's a bijection between Prop and bool, so Prop being like bool isn't so far off (docs#equiv.Prop_equiv_bool)

The big difference is that when you have a term of bool in hand, you can tell whether it is tt or ff by computing long enough. But when you have p : Prop, there's no procedure you can use to decide (in general) whether p = true or p = false. You can only infer that p = true if you manage to find a proof h : p or that p = false if you manage to find a proof h : ¬p.

Kyle Miller (Sep 26 2022 at 23:10):

There's also the big difference that bool and Prop are at different "levels", as Matt has mentioned. Here's a diagram that tries to illustrate this: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Prop.20.3A.3D.20Sort.200.20Motivation/near/252362723

Matt Diamond (Sep 26 2022 at 23:10):

right... Propositions are not necessarily decidable

Arien Malec (Sep 26 2022 at 23:11):

The "typechecking is proof" paradigm is super deep. Playing around with my proof the issue with proving p ∨ r in the ¬p context is not the p vs ¬p issue but that I haven't found a proof hr: r in that context.

Matt Diamond (Sep 26 2022 at 23:12):

yeah that sounds right, in the sense that you're able to prove p ∨ r if you have a proof of r (though you could also prove it if you had a proof of p)

Arien Malec (Sep 26 2022 at 23:13):

Really appreciate the help getting my head wrapped the right way around these concepts.

Matt Diamond (Sep 26 2022 at 23:14):

no problem!

Matt Diamond (Sep 26 2022 at 23:21):

(did you mean to write p → r instead of p ∨ rabove? if so, then you've got the right idea)

Kyle Miller (Sep 26 2022 at 23:22):

I was interpreting that as, if you want to prove p ∨ r but you have ¬p, then you know you need a proof of r.

Matt Diamond (Sep 26 2022 at 23:25):

oh right... that also makes sense

(λ (hnp : ¬p), (λ (hr : r), or.inl (λ (hp₂ : p), hr)) would be a proof of ¬p → r → p ∨ r

I wrote this above and I just realized it's not true, so I was hoping I didn't confuse him... the point is that it proves (p → r) ∨ [anything else], not p ∨ r

I'm sure he'll figure it out

Arien Malec (Sep 27 2022 at 00:07):

I got it modulo typos!


Last updated: Dec 20 2023 at 11:08 UTC