# Zulip Chat Archive

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

`variables (α : Type) (r : Prop)`

line as well, so that anyone can copy-paste your code right awayYes -- 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