# Zulip Chat Archive

## Stream: new members

### Topic: TPIL Chapter 3 Exercises

#### Rocky Kamen-Rubio (Mar 05 2020 at 19:33):

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 (Mar 05 2020 at 19:50):

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 (Mar 05 2020 at 19:51):

Q2: your term is not really complete so it's not surprising you have errors. Why not put in some `_`

s or `sorry`

s to make the term compile?

#### Kevin Buzzard (Mar 05 2020 at 19:51):

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

#### Kevin Buzzard (Mar 05 2020 at 19:53):

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 (Mar 05 2020 at 19:58):

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 (Mar 05 2020 at 20:05):

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 (Mar 05 2020 at 20:07):

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 (Mar 05 2020 at 20:27):

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 (Mar 05 2020 at 20:29):

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 (Mar 05 2020 at 20:29):

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

#### Kevin Buzzard (Mar 05 2020 at 20:31):

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 (Mar 05 2020 at 20:33):

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 (Mar 05 2020 at 20:34):

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 (Mar 05 2020 at 20:44):

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 (Mar 05 2020 at 21:18):

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 (Mar 05 2020 at 21:19):

do cases on `p`

#### Rocky Kamen-Rubio (Mar 05 2020 at 21:22):

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 (Mar 05 2020 at 21:22):

Prove `false`

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

)

#### Reid Barton (Mar 05 2020 at 21:52):

Q3 you have some extraneous commas after applying `or.elim`

#### Reid Barton (Mar 05 2020 at 21:53):

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

Last updated: May 12 2021 at 05:19 UTC