Stream: Coq devs & plugin devs

Topic: -indices-matter changing eliminator of eq


view this post on Zulip Ali Caglayan (Apr 01 2022 at 17:46):

With -indices-matter eq has the same type but cannot generate rec and rect. How exactly does -indices-matter get in the way of the eliminator?

view this post on Zulip Ali Caglayan (Apr 01 2022 at 17:48):

I only remember this comment from @Gaëtan Gilbert but I don't really understand what is going on. https://github.com/coq/coq/pull/15260#discussion_r759329432

view this post on Zulip Ali Caglayan (Apr 01 2022 at 17:49):

eq with indices matter looks like: eq : forall [A : Type], A -> A -> Prop
eq without indices matter looks like eq : forall [A : Type], A -> A -> Prop

view this post on Zulip Ali Caglayan (Apr 01 2022 at 17:50):

Where is the magic happening?

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2022 at 17:52):

the difference is not the type nor the constructor, it's what is allowed in the eliminator

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 17:52):

inductives can be defined in Prop either if they are small enough (then they get _rect) or by squashing
indices-matter forces squashing for eq

view this post on Zulip Ali Caglayan (Apr 01 2022 at 17:54):

The "small enough" part being the singleton business?

view this post on Zulip Ali Caglayan (Apr 01 2022 at 17:57):

Are the small ones the same ones picked out by SProp? Acc etc.?

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 17:58):

rules for non squashed Prop:

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 17:59):

Acc is still Prop with indices matter (it has no indices thanks to non recursively uniform parameters)

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:02):

if indices matter, all indices in Prop or SProp

Is it known that this causes problems when dropped?

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:03):

it's the definition of indices matter

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:03):

I was always under the impression that -indices-matter was really talking about universe levels not comparing between prop and other sorts.

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:04):

I don't know what that's supposed to mean so I can't tell if it's correct

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:05):

The reason we don't allow an indexed inductive to live in a universe lower than its indices is because we can get Russel style problems no?

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:06):

My point is that prop is not an ordinary universe level

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:07):

universe rules for inductives in general, let U be the sort of the inductive

OR U impredicative and the inductive is squashed

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:09):

strictly speaking indices-matter is designed for HoTT (where @paths A x y must be in same or higher universe as A)
since HoTT isn't supposed to use Prop indices-matter could do anything on Prop and it doesn't matter since nobody knows what it means

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:11):

Exactly, so the second condition might be a bit too strict. I wonder if it is consistent to relax it so that we don't compare between SProp,Prop and Set,Type.

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:12):

too strict for what? it's consistent without axioms since no-indices-matter is consistent

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:13):

so that we don't compare between SProp,Prop and Set,Type.

WDYM?

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:15):

Not enabling -indices-matter is not exactly allowing any size for the indices however. For example, the following doesn't work (with uni poly):

Inductive Box (A : Type) : Set :=
| a : A -> Box A.

sorry more correctly:

Inductive Box : forall (A : Type), Set :=
| a {A : Type} : A -> Box A.

I guess here the constructor size check is what is stopping this.

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:17):

because of the constructor argument
univ poly does nothing on this

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:18):

Gaëtan Gilbert said:

too strict for what? it's consistent without axioms since no-indices-matter is consistent

I'm looking at it from the perspective of enabling -indices-matter everywhere. But I always get confused since all the issues are Prop related which -indices-matter wasn't even designed for.

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:20):

there is a transformation from inductives with indices to inductives with non recursively uniform parameters + a special equality type
if the special equality type is in the same universe as its type argument you get indices-matter
if it's in Prop you get no-indices-matter with uip off
if it's in sprop you get no-indices-matter with uip on

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:21):

so you can't have indices-matter with unsquashed eq in prop

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:23):

(I should have remembered that instead of saying stuff about how hott doesn't care what we do with prop)

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:25):

Is that transformation detailed anywhere?

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:27):

it's pretty trivial, if you have

Inductive Ind params : indices -> U := C : forall args, Ind params (f args)

you transform to

Inductive Ind params indices : U := C : forall args, f args = indices -> Ind params indices.

(where params, indices, args and f are telescopes for full generality)

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:28):

Right, I've seen this before actually

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:29):

But I saw it in a different dress. Its the translation between indexed W-types and W-types?

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:30):

In fact, I even ported Jasper's formalization of it to the HoTT library: https://github.com/HoTT/HoTT/blob/master/theories/Types/IWType.v

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:30):

There is no UIP involved in this translation however

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:31):

mine doesn't use uip either
it's probably basically the same thing

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:31):

However these IW-types inherit their "indices mattering" from the definition of the IW-type

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:32):

Which is just

Inductive IW
  (I : Type) (** The indexing type *)
  (A : Type) (** The type of labels / constructors / data *)
  (B : A -> Type) (** The the type of arities / arguments / children *)
  (i : A -> I) (** The index map (for labels) *)
  (j : forall x, B x -> I) (** The index map for arguments *)
  : I -> Type :=
| iw_sup (x : A)
    : (forall (y : B x), IW I A B i j (j x y)) -> IW I A B i j (i x).

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:32):

I played around with similar stuff a while back but never submitted anywhere
https://github.com/SkySkimmer/HoTTClasses/blob/f9affefaa088d02ca7e6e901580ae6f9ff13ca40/theories/inductives/inductives.v#L79-L121

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:33):

So all of this doesn't really have to do with inductive types I suppose. It really is a property of whatever equality you have.

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:33):

InductiveS is a description of an inductive (with only recursive parameters)
indT implements it with indices
indT' with nonrec params

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 18:38):

Ali Caglayan said:

So all of this doesn't really have to do with inductive types I suppose. It really is a property of whatever equality you have.

I guess it depends on if you see equality as more primitive or as just a specific inductive

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:42):

Your formalization is very cool.

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:42):

Thank you very much for the interesting discussion.

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:43):

I seem to recall an example of -indices-matter breaking things in the test-suite for non-prop related things.

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:45):

Variables (A B : Type) (x : A) (f : A -> B) (b : bool) (vT vF : A).

Variant if_spec (not_b : Prop) : bool -> A -> Set :=
  | IfSpecTrue  of      b : if_spec not_b true vT
  | IfSpecFalse of  not_b : if_spec not_b false vF.

From ssrbool.v

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:45):

Not in the test-suite actually

view this post on Zulip Ali Caglayan (Apr 01 2022 at 18:46):

So A can be in a big universe but if_spec lands in Set

view this post on Zulip Gaëtan Gilbert (Apr 01 2022 at 19:15):

what about it?


Last updated: Feb 06 2023 at 00:03 UTC