Sigma type with Prop

Stream: new members

[MrQubo]

Is it possible to have sigma type with first element being Prop?

def head_pred? (l : List Nat) (_ : l.length > 0 := by simp_all_arith) : Option Nat := match l[0] with
| Nat.zero => none
| Nat.succ n => some n

def head_isPos' (l : List Nat) (_ : l.length > 0 := by simp_all_arith) : Prop :=
  (head_pred? l).isSome

def head_isPos (l : List Nat) : Prop := Σ _ : l.length > 0, head_isPos' l

def head_isPos_to_head_pred (l : List Nat) (h₀ : head_isPos l) : Nat :=
  have ⟨h₁, h₂⟩ := h₀
  _

I've tried using \exists instead of \S, but that makes it impossible to use it in non-Prop context.

[Riccardo Brasca]

Are you looking for PSigma?

[MrQubo]

Riccardo Brasca said:

Are you looking for PSigma?

It's written Σ', right? I've tried it, doesn't work either.

[MrQubo]

Ah, wait, it works, but the type of Σ' _ : l.length > 0, head_isPos' l is Type, not Prop.
Shouldn't it be Prop if the second element of a sigma pair is Prop?

[Edward van de Meent]

unfortunately, using the same thing in either case will give bad API

[MrQubo]

Not formally, it's kinda the same as l.length > 0 ∧ head_isPos' l, but I need _ : l.length > 0 to pass it as an argument to head_isPos' l.

[Edward van de Meent]

this is because if you want an inductive to vary over Sort u, it can't have large elimination even when it is Sort 1 or above

[Edward van de Meent]

because of that, inductives are always(*) either Type u or Prop

[Edward van de Meent]

*there is an option to disable the check enforcing this resulting in a Sort _-typed inductive with Prop-only elimination

[Edward van de Meent]

as a result, you really should not try to use the same type in both cases

[Edward van de Meent]

use PSigma when you need a Type and Exists when you need a Prop

[Aaron Liu]

Why does ∃ _ : l.length > 0, head_isPos' l not work for you?

[Riccardo Brasca]

If the problem with ∃ is that you cannot write obtain ... := in defining, say, a number, the solution is to use Classical.choose instead of obtain.

[Riccardo Brasca]

(in that case this is a nice example of an #xy problem :))

[Aaron Liu]

In this case since both fields are a Prop, you can actually just use the field notation.

[Robin Arnez]

MrQubo schrieb:

I've tried using \exists instead of \S, but that makes it impossible to use it in non-Prop context.

That's not correct, projections x.1 and x.2 should work if you have Props on both sides.

[MrQubo]

Robin Arnez said:

MrQubo schrieb:

I've tried using \exists instead of \S, but that makes it impossible to use it in non-Prop context.

That's not correct, projections x.1 and x.2 should work if you have Props on both sides.

head_isPos_to_head_pred in my example shows that \exists doesn't work. The error is

tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop

This error is explained in the documentation for Exists.

[MrQubo]

It looks like this works, would it be a problem if PSigma from Init.Core was defined in a way that for a Prop argument type of PSigma is also Prop?

def head_pred? (l : List Nat) (_ : l.length > 0 := by simp_all_arith) : Option Nat := match l[0] with
| Nat.zero => none
| Nat.succ n => some n

def head_isPos' (l : List Nat) (_ : l.length > 0 := by simp_all_arith) : Prop :=
  (head_pred? l).isSome

structure SigmaProp {α : Prop} (β : α → Prop) : Prop where
  fst : α
  snd : β fst

def head_isPos (l : List Nat) : Prop := @SigmaProp (l.length > 0) (@head_isPos' l)

def head_isPos_to_head_pred (l : List Nat) (h₀ : head_isPos l) : Nat :=
  have ⟨_, _⟩ := h₀
  let pred? := head_pred? l
  have h : pred?.isSome := by simp_all [head_isPos']
  pred?.get h

[MrQubo]

Edward van de Meent said:

this is because if you want an inductive to vary over Sort u, it can't have large elimination even when it is Sort 1 or above

Indeed, this means it's impossible to have PSigma be Prop. I.e., this doesn't work structure PSigma' {α : Sort u} (β : α → Sort v) : Sort (max u v).

[MrQubo]

Would it be possible to define exists elimination in a way that if first argument is Sort 0, than it can be eliminated in a non-Prop goal? This would make sense, as there's only one instance (up to propext) for the first argument of Exists.

[MrQubo]

I'll try with PSigma, maybe it won't cause a problem if type of head_isPos is Type and not Prop.

[Kyle Miller]

@MrQubo You're misunderstanding what Robin's saying: you can use projection notation, like h₀.1 and h₀.2. Using have ⟨_, _⟩ := h₀ won't work

[Kyle Miller]

(I didn't test it — in principle it should work with numerical projections. There's a chance that there's some artificial limitation in the elaborator that causes an error still. But, I do expect numerical projections to work with Exists if both types are Props.)

[MrQubo]

Oh, you're right. In my brain have ⟨_, _⟩ := h₀ was just a syntax sugar for have _ := h₀.1; have _ := h₀.2.

[Edward van de Meent]

Riccardo Brasca said:

If the problem with ∃ is that you cannot write obtain ... := in defining, say, a number, the solution is to use Classical.choose instead of obtain.

you shouldn't be in tactic mode when defining a number anyway :upside_down:

[MrQubo]

Edward van de Meent said:

Riccardo Brasca said:

If the problem with ∃ is that you cannot write obtain ... := in defining, say, a number, the solution is to use Classical.choose instead of obtain.

you shouldn't be in tactic mode when defining a number anyway :upside_down:

Tbh, in same cases I find it easier to use tactic mode, this is because things like apply? can help you find functions you need, and I can rewrite to term mode later.