tutorial_question

Stream: general

[Daniel Papp]

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]

What's the definition of up_bounds?

[Daniel Papp]

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

[Mario Carneiro]

Notice that it's a forall

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

yes

[Mario Carneiro]

Propositions are types

[Daniel Papp]

Yeah, I have to get used to that.

[Daniel Papp]

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

[Daniel Papp]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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