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

Simplification in imset2 should be locked #26

Open
hivert opened this issue Aug 29, 2018 · 1 comment
Open

Simplification in imset2 should be locked #26

hivert opened this issue Aug 29, 2018 · 1 comment

Comments

@hivert
Copy link
Member

hivert commented Aug 29, 2018

Consider the following code:

Variable (f1 f2 : {fset nat}).
Lemma bla : [fset (n1 + n2)%N | n1 in f1, n2 in f2] == fset0.
Proof.
rewrite /=.

Then the goal is:

  f1, f2 : {fset nat}
  ============================
  Imfset.imfset2 imfset_key (K:=nat_choiceType) (T1:=nat_choiceType)
    (T2:=fun _ : nat => nat_choiceType) (fun n1 : nat => [eta addn n1])
    (p1:=mem_fin (fin_finpred (pT:=fset_finpredType nat_choiceType) f1))
    (p2:=fun _ : nat =>
         mem_fin (fin_finpred (pT:=fset_finpredType nat_choiceType) f2))
    (Phantom (mem_pred nat) (mem f1))
    (Phantom (nat -> mem_pred nat) (fun _ : nat => mem f2)) == fset0

Which is completely unreadable. I think the simplification should not be possible except after some form of unlocking.

@CohenCyril
Copy link
Member

This looks more like a notation not printing correctly bug than a simplification problem... I will investigate the problem.

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