Add lemmas and max for Qp

Add a few extra lemmas for Qp and adds a max operation for Qp. The lemmas for max are not exhaustive. The names of the lemmas are consistent with those in GenericMinMax.

The library GenericMinMax contains a way to implement max (see for instance how it's used with Q). I'm not sure if that's the better way to do it. But, modules aren't used in this way anywhere in stdpp so I opted to not use it.

The library GenericMinMax contains a way to implement max (see for instance how it's used with Q). I'm not sure if that's the better way to do it. But, modules aren't used in this way anywhere in stdpp so I opted to not use it.

No strong opinion. I think what you've done is fine. Thanks.

Do we already have a min or is it not needed somehow? We have sued min on Qp in lambdaRust.

added 2 commits

• 130451f1 - Address comments regarding max on Qp
• ada15c59 - Add min for Qp, tweak proofs

Compare with previous version

I've addressed the feedback, added min, and tweaked a few of the proofs.

added 1 commit

• f1130fc2 - Make small tweaks to Qp lemmas

Compare with previous version

Thanks for the feedback. I've made changes accordingly.

LGTM. @jung : any further comments?

Nothing sticks out to me, seems reasonable.

Please add a changelog entry though.

added 1 commit

• b5a029c7 - Update changelog

Compare with previous version

Done.

Merging. Thanks a lot!

resolved all threads

merged

mentioned in commit 8cdab430

!182 (merged) was useful for this MR. It caught that it used auto generated names :)

https://gitlab.mpi-sws.org/iris/stdpp/-/jobs/87976

Now we just need to make sure we detect such things before landing. ;) See ci#2 (closed).

mentioned in merge request !187 (merged)

mentioned in merge request !188 (merged)