`gset_to_coPset` shows implementation on `simpl` when called on a empty constant set.
Consider the following example.
From stdpp Require Import coPset.
Lemma test :
gset_to_coPset (∅ ∪ ∅) = ∅.
Proof.
simpl. rewrite union_empty_l_L.
Abort.
I expected the simpl
to do nothing, and I can proceed with the rewrite
. However, it instead inlined the definition of gset_to_coPset
, resulting in the following Coq context.
(let
'{| gmap.gmap_car := gmap_car |} := ∅ ∪ ∅ in
let
'{| pmap.pmap_car := t; pmap.pmap_prf := Ht |} := gmap_car in
Pset_to_coPset_raw t ↾ Pset_to_coPset_wf t Ht) = ∅
The rewrite then fails with the following message.
Unable to satisfy the following constraints:
?H : "ElemOf ?A (gmap.gmap positive ())"
?H1 : "Singleton ?A (gmap.gmap positive ())"
?H3 : "SemiSet ?A (gmap.gmap positive ())"
?LeibnizEquiv0 : "LeibnizEquiv (gmap.gmap positive ())"
Not preforming simpl
makes the rewrite
work fine.
The easiest solution I found was to do simpl never
for gset_to_coPset
. I feel like this should be the default since the user should never need to look at the inner definition of gset_to_coPset
, being cryptic as it is.
Are there more better/intended solutions?
Edited by Janggun Lee