## Stream: new members

### Topic: Need help with exists.intro

#### Lars Ericson (Nov 26 2020 at 17:19):

I can't figure out how to get the syntax right on this:

open classical
variables (α : Type*) (p q : α → Prop)
variable r : Prop

example : r → (∃ x : α, r) :=
begin
intro h,
exact exists.intro r h,
end


the goal state before the exists.intro is

α : Type u_1,
r : Prop,
h : r
⊢ ∃ (x : α), r


So I have proof h of r but it's saying

Display GoalDisplay Messages
9:8: error:
type mismatch at application
exists.intro r
term
r
has type
Prop : Type
but is expected to have type
α : Type u_1
state:
α : Type u_1,
r : Prop,
h : r
⊢ ∃ (x : α), r


I want x but I don't know how to declare x:α because it won't let me do something like

assume x,


before the exact, complaining that

assume tactic failed, Pi/let expression expected
state:
α : Type u_1,
r : Prop,
h : r
⊢ ∃ (x : α), r


#### Bryan Gin-ge Chen (Nov 26 2020 at 17:36):

The example is false if α is an empty type, so you'll need to add an additional assumption of nonempty α and use that.

#### Logan Murphy (Nov 26 2020 at 17:38):

example (H : inhabited α) : r → (∃ x : α, r) :=
begin
intro h_r,
use H.default, assumption
end


#### Lars Ericson (Nov 26 2020 at 17:38):

Thank you @Bryan Gin-ge Chen and @Logan Murphy . In conclusion, this setup in the text:

open classical

variables (α : Type*) (p q : α → Prop)
variable a : α
variable r : Prop

example : (∃ x : α, r) → r := sorry


is unsolvable without additional language they didn't provide.

#### Bryan Gin-ge Chen (Nov 26 2020 at 17:40):

Well, that setup is actually correct because it has variable a : ﻿α.

#### Lars Ericson (Nov 26 2020 at 17:41):

@Bryan Gin-ge Chen , that is a bit counterintuitive because a is not referenced at all in the example.

#### Marc Huisinga (Nov 26 2020 at 17:42):

Lars Ericson said:

Bryan Gin-ge Chen , that is a bit counterintuitive because a is not referenced at all in the example.

because you need it to prove the statement :)

#### Lars Ericson (Nov 26 2020 at 17:43):

What are the rules around inhabited, for example it doesn't like

example : r → (∃ x : inhabited α, r) := sorry


saying

function expected at
sorry
term has type
?m_1


I.e. I would rather say something explicitly in the theorem statement rather than rely on a context dependency for the proof to go through.

#### Lars Ericson (Nov 26 2020 at 17:45):

Doing this doesn't seem to help:

variables (α : inhabited Type*)


because then when I do this:

example : r → (∃ x : α, r) :=
begin
intro h,
exact exists.intro r h,
end


I get the error

Display GoalDisplay Messages
8:21: error:
type expected at
α
term has type
inhabited (Type u_1)


#### Lars Ericson (Nov 26 2020 at 17:48):

Even doing this:

example (H : inhabited α) : r → (∃ x : α, r) :=
begin
intro h_r,
use H.default, assumption
end


is very clunky because you're still using H, an unused variable, to introduce a property of α, rather than decorating α directly. It seems very un-denotational. Not that there's anything wrong with that, I'm just saying.

#### Logan Murphy (Nov 26 2020 at 17:50):

I don't know if this is the intended solution, but you can specify the instance in the variables

open classical

variables (α : Type*) (p q : α → Prop) [nonempty α]
variable r : Prop

example :  r → (∃ x : α, r) :=
begin
intros h_r, use classical.arbitrary α, assumption
end


#### Patrick Massot (Nov 26 2020 at 17:54):

Lars, what you are writing makes no sense at all. Did you read the explanation about inhabited in TPIL?

#### Patrick Massot (Nov 26 2020 at 17:55):

And if you don't like variables, why don't you simply write

example (α : Type*) (a : α) (r : Prop) :  (∃ x : α, r) → r := sorry


#### Bryan Gin-ge Chen (Nov 26 2020 at 17:57):

To be 100% clear, inhabited and nonempty are not needed at all given the setup in the text:

variables (α : Type*) (p q : α → Prop)
variable a : α
variable r : Prop

example : r → (∃ x : α, r) := λ h, exists.intro a h


#### Bryan Gin-ge Chen (Nov 26 2020 at 17:58):

They are only needed if variable a : α is omitted.

#### Logan Murphy (Nov 26 2020 at 17:58):

Yes, I think that's where miscommunication is happening. I didn't realize it was an exercise from TPIL at first

#### Logan Murphy (Nov 26 2020 at 18:00):

Also, the naive "tactic mode" version of Bryan's proof doesn't know about a

open classical

variables (α : Type*) (p q : α → Prop)
variable a : α
variable r : Prop

example :  r → (∃ x : α, r) :=
begin
intro r_h, use a, --fails
end


#### Patrick Massot (Nov 26 2020 at 18:01):

Yes, Lean won't try to guess which variable to include using a tactic proof.

#### Patrick Massot (Nov 26 2020 at 18:01):

And I think that relying on Lean to pick up variables from proofs is bad style.

#### Logan Murphy (Nov 26 2020 at 18:03):

So, the answer to Lars' original problem, is the proof inside the exact is correct, but putting it within the begin .. end takes away the crucial variable (assuming the variable is in the scope)

#### Lars Ericson (Nov 26 2020 at 18:08):

In summary, there's no way to make this begin end proof work?

open classical

variables (α : Type*) (p q : α → Prop)
variable a : α
variable r : Prop

example : r → (∃ x : α, r) :=
begin
intro h,
exact exists.intro r h,
end


because even with variable a : α in context, it's failing with

type mismatch at application
exists.intro r
term
r
has type
Prop : Type
but is expected to have type
α : Type u_1
state:
α : Type u_1,
r : Prop,
h : r
⊢ ∃ (x : α), r


I am trying to follow the pattern of this example, which works fine:

open nat

example : ∃ x : ℕ, x > 0 :=
begin
have h : 1 > 0, from zero_lt_succ 0,
exact exists.intro 1 h,
end


#### Bryan Gin-ge Chen (Nov 26 2020 at 18:10):

Yes, you have to add (a : α) explicitly to the list of assumptions of the example to get the tactic proof to work or add include a before the example. This is discussed at the end of 5.1 in TPiL.

#### Lars Ericson (Nov 26 2020 at 18:12):

No, still complaining:

open classical

variables (α : Type*) (p q : α → Prop)
variable a : α
variable r : Prop

example (a : α) : r → (∃ x : α, r) :=
begin
intro h,
exact exists.intro r h,
end


gives

Display GoalDisplay Messages
10:8: error:
type mismatch at application
exists.intro r
term
r
has type
Prop : Type
but is expected to have type
α : Type u_1
state:
α : Type u_1,
r : Prop,
a : α,
h : r
⊢ ∃ (x : α), r


#### Logan Murphy (Nov 26 2020 at 18:12):

you want exact exists.intro a h

#### Lars Ericson (Nov 26 2020 at 18:16):

Thank you @Logan Murphy , that works. Understanding is dawning. a is the evidence of an x such that r. r is not the evidence of the bound variable. OK. Sorry that took so long! The nat example was confusing in that regard, I didn't realize that it was saying that 1 was the evidence of the bound variable.

#### Logan Murphy (Nov 26 2020 at 18:17):

Exactly. The existential is quantified over alpha, so you need to give it an object of that type (of which the only known one is a), as well as a proof of the proposition r (in this case, h).

#### Lars Ericson (Nov 26 2020 at 18:18):

Still, that makes what should be the first and apparently most simple and basic exercise in the text actually an extremely tricky one.

#### Bryan Gin-ge Chen (Nov 26 2020 at 18:24):

Learning Lean from TPiL is definitely a challenge. But make sure you understand everything that's happening in each section before proceeding on to the following ones since the text moves quickly.

#### Logan Murphy (Nov 26 2020 at 18:26):

The explanation in the text is

The introduction rule is straightforward: to prove ∃ x : α, p x, it suffices to provide a suitable term t and a proof of p t.

Maybe this would be a bit more clear

The introduction rule is straightforward: to prove ∃ x : α, p x, it suffices to provide a suitable term t: α and a proof of p t.

It's also a bit more natural when the existential is a predicate on α,, rather than just some Prop
But that's also the point of the exercise :)

#### Lars Ericson (Nov 26 2020 at 18:32):

Yes, that is more clear. However I would have the text spell out the case where p is actually free of x entirely, because it confused me that I had to demonstrate the existence of something not actually used in p. It's a subtle point that wouldn't hurt getting walked through in a less terse way. I wonder if you had a classroom of 50 students and didn't help them as much as you've helped me, how many of them would be able to read "The introduction rule is straightforward: to prove ∃ x : α, p x, it suffices to provide a suitable term t: α and a proof of p t." and know that they had to declare a variable of type α and invoke at as evidence. I don't want to belabor the point, I just don't think anybody would get it without expert assistance. Thank you for your help!

#### Patrick Massot (Nov 26 2020 at 19:15):

Lars Ericson said:

I don't want to belabor the point, I just don't think anybody would get it without expert assistance.

This is simply wrong. I think at least 100 people from this chat learned all this from TPIL without expert assistance about this point. We also know that at least as many people completed the natural number game without asking any question to anyone. There is no issue with asking questions, and I think everybody answering your questions here is happy to do so. And suggesting improvements to documentation is great. But that sentence I quoted is wrong.

Last updated: May 10 2021 at 00:31 UTC