Mark gset methods as simpl never to stop `cbn` from unfolding them
This clarifies what's meant to happen anyway, and is apparently needed for cbn. (I haven't yet tried doing this at the mapset level).
Example of the problem: without this change, cbn mangles the goal in the following:
Goal {[1; 2; 3]} =@{gset nat} ∅.
Fail progress simpl.
progress cbn. Show.I'd want progress cbn to fail, instead the above gives:
The command has indeed failed with message:
Failed to progress.
1 subgoal
============================
{| mapset_car := {[1 := ()]} ∪ {[2 := ()]} ∪ {[3 := ()]} |} = ∅Merge request reports
Activity
- Resolved by Paolo G. Giarrusso
It seems fine to me to make more definitions
simpl never, but why does it make sense to do that proof proofs (e.g.,gset_leibniz) too? - Last reply by Paolo G. Giarrusso
added 2 commits
How about adding a test case so that we don't break this in the future? How about also adding the same test case for simpl?
(While we don't use cbn in std++, I am all in favor of improving support for cbn as long as that does not affect simpl. Thus using cbn in test cases would be perfectly fine.)
added S-waiting-for-author label
added 65 commits
-
0ac53934...c4a352b1 - 63 commits from branch
iris:master - eeb2ebd6 - gmap.v: reorder gset instances
- 38547507 - Mark gset methods as simpl never and add test
-
0ac53934...c4a352b1 - 63 commits from branch
added 1 commit
- 1dbfdf20 - Mark gset methods as simpl never and add test
added 1 commit
- dc91e447 - Mark gset methods as simpl never and add test
Added a few
Fail progress simpl/cbntests; they should cover everything, including decidable operations (with at least one case).FWIW, on these tests I only need the following — but I don't think reduction ever helps on
gsetso I'd stick to the current settings.Global Arguments gset_singleton : simpl never. Global Arguments gset_union : simpl never. Global Arguments gset_difference : simpl nomatch.mentioned in commit ac04787b
