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

Stream: new members

[Arien Malec]

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]

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]

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]

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]

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 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.

Cool! IIRC, in Haskell, I can define functions pointsfree, but not call them 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]

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]

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]

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

Proof in Haskell

data Or a b = L a | R b

intro_left :: a -> Or a b
intro_left = L

intro_right :: b -> Or a b
intro_right = R

elim :: Or a b -> (a -> c) -> (b -> c) -> c
elim (L a) f g = f a
elim (R b) f g = g b

or_assoc_right_pq :: Or p q -> Or p (Or q r)
or_assoc_right_pq =
  \hpq ->
    elim hpq
      ( \hp ->
        intro_left hp)
      ( \hq ->
        let hqr = intro_left hq
        in intro_right hqr)

or_assoc_right_r :: r -> Or p (Or q r)
or_assoc_right_r =
  \hr ->
    let hqr = intro_right hr
    in intro_right hqr

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

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]

typechecking is proof?

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

[Matt Diamond]

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

[Arien Malec]

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

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

[Kevin Buzzard]

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!