# 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 *absurd*ly 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 functionisthe 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 ∨ r`

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