Stream: general

Topic: Sort-indexed pi type

Yaël Dillies (Jun 19 2022 at 15:04):

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 (Jun 19 2022 at 15:06):

Your problem is that has_mul is only defined on Type

Eric Wieser (Jun 19 2022 at 15:07):

Aka Sort (1+u)

Eric Wieser (Jun 19 2022 at 15:07):

And not Sort (max u 1) or similar

Reid Barton (Jun 19 2022 at 15:07):

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

Yaël Dillies (Jun 19 2022 at 15:07):

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

Mario Carneiro (Jun 19 2022 at 15:09):

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

Yaël Dillies (Jun 19 2022 at 15:09):

Yeah, this is what I am trying to avoid.

Yaël Dillies (Jun 19 2022 at 15:10):

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

Mario Carneiro (Jun 19 2022 at 15:10):

because max u 1 does not play well with universe inference

Mario Carneiro (Jun 19 2022 at 15:11):

it's the same reason psigma is not the default

Yaël Dillies (Jun 19 2022 at 15:12):

Ah so we want phas_mul! :stuck_out_tongue:

Reid Barton (Jun 19 2022 at 15:12):

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

Reid Barton (Jun 19 2022 at 15:12):

just to establish a baseline here

Eric Wieser (Jun 19 2022 at 15:16):

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

Yaël Dillies (Jun 19 2022 at 15:17):

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

Yaël Dillies (Jun 19 2022 at 15:17):

Sort (max 0 1) = Type

What's the mwe?

Yaël Dillies (Jun 19 2022 at 15:24):

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

Yes

Eric Wieser (Jun 19 2022 at 21:36):

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

Reid Barton (Jun 19 2022 at 22:59):

How about just the ones that are actually needed?

Yaël Dillies (Jun 19 2022 at 23:01):

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 (Jun 21 2022 at 15:31):

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 (Jun 27 2022 at 10:34):

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 (Jun 27 2022 at 10:43):

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

Last updated: Dec 20 2023 at 11:08 UTC