Some lemmata for lists and non-empty lists

[pmbittner]

These are some lemmata we needed in our project Vatras for reasoning on non-empty lists. It seemed these lemmata could be generally useful to other people as well.

-- PR is part of Zurihac 2025

[Taneb]

These look like good additions! Can you update Changelog.md with these?

[pmbittner]

Ok, I updated the changelog as well. :)

[pmbittner]

I also migrated some additional lemmas from Data.List.Properties.

[JacquesCarette]

A few nits, but otherwise this is looking nice.

[Not a big fan of rewrite, but it's not a showstopper.]

[pmbittner]

Thank you for the review. :) I integrated the requested changes. I also got rid of the rewrite by introducing an analogous lemma to Data.List.Properties and then reusing that.

[gallais]

Happy with this; apart from two small naming issues (and related completeness question).

[pmbittner]

Hi everyone,

I implemented the requested changes. Implementing the length-++-≤ʳ theorem required some additional lemmata, which unfortunately required another theorem (++-identityʳ) which was located below in that file. So I had to reorder some theorems, including module definitions. Please check whether my changes remain idiomatic to the standard library.

(Maybe there is a simpler proof for length-++-≤ʳ but I did not find it yet.)

[JacquesCarette]

I wonder if this would be easier to prove as a corollary of length being preserved by permutations?

[pmbittner]

If I understand correctly, this means to

1. Establish a theorem that says that length is preserved under permutation.
2. Prove that xs ++ ys is a permutation of ys ++ xs.
3. Prove length-++-comm as a corollary.

This should be possible and the theorems 1 and 2 should be useful as well. I am not sure this would be a simpler as a sole means to prove length-++-comm though.

Given that there are multiple definitions of permutations, which one should be used here? Data.List.Relation.Binary.Permutation.Setoid or Data.List.Relation.Binary.Permutation.Propositional?

[JacquesCarette]

I know step 1 already exists, I've used it recently. I'm almost sure step 2 does as well.

I'd use Propositional as it is more precise in what it asserts.

[Taneb]

I'd caution against doing this for dependency tree reasons...

[pmbittner]

So how should we proceed with this PR?

[JacquesCarette]

(Note that I approved the changes, my suggestion above was for a potential future, not this. Now it's up to someone else to also approve the latest changes. Maybe @MatthewDaggitt can re-review?)