## Stream: general

### Topic: tutorial_question

#### 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?

#### Mario Carneiro (Feb 01 2021 at 19:29):

What's the definition of up_bounds?

#### Daniel Papp (Feb 01 2021 at 19:30):

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

#### Mario Carneiro (Feb 01 2021 at 19:30):

Notice that it's a forall

#### 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)

#### 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

#### Daniel Papp (Feb 01 2021 at 19:33):

Wait $a \in A$ is the type of H?

yes

#### Mario Carneiro (Feb 01 2021 at 19:33):

Propositions are types

#### Daniel Papp (Feb 01 2021 at 19:34):

Yeah, I have to get used to that.

#### Daniel Papp (Feb 01 2021 at 21:19):

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

#### 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?

#### 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).

#### 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?

#### 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

#### 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

#### 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

#### 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

#### 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

#### 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.

#### 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

#### 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)

#### 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