New property merge-is-superlist

[andreasabel]

Proofs that both lists involved in a merge are sublists of the result of the merge.

[Taneb]

I think these functions are incorrectly named; merge is the superlist, not the sublist. But on the other hand I don't think we ever use the term superlist, so I'm not sure what to call them

[andreasabel]

@Taneb wrote:

I think these functions are incorrectly named; merge is the superlist, not the sublist. But on the other hand I don't think we ever use the term superlist, so I'm not sure what to call them

Thanks for the comment, now I am using superlist.

[jamesmckinna]

Nice! Thanks for the response to reviews... I fully sympathise with the difficulty of finding names, here where they are imported from deep below the hierarchy (and Heterogeneous doesn't immediately suggest that its contents will be relevant to the homogeneous case)

[jamesmckinna]

Regarding superlist: do we have a universal property of merge as a supremum of the two sublists?

[Taneb]

Regarding superlist: do we have a universal property of merge as a supremum of the two sublists?

@jamesmckinna I couldn't find it. Could you make an issue for it, because I think it's important to have and also doesn't need to be done in this PR (I think it might need stronger preconditions on the lists)

[andreasabel]

Regarding superlist: do we have a universal property of merge as a supremum of the two sublists?

@jamesmckinna I couldn't find it. Could you make an issue for it, because I think it's important to have and also doesn't need to be done in this PR (I think it might need stronger preconditions on the lists)

Yeah,merge is only a supremum for totally ordered lists.
On arbitrary lists, merge is only a supremum up to permutation and I am not sure this is worth proving, as it is typically used on ordered lists.

[jamesmckinna]

Re: 'up to permutation' Is that not what is being captured by _⊆_? (EDITED: maybe I have misunderstood something fundamental here)
Re: the case of totally (linearly) order lists, is that not what is being addressed in the (now re-exported) version in Data.List.Relation.Unary.Sorted.TotalOrder.Properties? In this respect, pace @Taneb 's suggestion to raise it as a separate issue, how hard would it be to prove here, against the background assumptions of the lists being Sorted (EDITED: and hence there being a canonical choice of representative of the permutation equivalence class)?

[andreasabel]

@jamesmckinna wrote:

Re: 'up to permutation' Is that not what is being captured by _⊆_?

No, sublists are order-preserving, so the bigger list just inflates the smaller list by new elements, but the relative order of the old elements stays the same. (Up to permutation would be the "subset" concept for lists.)

Re: the case of totally (linearly) order lists, is that not what is being addressed in the (now re-exported) version in Data.List.Relation.Unary.Sorted.TotalOrder.Properties? In this respect, pace @Taneb 's suggestion to raise it as a separate issue, how hard would it be to prove here, against the background assumptions of the lists being Sorted

I think if the PR is meaningful as such, it should be accepted as such (avoiding feature creep that kills PRs).
More can always be done later.
I don't know how hard it is to prove that the merge is the lub, maybe it is just an inductive proof over the two lists being merged...

[MatthewDaggitt]

Hmm best to not rename things unnecessarily? If you wanted to you could add an extra lemma named ⊆-minimum here?

[andreasabel]

OK, I'll change, even though it makes the proof less readable, because []⊆ xs is unambiguous for [] ⊆ xs, while minimum xs would (in my intuitition) mean to extract the minimal element from list xs (see Haskell's Foldables).

[MatthewDaggitt]

(I've deleted the Squash me label, as we should always be squashing. For some reason Github's default changed recently, but I've enabled the Linear history option in the settings that should prevent us from not squashing them).

[andreasabel]

(I've deleted the Squash me label, as we should always be squashing. For some reason Github's default changed recently, but I've enabled the Linear history option in the settings that should prevent us from not squashing them).

I thought "linear history" still leaves two options: "rebase" and "squash", the first for well-engineered individual commits and the second for "commit followed by fixups". (So I put up a flag that "rebase" would be a bad option here...)

In my experience, Github's default is whatever you used the last time...

[gallais]

Looks good to me. We'll need a CHANGELOG entry though.

[MatthewDaggitt]

@andreasabel any chance you could add a CHANGELOG entry as @gallais requests and then I'll merge this in?

[andreasabel]

@MatthewDaggitt : Sorry, I missed the last comments.
Now there is a CHANGELOG entry.

Btw, why is CHANGELOG.md excluded from fix-whitespace?

[andreasabel]

Fine to merge now, @MatthewDaggitt ?

[MatthewDaggitt]

Btw, why is CHANGELOG.md excluded from fix-whitespace?

Unsure... I guess because it's not code?

[andreasabel]

Thanks for merging!

Btw, why is CHANGELOG.md excluded from fix-whitespace?

Unsure... I guess because it's not code?

Technically, markdown has this obscure (and imo ill-designed) feature that two trailing spaces force a line break (a <br/> tag). https://www.oasys.net/fragments/markdown-line-breaks/
I think one shouldn't make use of this feature, and then enforcing the usual whitespace discipline would be fine.