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

Stream: new members

[Carlesso Diego]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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
)

[Kevin Buzzard]

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?

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

The whole point is that r does not depend on anything

[Patrick Massot]

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⟩

[Patrick Massot]

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

[Carlesso Diego]

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!

[Mario Carneiro]

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⟩⟩

[Mario Carneiro]

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 )

[Carlesso Diego]

Thank you!, that's perfect!

[Kevin Buzzard]

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 :-)

[Carlesso Diego]

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! :)