Big ops and lattices in stdpp?
Hi,
I currently have a meet-semilattice, and I want to show that if a map m1
is "less" than m2
, in the sense that m1
's values are pointwise less than those of m2
's by the lattice order, then the meet of m1
values is also less than that of m2
. I don't see a clean way to prove this, as I define the meet as a fold over the list of values.
I'd like a more structure way to define the meet as big ops in Iris. Is is possible to generalize big ops so that they need not depend on ofe's?
Also, I believe lattices would be useful enough to be in stdpp, although our development of them in iGPS is a bit under-developed.
What do you think?