More documentation on the syntax of quantifiers?

Stream: new members

[Arien Malec]

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]

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]

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]

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]

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]

Why are your funs taking two y arguments?

[Arien Malec]

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

[Kyle Miller]

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]

That's not the type signature that you're aiming for with your example, right?

[Arien Malec]

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]

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]

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]

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

[Kyle Miller]

You use fun to create functions/foralls/implications

[Kyle Miller]

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]

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

[Kyle Miller]

∀ x, p x and ∀ (x : α), p x are exactly the same in this context.

[Kyle Miller]

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]

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]

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]

(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]

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]

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]

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]

@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]

@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]

@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]

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]

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

[Kyle Miller]

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

[Kyle Miller]

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]

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]

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]

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

[Kyle Miller]

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]

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

[Arien Malec]

since p is now defined as α → Prop rather than Prop there's an extra argument hidden here it seems?

[Kyle Miller]

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]

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]

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]

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]

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]

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]

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]

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]

Lean doesn't care about the fact that there's a p that's α → Prop

[Kyle Miller]

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]

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

[Arien Malec]

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]

To repeat back, ∀ (x : α), q x already is an implication, or only works when q is Type -> Prop?

[Kyle Miller]

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]

Here's an exercise for you:

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

[Arien Malec]

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]

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]

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]

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]

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]

yep, sartori achieved. Thanks!