Big ops and lattices in stdpp?
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?