Zulip Chat Archive

Stream: new members

Topic: TPIL Chapter 3 Exercises


view this post on Zulip 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)))

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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. .

view this post on Zulip 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))))

view this post on Zulip 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!

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Mar 05 2020 at 20:29):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)))

view this post on Zulip 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).

view this post on Zulip Mario Carneiro (Mar 05 2020 at 21:19):

do cases on p

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Reid Barton (Mar 05 2020 at 21:52):

Q3 you have some extraneous commas after applying or.elim

view this post on Zulip 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