## Stream: new members

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

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

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

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


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

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

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

#### Patrick Massot (Dec 04 2018 at 10:49):

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

#### Patrick Massot (Dec 04 2018 at 10:49):

The whole point is that r does not depend on anything

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

#### Patrick Massot (Dec 04 2018 at 10:54):

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

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

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


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


#### Carlesso Diego (Dec 04 2018 at 13:03):

Thank you!, that's perfect!

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

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