Stream: math-comp users

Topic: Proving [fset x | x in A & x \in B] = B

Ricardo (Jan 16 2023 at 18:05):

Hi. How would you prove [fset x | x in A & x \in B] = B where B = A \ C and A, B and C are mathcomp.finmap sets?

I imagine one way would be to transform [fset x | x in A & x \in B] into [fset x | x in B] and then use imfset_id.

Ana de Almeida Borges (Jan 16 2023 at 18:48):

There must be many ways to do so, but this one seems straightforward enough. Note that inE accomplishes a lot but for some reason prints k \in mem_fin (fset_finpred A) instead of k \in A, which hides the fact that the goal is a simple consequence of the properties of && at that point (or case analysis, as you prefer).

From mathcomp Require Import all_ssreflect finmap.
Open Scope fset.

Lemma foo (K : choiceType) (A C : {fset K}) :
[fset x | x in A & x \in A \ C] = A \ C.
Proof.
apply/fsetP => k.
rewrite !inE.
rewrite -[_ \in mem_fin (fset_finpred _)]/(k \in A).
by case: (k \in A); rewrite ?andbF.
Qed.


Ricardo (Jan 16 2023 at 19:35):

Thank you @Ana de Almeida Borges. After understanding your code I feel like I'm starting to get an intuion on how to bring the goal to a state where inE can be most useful.

Alexander Gryzlov (Jan 16 2023 at 21:53):

You can "shake" the predicate notation down by refolding it, also you can use the idempotency of && instead of case, rolling the last 3 lines into

by rewrite !inE /= unfold_in topredE andbCA andbb.

Last updated: Jul 23 2024 at 21:01 UTC