finmap
finmap copied to clipboard
math-comp
Finite sets, finite maps, multisets and generic sets
Does it make sense to move [`unit_irrelevance`](https://github.com/math-comp/finmap/blob/92a959e9e91ca356b937923bc823c7f7bb9029b5/order.v#L290) elsewhere in Coq's part of ssreflect or mathcomp? E.g. to `ssrfun`, near [`unitE` lemma](https://github.com/coq/coq/blob/a9e0f0ee9e4936d700d39faaa20568c0c561b8fa/plugins/ssr/ssrfun.v#L280), which in turn could be used to prove the...
Consider the following code: ``` Variable (f1 f2 : {fset nat}). Lemma bla : [fset (n1 + n2)%N | n1 in f1, n2 in f2] == fset0. Proof. rewrite /=....
I'm afraid I might be not expert enough with canonical structure to finish my pull request https://github.com/math-comp/finmap/pull/8. Here is what could possibly done 1 - Any subtype of a porder/order...
Note on what we discussed at Dagstuhl 18341: - The name "reverse" order looks bad to me. Indeed the reverse lexicographic order is not the reverse of the lex order....
Is there a plan to define order-preserving morphisms and some of their theory?
The notation [`x] badly interact with the [] selector and the notation for the norm.
Hello, Through an experimental formalization of well-foundedness of multiset ordering, I found the following finmap/multiset lemmas convenient. Some of them might also be useful for general use. (Update: proofs are...
Iirc, we removed the generic sets from master and recorded them in the following branch (as a draft PR) https://github.com/math-comp/finmap/pull/108 So therefore it might be better to remove the mention...
