Zulip Chat Archive

Stream: new members

Topic: Confused with double "exists"


view this post on Zulip Walter Moreira (May 07 2020 at 01:50):

I'm going over the tutorial proposed by @Patrick Massot . I'm confused about what it means the double "exists" in a judgement like

key :  (n : ),  (a : ) (H : a  A), a < x + 1 / (n + 1)

How does that notation translates into bare Exists? Is it a way to ask Lean to display the unfolding of the definition?

view this post on Zulip Reid Barton (May 07 2020 at 02:05):

It means

key :  (n : ),  (a : ),  (H : a  A), a < x + 1 / (n + 1)

view this post on Zulip Walter Moreira (May 07 2020 at 02:27):

Thank you @Reid Barton That's what I was expecting. I got confused about it with the application of choose u hu using key which added

hu :  (n : ), u n  A  u n < x + 1 / (n + 1)

and I couldn't see how Lean was generating the \wedge in that clause. It seems that it becomes more clear when doing choose u v hu which generates two functions.

I guess that Lean automatically combines them with \wedge if I provide only one variable?

view this post on Zulip Reid Barton (May 07 2020 at 02:29):

I think the choose tactic has some specific magic to get rid of unnecessary ∃ (in the sense that the variable, here H, is not used) and turn them into ∧.

view this post on Zulip Patrick Massot (May 07 2020 at 08:00):

This is very similar to what is explained at https://github.com/leanprover-community/tutorials/blob/a1b5620e098deb0c06c902b1151b02aca5f46033/src/exercises/06_sub_sequences.lean#L67-L73 but I should probably repeat that comment. Also, you can ask Lean to rewrite this abbreviation using rw exists_prop.


Last updated: May 14 2021 at 06:16 UTC