Add properties of algebraic semilattices

[sstucki]

...and update dependencies.

I noticed that algebraic semilattices are now defined as a structure in the Algebra module, so I thought it might be nice to also add a Algebra.Properties module for them (similar to that for lattices).

I moved some of the properties from Algebra.Properties.Lattice to Algebra.Properties.Semilattice and updated the former so as not to break dependencies.

[MatthewDaggitt]

Thanks a lot, that's great!

I've just merged #535 in, which redefines lattices in terms of semilattices so you may need to do a little tweaking of the PR... apologies!

Edit: Also could you document which proofs have been moved in the CHANGELOG. Thanks!

[sstucki]

@MatthewDaggitt: OK that should be easy to fix, but is defining lattices in terms of semilattices really a good idea? Before, idempotence of the meet and join operations was a consequence of absorption (which was proved in Algebra.Properties.Lattice, but now it becomes a law (i.e. a field) in IsLattice. I actually preferred the old version of Lattice, because it requires fewer laws to be assumed (and more to be derived).

[MatthewDaggitt]

Hmm that's a good point. Compositionality is better with the new structure, but the downside is that idempotence must be proved directly...

I guess that the changes should probably be reverted. Apologies, I don't have time at the moment, but I'll try and get round to it in the next couple of weeks.

[sstucki]

OK, I fixed the PR so that it should hopefully pass the CI now, commented out the (now redundant) idempotence theorems in Algebra.Properties.Lattice, and left a FIXME comment there.

I'll leave it up to you whether to merge the PR now or later. In either case, it should be easy to adjust Algebra.Properties.Lattice once the changes in the definitions of IsLattice and Lattice have been reverted.

[sstucki]

Actually, I still have to update the CHANGELOG as well before the PR can be merged.

If you want, I can update the PR to include a (separate) commit reverting the changes to the lattice records to make things easier.

WDYT?

[WolframKahl]

Compositionality is better with the new structure, but the downside is that idempotence must be proved directly...

One could still provide a smart constructor that takes the old `field`s.

[MatthewDaggitt]

One could still provide a smart constructor that takes the old fields.

Hmm it would be quite a long constructor... Passing 8(?) parameters to it isn't going to be very neat. Given the downsides, probably better to err on the side of minimising non-backwards compatible changes.

If you want, I can update the PR to include a (separate) commit reverting the changes to the lattice records to make things easier.

If you have the time @sstucki that would be great, thanks!

[sstucki]

Here you go @MatthewDaggitt.

[sstucki]

@MatthewDaggitt, let me know if there's anything else you need from me to merge this PR.

[MatthewDaggitt]

Nope, looks good thanks! Merging in

[sstucki]

OK, thanks!

[MatthewDaggitt]

@sstucki I forgot to ask. Given that you've contributed modules, would you like to be added to authors list and if so under what name?

[sstucki]

Sure! You can add me as Sandro Stucki. Thanks and happy holidays!