Add proofs to Data.List.Properties

[mildsunrise]

Hi! This is my first PR, apologies if I'm missing something.

This adds a series of proofs to Data.List.Properties that I consider general enough to be in the stdlib, and in most cases already exist for other list operations. This proves, in order:

• interaction with map, for list operations where it makes sense and was missing
• congruence for higher order operations, where missing (except for those acting on Decidables, which I am still working on, and unsnoc which is challenging because of the indexed datatype)
• for alignWith / align, zipWith / zip and unzipWith / unzip:
  • effect of swapping function arguments / inputs
  • equivalence of swapping function arguments if function is commutative
• interaction of take with itself and with drop
• unzipWith + zipWith being inverses (with particular cases for the non-With versions)
• interaction with ++, for operations where it makes sense and was missing

It also fixes a module that was defining a parameter that was not used in the proofs. I've tried to respect conventions of that file where possible, please tell me if there's anything that could be improved :)

[jamesmckinna]

Meta-comment: Should we fix mapMaybe first? Cf. https://github.com/agda/agda/issues/5833 and links there to @omelkonian 's implementation?

[MatthewDaggitt]

What would "fixing" it involve?

[jamesmckinna]

What would "fixing" it involve?

As in Orestis' prelude, write catMaybe before mapMaybe as the composition of catMaybe and map... which avoids the awkward with construction... see #2361

And apologies to @mildsunrise for hijacking a very nice first PR with a hobby-horse of mine!

[mildsunrise]

@MatthewDaggitt thanks for the thorough review! I've responded to your points and will act on them soon-ish, probably today

@jamesmckinna is it okay if I add the proposed fix to this PR, or would you rather keeping it in a separate PR, merging that one, and then rebasing this one on top?

[MatthewDaggitt]

As in Orestis' prelude, write catMaybe before mapMaybe as the composition of catMaybe and map... which avoids the awkward with construction...

Is this is a backwards compatible change with respect to reduction behaviour? We shouldn't do it now, if it's not.

[jamesmckinna]

I'll put my hobby-horse back in the stable... @MatthewDaggitt 's comment suggests we exercise caution. I'll investigate separately, and then take the knock-on hit from your additions downstream @mildsunrise so no action required on your part from me!

[mildsunrise]

to my understanding it should have equivalent reduction behavior, but yes, it's good to be cautious. okay then, I'll fix the 2 remaining issues

[mildsunrise]

all done. let me know if you need anything else on my part, such as squashing the fixup commits into the original commits

[mildsunrise]

I've added a couple more properties, mapMaybe-++ and unzipWith-++ since their proof was similar enough to the existing proofs. If it feels like too much, I can leave them out of this PR

[mildsunrise]

(I'll be a bit busy these days, but I'd rather not block other PRs with this one, so please ping me if action is needed on my part)

[jamesmckinna]

@MatthewDaggitt can you re-review (re: the cong lemmas?) and/or merge now, please? I think that this one is ready now ;-)

[gallais]

I think we just need the d \== e assumption to be removed and then we're good to merge.

[MatthewDaggitt]

Yup once removed, will merge :+1:

[mildsunrise]

I see that #2361 was merged before this PR. given that catMaybes is no longer defined in terms of mapMaybe, it becomes necessary to prove properties about catMaybes directly. And once this is done, the properties of mapMaybe can be simplified to use those new proofs.

2361 already did that with length-mapMaybe (added length-catMaybes). I've went ahead and done the same with the other three mapMaybe properties.