Refactor.

1. Improve naming
2. Make `wf_` proofs of `gmap` and `pmap` opaque
3. Avoid `bind` and `fmap` combinators for `SProp`
4. Drop `simpl` tests

Items 2-3 are crucial for performance, otherwise each operation checks if the map
is still well-formed, which destroys log(n) complexity of map operations.

Why 3 is needed is subtle: The `bind` and `fmap` lemmas for `SProp` contain Booleans
as implicit arguments, which are eagerly evaluated by `vm_compute`.

As a result of 2-3, `simpl` will not normalize proofs to `stt`, and `simpl` tests
do not give a desirable result.

tests/gmap.ref

@@ -77,4 +77,4 @@ Failed to progress.
 1 goal
   
   ============================
-  Some true = Some true
+  {[3 := false; 2 := true]} !! 2 = Some true

tests/gmap.v

@@ -69,42 +69,79 @@ Proof.
   reflexivity.
 Qed.
 
-Theorem gmap_insert_comm :
-  <[3:=false]> {[2:=true]} =@{gmap nat bool} <[2:=true]> {[3:=false]}.
-Proof.
-  simpl. Show.
-  reflexivity.
-Qed.
+Definition pmap_insert_positives (n : positive) : Pmap unit :=
+  Pos.iter (λ rec p m,
+    rec (p + 1)%positive (<[p:=tt]> m)) (λ _ m, m) n 1%positive ∅.
+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).
+
+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.
+Time Eval vm_compute in pmap_insert_positives_test 8000.
+Time Eval vm_compute in pmap_insert_positives_test 16000.
+Time Eval vm_compute in pmap_insert_positives_test 32000.
+Time Eval vm_compute in pmap_insert_positives_test 64000.
+Time Eval vm_compute in pmap_insert_positives_test 128000.
+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.
+*)
+
+Definition gmap_insert_positives (n : positive) : gmap positive unit :=
+  Pos.iter (λ rec p m,
+    rec (p + 1)%positive (<[p:=tt]> m)) (λ _ m, m) n 1%positive ∅.
+Definition gmap_insert_positives_rev (n : positive) : gmap positive unit :=
+  Pos.iter (λ rec p m,
+    rec (p - 1)%positive (<[p:=tt]> m)) (λ _ m, m) n n ∅.
+
+(* Test that the time increases linearly *)
+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.
+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.
+Time Eval vm_compute in gmap_insert_positives_test 8000.
+Time Eval vm_compute in gmap_insert_positives_test 16000.
+Time Eval vm_compute in gmap_insert_positives_test 32000.
+Time Eval vm_compute in gmap_insert_positives_test 64000.
+Time Eval vm_compute in gmap_insert_positives_test 128000.
+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.
+*)
 
-Transparent gmap_empty.
-Arguments map_insert _ _ _ / _ _ _ _ : assert.
-Arguments Plookup _ _ _ / : assert.
+Theorem gmap_insert_comm :
+  {[ 3:=false; 2:=true]} =@{gmap nat bool} {[ 2:=true; 3:=false ]}.
+Proof. simpl. Show. reflexivity. Qed.
 
 Theorem gmap_lookup_concrete :
-  lookup (M:=gmap nat bool) 2 (<[3:=false]> {[2:=true]}) = Some true.
+  lookup (M:=gmap nat bool) 2 {[ 3:=false; 2:=true ]} = Some true.
 Proof. simpl. Show. reflexivity. Qed.
 
-Fixpoint insert_l (m:gmap Z unit) (l: list Z) : gmap Z unit :=
-  match l with
-  | [] => m
-  | p::l => <[p:=tt]> (insert_l m l)
-  end.
-
-Fixpoint n_positives (n:nat) (p:Z) : list Z :=
-  match n with
-  | 0 => []
-  | S n => p :: n_positives n (1 + p)%Z
-  end.
-
-Fixpoint n_positives_rev (n:nat) (p:Z) : list Z :=
-  match n with
-  | 0 => []
-  | S n => p :: n_positives_rev n (p - 1)%Z
-  end.
-
-Theorem gmap_lookup_insert_fwd_rev :
-  insert_l ∅ (n_positives 500 1) = insert_l ∅ (n_positives_rev 500 500).
-Proof.
-  cbn [n_positives n_positives_rev Z.add Z.pos_sub Pos.add Pos.succ].
-  Time reflexivity.
-Qed.
+Theorem gmap_insert_positives_reflexivity_500 :
+  gmap_insert_positives 500 = gmap_insert_positives_rev 500.
+Proof. reflexivity. Qed.
+Theorem gmap_insert_positives_reflexivity_1000 :
+  gmap_insert_positives 1000 = gmap_insert_positives_rev 1000.
+Proof. (* this should take about a second *) reflexivity. Qed.
+
+Theorem gmap_insert_positives_union_reflexivity_500 :
+  (gmap_insert_positives_rev 400) ∪
+    (gmap_insert_positives 500 ∖ gmap_insert_positives_rev 400)
+  = gmap_insert_positives 500.
+Proof. reflexivity. Qed.
+Theorem gmap_insert_positives_union_reflexivity_1000 :
+  (gmap_insert_positives_rev 800) ∪
+    (gmap_insert_positives 1000 ∖ gmap_insert_positives_rev 800)
+  = gmap_insert_positives 1000.
+Proof. reflexivity. Qed.

theories/coPset.v

@@ -281,7 +281,8 @@ 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) (is_true_intro $ coPset_to_Pset_wf _ Ht)).
+  let (t,Ht) := X in
+  Mapset (PMap (coPset_to_Pset_raw t) (SIs_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 +311,8 @@ 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 _ (is_true_elim Ht).
+  let 'Mapset (PMap t Ht) := X in
+  Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ (SIs_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 +322,14 @@ Qed.
 
 (** * Conversion to and from gsets of positives *)
 Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf positive m.
-Proof. unfold gmap_wf. apply is_true_intro. by rewrite bool_decide_spec. Qed.
+Proof. unfold gmap_wf. apply SIs_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 _ (is_true_elim Ht).
+  let 'Mapset (GMap (PMap t Ht) _) := X in
+  Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ (SIs_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

@@ -54,8 +54,8 @@ 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; apply is_true_fmap; rewrite !bool_decide_spec.
-  intros Hm p x. destruct (decide (encode i = p)) as [<-|?].
+  intros Hm%sprop_decide_unpack. apply sprop_decide_pack.
+  intros p x. destruct (decide (encode i = p)) as [<-|?].
   - rewrite decode_encode; eauto.
   - rewrite lookup_partial_alter_ne by done. by apply Hm.
 Qed.
@@ -67,16 +67,16 @@ 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; apply is_true_fmap; rewrite !bool_decide_spec.
-  intros ? p x. rewrite lookup_fmap, fmap_Some; intros (?&?&?); eauto.
+  intros Hm%sprop_decide_unpack. apply sprop_decide_pack.
+  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),
   GMap (f <$> m) (gmap_fmap_wf f 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; apply is_true_fmap; rewrite !bool_decide_spec.
-  intros ? p x; rewrite lookup_omap, bind_Some; intros (?&?&?); eauto.
+  intros Hm%sprop_decide_unpack. apply sprop_decide_pack.
+  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),
   GMap (omap f m) (gmap_omap_wf f m Hm).
@@ -84,11 +84,8 @@ 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.
-  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.
+  intros Hm1%sprop_decide_unpack Hm2%sprop_decide_unpack. apply sprop_decide_pack.
+  intros p z. rewrite lookup_merge by done.
   destruct (m1 !! _) eqn:?, (m2 !! _) eqn:?; naive_solver.
 Qed.
 Global Instance gmap_merge `{Countable K} : Merge (gmap K) :=

theories/pmap.v

@@ -127,24 +127,36 @@ Lemma PNode_lookup {A} o (l r : Pmap_raw A) i :
   PNode' o l r !! i = PNode o l r !! i.
 Proof. by destruct i, o, l, r. Qed.
 
-Lemma Psingleton_wf {A} i (x : A) : Pmap_wf (Psingleton_raw i x).
+Local Lemma Psingleton_wf' {A} i (x : A) : Pmap_wf (Psingleton_raw i x).
 Proof. induction i as [[]|[]|]; simpl; rewrite ?andb_true_r; auto. Qed.
-Lemma Ppartial_alter_wf {A} f i (t : Pmap_raw A) :
-  Pmap_wf t → Pmap_wf (Ppartial_alter_raw f i t).
+Local Lemma Ppartial_alter_wf {A} f i (t : Pmap_raw A) :
+  SIs_true (Pmap_wf t) → SIs_true (Pmap_wf (Ppartial_alter_raw f i t)).
 Proof.
+  intros Hwf%SIs_true_elim. apply SIs_true_intro. revert Hwf.
   revert i; induction t as [|o l IHl r IHr]; intros i ?; simpl.
-  - destruct (f None); auto using Psingleton_wf.
+  - destruct (f None); auto using Psingleton_wf'.
   - destruct i; simpl; eauto.
 Qed.
-Lemma Pfmap_wf {A B} (f : A → B) t : Pmap_wf t → Pmap_wf (Pfmap_raw f t).
+Local Lemma Pfmap_wf {A B} (f : A → B) t :
+  SIs_true (Pmap_wf t) → SIs_true (Pmap_wf (Pfmap_raw f t)).
 Proof.
+  intros Hwf%SIs_true_elim. apply SIs_true_intro. revert Hwf.
   induction t as [|[x|] [] ? [] ?]; simpl in *; rewrite ?andb_True; intuition.
 Qed.
-Lemma Pomap_wf {A B} (f : A → option B) t : Pmap_wf t → Pmap_wf (Pomap_raw f t).
+Local Lemma Pomap_wf' {A B} (f : A → option B) t :
+  Pmap_wf t → Pmap_wf (Pomap_raw f t).
 Proof. induction t; simpl; eauto. Qed.
-Lemma Pmerge_wf {A B C} (f : option A → option B → option C) t1 t2 :
-  Pmap_wf t1 → Pmap_wf t2 → Pmap_wf (Pmerge_raw f t1 t2).
-Proof. revert t2. induction t1; intros []; simpl; eauto using Pomap_wf. Qed.
+Local Lemma Pomap_wf {A B} (f : A → option B) t :
+  SIs_true (Pmap_wf t) → SIs_true (Pmap_wf (Pomap_raw f t)).
+Proof. intros. by apply SIs_true_intro, Pomap_wf', SIs_true_elim. Qed.
+Local Lemma Pmerge_wf {A B C} (f : option A → option B → option C) t1 t2 :
+  SIs_true (Pmap_wf t1) → SIs_true (Pmap_wf t2) →
+  SIs_true (Pmap_wf (Pmerge_raw f t1 t2)).
+Proof.
+  intros Hwf1%SIs_true_elim Hwf2%SIs_true_elim.
+  apply SIs_true_intro. revert Hwf1 Hwf2.
+  revert t2. induction t1; intros []; simpl; eauto using Pomap_wf'.
+Qed.
 
 Lemma Plookup_empty {A} i : (∅ : Pmap_raw A) !! i = None.
 Proof. by destruct i. Qed.
@@ -256,7 +268,7 @@ Qed.
 
 (** Packed version and instance of the finite map type class *)
 Inductive Pmap (A : Type) : Type :=
-  PMap { pmap_car : Pmap_raw A; pmap_prf : is_true (Pmap_wf pmap_car) }.
+  PMap { pmap_car : Pmap_raw A; pmap_prf : SIs_true (Pmap_wf pmap_car) }.
 Global Arguments PMap {_} _ _ : assert.
 Global Arguments pmap_car {_} _ : assert.
 Global Arguments pmap_prf {_} _ : assert.
@@ -274,25 +286,23 @@ Global Instance Pmap_eq_dec `{EqDecision A} : EqDecision (Pmap A) := λ m1 m2,
 
 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) (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) (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) (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 _ (is_true_bind Ht1 (λ Ht1,
-          is_true_bind Ht2 (λ Ht2,
-          is_true_intro $ Pmerge_wf f _ _ Ht1 Ht2))).
+Global Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) :=
+  λ f i '(PMap t Ht),
+    PMap (partial_alter f i t) (Ppartial_alter_wf f i _ Ht).
+Global Instance Pfmap : FMap Pmap := λ A B f '(PMap t Ht),
+  PMap (f <$> t) (Pfmap_wf f _ Ht).
+Global Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ '(PMap t Ht),
+  Pto_list_raw 1 t [].
+Global Instance Pomap : OMap Pmap := λ A B f '(PMap t Ht),
+  PMap (omap f t) (Pomap_wf f _ Ht).
+Global Instance Pmerge : Merge Pmap := λ A B C f '(PMap t1 Ht1) '(PMap t2 Ht2),
+  PMap _ (Pmerge_wf f _ _ Ht1 Ht2).
 
 Global Instance Pmap_finmap : FinMap positive Pmap.
 Proof.
  split.
-  - intros ? [t1 ?] [t2 ?] ?; apply Pmap_eq, Pmap_wf_eq; auto using is_true_elim.
+  - intros ? [t1 ?] [t2 ?] ?.
+    apply Pmap_eq, Pmap_wf_eq; auto using SIs_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 decidable.
 From stdpp Require Import options.
 
-Definition is_true (b: bool): SProp := if b then sUnit else sEmpty.
+Definition SIs_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 SIs_true_intro {b: bool} : Is_true b → SIs_true b.
+Proof. destruct b; [constructor | intros []]. Qed.
+Lemma SIs_true_elim {b: bool} : SIs_true b → Is_true b.
+Proof. destruct b; simpl; [constructor | intros []]. Qed.
 
-Lemma is_true_elim {b: bool} : is_true b → Is_true b.
-Proof.
-  destruct b; simpl; [constructor | intros []].
-Defined.
+Definition sprop_decide (P : Prop) `{!Decision P} : SProp :=
+  SIs_true (bool_decide P).
 
-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.
+Lemma sprop_decide_pack (P : Prop) `{!Decision P} : P → sprop_decide P.
+Proof. intros HP. apply SIs_true_intro, bool_decide_pack, HP. Qed.
+Lemma sprop_decide_unpack (P : Prop) `{!Decision P} : sprop_decide P → P.
+Proof. intros HP. apply (bool_decide_unpack P), SIs_true_elim, HP. Qed.