Experiment with SProp to make gmap operations compute nicely

Currently both Pmap and gmap are sigma types of the form {x:T | Is_true (wf x : bool)}. If they were instead written {x:T | sis_true (wf x : bool) : SProp} (using sis_true (b:bool) : SProp := if b then sUnit else sEmpty), then the well-formedness proof would be in SProp. This gives not just proof irrelevance but definitional proof irrelevance, which I think means proofs will compute away properly when reducing gmap operations in Coq.

mentioned in issue #84

I did this experiment for Pmap and got std++ to compile. It required a few minor changes in coPset, which constructs well-formedness proofs directly and thus breaks the Pmap abstraction.

This works out pretty easily because there's a bijection between Is_true b and sis_true b.

This gives not just proof irrelevance but definitional proof irrelevance, which I think means proofs will compute away properly when reducing gmap operations in Coq.

Yes, that's what I would expect too. See also my comment here.

This means we need to drop support for Coq <8.10 though.

mentioned in merge request !188 (merged)

mentioned in merge request !189 (closed)

mentioned in merge request !309 (merged)

mentioned in commit 8dbccce2

closed with merge request !309 (merged)

!309 (merged) got reverted, so reopening this.

reopened

mentioned in issue #64

Did the performance issue mentioned in the revert ever get investigated?

BTW you may want to consider using an inductive for sis_true (with a lemma sis_true false -> sEmpty, or even setting UIP locally to the inductive's declaration)

No, we didn't really have any good ideas for how to even start investigating that.

Timing results are here.