difference between exists with Type and Prop

Stream: new members

[Andrew Lubrino]

I've noticed that there are two types (and maybe others) of existential quantifiers in Lean. The first is more familiar to me and looks something like \ex (t : U), P t. In this case t is a Type (or in some places Sort, but I'm not exactly sure what this is). But then there's another existential that has the same structure, but instead of Type, t is a Prop. mathlib tells me that (∃ (h : p), q) ↔ p ∧ qwhere p is a Prop from exists_prop. I can memorize that this is true, but I'm trying to understand why we need this structure and what it is used for. If it's really just the same as conjunction, why don't we just always call it conjunction and cut out the confusing notation? I'd like to build some kind of internal justification that this is true.

[Kyle Miller]

That (∃ (h : p), q) ↔ p ∧ q lemma is a special case -- it's when q does not depend on p being true (more precisely: it's when the expression in the body of the existential doesn't make use of the h proof).

[Kyle Miller]

Sort is a way to make things be able to take either Prop or Type, so that we don't have to have a multitude of parallel definitions for each possibility. Sort 0 = Prop, Sort 1 = Type 0 = Type, Sort 2 = Type 1, and so on.

[Andrew Lubrino]

Okay. I think that makes things more clear. If p and q are larger statements, how would I tell if q depends on p? I'm guessing that if they share none of the same variables then q doesn't depend on p? Or is it really just as long as p doesn't appear anywhere after the comma in the existential?

[Andrew Lubrino]

Oh sorry, I just read your edit. That makes sense

[Andrew Lubrino]

so if instead we had(∃ (h : p), q ∧ p) , we wouldn't be able to use that lemma right? because the statement after the comma uses the h

[Kyle Miller]

That doesn't use h -- it needs to actually use h somewhere -- so the lemma still applies. I'll try to cook up a realistic example.

[Kyle Miller]

example {α : Type} (l : list α) (x : α) :
  ∃ (n : ℕ) (h : n < l.length), l.nth_le n h = x :=
sorry

[Kyle Miller]

Having multiple variables in an existential is the same as this:

example {α : Type} (l : list α) (x : α) :
  ∃ (n : ℕ), ∃ (h : n < l.length), l.nth_le n h = x :=
sorry

[Kyle Miller]

The function docs#list.nth_le takes both an index into a list and a proof that the index doesn't exceed its length.

[Andrew Lubrino]

Okay, I understand. the hypothesis in the existential is referenced by name, h, after the comma. In this case we couldn't use the lemma I was talking about above.

[Andrew Lubrino]

that makes more sense. I'm still a bit confused about having a Prop hypothesis in the existential. It's not something normally covered in an intro formal logic text, so I'm still trying to wrap my head around that

[Andrew Lubrino]

any good reading material you could suggest on that topic?

[Kyle Miller]

Prop existentials can be thought of as if statements, if that helps:

open_locale classical

example {P : Prop} (Q : P → Prop) :
  (∃ (h : P), Q h) ↔ if h : P then Q h else false :=
begin
  split_ifs; simp[*],
end

(If statements are slightly different, hence the open_locale classical line to try to turn off that difference.)

[Kyle Miller]

It's interesting how in dependent type theory you can pass around the fact h that a particular proposition P is true. The only book I know about is #tpil, but I'm not sure where it might talk specifically about this. Though, after working with dependent types for a while, it feels surprisingly natural that you can do this with existentials.

[Andrew Lubrino]

that's interesting. i've been meaning to work through that book. it would probably help me plug up all the gaps in my basics. thanks for all the help here!