## 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 sorrys 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