- Aug 28, 2023
-
-
Ralf Jung authored
-
Ralf Jung authored
use ssreflect rewrite for multiset tactics Closes #195 See merge request iris/stdpp!497
-
-
Ralf Jung authored
-
- Aug 03, 2023
-
-
Robbert Krebbers authored
Add lemmas for commuting funcs with folds See merge request iris/stdpp!478
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Isaac van Bakel authored
-
Robbert Krebbers authored
-
Isaac van Bakel authored
I thought this would make it clear that "acc" means "accumulator" in the fold, without making the names too verbose. This arose out of a misreading of "acc" as "assoc", which I want to avoid.
-
Isaac van Bakel authored
All these lemmas admit stronger versions which only care about the commutativity of the fold and accumulator functions for the data structure elements, rather than for the whole type. Each lemma has been strengthened in line with the rest of its file, which is why there are some discrepancies across the definitions. This was inspired by the fact that the original version of the lemma for maps was in fact slightly stronger in its commutativity conditions. Only the map version permits a preorder instead of an equivalence - though in principle, the commutativity conditions should allow all versions to only require a preorder. The reason for this is that the map induction principle used is much stronger, and already handles insertion commutativity "internally", which allows for the right kind of rewriting. The other proofs get stuck trying to show that the preorder should strengthen to an equivalence on a certain class of elements in the fold. To save my sanity, I've just required an equivalence everywhere for these instead.
-
Isaac van Bakel authored
This adds a multiset-equivalent to the set API's `set_fold_disj_union_strong`, which strengthens the fold function condition to only need to apply to (multi)set elements - note that in a multiset, elements can be equal, so there is no inequality in the fold condition. It also now applies to any preorder which respects the fold function.
-
Isaac van Bakel authored
Part of the feedback on #478. This extends the lemmas for commuting unitary functions in and out folds to lists and finite sets.
-
Isaac van Bakel authored
These lemmas were helpful to me in recent proofs (in particular, the multiset one is used for iris/iris#923.) They allow for moving a unitary function on a fold accumulator in and out of the fold as necessary, provided the function commutes appropriately with the fold function. Both versions technically admit a more general type - that is, the type of the accumulator doesn't have to match the multiset or map element type in the general case. However, proving these more general versions is much harder, so I've left it to whoever may want to use them in the future. The location of the multiset lemma in the file is not ideal, since it has to come after `gmultiset_ind`, which is well after all the other fold lemmas. However, proving it without `gmultiset_ind` is much harder, and moving `gmultiset_ind` further up the file is itself non-trivial, so I've opted not to try.
-
Robbert Krebbers authored
Correct `Params` instances for `lookup` and `singletonM`. See merge request iris/stdpp!494
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
add pair_equiv See merge request iris/stdpp!490
-
Ralf Jung authored
Better way of writing `Proper` premises in fin sets See merge request iris/stdpp!493
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Aug 02, 2023
-
-
Ralf Jung authored
add some map-fmap lemmas See merge request iris/stdpp!489
-
Robbert Krebbers authored
Use `Proper (.. => impl)` instead of `Proper (.. => iff)` and `∀ x, Proper ..` instead of `Proper ((=) ==> ..)`. The new premises are easier to prove (both `solve_proper` and manual proof).
-
Robbert Krebbers authored
Change premise `Equivalence` into `PreOrder` for `set_fold_proper`. See merge request iris/stdpp!492
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Add a number of missing intersection lemmas Closes #166 See merge request iris/stdpp!491
-
- Jul 29, 2023
-
-
Marijn van Wezel authored
-
- Jul 27, 2023
- Jul 25, 2023
-
-
Robbert Krebbers authored
Remove Permutation Proper workaround that is not needed in Coq >= 8.15. See merge request iris/stdpp!486
-
Robbert Krebbers authored
Fixed by https://github.com/coq/coq/issues/14571
-
- Jul 21, 2023
-
-
Robbert Krebbers authored
Add fin notations See merge request iris/stdpp!484
-
-
- Jun 02, 2023
-
-
Ralf Jung authored
add filter_dom (from Perennial) See merge request iris/stdpp!482
-
Ralf Jung authored
-