Adding an (existentially quantified) sublist

[ajrouvoet]

We have Sublist.Inductive to relationally define what xs are sublists/OPEs of a given ys. It seems useful to me to actually define a notion Sublist ys to existentially quantify over the xs, with definitions:

  ⊤ : ∀ {l} → Sublist l
  ⊥ : ∀ {l} → Sublist l
  Empty : ∀ {l} → Sublist l → Set a
  _∪_ : ∀ {l} → (xs ys : Sublist l) → Sublist l
  _∩_ : ∀ {l} → (xs ys : Sublist l) → Sublist l

This is completely analogue to the notion Fin.Subset n for natural numbers.

I have these definitions sitting in a branch here. I would like some input on:

• [ ] Where should this be defined?
• [ ] Equality of a sublist to ⊤ appears hard to prove in practice. Proving that the reification of a sublist of xs is equal to xs seems more practical. This begs for the definition of Every as a counterpart to Empty.

[gallais]

_∪_ : ∀ {l} → (xs ys : Sublist l) → Sublist l
_∩_ : ∀ {l} → (xs ys : Sublist l) → Sublist l

Ooooh fancy. I don't think we have meet & joins for the current inductive sublists?

I don't know where this would go. As for the last point: can't we add a proof that if reify equals xs then the sublist equals ⊤ whenever the setoid equalities are irrelevant?

[ajrouvoet]

We do not have those now indeed, probably exactly because the left operand of the output is then existentially quantified.

The latter proof I have indeed. So maybe naming the intermediate representation is unnecessary?

After your note on the other issue about closure I realized that this is another example of the closure of a relation, but using the 'somewhere' modality, rather than the everywhere. Might be useful to define that modality and define Sublist as such.

[MatthewDaggitt]

As for location I've been thinking about adding a Predicate subfolder to match the Relation folder for compositional data. This should really live in Data.List.Predicate.Sublist right? The only problem is that Any and All are so widely used that it's going to be backwards compatible nightmare.... I guess we could deprecate the module.

[gallais]

I was thinking about that but we have Relation.Unary rather than Predicate. So for consistency we should maybe reorganise the whole Data.List.Relation into Data.List.Relation.Unary and Data.List.Relation.Binary?

We could maintain backwards compatibility by having placeholder modules for a while with the old name and re-exporting the new one. Then we would really need WARNING_ON_IMPORT to be sure we can get rid of them at some point in the future.

[MatthewDaggitt]

Good point! Do you think there's any prospect of such a magic WARNING_ON_IMPORT sneaking into the next release of Agda? :smile:

[gallais]

There's a feature freeze at the moment so the answer is no. Plus I'm currently making sure I finally ship my thesis. :D

But I may find the time to write something like over the Xmas holidays.

[MatthewDaggitt]

Plus I'm currently making sure I finally ship my thesis. :D

Congrats!

Okay no problem. The warnings can always come later. @ajrouvoet mind if you hold off on your PR until we complete this rearrangement?

[ajrouvoet]

@MatthewDaggitt SGTM. Currently there really is no natural place for this code anyway. I'm using the Sublist elsewhere and still adding properties to it, so holding off sounds fine :)

[MatthewDaggitt]

Unblocked.

[jamesmckinna]

Does the refactoring of Data.List.Relation.Unary.{Prefix|Suffix} as instances of abstract divisibility #2604 close this, or rather, can we refactor the proposed constructions as suitable lubs/glbs for the corresponding orderings?

[gallais]

Sublist is more general surely?

[jamesmckinna]

Sublist is more general surely?

Yes, I'm an idiot!

[jamesmckinna]

We do not have those now indeed, probably exactly because the left operand of the output is then existentially quantified.

As befits the abstract name of a universal construction: we shouldn't care! only the universal property matters!?