Zulip Chat Archive

Stream: new members

Topic: sigma/psigma

petercommand (Nov 03 2018 at 15:15):

What's the reason for having types like sigma/psigma, sum/psum at the same time?

Kevin Buzzard (Nov 03 2018 at 15:15):

Is it to do with universes?

petercommand (Nov 03 2018 at 15:17):

Like, when would I want to use psigma instead of sigma/Exists?

Reid Barton (Nov 03 2018 at 15:18):

psigma instead of Exists: because you want to keep the information of what the things are whose existence you claim

Reid Barton (Nov 03 2018 at 15:19):

psigma with a Prop is basically the same as subtype, whereas Exists is like nonempty

Reid Barton (Nov 03 2018 at 15:20):

psigma instead of sigma: if you want to use a Prop instead of a Type, or you might want either a Prop or a Type

Chris Hughes (Nov 03 2018 at 15:20):

The equation compiler uses psigma a lot. | (a : nat) (b : nat) (h : 0 < b) is essentially matching on Σ' a b : ℕ, 0 < b underneath.

Reid Barton (Nov 03 2018 at 15:23):

I've found psigma most useful in conjunction with the Σ' binder notation with multiple variables where the eventual "body" is a Prop

Mario Carneiro (Nov 03 2018 at 15:26):

isn't that exists?

Reid Barton (Nov 03 2018 at 15:26):

like "a pair consisting of an open set U and a function f : U -> R which sends x to 0" = Σ' (u : set α) (hu : is_open u) (f : u → ℝ), f x = 0

Chris Hughes (Nov 03 2018 at 15:27):

What's the point of using sigma instead of psigma?

Mario Carneiro (Nov 03 2018 at 15:28):

psigma has a difficult target universe

Mario Carneiro (Nov 03 2018 at 15:28):

Sort (max u 1) is hard to work with

Mario Carneiro (Nov 03 2018 at 15:28):

because it's not algebraic: max u 1 = 1 does not have a unique solution

Mario Carneiro (Nov 03 2018 at 15:29):

so lean will often give up on otherwise solvable universe unification problems

Mario Carneiro (Nov 03 2018 at 15:30):

where Type u = Sort u+1 has the much easier solution u+1 = 1 -> u = 0

Mario Carneiro (Nov 03 2018 at 15:30):

In fact, there are some expressions which do not have any solution, although you might think it does: max u 1 = v+1 has no solution for u

Reid Barton (Nov 03 2018 at 15:32):

hmm, that max 1 is coming from Lean bumping up the level of a structure I guess? Is it actually wanted? Why should psigma.{0 0} not be a Prop?

Mario Carneiro (Nov 03 2018 at 15:34):

That was deliberate. You can define your own psigma' that lives in Sort (max u v)

Mario Carneiro (Nov 03 2018 at 15:34):

but you will find it's not all it's cracked up to be

Mario Carneiro (Nov 03 2018 at 15:34):

in particular, it has a recursor like exists

Mario Carneiro (Nov 03 2018 at 15:35):

it's not "data"

Mario Carneiro (Nov 03 2018 at 15:38):

and if you specialize to u > 0 you get the mystery type, which is neither proof nor data

petercommand (Nov 03 2018 at 15:38):

In fact, there are some expressions which do not have any solution, although you might think it does: max u 1 = v+1 has no solution for u

why does max u 1 = v+1 not have any solutions?

Mario Carneiro (Nov 03 2018 at 15:39):

because there is no universe expression that gives the solution

Reid Barton (Nov 03 2018 at 15:39):

Actually, I can't :)

structure ppsigma {α : Sort u} (β : α → Sort v) : Sort (max u v) := mk :: (fst : α) (snd : β fst)
-- invalid universe polymorphic structure declaration, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'l+1' or 'max 1 l')

Reid Barton (Nov 03 2018 at 15:39):

But I guess it's because otherwise I would be in the situation you describe.

Mario Carneiro (Nov 03 2018 at 15:40):

That's because you used structure, it tried and failed to define the projections

Reid Barton (Nov 03 2018 at 15:41):

Oh, I see

Reid Barton (Nov 03 2018 at 15:41):

Why doesn't singleton elimination help here?
If I manually replace u = v = 0, then I get an eliminator to any sort

Mario Carneiro (Nov 03 2018 at 15:42):

@petercommand for each fixed v there is a solution for u, but there is no solution function u(v)

Reid Barton (Nov 03 2018 at 15:42):

Just a weird edge case that Lean doesn't support?

Mario Carneiro (Nov 03 2018 at 15:42):

because you need one recursor that is polymorphic in u,v

Mario Carneiro (Nov 03 2018 at 15:43):

and that recursor will have one extra universe variable depending on whether max u v = 0

Mario Carneiro (Nov 03 2018 at 15:43):

there is no way to do that with universe expressions

Mario Carneiro (Nov 03 2018 at 15:44):

you could have two recursors, but this breaks parametricity

Reid Barton (Nov 03 2018 at 15:45):

I'm trying out different u and v values and in every case I get an eliminator which goes to any sort.
However there is a difference when u = v = 0, which is that the C doesn't take the ppsigma value as an argument then

Mario Carneiro (Nov 03 2018 at 15:45):

singleton elimination doesn't help because A and B aren't subsingletons

Mario Carneiro (Nov 03 2018 at 15:46):

That's just a convenience thing, the usual recursor is at drec_on

Mario Carneiro (Nov 03 2018 at 15:47):

for small eliminating props the dependent and nondependent recursors are interdefinable

Reid Barton (Nov 03 2018 at 15:52):

inductive ppsigma00 {α : Sort 0} (β : α → Sort 0) : Sort (max 0 0) | m (fst : α) (snd : β fst) : ppsigma00
#check @ppsigma00.drec_on
│ ppsigma00.drec_on :
│   Π {α : Prop} {β : α → Prop} {C : ppsigma00 β → Sort u_1} (n : ppsigma00 β),
│     (Π (fst : α) (snd : β fst), C _) → C n

inductive ppsigma11 {α : Sort 1} (β : α → Sort 1) : Sort (max 1 1) | m (fst : α) (snd : β fst) : ppsigma11
#check @ppsigma11.rec_on
│ ppsigma11.rec_on :
│   Π {α : Type} {β : α → Type} {C : ppsigma11 β → Sort u_1} (n : ppsigma11 β),
│     (Π (fst : α) (snd : β fst), C (ppsigma11.m fst snd)) → C n