Need help with exists.intro

Stream: new members

[Lars Ericson]

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]

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]

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

[Lars Ericson]

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]

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

[Lars Ericson]

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

[Marc Huisinga]

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]

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]

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]

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]

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]

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

[Patrick Massot]

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]

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]

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

[Logan Murphy]

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

[Logan Murphy]

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]

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

[Patrick Massot]

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

[Logan Murphy]

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]

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]

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]

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]

you want exact exists.intro a h

[Lars Ericson]

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]

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]

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]

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]

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]

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]

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.