Merge branch 'gset-simpl-never' into 'master'

Mark gset methods as simpl never to stop `cbn` from unfolding them

See merge request iris/stdpp!298

CHANGELOG.md

@@ -151,6 +151,8 @@ API-breaking change is listed.
   `map_filter_singleton_False`, `map_filter_comm`, `map_union_least`,
   `map_subseteq_difference_l`, `insert_difference`, `insert_difference'`,
   `difference_insert`, `difference_insert_subseteq`. (by Hai Dang)
+- Tweak reduction on `gset`, so that `cbn` matches the behavior by `simpl` and
+  does not unfold `gset` operations. (by Paolo G. Giarrusso, BedRock Systems)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

tests/gmap.ref

+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  {[1; 2; 3]} = ∅
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  elements {[1; 2; 3]} = []
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  {[1; 2; 3]} ∖ {[1]} ∪ {[4]} ∩ {[10]} = ∅ ∖ {[2]}
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  1 ∈ dom (gset nat) (<[1:=2]> ∅)
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (∅ = {[1; 2; 3]}) = false
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (∅ ≡ {[1; 2; 3]}) = false
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (1 ∈ {[1; 2; 3]}) = true
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (∅ ## {[1; 2; 3]}) = true
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (∅ ⊆ {[1; 2; 3]}) = true

tests/gmap.v

+From stdpp Require Import gmap.
+
+Goal {[1; 2; 3]} =@{gset nat} ∅.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+Abort.
+
+Goal elements (C := gset nat) {[1; 2; 3]} = [].
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+Abort.
+
+Goal
+  {[1; 2; 3]} ∖ {[ 1 ]} ∪ {[ 4 ]} ∩ {[ 10 ]} =@{gset nat} ∅ ∖ {[ 2 ]}.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+Abort.
+
+Goal 1 ∈ dom (M := gmap _ _) (gset _) (<[ 1 := 2 ]> ∅).
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+Abort.
+
+Goal bool_decide (∅ =@{gset _} {[ 1; 2; 3 ]}) = false.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.
+
+Goal bool_decide (∅ ≡@{gset _} {[ 1; 2; 3 ]}) = false.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.
+
+Goal bool_decide (1 ∈@{gset _} {[ 1; 2; 3 ]}) = true.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.
+
+Goal bool_decide (∅ ##@{gset _} {[ 1; 2; 3 ]}) = true.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.
+
+Goal bool_decide (∅ ⊆@{gset _} {[ 1; 2; 3 ]}) = true.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.

theories/gmap.v

@@ -237,6 +237,7 @@ Definition gset K `{Countable K} := mapset (gmap K).
 
 Section gset.
   Context `{Countable K}.
+  (* Lift instances of operational TCs from [mapset] and mark them [simpl never]. *)
   Global Instance gset_elem_of: ElemOf K (gset K) := _.
   Global Instance gset_empty : Empty (gset K) := _.
   Global Instance gset_singleton : Singleton K (gset K) := _.
@@ -244,10 +245,6 @@ Section gset.
   Global Instance gset_intersection: Intersection (gset K) := _.
   Global Instance gset_difference: Difference (gset K) := _.
   Global Instance gset_elements: Elements K (gset K) := _.
-  Global Instance gset_leibniz : LeibnizEquiv (gset K) := _.
-  Global Instance gset_semi_set : SemiSet K (gset K) | 1 := _.
-  Global Instance gset_set : Set_ K (gset K) | 1 := _.
-  Global Instance gset_fin_set : FinSet K (gset K) := _.
   Global Instance gset_eq_dec : EqDecision (gset K) := _.
   Global Instance gset_countable : Countable (gset K) := _.
   Global Instance gset_equiv_dec : RelDecision (≡@{gset K}) | 1 := _.
@@ -255,6 +252,27 @@ Section gset.
   Global Instance gset_disjoint_dec : RelDecision (##@{gset K}) := _.
   Global Instance gset_subseteq_dec : RelDecision (⊆@{gset K}) := _.
   Global Instance gset_dom {A} : Dom (gmap K A) (gset K) := mapset_dom.
+
+  Global Arguments gset_elem_of : simpl never.
+  Global Arguments gset_empty : simpl never.
+  Global Arguments gset_singleton : simpl never.
+  Global Arguments gset_union : simpl never.
+  Global Arguments gset_intersection : simpl never.
+  Global Arguments gset_difference : simpl never.
+  Global Arguments gset_elements : simpl never.
+  Global Arguments gset_eq_dec : simpl never.
+  Global Arguments gset_countable : simpl never.
+  Global Arguments gset_equiv_dec : simpl never.
+  Global Arguments gset_elem_of_dec : simpl never.
+  Global Arguments gset_disjoint_dec : simpl never.
+  Global Arguments gset_subseteq_dec : simpl never.
+  Global Arguments gset_dom : simpl never.
+
+  (* Lift instances of other TCs. *)
+  Global Instance gset_leibniz : LeibnizEquiv (gset K) := _.
+  Global Instance gset_semi_set : SemiSet K (gset K) | 1 := _.
+  Global Instance gset_set : Set_ K (gset K) | 1 := _.
+  Global Instance gset_fin_set : FinSet K (gset K) := _.
   Global Instance gset_dom_spec : FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
 
   (** If you are looking for a lemma showing that [gset] is extensional, see