From 4bd5ba38e4f6c6456a8fcc39364a67b51fde92f2 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Tue, 26 Nov 2019 17:28:36 +0100 Subject: Explicit `bigop` enumeration handling Added lemmas `big_enum_cond`, `big_enum` and `big_enumP` to handle more explicitly big ops iterating over explicit enumerations in a `finType`. The previous practice was to rely on the convertibility between `enum A` and `filter A (index_enum T)`, sometimes explicitly via the `filter_index_enum` equality, more often than not implicitly. Both are likely to fail after the integration of `finmap`, as the `choiceType` theory can’t guarantee that the order in selected enumerations is consistent. For this reason `big_enum` and the related (but currently unused) `big_image` lemmas are restricted to the abelian case. The `big_enumP` lemma can be used to handle enumerations in the non-abelian case, as explained in the `bigop.v` internal documentation. The Changelog entry enjoins clients to stop relying on either `filter_index_enum` and convertibility (though this PR still provides both), and warns about the restriction of the `big_image` lemma set to the abelian case, as it it a possible source of incompatibility. --- mathcomp/algebra/mxalgebra.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/algebra/mxalgebra.v') diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 38beffc..7e1dfbb 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -2091,7 +2091,7 @@ Lemma mxdirect_delta n f : {in P &, injective f} -> Proof. pose fP := image f P => Uf; have UfP: uniq fP by apply/dinjectiveP. suffices /mxdirectP : mxdirect (\sum_i <>). - rewrite /= !(bigID [mem fP] predT) -!big_uniq //= !big_map !big_filter. + rewrite /= !(bigID [mem fP] predT) -!big_uniq //= !big_map !big_enum. by move/mxdirectP; rewrite mxdirect_addsE => /andP[]. apply/mxdirectP=> /=; transitivity (mxrank (1%:M : 'M[F]_n)). apply/eqmx_rank; rewrite submx1 mx1_sum_delta summx_sub_sums // => i _. -- cgit v1.2.3