Zulip Chat Archive

Stream: general

Topic: tutorial_question


view this post on Zulip Daniel Papp (Feb 01 2021 at 19:27):

So here is an exact statement -> https://github.com/leanprover-community/tutorials/blob/master/src/exercises/00_first_proofs.lean#L160 I don't quite understand. hx.2 is

  x \in up_bounds(low_bounds A)

and we sort of apply it as a function? I don't really understand how can we turn the above statement into a function or I'm just mistaken and this is something completely different?

view this post on Zulip Mario Carneiro (Feb 01 2021 at 19:29):

What's the definition of up_bounds?

view this post on Zulip Daniel Papp (Feb 01 2021 at 19:30):

https://github.com/leanprover-community/tutorials/blob/master/src/exercises/00_first_proofs.lean#L27

view this post on Zulip Mario Carneiro (Feb 01 2021 at 19:30):

Notice that it's a forall

view this post on Zulip Mario Carneiro (Feb 01 2021 at 19:31):

x \in {y | \forall a, P(y,a)} unfolds to \forall a, P(x, a) so applying it to b yields P(x, b)

view this post on Zulip Mario Carneiro (Feb 01 2021 at 19:32):

In fact, the notation ∀ a ∈ A, a ≤ x is sugar for ∀ a, ∀ (H : a ∈ A), a ≤ x so it's two foralls, hence two applications are used in the proof

view this post on Zulip Daniel Papp (Feb 01 2021 at 19:33):

Wait aAa \in A is the type of H?

view this post on Zulip Mario Carneiro (Feb 01 2021 at 19:33):

yes

view this post on Zulip Mario Carneiro (Feb 01 2021 at 19:33):

Propositions are types

view this post on Zulip Daniel Papp (Feb 01 2021 at 19:34):

Yeah, I have to get used to that.

view this post on Zulip Daniel Papp (Feb 01 2021 at 21:19):

I watched Wadler's talk at Strangeloop in the end. Now I have a good idea.

view this post on Zulip Daniel Papp (Feb 01 2021 at 21:19):

Is there a part of the documentation which gives some idea how to desugar things in lean?

view this post on Zulip Mario Carneiro (Feb 01 2021 at 21:23):

most of that is defined when the notation is introduced. I don't have any particular place to point to for this one; the basic idea is that if you have a binder like \all (a op b), ... or \ex (a op b), ... where op is some infix operator and a is a variable, then it duplicates the binder to \all a, \all (H : a op b) or \ex a, \ex (H : a op b).

view this post on Zulip Daniel Papp (Feb 01 2021 at 21:29):

I see. Maybe a stupid question, but how are the quantifiers transformed into types? I mean I understand that conjunction is transformed into the product type and implication transformed into functions, but how is the universal quantifier transformed into a type?

view this post on Zulip Mario Carneiro (Feb 01 2021 at 21:30):

A universal quantifier is the same (literally the same thing in lean) as the Pi type, a dependent function type

view this post on Zulip Mario Carneiro (Feb 01 2021 at 21:30):

\forall x : A, B x is the type of functions f such that for a in A, f a : B a

view this post on Zulip Mario Carneiro (Feb 01 2021 at 21:31):

You can also use \Pi instead of \forall; lean prefers \forall in pretty printing if B x is a proposition

view this post on Zulip Mario Carneiro (Feb 01 2021 at 21:32):

Lean 4 is switching to the adga-style notation (x : A) -> B x which makes the notational similarity to implication more obvious

view this post on Zulip Mario Carneiro (Feb 01 2021 at 21:33):

in lean A -> B is both the nondependent function type and also implication of propositions, and is a special case of Pi/forall when the rhs doesn't depend on the lhs

view this post on Zulip Daniel Papp (Feb 01 2021 at 21:37):

Ok, I guess I need to read up on this too. The wikipedia page says that the Sigma type is the pair of the existential quantifier in a similar sense.

view this post on Zulip Mario Carneiro (Feb 01 2021 at 21:43):

Yep, \ex (x : A), B x is a pair of an a : A and b : B a

view this post on Zulip Mario Carneiro (Feb 01 2021 at 21:44):

in this case though lean has a distinct definition called \Sigma which does the same thing but for data (non-propositions)

view this post on Zulip Mario Carneiro (Feb 01 2021 at 21:45):

the reason being that an existential is always a proposition even if A is not, so there is no "first projection" function from \ex (x : A), B x to A, while there is a first and second projection for \Sigma


Last updated: May 11 2021 at 23:11 UTC