Stream: math-comp users

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


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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