Sort-indexed pi type

Stream: general

[Yaël Dillies]

In Con(NF), we need a huge recursion involving a lot of data defined by well-founded recursion, including a group Strof the form Str a := Π b < a, Str b (the fact that it's well-founded is irrelevant to the question, though).

I wish I could provide (Π b < a, group (Str b)) → group (Str a) with two nested applications of docs#pi.group, but the indexing type is only allowed to be a type and b < a is a prop. If I generalize I : Type* to I : Sort* in pi.group, I get

type mismatch at application
  group (Π (i : I), f i)
term
  Π (i : I), f i
has type
  Sort (max u (v+1)) : Type (max u (v+1))
but is expected to have type
  Type ? : Type (?+1)

while Sort (max u (v+1)) is of course never Prop. Am I doomed and is there really no way around using a subtype to index my elements (namely, having b : {b // b < a})?

[Eric Wieser]

Your problem is that has_mul is only defined on Type

[Eric Wieser]

Aka Sort (1+u)

[Eric Wieser]

And not Sort (max u 1) or similar

[Reid Barton]

I think it will be easiest to just add a second instance with I : Prop

[Yaël Dillies]

I guess I could provide separate instances for Prop-indexed groups?

[Mario Carneiro]

You could also define Str a := Π b: {b // b < a}, Str b

[Yaël Dillies]

Yeah, this is what I am trying to avoid.

[Yaël Dillies]

Is generalizing has_mul (but none of the lemmas) to Sort undesirable because it complicates the universe signature?

[Mario Carneiro]

because max u 1 does not play well with universe inference

[Mario Carneiro]

it's the same reason psigma is not the default

[Yaël Dillies]

Ah so we want phas_mul! :stuck_out_tongue:

[Reid Barton]

presumably you could also just write the group instance by hand in 3 lines

[Reid Barton]

just to establish a baseline here

[Eric Wieser]

What instance? I thought the problem is that the type of that instance is invalid

[Yaël Dillies]

No, it is valid for Prop and Type* separately.

[Yaël Dillies]

Sort (max 0 1) = Type

[Eric Wieser]

What's the mwe?

[Yaël Dillies]

import algebra.group.pi

example {ι : Prop} {α : ι → Type*} [Π i, group (α i)] : group (Π i, α i) := sorry
example {ι : Type*} {α : ι → Type*} [Π i, group (α i)] : group (Π i, α i) := sorry
example {ι : Sort*} {α : ι → Type*} [Π i, group (α i)] : group (Π i, α i) := sorry

I guess

[Eric Wieser]

Is that already an error?

[Yaël Dillies]

Yes

[Eric Wieser]

Duplicating every instance on pi for Prop in addition to Type* does sound rather unappealing

[Reid Barton]

How about just the ones that are actually needed?

[Yaël Dillies]

I am happy to leave them in the con-nf repo until we figure out which ones we actually need. That recursion is nasty and our approach will probably change several times.

[Yaël Dillies]

For reference, @Jason KY. just hit the same problem for order classes on Xena. I guess that's a bit pathological because it was to get monotonicity of a prop-indexed function to use docs#monotone_nat_of_le_succ

[Yaël Dillies]

Without introducing the duplicated instances, could we at least make docs#tactic.pi_instance_derive_field work on Prop-indexed pi-types?

[Yaël Dillies]

Sorry for the noise, the error message was obscure but I was just missing previous instances. It all just works.