Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Notation issues for imfset #73

Open
chdoc opened this issue Aug 25, 2020 · 2 comments
Open

Notation issues for imfset #73

chdoc opened this issue Aug 25, 2020 · 2 comments

Comments

@chdoc
Copy link
Member

chdoc commented Aug 25, 2020

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
Copy link
Member

CohenCyril commented Aug 25, 2020

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.

@CohenCyril CohenCyril pinned this issue Aug 25, 2020
@chdoc
Copy link
Member Author

chdoc commented Aug 26, 2020

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. 😒

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants