# Zulip Chat Archive

## Stream: new members

### Topic: More documentation on the syntax of quantifiers?

#### Arien Malec (Sep 29 2022 at 18:40):

I'm working through TPIL4 (I don't believe the issues are any different in Lean3) and I find the documentation in TPIL to be under-explanatory for the syntax of quantifiers. For example, I don't understand why this works:

```
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
fun h1 : (∀ y, p y → q y) =>
fun (h2 : (∀ y, p y)) =>
fun (y : α) => (h1 y) (h2 y)
```

and why this does not...

```
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
fun (h: ∀ x, p x → q x) =>
fun {y: α} (hpy: p y) => (h y) hpy
```

or this

```
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
fun (h: ∀ x, p x → q x) => fun y =>
fun {y: α} (hpy: p y) => (h y) (hpy y)
```

and there doesn't seem to be anything in TPIL that explains *why* one works and one does not, or why lean4 gets very particular about constraining `y : α`

in some contexts but is quite happy to understand `y`

in others. I feel like I'm just trying things at random as opposed to having a deep theory about how Lean models the syntax of quantifiers...

#### Kyle Miller (Sep 29 2022 at 18:48):

The type `(∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x)`

is for a function that takes three arguments in the following order: a `∀ x, p x → q x`

, a `∀ x, p x`

, and an `α`

(I'm guessing based on context; it depends on what `q`

is)

#### Kyle Miller (Sep 29 2022 at 18:50):

Your `fun (h: ∀ x, p x → q x) => fun {y: α} (hpy: p y) => (h y) hpy`

(or, equivalently, `fun (h: ∀ x, p x → q x) {y: α} (hpy: p y) => (h y) hpy`

) has the wrong type for the second argument.

#### Kyle Miller (Sep 29 2022 at 18:50):

It looks like you're mistaking `(∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x)`

for `(∀ x, p x → q x) → (∀ x, p x → (∀ x, q x))`

#### Arien Malec (Sep 29 2022 at 18:52):

Fair. So if I fix the quantifier

```
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
fun (h: ∀ x, p x → q x) => fun y =>
fun {y: α} (hpy: ∀ y, p y) => (h y) (hpy y)
```

I get

```
type mismatch
fun {y} hpy => h y (hpy y)
has type
∀ {y : α}, (∀ (y : α), p y) → q y : Prop
but is expected to have type
∀ (x : α), q x : Prop
```

which seems to say that there's a quantifier problem in the result?

#### Kyle Miller (Sep 29 2022 at 18:53):

Why are your `fun`

s taking two `y`

arguments?

#### Arien Malec (Sep 29 2022 at 18:53):

But in the function that works, we don't specify quantifiers....

#### Kyle Miller (Sep 29 2022 at 18:55):

The error is telling you that `fun {y} hpy => h y (hpy y)`

has type `∀ {y : α}, (∀ (y : α), p y) → q y`

. It's something that takes an `α`

called `y`

and a `∀ (y : α), p y`

(with a differently scoped `y`

) and returns a `q y`

#### Kyle Miller (Sep 29 2022 at 18:56):

That's not the type signature that you're aiming for with your `example`

, right?

#### Arien Malec (Sep 29 2022 at 18:57):

OK, if I take the indirection out, I get the same result

```
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
fun (h: ∀ x, p x → q x) =>
fun {y: α} (hpy: ∀ y, p y) => (h y) (hpy)
```

which gives me the opposite error. Again, not disputing that one works and one doesn't -- I just don't read TPIL or any other documentation and having a theory as to the case of why I've quantified correctly in the first example up top, but incorrectly in the second.

#### Kyle Miller (Sep 29 2022 at 18:59):

Just keep in mind that `∀ (x : α), p x`

is how you write the type of a function that takes something of `α`

(called `x`

) and returns something of type `p x`

(which depends on the input value, so it's a *dependent* type). And, if the result is independent of the input value, it uses the arrow notation, so for example `p x → q x`

is the type of a function whose output type does not depend on the input value.

#### Andrew Yang (Sep 29 2022 at 18:59):

I've only used Lean3 so I'm not that sure, but I think the problem is that the order of `y`

and `hpy`

in the quantifier is reversed?

#### Kyle Miller (Sep 29 2022 at 19:00):

So implication/arrow is a special case of the forall notation, which we use because it looks nicer.

#### Kyle Miller (Sep 29 2022 at 19:00):

You use `fun`

to create functions/foralls/implications

#### Kyle Miller (Sep 29 2022 at 19:01):

So, just using the type, you know that your `fun`

has to look like

```
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ (x : α), q x) :=
fun (hpq : ∀ x, p x → q x) (hp : ∀ x, p x) (x : α) => ... something of type q x ...
```

#### Kyle Miller (Sep 29 2022 at 19:02):

You're allowed to drop the type from the forall syntax if it can be inferred.

#### Kyle Miller (Sep 29 2022 at 19:02):

`∀ x, p x`

and `∀ (x : α), p x`

are exactly the same in this context.

#### Kyle Miller (Sep 29 2022 at 19:02):

The `α`

itself is not being quantified, and the inference might be why you're feeling like you want to include `α`

as an extra argument to your functions.

#### Kyle Miller (Sep 29 2022 at 19:06):

Just to give one more example: if `p q : Prop`

, then `∀ (h : p), q`

and `p → q`

are exactly the same, since `q`

does not syntactically depend on `h`

.

#### Kyle Miller (Sep 29 2022 at 19:15):

Anyway, I hope this helps. I believe you mentioned you were familiar with Ocaml and Haskell, so the angle I'm going for is "`fun`

is an anonymous lambda, forall/implication are fancy function types, and you just need to get the correct number of arguments with the right types."

#### Kyle Miller (Sep 29 2022 at 19:19):

(A hint: be sure to take a look at the goal view in your editor to see what the actual types are after they've been elaborated. Here, using Lean 3, I see that the example's goal is `(∀ (x : α), p x → q x) → (∀ (x : α), p x) → ∀ (x : α), q x`

when pretty printed. This can be useful in other situations when Lean inserts additional arguments for you, for example in the `∀ x ∈ s, p x`

construct.)

#### Arien Malec (Sep 29 2022 at 19:47):

If I drop the `{y: α}`

I get

```
application type mismatch
p y
argument
y
has type
∀ (x : α), p x : Prop
but is expected to have type
α : Type
```

#### Arien Malec (Sep 29 2022 at 20:01):

Since we've defined `variable (α : Type) (p q : α → Prop)`

, the general flow of going from "for all x, IsHuman x implies IsMortal x" implies "for all x IsHuman x" implies "for all x Is Mortal X" which is what the types want.

But as I follow the goals, unless I get the invocation just so, the quantifiers are all messed up, As an example,

```
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
fun (h: ∀ x, p x → q x) =>
fun {y: α} (hpy: p y) => (h y) hpy
```

leads to this error, which doesn't make any sense to me

```
type mismatch
h y hpy
has type
q y : Prop
but is expected to have type
q hpy : Prop
```

#### Andrew Yang (Sep 29 2022 at 20:05):

Does this not work?

```
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
fun (h: ∀ x, p x → q x) =>
fun (hpy: ∀ y, p y) {y: α} => (h y) (hpy y)
```

#### Kyle Miller (Sep 29 2022 at 20:08):

@Arien Malec Given that the second argument is supposed to be of type `∀ x, p x`

, why are you writing that second `fun`

with its first argument having type `α`

?

```
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
fun (h: ∀ x, p x → q x) =>
fun {y: α} (hpy: p y) => (h y) hpy
```

Please let me know what about what I wrote doesn't make sense.

#### Kyle Miller (Sep 29 2022 at 20:09):

@Andrew Yang Just note that the `{y: α}`

"should" be `(y: α)`

since the expected type has an explicit argument rather than an implicit one. It doesn't matter in this case.

#### Kyle Miller (Sep 29 2022 at 20:11):

@Arien Malec Just to check, are you familiar with how `fun {y: α} (hpy: p y) => (h y) hpy`

is equivalent to `fun {y: α} => fun (hpy: p y) => (h y) hpy`

?

#### Arien Malec (Sep 29 2022 at 20:12):

yep, that's not the issue here, it's how quantifiers interact.

And in particular why we have to have a `(y: α)`

in the last place here.

#### Kyle Miller (Sep 29 2022 at 20:13):

It's because it corresponds to the argument for `∀ x, q x`

#### Kyle Miller (Sep 29 2022 at 20:14):

I'm curious what you're seeing as "interacting" quantifiers

#### Kyle Miller (Sep 29 2022 at 20:15):

Here's another hint. The following types are completely equivalent:

```
(∀ (x : α), p x → q x) → (∀ (x : α), p x) → ∀ (x : α), q x
∀ (hpq : ∀ (x : α), p x → q x) (hp : ∀ (x : α), p x) (x : α), q x
```

#### Arien Malec (Sep 29 2022 at 20:19):

So what's perhaps misleading me is that in the previous chapter of TPIL, I get to do things like

`theorem and_dist_right {p q r: Prop} : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := sorry`

and my types there are implicit parameters, but now I have a very explicit `x`

that appears in the argument list that appears to be the key to making all the types work.

Again, not confused by the currying here, but probably by the way `p`

is defined here as opposed to the way `p`

is defined in the previous chapter.

#### Kyle Miller (Sep 29 2022 at 20:19):

Tactics are also useful for poking around and seeing what's what. The `intros`

tactic is for automatically creating `fun`

s:

```
variable (α : Type) (p q : α → Prop)
example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
by
intros
/-
α : Type
p q : α → Prop
: ∀ (x : α), p x → q x -- the first argument
: ∀ (x : α), p x -- the second argument
x✝ : α -- the third argument
⊢ q x✝ -- the goal (q x)
-/
```

#### Arien Malec (Sep 29 2022 at 20:20):

From NNG, this would be very grokable in tactics land.

#### Kyle Miller (Sep 29 2022 at 20:21):

Arien Malec said:

`theorem and_dist_right {p q r: Prop} : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := sorry`

With this example, `p`

, `q`

, and `r`

are automatically introduces (no need for `fun`

) since they come "before the colon".

#### Kyle Miller (Sep 29 2022 at 20:21):

It's not about implicit/explicit arguments, just to clarify

#### Arien Malec (Sep 29 2022 at 20:21):

since `p`

is now defined as `α → Prop`

rather than `Prop`

there's an extra argument hidden here it seems?

#### Kyle Miller (Sep 29 2022 at 20:23):

Also, by the way, if those `p`

, `q`

, and `r`

came "after the colon" you'd start like this:

```
theorem and_dist_right : ∀ {p q r: Prop}, p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) :=
fun {p q r : Prop} (h : p ∧ (q ∨ r)) => sorry
```

#### Kyle Miller (Sep 29 2022 at 20:24):

Arien Malec said:

since

`p`

is now defined as`α → Prop`

rather than`Prop`

there's an extra argument hidden here it seems?

No, there's nothing special about `α → Prop`

. That just means `p`

needs to take an argument.

#### Kyle Miller (Sep 29 2022 at 20:25):

If you want this new example to look analogous to `and_dist_right`

, it could easily be

```
example {α : Type} {p q : α → Prop} : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
sorry
```

#### Kyle Miller (Sep 29 2022 at 20:26):

You could even write this as

```
example (α : Type) (p q : α → Prop) (hpq : ∀ x, p x → q x) (hp : ∀ x, p x) (x : α) : q x :=
sorry
```

if you want to avoid needing to write the `fun`

s yourself.

#### Kyle Miller (Sep 29 2022 at 20:27):

Notice it's `hp : ∀ x, p x`

. This `hp`

is a function that takes any arbitrary `x : α`

and returns a proof of `p x`

for that `x`

.

#### Kyle Miller (Sep 29 2022 at 20:28):

This is different from taking arguments `{y: α} (hpy: p y)`

, which is saying "here is some specific `y : α`

for which `p y`

is true"

#### Arien Malec (Sep 29 2022 at 20:29):

Right, again that's the lightbulb moment here -- since we've defined `p`

as `α → Prop`

I need to give it something of type `α`

, which is why I need a `(y : α)`

in the last parameter.

#### Kyle Miller (Sep 29 2022 at 20:31):

No, it's so much simpler than that, it's because the end of the type is `∀ (x : α), q x`

, so the last argument is this `x : α`

from the quantifier

#### Kyle Miller (Sep 29 2022 at 20:31):

Lean doesn't care about the fact that there's a `p`

that's `α → Prop`

#### Kyle Miller (Sep 29 2022 at 20:33):

Just so we're on the same page, you're reading these forall quantifications as being the same sort of thing as an implication, right?

#### Kyle Miller (Sep 29 2022 at 20:33):

(they're both "pi types" under the hood, just pretty printed differently)

#### Arien Malec (Sep 29 2022 at 20:33):

`q`

is defined the same way, which is why `q x`

even makes sense, right? `q x`

is a `Prop`

because `q`

is `α → Prop`

I thought all along that my problem was with the quantifiers, but it was with not having anything of type `α `

to apply this to.

Now I *still don't understand why Lean was telling me

```
type mismatch
h y hpy
has type
q y : Prop
but is expected to have type
q hpy : Prop
```

#### Arien Malec (Sep 29 2022 at 20:34):

To repeat back, `∀ (x : α), q x`

already is an implication, or only works when `q`

is `Type -> Prop`

?

#### Kyle Miller (Sep 29 2022 at 20:36):

It is already the same sort of thing as an implication. A function that takes something of type alpha (call it `x`

) and returns something of type `q x`

.

#### Kyle Miller (Sep 29 2022 at 20:36):

Here's an exercise for you:

```
example (α : Type) (p q : Prop) : (∀ (x : α), p → q) → (∀ (x : α), p) → ∀ (x : α), q :=
sorry
```

#### Arien Malec (Sep 29 2022 at 20:36):

Or quoting from the book, in language I didn't understand "If `p`

is any expression, `∀ x : α, p`

is nothing more than alternative notation for `(x : α) → p`

, with the idea that the former is more natural than the latter in cases where p is a proposition. "

#### Kyle Miller (Sep 29 2022 at 20:37):

The `(x : α) → foo`

notation is equivalent to `∀ x : α, foo`

, where `foo`

can be any expression involving (or not involving) `x`

. If `foo`

does not involve `x`

, then the notation is also equivalent to `α → foo`

.

#### Arien Malec (Sep 29 2022 at 20:40):

```
example (α : Type) (p q : Prop) : (∀ (x : α), p → q) → (∀ (x : α), p) → ∀ (x : α), q :=
fun (h₁: ∀ (y : α), p → q) => fun (h₂: ∀ (x : α), p) => fun (x : α) => (h₁ x) (h₂ x)
```

#### Kyle Miller (Sep 29 2022 at 20:41):

The point of this exercise is that there is absolutely no difference between it and your other one for how you prove it.

#### Kyle Miller (Sep 29 2022 at 20:42):

For that last error message you were getting, I'm pretty sure it's telling you something irrelevant because you didn't have the `fun`

s structured correctly

#### Arien Malec (Sep 29 2022 at 20:43):

yep, sartori achieved. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC