Zulip Chat Archive

Stream: new members

Topic: Need help with exists.intro


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Logan Murphy (Nov 26 2020 at 17:38):

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

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Nov 26 2020 at 17:40):

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

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Nov 26 2020 at 17:58):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Nov 26 2020 at 18:01):

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

view this post on Zulip Patrick Massot (Nov 26 2020 at 18:01):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Logan Murphy (Nov 26 2020 at 18:12):

you want exact exists.intro a h

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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!

view this post on Zulip 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