# Zulip Chat Archive

## Stream: new members

### Topic: Why does this code work (and is there a simpler way)?

#### Arien Malec (Sep 20 2022 at 17:54):

Working through Theorem Proving in Lean via the exercises, and doing `or_assoc`

```
lemma or_assoc_right_pq {p q r : Prop} : p ∨ q → p ∨ (q ∨ r) :=
assume hpq: p ∨ q,
show p ∨ (q ∨ r), from hpq.elim
( assume hp: p,
show p ∨ (q ∨ r), from or.intro_left (q ∨ r) hp)
( assume hq: q,
have hqr: q ∨ r, from or.intro_left r hq,
show p ∨ (q ∨ r), from or.intro_right p hqr)
lemma or_assoc_right_r {p q r: Prop} : r → p ∨ (q ∨ r) :=
assume hr: r,
have hqr: q ∨ r, from or.intro_right q hr,
show p ∨ (q ∨ r), from or.intro_right p hqr
lemma or_assoc_right {p q r : Prop} : (p ∨ q) ∨ r → p ∨ (q ∨ r) :=
assume hpqr : (p ∨ q) ∨ r,
show p ∨ (q ∨ r), from or.elim hpqr
(or_assoc_right_pq)
(or_assoc_right_r)
```

(As an aside, I'm not sure if I'm using "`right`

" in an Leanly way -- using it here to state that in a mutual implication, I'm going to the right).

Why doesn't `or_assoc_right_pq`

need any parameters? It's somehow picking everything up from context.... I'd have expected I'd need to `assume`

the starting point first....

My informal mental proof for associativity is each side of the double implication "p \or q \or r" implies at least one of the props, QED -- is there a simpler proof structure that gets more to the heart of the proof here rather than tediously going through each of the subcases in each direction of the double implication?

#### Kevin Buzzard (Sep 20 2022 at 18:20):

There are tactics which solve all of these goals in one line, if that's what you're asking. TPIL is just giving you practice writing low-level proofs.

#### Patrick Johnson (Sep 20 2022 at 19:14):

Why doesn't

`or_assoc_right_pq`

need any parameters? It's somehow picking everything up from context.... I'd have expected I'd need to assume the starting point first....

The place you're using `or_assoc_right_pq`

requires a proof of `p ∨ q → p ∨ (q ∨ r)`

. The statement basically says *"If we assume p ∨ q, we have p ∨ (q ∨ r)"*. You don't need to assume anything, because the statement of

`or_assoc_right_pq`

already says that for any `p q r : Prop`

, if we assume `p ∨ q`

, we have `p ∨ (q ∨ r)`

. Since `p q r`

are implicit in `or_assoc_right_pq`

, we don't need to provide them either. That's why `or_assoc_right_pq`

is enough. If you deliberately want to assume `p ∨ q`

(for whatever reason), it will be `(assume h : p ∨ q, or_assoc_right_pq h)`

, but it eta-reduces to `or_assoc_right_pq`

anyway.My informal mental proof for associativity is each side of the double implication

`p ∨ q ∨ r`

implies at least one of the props, QED -- is there a simpler proof structure that gets more to the heart of the proof here rather than tediously going through each of the subcases in each direction of the double implication?

What "double implication" are you referring to? Do you mean that because both `(p ∨ q) ∨ r`

and `p ∨ (q ∨ r)`

implies that at least one of `p q r`

is true means that `(p ∨ q) ∨ r ↔ p ∨ (q ∨ r)`

? If so, then that's not a valid inference rule. For example, both `p ∧ q`

and `p ∨ q`

implies that at least one of `p q`

is true, but `p ∧ q ↔ p ∨ q`

is not true for all `p q`

. Or did you mean something else?

Note that the problem with the statement *"at least one of the props is true"* is that in order to formalize it, you need to somehow represent the set of propositions `p`

, `q`

and `r`

, and state that at least one of the propositions in that set is true. However, in order to construct the set, you need to iterate over propositions `p q r`

, and the way you're constructing the set affects the proof. At the end, you'll end up doing the same thing as in your original proof, but more complicated.

#### Arien Malec (Sep 20 2022 at 20:00):

Nope, understand this is `simp`

and friends, ultimately. Just wondering (a) why my `or_assoc _right_pq`

works without parameters, and (b) whether there's a more intuitive way of doing this proof that maps to intuition.

#### Arien Malec (Sep 20 2022 at 21:07):

Patrick Johnson said:

Why doesn't

`or_assoc_right_pq`

need any parameters? It's somehow picking everything up from context.... I'd have expected I'd need to assume the starting point first....The place you're using

`or_assoc_right_pq`

requires a proof of`p ∨ q → p ∨ (q ∨ r)`

. The statement basically says"If we assume. You don't need to assume anything, because the statement of`p ∨ q`

, we have`p ∨ (q ∨ r)`

"`or_assoc_right_pq`

already says that for any`p q r : Prop`

, if we assume`p ∨ q`

, we have`p ∨ (q ∨ r)`

. Since`p q r`

are implicit in`or_assoc_right_pq`

, we don't need to provide them either. That's why`or_assoc_right_pq`

is enough. If you deliberately want to assume`p ∨ q`

(for whatever reason), it will be`(assume h : p ∨ q, or_assoc_right_pq h)`

, but it eta-reduces to`or_assoc_right_pq`

anyway.Cool! IIRC, in Haskell, I can define functions pointsfree, but not

callthem that way, so that's a new trick to me.My informal mental proof for associativity is each side of the double implication

`p ∨ q ∨ r`

implies at least one of the props, QED -- is there a simpler proof structure that gets more to the heart of the proof here rather than tediously going through each of the subcases in each direction of the double implication?`What "double implication" are you referring to? Do you mean that because both `(p ∨ q) ∨ r` and `p ∨ (q ∨ r)` implies that at least one of `p q r` is true means that `(p ∨ q) ∨ r ↔ p ∨ (q ∨ r)`? If so, then that's not a valid inference rule. For example, both `p ∧ q` and `p ∨ q` implies that at least one of `p q` is true, but `p ∧ q ↔ p ∨ q` is not true for all `p q`. Or did you mean something else?`

I think I'm in mental logic trap where I'm assuming associativity to prove associativity, and when I want to say it rigorously, I'm down to the logic I proposed. (p ∨ q) ∨ r, so if the right side is true, so is q ∨ r and then so is… Just getting my feet wet with both Lean and formal theorem proving, so trying to test all my confusion.

Thanks!

#### Matt Diamond (Sep 20 2022 at 21:27):

Cool! IIRC, in Haskell, I can define functions pointsfree, but not call them that way, so that's a new trick to me.

You're just passing one function (implication) as an argument to another... I'd be surprised if you haven't encountered that in Haskell!

#### Arien Malec (Sep 21 2022 at 03:18):

Matt Diamond said:

You're just passing one function (implication) as an argument to another... I'd be surprised if you haven't encountered that in Haskell!

If I'm reasoning through this, the signature of `iff.intro`

is `(a → b) → (b → a) → (a ↔ b)`

so in

```
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
iff.intro or_assoc_right or_assoc_left)
```

I'm just passing functions, and everything typechecks, and…typechecking is proof? I've never called anything, there's no entry point to my program, but because it complies I've typechecked against `(p ∨ q) ∨ r ↔ p ∨ (q ∨ r)`

?

#### Patrick Johnson (Sep 21 2022 at 03:21):

Here is your proof transliterated to Haskell. As you can see, it typechecks.

Proof in Haskell

I guess you mean that in Haskell you can't have implicit arguments, like you can in Lean (regarding `p q r : Prop`

)? Actually, `p q r`

**are** implicit in Haskell. You can enable the `forall`

syntax with `{-# LANGUAGE RankNTypes #-}`

. Also, you can make them explicit with `{-# LANGUAGE ScopedTypeVariables TypeApplications #-}`

and the syntax would be:

```
or_assoc_right :: forall p q r. Or (Or p q) r -> Or p (Or q r)
or_assoc_right =
\hpqr ->
elim hpqr
(or_assoc_right_pq @p @q @r)
(or_assoc_right_r)
```

#### Matt Diamond (Sep 21 2022 at 03:24):

typechecking is proof?

basically... at least when your return type is a proposition and your lemma returns a term of it

#### Matt Diamond (Sep 21 2022 at 03:25):

it can be a bit strange, coming from the programming side of things

#### Arien Malec (Sep 21 2022 at 04:03):

I'm deeply in "Typechecking the Technical Interview" land now!

Thanks so much -- I'm learning a great deal...

#### Kevin Buzzard (Sep 21 2022 at 04:08):

Yeah one reason I like lean is that I was always lousy at writing algorithms, but lean proofs don't run! As long as they typecheck you've proved the theorem!

Last updated: Dec 20 2023 at 11:08 UTC