Proofs with negations

Stream: new members

[Arien Malec]

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]

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]

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]

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]

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

[Matt Diamond]

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

[Matt Diamond]

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

[Matt Diamond]

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]

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

[Matt Diamond]

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

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

[Arien Malec]

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]

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

[Arien Malec]

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]

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]

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]

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]

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

[Matt Diamond]

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]

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

[Damiano Testa]

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]

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]

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]

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]

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

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]

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

[Kyle Miller]

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]

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]

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]

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]

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]

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]

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]

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]

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

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

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]

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]

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

[Matt Diamond]

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]

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]

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

[Matt Diamond]

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

[Matt Diamond]

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]

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

[Arien Malec]

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

[Matt Diamond]

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

[Matt Diamond]

which is just true in any context

[Matt Diamond]

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]

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

[Matt Diamond]

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

[Matt Diamond]

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]

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

[Matt Diamond]

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]

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]

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]

right... Propositions are not necessarily decidable

[Arien Malec]

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]

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]

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

[Matt Diamond]

no problem!

[Matt Diamond]

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

[Kyle Miller]

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]

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]

I got it modulo typos!