Sigma type for proposition and its proof

Stream: lean4

[Leni Aniva]

Is there a way to express the type (Prop, proof of .0)? For example I can do this:

#check Sigma.mk Nat 4

but I cannot do this

#check Sigma.mk (∀ (a b: Nat), a + b = b + a) Nat.add_comm

The closest thing I can think of is the Std.HashMap type:

def _root_.Std.HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := {m : Imp α β // m.WF}

which couples an object along with a proposition about the object. Why is this use case ok while the one I contrived doesn't typecheck?

[Yaël Dillies]

Is docs#PSigma what you want?

[Leni Aniva]

Yaël Dillies said:

Is docs#PSigma what you want?

This still doesn't typecheck:

#check PSigma.mk (∀ (a b: Nat), a + b = b + a) Nat.add_comm

[Kevin Buzzard]

The reason your original code doesn't typecheck is that Prop isn't Type u for any u, Prop is something like "Type -1" but that doesn't actually make sense. The type of Sigma.mk is Sigma.mk.{u, v} {α : Type u} {β : α → Type v} (fst : α) (snd : β fst) : Sigma β so it's demanding Type u. The point of PSigma is that it avoids this.

[Leni Aniva]

but I've replaced Sigma with PSigma and it still doesn't typecheck

[Kevin Buzzard]

The type of PSigma.mk is PSigma.mk.{u, v} {α : Sort u} {β : α → Sort v} (fst : α) (snd : β fst) : PSigma β. What do you want beta to be here? It's supposed to be a function.

[Leni Aniva]

Can it just be the identity function?

[Leni Aniva]

I want snd to typecheck to fst

[Kevin Buzzard]

I am not the best at this sort of foundational stuff but Lean needs to be able to guess alpha and beta and right now I'm not sure what you have in mind for these.

[Eric Wieser]

This works:

#check (⟨∀ (a b: Nat), a + b = b + a, Nat.add_comm⟩ : Σ' p : Prop, p)

as does

#check (⟨_, Nat.add_comm⟩ : Σ' p : Prop, p)

[Henrik Böving]

The simple approach to this would be to just ship it yourself without thinking^^

structure Simple where
  p : Prop
  h : p

since there isn't really much interesting API for PSigma anyways.

[Eric Wieser]

I think the takeaway here is that Sigma.mk and PSigma.mk don't really work unless you also write out the type you expect, as Lean can't infer the family. You wrote the type in your question here though, you just forgot to tell it to Lean!

[Leni Aniva]

Thanks!

[Leni Aniva]

Does the { .. // .. } thing from Std.HashMap work the same way?

[Leni Aniva]

Std.HashMap uses this expression {m : Imp α β // m.WF} which couples a propositon about an object with the object itself and I couldn't find out about how the // operator works

[Kevin Buzzard]

That's notation for docs#Subtype

[Henrik Böving]

That's a subtype, it works a bit different as the left hand side is data and the right hand side is proof about the data

[Leni Aniva]

Is Subtype just a special case for PSigma?

[Henrik Böving]

One could say that yes.