[ add ] filter-∩, filter-map and filter-swap for Data.List.Properties

[IchiganCS]

I recently was surprised that the standard library doesn't prove these two laws, so I quickly added them.

filter-∩    : filter (P? ∩? Q?) ≗ filter P? ∘ filter Q?
filter-swap : filter P? ∘ filter Q? ≗ filter Q? ∘ filter P?

I hope I followed all guidelines etc.
There is one thing where opinions can differ in style: filter-swap could either be proven by directly pattern matching on P? x and Q? x respectively, but I feel like using propositional equality is more elegant. The downside is the additional module definition (which could maybe be written differently? - I'm new to Agda).

Edit:

map-filter-swap   : ∀ {P : Pred B p} (f : A → B) (p? : Decidable₁ P) 
                    → filter p? ∘ map f ≗ map f ∘ filter (p? ∘ f)

would also be a nice addition.

[jamesmckinna]

Thanks very much for the first PR!

With some suggestions for streamlining your submitted code.

[jamesmckinna]

As for your proposed

map-filter-swap   : ∀ {P : Pred B p} (f : A → B) (p? : Decidable₁ P) 
                    → filter p? ∘ map f ≗ map f ∘ filter (p? ∘ f)

would also be a nice addition.

That seems good, too, but think that filter-map would be a name more in line with our conventions.

As for direct-style proofs vs. appeal to existing lemmas, and use of function equalities, the latter as you have chosen, does seem nice. If there are opportunities to refactor later, the let's do that later. For now, a nice first contribution!

[IchiganCS]

I added the filter-map (much better name, true) and also integrated the minor readability fixes you suggested - thanks for your kind suggestions!

[jamesmckinna]

And you'll need to add a CHANGELOG entry with the new additions...

[IchiganCS]

Sorry for that oversight - i was so eager to install fix-whitespace and run it that I forgot that -_-

Done now! Sorry for the many commits, I think squashing them would be best.

[jamesmckinna]

Sorry for that oversight - i was so eager to install fix-whitespace and run it that I forgot that -_-

Done now! Sorry for the many commits, I think squashing them would be best.

We squash on merge.

[jamesmckinna]

Two quick nit picks:

• for each block of additions, we tend to align the : for readability
• just as for the second and third, there's no need to mention the quantification over P?, Q? etc., neither is it really necessary to mention the f binding in the first one...

The last point may be more of an individual opinion than canon, but AFAIAC, the reader who wants to know the details of implicit vs. explicit quantification can, and will do so in the source. At the current moment of writing, we don't attempt to machine-check any validity criteria for CHANGELOGs, so they can only be considered advisory, rather than definitive!