Existential quantifier and Sigma type

Stream: new members

[Martin Dvořák]

I am confused about existential quantifiers and Sigma types.

constant α : Type
constant p : α -> Prop
#check Π x : α, p x
#check ∀ x : α, p x
#check Σ x : α, p x
#check ∃ x : α, p x

Why is Σ x syntactically incorrect whereäs both Π x and ∀ x are syntactically correct (and mean the same thing)? Isn't ∀ just a syntactic sugar for Π in the same way that ∃ is, at least I supposed, a syntactic sugar for Σ under the assumption that p x : Prop ?

[Reid Barton]

(First, all of these are syntactically correct.)
∀ and Π are indeed the same, but ∃ and Σ are completely separate: the first is docs#Exists and the second is docs#sigma.

[Martin Dvořák]

Oh, sorry, I considered type mismatch to be a kind of syntactic error.

[Martin Dvořák]

How can I find a similar documentation for Pi instead of Sigma?

[Chris B]

Pi is a primitive. There's some info on it in section 4.1 of TPIL.

[Martin Dvořák]

What is the difference between Pi being primitive and Sigma not being primitive? Does Pi have a constructor (as a structure) as well?

[Chris B]

No, it doesn't have a constructor. Pi/forall is a kind of expression that the kernel handles directly because it's 'part of the system'. Sigma is an inductive type that gets declared by users.

[Martin Dvořák]

Oh, thank you!

[Martin Dvořák]

This leaves me with the last question: Why cannot ∃ be translated to Σ in the similar way how ∀ is translated to Π (or maybe not translated to the other symbol but both being translated to the same kernel expression)?

[Eric Wieser]

∀ only exists in the pretty printer and as notation (for Π a, p a when p a : Prop), there's no real translation happening. docs#sigma and docs#Exists are different types.

[Martin Dvořák]

Yes, thanks, but why do they need to be different types?

[Eric Wieser]

Because they reside in different universes

[Eric Wieser]

Respectively, sigma p : Type (max u v), psigma p : Sort (max 1 u v), Exists p : Prop

[Eric Wieser]

arguably we don't need both sigma and psigma, beyond the fact that Sort (max 1 u v) isannoying vs Type (max u v)

[Martin Dvořák]

I can now see that

constant α : Type
constant p : α -> Type 3
#check ∀ x : α, p x

is also correct.

[Martin Dvořák]

Eric Wieser said:

Because they reside in different universes

But why can Π x : α eat p : α -> Sort 0 which Σ x : α rejects?

[Eric Wieser]

sigma rejects that because it's defined to reject that

[Eric Wieser]

psigma, Σ' x, p x doesn't, but is more annoying to work with

[Martin Dvořák]

Yes, I see, but why is Π ok with that?

[Eric Wieser]

Because it's not defined like sigma?

[Eric Wieser]

The similarities end with the syntax being similar

[Martin Dvořák]

Is there a fundamental reason why Π can be more versatile than Σ is?

[Eric Wieser]

maybe this helps compare the exact differences:

universes u v
-- the most general form of pi, just so that we can #check
def Pi' {α : Sort u} (x : α → Sort v) := Π i, x i

#check @Pi'.{u v}    -- Π {α : Sort u}, (α → Sort v) → Sort (imax u v)
#check @psigma.{u v} -- Π {α : Sort u}, (α → Sort v) → Sort (max 1 u v)
#check @sigma.{u v}  -- Π {α : Type u}, (α → Type v) → Type (max u v)
#check @Exists.{u}   -- Π {α : Sort u}, (α → Prop)   → Prop

[Martin Dvořák]

Oh, it seems to be the magic inside imax.

[Chris B]

Martin Dvořák said:

Is there a fundamental reason why Π can be more versatile than Σ is?

That's just how the type theory works. Inductive types have to abide by certain rules to keep things from being inconsistent.

[Mario Carneiro]

A variation on psigma with the type Π {α : Sort u}, (α → Sort v) → Sort (imax u v) would not be desirable, because it would not have a first projection (like exists) and would also not have proof irrelevance, so it is sort of the worst of both worlds

[Mario Carneiro]

(p)sigma and exists have fundamentally different ways of getting information out of them: sigma has first and second projections, while Exists uses Exists.rec which only works for proving propositions, but on the other hand satisfies equations like \<0, trivial\> = \<1, trivial\> (as elements of, say, \exists n : nat, true)

[Eric Wieser]

(I assume you meant "like (p)sigma" and not "like exists") words are hard, "would not (have X like Y)" vs "(would not have X) like Y"

[Mario Carneiro]

the parenthetical refers to the previous 6 words, not just the last 2

[Martin Dvořák]

Can you please check for me that I extracted the main informations correctly?
image.png

[Mario Carneiro]

"they don't have a constructor; they live kind of beyond the system" is inaccurate. Pi has a constructor, it is docs#expr.pi . It is a builtin term constructor, unlike all other constructors which use docs#expr.const for various choices of constant

[Reid Barton]

Maybe it would also help to get rid of the type theory language. Let's just define a "proposition" to be a set with at most one element. If we form the product of a bunch of propositions, the result is again a proposition. However if we form the sum of a bunch of propositions, there's no reason why the result should have at most one element. Then I can decide to either truncate it to make a proposition again, or not. That's the difference between Exists and sigma.

[Mario Carneiro]

α × β is not shorthand syntax for Σ _ : α, β. The former uses prod and the latter uses sigma. (Yes, this is not consistent with the behavior for → / ∀.)

[Eric Wieser]

But it could have been, right? It just would have been annoying to use had it been defined that way.

[Mario Carneiro]

Yes, you could conceivably define it that way. You would probably want more builtin sugar for it

[Mario Carneiro]

I'm sure there are examples where the type inference is not as good

[Chris B]

Mario Carneiro said:

Pi has a constructor, it is docs#expr.pi .

I think introducing meta inductive expr sort of overloads the statement "Pi has a constructor" in a way that might not be helpful to someone learning the type theory.

[Chris B]

E.g. TPIL introduces Pi as something that's explicitly not an inductive: in Lean’s library, every concrete type other than the universes and every type constructor other than Pi is an instance of a general family of type constructions known as inductive types.

[Mario Carneiro]

True. But "beyond the system" was the main thing I wanted to address. It is more primitive than usual, but still something in the system

[Martin Dvořák]

Mario Carneiro said:

"they don't have a constructor; they live kind of beyond the system" is inaccurate. Pi has a constructor, it is docs#expr.pi . It is a builtin term constructor, unlike all other constructors which use docs#expr.const for various choices of constant

What does (elaborated : bool := tt) mean, please?

[Mario Carneiro]

To simplify representation, lean uses the same inductive type for both expr := expr tt and pexpr := expr ff, but pexpr (pre-expression) is only used during parsing and you can ignore it for the purpose of learning the theory

[Martin Dvořák]

Thank you all for your replies! It will take me a longer while to understand it and summarize it. Until then, my study notes will contain those mistakes that were pointed out above.

[Martin Dvořák]

Chris B said:

E.g. TPIL introduces Pi as something that's explicitly not an inductive: in Lean’s library, every concrete type other than the universes and every type constructor other than Pi is an instance of a general family of type constructions known as inductive types.

This sentence doesn't refer to the meaning of the word instance that is connected to typeclasses, does it?

[Martin Dvořák]

Current version of my notes contains:
image.png

[Eric Wieser]

It's hard to rell from the pixels, but you seem to be using (a, b) as notation for sigma.mk, whereas it's actually notation for prod.mk. Maybe those are angle brackets and the image is too small to tell though.

[Martin Dvořák]

Is z = (a, b) incorrect?

[Martin Dvořák]

Eh. The tuple notation in parenthesis is for prod, right? For sigma, I should have used chevrons (langle and rangle), right?

[Eric Wieser]

"chevrons" work for all inductive types with one constructor, so both prod and sigma. (_, _, ...) is only for prod

[Martin Dvořák]

Can I do a product of three types without nesting them? Or is it a property of the ˙( )˙ that it gets flattened?

[Adam Topaz]

The chevrons associate to the right, so \<_,\<_,_\>\> is the same as \<_,_,_\>.

[Martin Dvořák]

Does the same apply for parentheses?

[Adam Topaz]

I would imagine so...

[Adam Topaz]

As long as you don't define your triple product at (A \x B) \x C, but rather use A \x B \x C, you should be able to write (a,b,c) (or with \<...\>)

[Martin Dvořák]

Oh yes. And \times associates in the same way. For example int × Type × nat is a short for int × (Type × nat).

[Chris B]

Martin Dvořák said:

Chris B said:

E.g. TPIL introduces Pi as something that's explicitly not an inductive: in Lean’s library, every concrete type other than the universes and every type constructor other than Pi is an instance of a general family of type constructions known as inductive types.

This sentence doesn't refer to the meaning of the word instance that is connected to typeclasses, does it?

It does not.

[Martin Dvořák]

Did I get it right, please?
image.png

[Horatiu Cheval]

The parentheses don't stand for g.mk, but for prod.mk. In your notations g is a term of a product type, the prefix is the name of the type, not the term

[Martin Dvořák]

Oh, thank you!
Is it all right now?
image.png

[Horatiu Cheval]

Well, conceptually at least yes, if you just want to use g to simplify the notation in your notes.

[Horatiu Cheval]

But keep in mind that won't work as actual Lean code. If you were to define g := prod, then g.mk still wouldn't exist, only prod.mk

[Martin Dvořák]

I am not sure whether I understand you. In my snippet, I have g = τ × δ which is g = prod τ δ and not just g = prod.

[Martin Dvořák]

Does g.mk exists then? Or how can I write a term of the type g without the syntactic sugar?

[Eric Wieser]

No, only prod.mk exists. You'd write prod.mk bar baz

[Martin Dvořák]

:-o

[Martin Dvořák]

Does h.mk exist?

[Horatiu Cheval]

Also note that there is only one prod.mk for all \tau and \delta, it's not that for each two types you get some other (prod \tau \delta).mk (that's what your notation would suggest to me)

[Horatiu Cheval]

No, for Sigma it's the same thing, and probably for any such type definition

[Martin Dvořák]

Horatiu Cheval said:

No, for Sigma it's the same thing, and probably for any such type definition

Are you replying to h.mk here?

[Horatiu Cheval]

Yes

[Martin Dvořák]

Ah. Thanks a lot!

[Martin Dvořák]

When I write prod.mk it works but when I write Σ.mk it doesn't work. How can I invoke the constructor explicitly (without chevrons)?

[Horatiu Cheval]

docs#sigma.mk

[Martin Dvořák]

I wrote:

constant α : Type
constant β : α → Type
constant a : α
constant b : β a
#check sigma.mk a b
#check Σ x : α , β x

The output is:

⟨a, b⟩ : sigma β
Σ (x : α), β x : Type

By looking at it, I don't know what the relationship between them is. So I added:

def mytype := Σ x : α , β x
#check sigma.mk a b

Unfortunately, the output is again:

⟨a, b⟩ : sigma β

How can I obtain (sigma.mk a b) : mytype please?

[Horatiu Cheval]

Does #check (sigma.mk a b : mytype) work? In any case, the thing is that you have to explicitly type-annotate it

[Martin Dvořák]

By #check (sigma.mk a b : mytype) I obtain ⟨a, b⟩ : Σ (x : α), β x which makes me more happy than the previous thing.

[Martin Dvořák]

What would happen if, for concrete types, I would end up with β a being int for example? Would it still know that a term constructed by sigma.mk a 5 is of the type mytype?

[Horatiu Cheval]

The way it's written here no, I don't think you will be able to do def x : mtytype := sigma.mk a 5, because mytype is just Type, it's not parametrized. In your definition \alpha and \beta are fixed constants, so they argument for the type mytype

[Horatiu Cheval]

You would be able to do that if used variable instead of constant for example

[Martin Dvořák]

Is it now correct?
image.png

[Martin Dvořák]

I originally (wrongly) assumed that I could use mytype.mk and I would get (when provided correct arguments) a term of the type mytype. Now I can see that I cannot do it.

As a result, it makes me uncomfortable that I must write e.g. sigma.mk 5 9 but there are many possible sigma types which my term could be an instance of.

[Horatiu Cheval]

It seems correct

[Horatiu Cheval]

But I don't really understand your last statement

[Martin Dvořák]

The reason is that there are many possibly functions that send 5 to nat

[Martin Dvořák]

Let's say I have f : int -> Type and g : int -> Type. Let's say they agree on the value of f 5 = nat = g 5. Now I call sigma.mk 5 9. Do I have an instance of sigma f or of signa g?

[Horatiu Cheval]

Does that even typecheck? It shouldn't

[Horatiu Cheval]

I'm talking about sigma.mk 5 9

[Horatiu Cheval]

Because 9 is not a function

[Martin Dvořák]

Why should I put function on the position of 9 in my expression? I have f 5 = nat and not something like f 5 = (nat -> nat).

[Adam Topaz]

In general you need to use type annotations to tell lean what the type family is when defining a term of a sigma type.

[Martin Dvořák]

Should I write something like let myvalue := (sigma.mk 5 9 : mytype) ?

[Horatiu Cheval]

Oh right, sorry. I thought you meant sigma 5 9

[Adam Topaz]

What's mytype?

[Martin Dvořák]

Adam Topaz said:

What's mytype?

Say Σ x : int, f x.

[Adam Topaz]

def foo : Σ (n : ℕ), ℕ := ⟨2,3⟩
def bar : Σ (n : ℕ), ℤ := ⟨2,3⟩

lemma does_not_typecheck : foo = bar := sorry

[Adam Topaz]

I would write let myvalue : mytype := ...

[Adam Topaz]

If you want to define something inline, then you can do (... : mytype)

[Adam Topaz]

Maybe a better example:

def f : ℕ → Type
| 0 := ℕ
| 1 := ℤ
| _ := ℕ

def g : ℕ → Type
| _ := ℤ

def foo : sigma f := ⟨1, (2 : ℤ)⟩
def bar : sigma g := ⟨1, (2 : ℤ)⟩

lemma also_does_not_typecheck : foo = bar := sorry

[Martin Dvořák]

Thank you! Your last example explains a lot!

[Martin Dvořák]

I still wasn't technically correct, was I?
image.png
Here (prod.mk bar baz) automatically becomes a term of the type τ × δ hence it can be used as an argument of the type g. This isn't true for (sigma.mk bar baz) because I would have to explicitly say that I want a term of the type h (or something definitionally equal to h).

[Adam Topaz]

The type will generally not be inferred from context if you only write sigma.mk a b or \<a,b\>.

[Martin Dvořák]

But it will be inferred for (a,b), right?

[Adam Topaz]

Even if you write sigma.mk a b, there will be a metavariable because lean wouldn't know what the type family is without further hints

[Adam Topaz]

For (a,b) you will get a term of the product, and since lean knows the type of a and b, the type of (a,b) is inferred correctly.

[Martin Dvořák]

For prod.mk a b I will automatically get inferred the right type.

[Adam Topaz]

Try this out in a vscode and see what happens:

def foo := sigma.mk (1 : ℕ) (2 : (λ t, ℕ) 1)
def bar := sigma.mk (1 : ℕ) (2 : ℕ)

[Martin Dvořák]

Only the first one passes the typecheck!

[Martin Dvořák]

Mario Carneiro said:

I'm sure there are examples where the type inference is not as good

Is [the thing we discussed today (above)] an example of what you were talking about?

[Martin Dvořák]

Adam Topaz said:

The type will generally not be inferred from context if you only write sigma.mk a b or \<a,b\>.

highlight 1

[Martin Dvořák]

(deleted)

[Martin Dvořák]

Adam Topaz said:

For (a,b) you will get a term of the product, and since lean knows the type of a and b, the type of (a,b) is inferred correctly.

highlight 2

[Martin Dvořák]

@Mario Carneiro To save you some scrolling and reading, just have a look at the two comments (highlight 1 & 2) above. Is it the motivation you were talking about — sigma could be used for prod but the type inference would be worse.

[Wojciech Nawrocki]

Apologies to derail slightly with a tangential question -- @Martin Dvořák are you using some mind/concept mapping software in the screenshots? If so, which?

[Mario Carneiro]

@Martin Dvořák Sure, yes that's an example. I haven't seen the trick with using a beta redex for the second pair element before, but it makes sense that it would work

[Martin Dvořák]

Wojciech Nawrocki said:

Apologies to derail slightly with a tangential question -- Martin Dvořák are you using some mind/concept mapping software in the screenshots? If so, which?

Yes, it is OrgPad.
https://orgpad.com/

I will be glad if you give me any comments on my (current version of) study notes about Lean.
https://orgpad.com/s/ZBGjrzoGIBb