Sigma types

Stream: general

[Sebastien Gouezel]

To clean up some expressions, I would like to rewrite ⟨x, y⟩.1as x (and likewise for y). I was surprised to see that simpdoes not do it. Still, rwworks fine with the following lemma.

lemma sigma_fst_eq (α : Type) (F : α → Type) (x : α) (y : F x) :
  (⟨x, y⟩ : Σa:α, F a).1 = x := rfl

I am sure that this is somewhere in the library, but I could not find it (and library_search only answers rfl, which is not that helpful here :).

[Kevin Buzzard]

Does dsimp do it?

[Kevin Buzzard]

I guess you can use change or show. I often find myself having to break a series of rewrites because I need a show to continue.

[Jesse Michael Han]

dsimp should do this kind of eta(?) reduction

[Sebastien Gouezel]

dsimp works fine, thanks. I wanted to avoid change or show as much as possible, as my goals are rather messy...

[Kevin Buzzard]

show can be used like this: show succ _ = _; I've sometimes found this useful if all I want to do is slightly change something which happens to conveniently located! But I do think there's an argument for having these lemmas in there somewhere. On the other hand I've also thought that huge numbers of rewrites might be harder to maintain in the future; with the occasional show you remind us where we're supposed to be.

[Yaël Dillies]

Why does docs#sigma forbid Prop? That is, why can't we use docs#psigma everywhere?

[Eric Wieser]

See also docs#prod and docs#pprod. I think the reason we don't use them is the same as the reason that Type exists at all

[Eric Wieser]

Note the inferred universe is more complex for psigma:

#check @sigma
-- sigma : Π {α : Type u_1}, (α → Type u_2) → Type (max u_1 u_2)
#check @psigma
-- psigma : Π {α : Sort u_1}, (α → Sort u_2) → Sort (max 1 u_1 u_2)

[Eric Wieser]

I'm not sure I understand why that needs to be max 1 and not just max for psigma

[Yaël Dillies]

So universe simplification reasons?

[Eric Wieser]

Ah, if you force it into that universe with structure psigma' {α : Sort u} (β : α → Sort v) : Sort (max u v), Lean complains with

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')

[Yaël Dillies]

Ah yeah, Lean wants to know when something is a Prop.

[Eric Wieser]

I'm not sure I understand why it needs to know that here

[Yaël Dillies]

In that particular context, I don't know. But I assume it has to do with propositional irrelevance?

[Yaël Dillies]

#9908

[Mario Carneiro]

It is because an inductive type that does not target Type u may have a small eliminator, i.e. the target in the sigma.rec function will be Prop instead of Sort l. If the inductive type is sometimes Prop and sometimes not, then sigma.rec has to have two different types depending on some of its other universe arguments, or else you have to be pessimistic and assume it is always a small eliminator, which would end up making psigma just a crappy version of exists

[Mario Carneiro]

Once upon a time the restriction did not exist and it would do exactly this. As a result, you could create this type:

inductive {u} foo : Sort u | A | B
def mystery := foo.{1}
def A : mystery := foo.A
def B : mystery := foo.B
example : A = B := sorry -- unprovable because `mystery` does not have proof irrelevance
example : A ≠ B := sorry -- unprovable because `foo` is a small eliminator

[Mario Carneiro]

Actually scratch that, the existing restriction does not prevent this code from compiling, and it has the described behavior

[Mario Carneiro]

Oh, the error message is only for structure, because in that case lean wants to build projection functions and it can't do so on a small eliminator

[Yury G. Kudryashov]

It would be nice to have this documented somewhere.