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/ssreflect/binomial.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/ssreflect/binomial.v')

diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index 8bdb426..1649a89 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -386,8 +386,8 @@ rewrite -card_uniq_tuples.
 have bijFF: {on (_ : pred _), bijective (@Finfun D T)}.
   by exists fgraph => x _; [apply: FinfunK | apply: fgraphK].
 rewrite -(on_card_preimset (bijFF _)); apply: eq_card => /= t.
-rewrite !inE -(big_andE predT) -big_filter big_all -all_map.
-by rewrite -[injectiveb _]/(uniq _) [map _ _]codom_ffun FinfunK.
+rewrite !inE -(big_andE predT) -big_image /= big_all.
+by rewrite -[t in RHS]FinfunK -codom_ffun.
 Qed.
 
 Lemma card_inj_ffuns D T :
-- 
cgit v1.2.3