Notation issues for `imfset`

[chdoc]

The following script showcases some unfortunate notation behaviors (on the current coq.dev and finmap.dev)

From mathcomp Require Import all_ssreflect finmap.

Open Scope fset_scope.
 
Lemma fsetIsep (T : choiceType) (A B : {fset T}) : 
  A `&` B = [fset x in A | x \in B].

(* Goal: A `&` B = [fset (x : T) | x in A & x \in B] *)

rewrite /fsetI.

(* Goal: [fset x | x in A & x \in B] = [fset x | x in A & x \in B] *)

Fail reflexivity.

apply/fsetP => x; rewrite !inE.

(* Goal: (x \in A) && (x \in B) = (x \in mem_fin (fset_finpred A)) && (x \in B) *)

rewrite /=.

(* Goal:  (x \in A) && (x \in B) = (x \in [eta mem_seq (T:=T) A]) && (x \in B) *)

reflexivity.

Qed.

[CohenCyril]

This is bad indeed. For one part of my defense (FWIW) you are not supposed to unfold fsetI ;) What happens next with !inE /= is highly embarrassing... I will look into this, thanks for pointing it out.

[chdoc]

For one part of my defense (FWIW) you are not supposed to unfold fsetI ;)

Yes, I realized that. Indeed, unfolding the defined operations can cause even more "funny" behaviors. I you replace & with \, then rewrite !inE /= will rewrite the unfolded [fset x | x in A & x \notin B] to (x \notin B) && (x \in A), presumably because it (still) uses the in_fsetD rule rather than the in_fset rule that one would expect to get from the printed goal. Ineed, rewriting with in_fset !inE /= gives the expected [eta mem_seq ...] mess. :unamused: