# Zulip Chat Archive

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

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

yes

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

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