TPIL Chapter 3 Exercises

Stream: new members

[Rocky Kamen-Rubio]

I'm working through the exercises in TIPL and am having trouble with some of the exercises

#3.1

Q1:I'm getting an error on the or.elim in the following code. Lean is saying that it's expecting a type p∨q but is getting type q∨p.

example : p ∨ q ↔ q ∨ p :=
  iff.intro (assume h : p ∨ q, or.elim h
    (assume hp : p, show q ∨ p, from or.intro_right q hp)
    (assume hq : q, show q ∨ p, from or.intro_left p hq))
  (assume h2 : q ∨ p, or.elim h2
    (assume hq : q, show q ∨ p, from or.intro_left p hq)
    (assume hp : p, show q ∨ p, from or.intro_right q hp))

Q2: I'm getting type mismatch errors again for show and or.intro in the last line of this exercise.

example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
  iff.intro
    (assume h : (p ∨ q) ∨ r, or.elim h
      (assume hpq : p ∨ q, or.elim hpq
        (assume hp : p, show p ∨ (q ∨ r), from or.intro_left p hp)))

[Kevin Buzzard]

Q1: the error is indeed expected. Do you know what the second input to the iff.intro is supposed to be a proof of? And can you see what you're proving?

[Kevin Buzzard]

Q2: your term is not really complete so it's not surprising you have errors. Why not put in some _s or sorrys to make the term compile?

[Kevin Buzzard]

But honestly these "verbose mode" things are hell to debug. Why not use full term mode or full tactic mode?

[Kevin Buzzard]

For Q2 the full errors tell you exactly what you are doing wrong. Lean tells you exactly what it expects you to be proving and what you are proving.

[Kevin Buzzard]

The show is fine, Lean is just confused by the fact that you made an error later. Can you understand the error message?

[Rocky Kamen-Rubio]

Q1: I thought the second input to iff.intro was just in the "other direction", so wouldn't it work essentially the same as the first input but with the p and q reversed?

Q2: You're right, I missed a whole chunk of code when I copied it over. Here is the full proof. The errors still hold though

example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
  iff.intro
    (assume h : (p ∨ q) ∨ r, or.elim h
      (assume hpq : p ∨ q, or.elim hpq
        (assume hp : p, show p ∨ (q ∨ r), from or.intro_left p hp)
        (assume hq : q, show p ∨ (q ∨ r), from or.intro_right (q ∨ r) (or.intro_left q hq)))
      (assume hr : r, show p ∨ (q ∨ r), from or.intro (q ∨ r) (or.intro_left r hr)))
    (assume h2 : p ∨ (q ∨ r), or.elim h2
      (assume hp : p, show (p ∨ q) ∨ r, from or.intro_left (p ∨ q) (or.intro_left p hp))
      (assume hqr : (q ∨ r), or.elim hqr
        (assume hq : q, show (p ∨ q) ∨ r, from or.intro_left (p ∨ q) (or.intro_right q hq))
        (assume hr : r, show (p ∨ q) ∨ r, from or.intro_right r hr)))

Do you think it isn't productive to practice these proofs outside of tactic mode? I feel somewhat comfortable with tactic mode, but wanted to fully understand TIPL since I feel like I still don't understand a lot of what's going on in the chat/in other definitions I try to use. .

[Rocky Kamen-Rubio]

Q3: I'm getting a term mismatch for the two assume statements I'm passing intro iff.intro. I think I'm misunderstanding how iff.intro works more generally. Any guidance would be appreciated.

example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
iff.intro
  (assume h : p ∧ (q ∨ r),
  or.elim (and.right h),
    (assume hq : q, show (p ∧ q) ∨ (p ∧ r),
    from or.intro_left (p ∧ q) (and.intro (and.left h)  hq))
    (assume hr : r, show (p ∧ q) ∨ (p ∧ r),
    from or.intro_right (p ∧ r) (and.intro (and.left h)  hr)))
  (assume h : (p ∧ q) ∨ (p ∧ r),
  or.elim h,
    (assume hpq : p ∧ q, show p ∧ (q ∨ r),
    from and.intro (and.left hpq) (or.intro_left q (and.right hpq)))
    (assume hpr : p ∧ r, show p ∧ (q ∨ r),
    from and.intro (and.left hpr) (or.intro_left r (and.right hpr))))

[Kevin Buzzard]

I personally have never seen the point of this super-verbose term mode. But others clearly think differently because it's explained in TPIL!

[Kevin Buzzard]

Your Q3 the errors are a real mess and I just look at all this super-verbose term mode and think "if this was my problem I'd just start again"

[Kevin Buzzard]

I'm sure it's possible to debug but I don't fancy it

[Kevin Buzzard]

The error

  type mismatch, term
    (?m_3, ?m_4)
  has type
    ?m_1 × ?m_2 : Type (max ? ?)
  but is expected to have type
    p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r : Prop

just indicates that you've got the brackets wrong somewhere.

[Kevin Buzzard]

I would start like this:

example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
iff.intro _ _

and I'd just keep checking that the errors were not insane at all stages.

[Bryan Gin-ge Chen]

As Kevin says, there's a way to build up proofs of simple logical propositions like this by "chasing underscores". I worked through a different example here and in another post linked there.

[Rocky Kamen-Rubio]

I resolve Q2. I misread how or.intro is defined. Its first input should be the type of the term NOT being exacted. Fixing this now makes the proof compile successfully.

example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
  iff.intro
    (assume h : (p ∨ q) ∨ r, or.elim h
      (assume hpq : p ∨ q, or.elim hpq
        (assume hp : p, show p ∨ (q ∨ r), from or.intro_left (q ∨ r) hp)
        (assume hq : q, show p ∨ (q ∨ r), from or.intro_right p (or.intro_left r hq)))
      (assume hr : r, show p ∨ (q ∨ r), from or.intro_right p (or.intro_right q hr)))
    (assume h2 : p ∨ (q ∨ r), or.elim h2
      (assume hp : p, show (p ∨ q) ∨ r, from or.intro_left r (or.intro_left q hp))
      (assume hqr : (q ∨ r), or.elim hqr
        (assume hq : q, show (p ∨ q) ∨ r, from or.intro_left r (or.intro_right p hq))
        (assume hr : r, show (p ∨ q) ∨ r, from or.intro_right (p ∨ q) hr)))

[Rocky Kamen-Rubio]

Q4: I'm confused how to handle an implication in the assumption of another implication, such as example : (((p → q) → p) → p) := sorry. I get intuitively that if we can get p out of p implying q, that means that p must always be true because "p implies q" doesn't give us p on its own. I don't see how we could translate that into lean though. I was thinking about doing a by_cases since this is in the classical logic section, but I feel like I don't have good tools to work with a variable like ((p → q) → p).

[Mario Carneiro]

do cases on p

[Rocky Kamen-Rubio]

Mario Carneiro said:

do cases on p

That was my original thought but I keep getting stuck here

example : (((p → q) → p) → p) :=
assume hpqp : (p → q) → p,
by_cases
  (assume hp : p, hp)
  (assume hnp : ¬ p, show ...)

I can't think of a way to use hpqp in a useful way here. I feel like maybe there's a function I'm forgetting.

[Mario Carneiro]

Prove false, by using the assumption and the implication (which will require you to prove p -> q)

[Reid Barton]

Q3 you have some extraneous commas after applying or.elim

[Reid Barton]

These term mode proofs require a lot of attention to detail.

[Lucas Teixeira]

I'm having a hard time with the classical problems, this is how far I got on the first one (Theorem boo) with before getting stuck. I may also just be completely on the wrong track too

open classical

variables p q r s : Prop


lemma helper : (¬r ∧ ¬s) → ¬(r ∨ s) :=
  (assume mh: (¬r ∧ ¬s),
   show ¬(r ∨ s),
   from (λ x: r ∨ s, or.elim x (λ hr: r, absurd hr mh.left) (λ hs: s, absurd hs mh.right) )
  )

lemma helper2 : ¬(r ∨ s) → ¬(p → r ∨ s) :=
  (assume mh : (r ∨ s) → false,
   show (p → r ∨ s) → false,
   from or.elim (em p)
     (assume x: p,
      show (p → r ∨ s) → false,
      from (λ f: (p → r ∨ s), mh (f x) )
     )
     (assume y: ¬p,
      show (p → r ∨ s) → false,
      from (λ g: (p → r ∨ s), ) -- This is where I'm stuck
     )
   )

theorem boo : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
  (assume mh: (p → r ∨ s),
   show ((p → r) ∨ (p → s)),
   from or.elim (em r)
     (assume hr: r,
      show ((p → r) ∨ (p → s)),
      from or.inl (λ hp: p, hr)
     )
     (assume hnr: ¬r,
      show ((p → r) ∨ (p → s)),
      from or.elim (em s)
        (assume hs: s,
         show ((p → r) ∨ (p → s)),
         from or.inr (λ hp1: p, hs)
        )
        (assume hns: ¬s,
         show ((p → r) ∨ (p → s)),
         from absurd mh -- helper2 (helper (and.intro hnr hns))
        )
     )
  )

[Mario Carneiro]

My suggestion for boo is to start by cases on em p

[Mario Carneiro]

you shouldn't need any other uses of EM

[Lucas Teixeira]

What do you mean exactly by cases on em p??
by_cases type is (p ->q) -> (~p ->q) -> q
while em p is p v ~p

[Lucas Teixeira]

My best guess is that you meant something like this:

theorem boo : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
  (assume mh: (p → r ∨ s),
   show ((p → r) ∨ (p → s)),
   from or.elim (em p)
     (assume hp: p,
      or.elim (mh hp)
        (λ hr: r, or.inl (λ hp: p, hr))
        (λ hs: s, or.inr (λ hp: p, hs))
     )
     (assume hnp: ¬p,
       by_cases mh ...
     )
  )

but that feels wrong and I think I'm misunderstanding you

[Chris B]

Pretty sure he meant or.cases_on, but you're pretty much there already with or.elim (em p).

[Chris B]

You're extremely close here. Without giving it away, just look at what resources you already have (the hypotheses) and look closely at the structure of the goal.

[Chris B]

Which I know sounds obvious.

[Lucas Teixeira]

Chris BThanks! I appreciate you giving me a nudge without giving it away. What I ended up with is this :

theorem boo : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
  (assume mh: (p → r ∨ s),
   show ((p → r) ∨ (p → s)),
   from or.elim (em p)
     (assume hp: p,
      or.elim (mh hp)
        (λ hr: r, or.inl (λ hp: p, hr))
        (λ hs: s, or.inr (λ hp: p, hs))
     )
     (assume hnp: p → false,
       or.inl(λ hp: p, absurd hp hnp )
     )
  )

Still, that last absurd feels a little brutish, and not so elegant.

Maybe there's another proof out there with a better pay off??

[Lucas Teixeira]

Wait, is posting final answers on this chat frowned upon?? I'll take it down if so

[Anne Baanen]

Perhaps spoiler tags?

````spoiler
```lean
theorem boo : _ := _
```
````

[Anne Baanen]

Becomes

theorem boo : _ := _

[Lucas Teixeira]

Anne Baanen Thanks for the tip!

[Will Wan]

How to prove this one?
¬(p → q) → p ∧ ¬q
Need help!

[Ruben Van de Velde]

What have you tried so far?

[Will Wan]

I tried to (em p).elim and (em q).elim, but cannot solve the hnp:¬p and hnq:¬q case. I think this is the wrong way.

[Ruben Van de Velde]

Try working by contradiction - you should be able to get there from ¬(p → q) and ¬(p ∧ ¬q) using some of the things you've proved before

[Eric Rodriguez]

I will say that casing on q is unnecessary

[Will Wan]

Managed to prove it by contradiction using lemma
¬(p ∧ ¬q) → (¬p ∨ q), (I used double em casing on p and q to prove this one, wonder why it works here)
(¬p ∨ q) → (p → q)
and finally ¬(p ∧ ¬q) → (p → q),
thanks! :)

[Eric Rodriguez]

for future's sake, my solution:

example {p q : Sort} [decidable p] : ¬(p → q) → p ∧ ¬q :=
λ h, decidable.by_cases (λ hp, ⟨hp, λ q, h (λ _, q)⟩) (λ hp, h.elim hp.elim)

[Fernand]

Hello, I'm also doing the exercises in the book Theorem Proving in Lean 4 and am not sure whether my proofs are actually correct.

My proof below does for example not return any error even though I have the impression that I'm not really proving anything:

¬(p ∧ q) → ¬p ∨ ¬q

variable (hpq : p ∧ q)

example : ¬(p ∧ q) → ¬p ∨ ¬q :=
fun h: ¬(p ∧ q) =>
Or.inl (fun hp : p => h hpq)

According to previous posts in this stream, the proof should be more elaborate than this and classical logic should be required. So whats going on?

[Reid Barton]

With variable (hpq : p ∧ q) you assumed p ∧ q, so then in the example from ¬(p ∧ q) it should be easy to prove anything.

[Fernand]

Thanks @Reid Barton seems obvious now that you mention it. I felt that I was cheating somehow so thanks for calling it out ;)