Use `SProp` to obtain better definitional equality for `pmap`, `gmap`, `gset`, `Qp`, and `coPset`

This MR ensures that more equalities hold definitionally, and can thus be proved by reflexivity or even by conversion as part of unification.

For example 1/4 + 3/4 = 1, or {[ 1 := 1; 2 := 2 ]} = {[ 2 := 2; 1 := 1 ]}, or {[ 1 ]} ∖ {[ 1 ]} = ∅ can be proved using a mere reflexivity with this MR. Moreover, if you have a goal that involves, say 1/4 + 3/4, then you can just apply a lemma involving 1 because both are convertible.

This MR is based on !189 (closed) but makes various changes:

• Use Squash instead of sUnit to ensure that coqchk comes back clean.
• Make the proofs of data structures like pmap and gmap opaque so that we obtain O(log n) operations. This MR includes some tests, but they are commented out because such timings cannot be tested by CI.
• Use SProp for coPset and Qp (!189 (closed) only considered pmap, gmap, and gset)
  • The change for coPset was pretty simple, but instead of a Sigma type, I had to use a record with an SProp field.
  • The change for Qp was more involved. Qp was originally defined in terms of Qc from the Coq standard lib, which itself is a Q + a Prop proof. Due to the Prop proof, I could no longer use Qc and had to inline an SProp version of Qp. In the process, I also decided to no longer use Q, which is defined as a pair of a Z and a positive, but just use pairs of positives. That avoids the need for a proof of the fraction being positive. None of these changes should be visible in the Qp API.

This MR changes the implementations of the aforementioned data structures, but their APIs should not have changed.

Fixes #85

theories/coPset.v

@@ -161,7 +161,9 @@ Proof.
 Qed.
 
 (** * Packed together + set operations *)
-Record coPset := CoPset {
+(** Add an underscore to [CoPset_] to avoid nameclash with Iris's
+[algebra.coPset.CoPset]. *)
+Record coPset := CoPset_ {
   coPset_car : coPset_raw;
   coPset_prf : SIs_true (coPset_wf coPset_car);
 }.
@@ -178,20 +180,20 @@ Global Instance coPset_eq_dec : EqDecision coPset := λ X1 X2,
   end.
 
 Global Instance coPset_singleton : Singleton positive coPset := λ p,
-  CoPset (coPset_singleton_raw p) (coPset_singleton_wf _).
+  CoPset_ (coPset_singleton_raw p) (coPset_singleton_wf _).
 Global Instance coPset_elem_of : ElemOf positive coPset := λ p X,
   e_of p (coPset_car X).
-Global Instance coPset_empty : Empty coPset := CoPset (coPLeaf false) stt.
-Global Instance coPset_top : Top coPset := CoPset (coPLeaf true) stt.
+Global Instance coPset_empty : Empty coPset := CoPset_ (coPLeaf false) stt.
+Global Instance coPset_top : Top coPset := CoPset_ (coPLeaf true) stt.
 Global Instance coPset_union : Union coPset :=
-  λ '(CoPset t1 Ht1) '(CoPset t2 Ht2),
-    CoPset (t1 ∪ t2) (coPset_union_wf _ _ Ht1 Ht2).
+  λ '(CoPset_ t1 Ht1) '(CoPset_ t2 Ht2),
+    CoPset_ (t1 ∪ t2) (coPset_union_wf _ _ Ht1 Ht2).
 Global Instance coPset_intersection : Intersection coPset :=
-  λ '(CoPset t1 Ht1) '(CoPset t2 Ht2),
-    CoPset (t1 ∩ t2) (coPset_intersection_wf _ _ Ht1 Ht2).
+  λ '(CoPset_ t1 Ht1) '(CoPset_ t2 Ht2),
+    CoPset_ (t1 ∩ t2) (coPset_intersection_wf _ _ Ht1 Ht2).
 Global Instance coPset_difference : Difference coPset :=
-  λ '(CoPset t1 Ht1) '(CoPset t2 Ht2),
-    CoPset (t1 ∩ coPset_opp_raw t2)
+  λ '(CoPset_ t1 Ht1) '(CoPset_ t2 Ht2),
+    CoPset_ (t1 ∩ coPset_opp_raw t2)
            (coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _)).
 
 Global Instance coPset_top_set : TopSet positive coPset.
@@ -347,7 +349,7 @@ Proof. induction t as [|[[]|]]; simpl; rewrite ?andb_True; auto. Qed.
 
 Definition Pset_to_coPset (X : Pset) : coPset :=
   let 'Mapset (PMap t Ht) := X in
-  CoPset (Pset_to_coPset_raw t) (Pset_to_coPset_wf _ Ht).
+  CoPset_ (Pset_to_coPset_raw t) (Pset_to_coPset_wf _ Ht).
 Lemma elem_of_Pset_to_coPset X i : i ∈ Pset_to_coPset X ↔ i ∈ X.
 Proof. destruct X as [[t ?]]; apply elem_of_Pset_to_coPset_raw. Qed.
 Lemma Pset_to_coPset_finite X : set_finite (Pset_to_coPset X).
@@ -364,7 +366,7 @@ Definition coPset_to_gset (X : coPset) : gset positive :=
 
 Definition gset_to_coPset (X : gset positive) : coPset :=
   let 'Mapset (GMap (PMap t Ht) _) := X in
-  CoPset (Pset_to_coPset_raw t) (Pset_to_coPset_wf _ Ht).
+  CoPset_ (Pset_to_coPset_raw t) (Pset_to_coPset_wf _ Ht).
 
 Lemma elem_of_coPset_to_gset X i : set_finite X → i ∈ coPset_to_gset X ↔ i ∈ X.
 Proof.
@@ -421,7 +423,7 @@ Fixpoint coPset_suffixes_raw (p : positive) : coPset_raw :=
 Lemma coPset_suffixes_wf p : SIs_true (coPset_wf (coPset_suffixes_raw p)).
 Proof. apply SIs_true_intro. induction p; simpl; eauto. Qed.
 Definition coPset_suffixes (p : positive) : coPset :=
-  CoPset (coPset_suffixes_raw p) (coPset_suffixes_wf _).
+  CoPset_ (coPset_suffixes_raw p) (coPset_suffixes_wf _).
 Lemma elem_coPset_suffixes p q : p ∈ coPset_suffixes q ↔ ∃ q', p = q' ++ q.
 Proof.
   unfold elem_of, coPset_elem_of; simpl; split.
@@ -454,9 +456,9 @@ Proof. apply SIs_true_intro. induction t as [[]|]; simpl; auto. Qed.
 Lemma coPset_r_wf t : SIs_true (coPset_wf (coPset_r_raw t)).
 Proof. apply SIs_true_intro.  induction t as [[]|]; simpl; auto. Qed.
 Definition coPset_l (X : coPset) : coPset :=
-  let (t,Ht) := X in CoPset (coPset_l_raw t) (coPset_l_wf _).
+  let (t,Ht) := X in CoPset_ (coPset_l_raw t) (coPset_l_wf _).
 Definition coPset_r (X : coPset) : coPset :=
-  let (t,Ht) := X in CoPset (coPset_r_raw t) (coPset_r_wf _).
+  let (t,Ht) := X in CoPset_ (coPset_r_raw t) (coPset_r_wf _).
 
 Lemma coPset_lr_disjoint X : coPset_l X ∩ coPset_r X = ∅.
 Proof.