# 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.

- The change for

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

Fixes #85

Edited by Ralf Jung