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

tests/gmap.v

@@ -7,11 +7,13 @@ Definition pmap_insert_positives_rev (n : positive) : Pmap unit :=
   Pos.iter (λ rec p m,
     rec (p - 1)%positive (<[p:=tt]> m)) (λ _ m, m) n n ∅.
 
-(* Test that the time is approximately n-log-n. We cannot test this on CI since
-you get different timings all the time.
 Definition pmap_insert_positives_test (p : positive) : bool :=
   bool_decide (pmap_insert_positives p = pmap_insert_positives_rev p).
 
+(* Test that the time is approximately n-log-n. We cannot test this on CI since
+you get different timings all the time. Instead we just test for [256000], which
+likely takes forever if the complexity is not n-log-n. *)
+(*
 Time Eval vm_compute in pmap_insert_positives_test 1000.
 Time Eval vm_compute in pmap_insert_positives_test 2000.
 Time Eval vm_compute in pmap_insert_positives_test 4000.
@@ -24,6 +26,8 @@ Time Eval vm_compute in pmap_insert_positives_test 256000.
 Time Eval vm_compute in pmap_insert_positives_test 512000.
 Time Eval vm_compute in pmap_insert_positives_test 1000000.
 *)
+Check "pmap_insert_positives_test".
+Eval vm_compute in pmap_insert_positives_test 256000.
 
 Definition gmap_insert_positives (n : positive) : gmap positive unit :=
   Pos.iter (λ rec p m,
@@ -37,7 +41,9 @@ Definition gmap_insert_positives_test (p : positive) : bool :=
   bool_decide (gmap_insert_positives p = gmap_insert_positives_rev p).
 
 (* Test that the time is approximately n-log-n. We cannot test this on CI since
-you get different timings all the time.
+you get different timings all the time. Instead we just test for [256000], which
+likely takes forever if the complexity is not n-log-n. *)
+(*
 Time Eval vm_compute in gmap_insert_positives_test 1000.
 Time Eval vm_compute in gmap_insert_positives_test 2000.
 Time Eval vm_compute in gmap_insert_positives_test 4000.
@@ -50,6 +56,8 @@ Time Eval vm_compute in gmap_insert_positives_test 256000.
 Time Eval vm_compute in gmap_insert_positives_test 512000.
 Time Eval vm_compute in gmap_insert_positives_test 1000000.
 *)
+Check "gmap_insert_positives_test".
+Eval vm_compute in gmap_insert_positives_test 256000.
 
 Check "gmap_insert_comm".
 Theorem gmap_insert_comm :