Zulip Chat Archive

Stream: new members

Topic: Exercises chapter 4 - α → (( ∀ x: α, r ) ↔ r)


view this post on Zulip Carlesso Diego (Dec 04 2018 at 10:40):

Hello! First time I write here! I'm trying to learn Lean step by step following the online tutorial "theorem proving in Lean" doing as many exercises as I can.
At the moment I'm having a problem (probably more on the logic part of the thing) on the first one of exercise 2 in chapter 4:
α → (( ∀ x: α, r ) ↔ r)

theorem e1: α → (( ∀ x: α, r ) ↔ r) :=
assume y:α,
iff.intro
(assume h: (∀ x, r),
show r, from h y
)
-- wrong from now on
(assume hr: r,
assume x : α,
assume hyr : (∀ x , r),
show (∀ x: α , r), from hyr
)

First of all, I don't know if assuming y:α solve the "α →" part, but I'm struggling in the second part of the iff.intro (I think that the first part is correct)
the error is :

" type mismatch at application
{mp := λ (h : α → r), show r, from h y, mpr := λ (hr : r) (x : α) (hyr : α → r), show α → r, from hyr}
term
λ (hr : r) (x : α) (hyr : α → r), show α → r, from hyr
has type
r → α → (α → r) → α → r
but is expected to have type
r → α → r "

And I understand why it returns that error, but, how am I supposed to show (∀ x: α , r) from r otherwise? It's probably something stupid I'm missing but as stupid as it is I can't see it. Looking at the others in ex2 I think it's probably something I'm getting wrong in bringing outside a universal quantifier.
Also, I've never used Zulip or something like that, so let me know if I did something wrong.

view this post on Zulip Kevin Buzzard (Dec 04 2018 at 10:42):

For Zulip -- if you write your code between triple backticks ``` then it gets formatted nicely. Even better, if you write ```lean for the top triple backtick then you get syntax highlighting as well.

view this post on Zulip Kevin Buzzard (Dec 04 2018 at 10:42):

theorem e1: α  ((  x: α, r )  r) :=
assume y:α,
iff.intro
(assume h: ( x, r),
show r, from h y
)
-- wrong from now on
(assume hr: r,
assume x : α,
assume hyr : ( x , r),
show ( x: α , r), from hyr
)

view this post on Zulip Kevin Buzzard (Dec 04 2018 at 10:43):

But your code doesn't run for me -- can you post some fully working example so I can get it to compile without having to think?

view this post on Zulip Patrick Massot (Dec 04 2018 at 10:47):

Carlesso, What Kevin means is you should include your variables (α : Type) (r : Prop) line as well, so that anyone can copy-paste your code right away

view this post on Zulip Patrick Massot (Dec 04 2018 at 10:48):

About the question itself, you are complicating things needlessly. It's probably because the question is a bit silly

view this post on Zulip Patrick Massot (Dec 04 2018 at 10:49):

The proof of the second implication is simply assume hr _, hr

view this post on Zulip Patrick Massot (Dec 04 2018 at 10:49):

The whole point is that r does not depend on anything

view this post on Zulip Patrick Massot (Dec 04 2018 at 10:53):

and the first one can be shortened to assume h, h y. If you really want to use term mode, you can go all the way down the obfuscation road until you reach theorem e1 (α : Type) (r : Prop): α → (( ∀ x: α, r ) ↔ r) := λ y, ⟨λ h, h y, λ h _, h⟩

view this post on Zulip Patrick Massot (Dec 04 2018 at 10:54):

The opposite extreme is to load mathlib and replace the proof by by tauto.

view this post on Zulip Carlesso Diego (Dec 04 2018 at 12:23):

Carlesso, What Kevin means is you should include your variables (α : Type) (r : Prop) line as well, so that anyone can copy-paste your code right away

Ok!, sorry about that, I will keep that in mind.

About the problem you are right! and what you suggest work well; I was aware of r but I wasn't able to "say" that in Lean.

About the question itself, you are complicating things needlessly. It's probably because the question is a bit silly

I was trying to be consistent with the "solution scheme" that the chapter has, for example (∀x, p x ∧ q x ) ↔ (∀ x, p x) ∧ (∀ x, q x) is :

variables ( α : Type) ( r : Prop) (p q : α  Prop)
theorem e2: (x, p x  q x )  ( x, p x)  ( x, q x) :=
iff.intro
    (
    assume h: ( x : α , p x  q x),
    show( x, p x)  ( x, q x), from and.intro
        (assume y: α, show p y, from and.left(h y))
        (assume y: α, show q y, from and.right(h y))
    )
    (assume h1:( x, p x)  ( x, q x),
    assume y:α,
    have hp: ( x, p x), from h1.left,
    have hq: ( x, q x), from h1.right,
    have hp2: p y, from hp y,
    have hq2 : q y, from hq y,
    show p y  q y, from and.intro hp2 hq2
    )

It's a different exercise; I don't know if it could be solved with your method (right now it works), I have not reached that part on TPIL yet I think, or I'm not very practical to use it right now; but it's just to show you what an exercise there looks like and what I was trying to get.
Thank you by the way, problem solved!

view this post on Zulip Mario Carneiro (Dec 04 2018 at 12:29):

here's a compactified proof of that theorem:

variables {α : Type} {p q : α  Prop}
theorem e2 : (x, p x  q x)  ( x, p x)  ( x, q x) :=
⟨λ H, ⟨λ x, (H x).left, λ x, (H x).right, λ H₁, H₂ x, H₁ x, H₂ x⟩⟩

view this post on Zulip Mario Carneiro (Dec 04 2018 at 12:32):

and a proof of the first theorem in that style:

theorem e1 : α  (( x : α, r)  r) :=
assume y : α,
iff.intro
  ( assume h : ( x, r),
    show r, from h y )
  ( assume hr : r,
    assume x : α,
    show r, from hr )

view this post on Zulip Carlesso Diego (Dec 04 2018 at 13:03):

Thank you!, that's perfect!

view this post on Zulip Kevin Buzzard (Dec 04 2018 at 13:11):

Carlesso, What Kevin means is you should include your variables (α : Type) (r : Prop) line as well, so that anyone can copy-paste your code right away

Yes -- sorry for the brevity! I just had 2 minutes before a lecture and I wanted to help but then the code didn't run so I had to give up :-)

view this post on Zulip Carlesso Diego (Dec 04 2018 at 13:26):

Carlesso, What Kevin means is you should include your variables (α : Type) (r : Prop) line as well, so that anyone can copy-paste your code right away

Yes -- sorry for the brevity! I just had 2 minutes before a lecture and I wanted to help but then the code didn't run so I had to give up :-)

Don't worry!, I didn't think about the variables thing, I'm working with different exercises in the same file and I forgot about them, totally my fault. Thank you for your time anyway! :)


Last updated: May 16 2021 at 21:11 UTC