Use SProp for Pmap and gmap sigma types

_CoqProject

@@ -5,6 +5,7 @@
 theories/options.v
 theories/base.v
 theories/tactics.v
+theories/sprop.v
 theories/option.v
 theories/fin_map_dom.v
 theories/boolset.v

tests/gmap.v

@@ -68,3 +68,7 @@ Proof.
   Show.
   reflexivity.
 Qed.
+
+Theorem gmap_insert_comm :
+  <[3:=false]> {[2:=true]} =@{gmap nat bool} <[2:=true]> {[3:=false]}.
+Proof. reflexivity. Qed.

theories/coPset.v

@@ -281,7 +281,7 @@ Fixpoint coPset_to_Pset_raw (t : coPset_raw) : Pmap_raw () :=
 Lemma coPset_to_Pset_wf t : coPset_wf t → Pmap_wf (coPset_to_Pset_raw t).
 Proof. induction t as [|[]]; simpl; eauto using PNode_wf. Qed.
 Definition coPset_to_Pset (X : coPset) : Pset :=
-  let (t,Ht) := X in Mapset (PMap (coPset_to_Pset_raw t) (coPset_to_Pset_wf _ Ht)).
+  let (t,Ht) := X in Mapset (PMap (coPset_to_Pset_raw t) (is_true_intro $ coPset_to_Pset_wf _ Ht)).
 Lemma elem_of_coPset_to_Pset X i : set_finite X → i ∈ coPset_to_Pset X ↔ i ∈ X.
 Proof.
   rewrite coPset_finite_spec; destruct X as [t Ht].
@@ -310,7 +310,7 @@ Lemma Pset_to_coPset_raw_finite t : coPset_finite (Pset_to_coPset_raw t).
 Proof. induction t as [|[[]|]]; simpl; rewrite ?andb_True; auto. Qed.
 
 Definition Pset_to_coPset (X : Pset) : coPset :=
-  let 'Mapset (PMap t Ht) := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ Ht.
+  let 'Mapset (PMap t Ht) := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ (is_true_elim 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).
@@ -320,13 +320,13 @@ Qed.
 
 (** * Conversion to and from gsets of positives *)
 Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf positive m.
-Proof. unfold gmap_wf. by rewrite bool_decide_spec. Qed.
+Proof. unfold gmap_wf. apply is_true_intro. by rewrite bool_decide_spec. Qed.
 Definition coPset_to_gset (X : coPset) : gset positive :=
   let 'Mapset m := coPset_to_Pset X in
   Mapset (GMap m (coPset_to_gset_wf m)).
 
 Definition gset_to_coPset (X : gset positive) : coPset :=
-  let 'Mapset (GMap (PMap t Ht) _) := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ Ht.
+  let 'Mapset (GMap (PMap t Ht) _) := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ (is_true_elim Ht).
 
 Lemma elem_of_coPset_to_gset X i : set_finite X → i ∈ coPset_to_gset X ↔ i ∈ X.
 Proof.

theories/gmap.v

@@ -20,8 +20,8 @@ Unset Default Proof Using.
 (** * The data structure *)
 (** We pack a [Pmap] together with a proof that ensures that all keys correspond
 to codes of actual elements of the countable type. *)
-Definition gmap_wf K `{Countable K} {A} (m : Pmap A) : Prop :=
-  bool_decide (map_Forall (λ p _, encode (A:=K) <$> decode p = Some p) m).
+Definition gmap_wf K `{Countable K} {A} (m : Pmap A) : SProp :=
+  sprop_decide (map_Forall (λ p _, encode (A:=K) <$> decode p = Some p) m).
 Record gmap K `{Countable K} A := GMap {
   gmap_car : Pmap A;
   gmap_prf : gmap_wf K gmap_car
@@ -31,8 +31,7 @@ Global Arguments gmap_car {_ _ _ _} _ : assert.
 Lemma gmap_eq `{Countable K} {A} (m1 m2 : gmap K A) :
   m1 = m2 ↔ gmap_car m1 = gmap_car m2.
 Proof.
-  split; [by intros ->|intros]. destruct m1, m2; simplify_eq/=.
-  f_equal; apply proof_irrel.
+  split; [by intros ->|intros]. destruct m1, m2; simplify_eq/=; done.
 Qed.
 Global Instance gmap_eq_eq `{Countable K, EqDecision A} : EqDecision (gmap K A).
 Proof.
@@ -43,7 +42,7 @@ Defined.
 (** * Operations on the data structure *)
 Global Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) :=
   λ i '(GMap m _), m !! encode i.
-Global Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap ∅ I.
+Global Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap ∅ stt.
 (** Block reduction, even on concrete [gmap]s.
 Marking [gmap_empty] as [simpl never] would not be enough, because of
 https://github.com/coq/coq/issues/2972 and
@@ -55,7 +54,7 @@ Global Opaque gmap_empty.
 Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A → option A) m i :
   gmap_wf K m → gmap_wf K (partial_alter f (encode (A:=K) i) m).
 Proof.
-  unfold gmap_wf; rewrite !bool_decide_spec.
+  unfold gmap_wf; apply is_true_fmap; rewrite !bool_decide_spec.
   intros Hm p x. destruct (decide (encode i = p)) as [<-|?].
   - rewrite decode_encode; eauto.
   - rewrite lookup_partial_alter_ne by done. by apply Hm.
@@ -68,7 +67,7 @@ Global Instance gmap_partial_alter `{Countable K} {A} :
 Lemma gmap_fmap_wf `{Countable K} {A B} (f : A → B) m :
   gmap_wf K m → gmap_wf K (f <$> m).
 Proof.
-  unfold gmap_wf; rewrite !bool_decide_spec.
+  unfold gmap_wf; apply is_true_fmap; rewrite !bool_decide_spec.
   intros ? p x. rewrite lookup_fmap, fmap_Some; intros (?&?&?); eauto.
 Qed.
 Global Instance gmap_fmap `{Countable K} : FMap (gmap K) := λ A B f '(GMap m Hm),
@@ -76,7 +75,7 @@ Global Instance gmap_fmap `{Countable K} : FMap (gmap K) := λ A B f '(GMap m Hm
 Lemma gmap_omap_wf `{Countable K} {A B} (f : A → option B) m :
   gmap_wf K m → gmap_wf K (omap f m).
 Proof.
-  unfold gmap_wf; rewrite !bool_decide_spec.
+  unfold gmap_wf; apply is_true_fmap; rewrite !bool_decide_spec.
   intros ? p x; rewrite lookup_omap, bind_Some; intros (?&?&?); eauto.
 Qed.
 Global Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f '(GMap m Hm),
@@ -85,8 +84,11 @@ Lemma gmap_merge_wf `{Countable K} {A B C}
     (f : option A → option B → option C) m1 m2 :
   gmap_wf K m1 → gmap_wf K m2 → gmap_wf K (merge f m1 m2).
 Proof.
-  unfold gmap_wf; rewrite !bool_decide_spec.
-  intros Hm1 Hm2 p z. rewrite lookup_merge; intros.
+  unfold gmap_wf.
+  refine (λ H1' H2', is_true_bind H1' (λ H1, is_true_bind H2' (λ H2, is_true_intro (_ H1 H2)))).
+  clear H1 H2 H1' H2'.
+  rewrite !bool_decide_spec.
+  intros Hm1 Hm2 p z; rewrite lookup_merge by done; intros.
   destruct (m1 !! _) eqn:?, (m2 !! _) eqn:?; naive_solver.
 Qed.
 Global Instance gmap_merge `{Countable K} : Merge (gmap K) :=
@@ -102,7 +104,7 @@ Proof.
   split.
   - unfold lookup; intros A [m1 Hm1] [m2 Hm2] Hm.
     apply gmap_eq, map_eq; intros i; simpl in *.
-    apply bool_decide_unpack in Hm1; apply bool_decide_unpack in Hm2.
+    apply sprop_decide_unpack in Hm1; apply sprop_decide_unpack in Hm2.
     apply option_eq; intros x; split; intros Hi.
     + pose proof (Hm1 i x Hi); simpl in *.
       by destruct (decode i); simplify_eq/=; rewrite <-Hm.
@@ -114,7 +116,7 @@ Proof.
     by contradict Hs; apply (inj encode).
   - intros A B f [m Hm] i; apply (lookup_fmap f m).
   - intros A [m Hm]; unfold map_to_list; simpl.
-    apply bool_decide_unpack, map_Forall_to_list in Hm; revert Hm.
+    apply sprop_decide_unpack, map_Forall_to_list in Hm; revert Hm.
     induction (NoDup_map_to_list m) as [|[p x] l Hpx];
       inversion 1 as [|??? Hm']; simplify_eq/=; [by constructor|].
     destruct (decode p) as [i|] eqn:?; simplify_eq/=; constructor; eauto.
@@ -122,7 +124,7 @@ Proof.
     feed pose proof (proj1 (Forall_forall _ _) Hm' (p',x')); simpl in *; auto.
     by destruct (decode p') as [i'|]; simplify_eq/=.
   - intros A [m Hm] i x; unfold map_to_list, lookup; simpl.
-    apply bool_decide_unpack in Hm; rewrite elem_of_list_omap; split.
+    apply sprop_decide_unpack in Hm; rewrite elem_of_list_omap; split.
     + intros ([p' x']&Hp'&?); apply elem_of_map_to_list in Hp'.
       feed pose proof (Hm p' x'); simpl in *; auto.
       by destruct (decode p') as [i'|] eqn:?; simplify_eq/=.

theories/pmap.v

@@ -8,6 +8,7 @@ Leibniz equality to become extensional. *)
 From Coq Require Import PArith.
 From stdpp Require Import mapset countable.
 From stdpp Require Export fin_maps.
+From stdpp Require Export sprop.
 From stdpp Require Import options.
 
 Local Open Scope positive_scope.
@@ -255,37 +256,43 @@ Qed.
 
 (** Packed version and instance of the finite map type class *)
 Inductive Pmap (A : Type) : Type :=
-  PMap { pmap_car : Pmap_raw A; pmap_prf : Pmap_wf pmap_car }.
+  PMap { pmap_car : Pmap_raw A; pmap_prf : is_true (Pmap_wf pmap_car) }.
 Global Arguments PMap {_} _ _ : assert.
 Global Arguments pmap_car {_} _ : assert.
 Global Arguments pmap_prf {_} _ : assert.
+
 Lemma Pmap_eq {A} (m1 m2 : Pmap A) : m1 = m2 ↔ pmap_car m1 = pmap_car m2.
 Proof.
   split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
-  simplify_eq/=; f_equal; apply proof_irrel.
+  simplify_eq/=; f_equal.
 Qed.
 Global Instance Pmap_eq_dec `{EqDecision A} : EqDecision (Pmap A) := λ m1 m2,
   match Pmap_raw_eq_dec (pmap_car m1) (pmap_car m2) with
   | left H => left (proj2 (Pmap_eq m1 m2) H)
   | right H => right (H ∘ proj1 (Pmap_eq m1 m2))
   end.
-Global Instance Pempty {A} : Empty (Pmap A) := PMap ∅ I.
+
+Global Instance Pempty {A} : Empty (Pmap A) := PMap ∅ stt.
 Global Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
 Global Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i m,
-  let (t,Ht) := m in PMap (partial_alter f i t) (Ppartial_alter_wf f i _ Ht).
+  let (t,Ht) := m in PMap (partial_alter f i t) (is_true_fmap (Ppartial_alter_wf f i _) Ht).
 Global Instance Pfmap : FMap Pmap := λ A B f m,
-  let (t,Ht) := m in PMap (f <$> t) (Pfmap_wf f _ Ht).
+  let (t,Ht) := m in PMap (f <$> t) (is_true_fmap (Pfmap_wf f _) Ht).
 Global Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
   let (t,Ht) := m in Pto_list_raw 1 t [].
 Global Instance Pomap : OMap Pmap := λ A B f m,
-  let (t,Ht) := m in PMap (omap f t) (Pomap_wf f _ Ht).
+  let (t,Ht) := m in PMap (omap f t) (is_true_fmap (Pomap_wf f _) Ht).
 Global Instance Pmerge : Merge Pmap := λ A B C f m1 m2,
-  let (t1,Ht1) := m1 in let (t2,Ht2) := m2 in PMap _ (Pmerge_wf f _ _ Ht1 Ht2).
+  let (t1,Ht1) := m1 in
+  let (t2,Ht2) := m2 in
+  PMap _ (is_true_bind Ht1 (λ Ht1,
+          is_true_bind Ht2 (λ Ht2,
+          is_true_intro $ Pmerge_wf f _ _ Ht1 Ht2))).
 
 Global Instance Pmap_finmap : FinMap positive Pmap.
 Proof.
-  split.
-  - by intros ? [t1 ?] [t2 ?] ?; apply Pmap_eq, Pmap_wf_eq.
+ split.
+  - intros ? [t1 ?] [t2 ?] ?; apply Pmap_eq, Pmap_wf_eq; auto using is_true_elim.
   - by intros ? [].
   - intros ?? [??] ?. by apply Plookup_alter.
   - intros ?? [??] ??. by apply Plookup_alter_ne.

theories/sprop.v

+From Coq Require Export Logic.StrictProp.
+From stdpp Require Import base decidable.
+From stdpp Require Import options.
+
+Definition is_true (b: bool): SProp := if b then sUnit else sEmpty.
+
+Lemma is_true_intro {b: bool} : Is_true b → is_true b.
+Proof.
+  destruct b; simpl; [ constructor | intros [] ].
+Defined.
+
+Lemma is_true_elim {b: bool} : is_true b → Is_true b.
+Proof.
+  destruct b; simpl; [constructor | intros []].
+Defined.
+
+Lemma is_true_fmap {P Q: bool} (lem: P → Q) : is_true P → is_true Q.
+Proof.
+  destruct Q; simpl; [ constructor | ].
+  intros.
+  destruct P; [ | exact H ].
+  exfalso. apply (lem I).
+Defined.
+
+Lemma is_true_bind {P Q: bool} (HP: is_true P) (lem: P → is_true Q) : is_true Q.
+Proof.
+  destruct Q; simpl; [ constructor | ].
+  apply (lem (is_true_elim HP)).
+Defined.
+
+Definition sprop_decide (P: Prop) {dec: Decision P} : SProp :=
+  is_true (bool_decide P).
+
+Lemma sprop_decide_pack (P: Prop) {dec: Decision P} : P → sprop_decide P.
+Proof.
+  intros H.
+  apply is_true_intro; auto using bool_decide_pack.
+Qed.
+Lemma sprop_decide_unpack (P: Prop) {dec: Decision P} : sprop_decide P → P.
+Proof.
+  intros H%is_true_elim.
+  eapply bool_decide_unpack; auto.
+Qed.
+
+(* currently unused; partial progress towards getting coPset to use SProp's Ssig
+rather than sig (with a proof in Prop) *)
+Definition proj1_Ssig {A:Type} {P:A → SProp} (e: Ssig P) : A :=
+  let (a, _) := e in a.
+Definition proj2_Ssig {A:Type} {P:A → SProp} (e: Ssig P) : P (proj1_Ssig e) :=
+  let (_, H) := e in H.
+Lemma Ssig_eq_pi {A:Type} {P:A → SProp}
+      (x y: Ssig P) : x = y ↔ proj1_Ssig x = proj1_Ssig y.
+Proof.
+  split; [intros ->; auto |].
+  destruct x, y; simpl; intros ->; auto.
+Qed.
+(* named after eq_sig_hprop *)
+Lemma eq_Ssig {A:Type} {P:A → SProp}
+      (x y: Ssig P) : proj1_Ssig x = proj1_Ssig y → x = y.
+Proof. apply Ssig_eq_pi. Qed.
+
+Global Instance Ssig_eq_dec {A:Type} {dec: EqDecision A} {P: A → SProp} : EqDecision (Ssig P).
+Proof.
+  intros x y.
+  destruct (decide (proj1_Ssig x = proj1_Ssig y)); [left|right].
+  - apply eq_Ssig; auto.
+  - abstract (intros ->; contradiction).
+Defined.