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

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 funs 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 funs structured correctly

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

yep, sartori achieved. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC