Port `coPset` to use `SProp`.

theories/coPset.v

@@ -68,7 +68,7 @@ Proof.
   assert (r = coPLeaf b) as -> by (apply IHr; try apply (λ p, Ht (p~1)); eauto).
   by destruct b.
 Qed.
-Lemma coPset_eq t1 t2 :
+Lemma coPset_wf_eq t1 t2 :
   (∀ p, e_of p t1 = e_of p t2) → coPset_wf t1 → coPset_wf t2 → t1 = t2.
 Proof.
   revert t2.
@@ -115,15 +115,26 @@ Fixpoint coPset_opp_raw (t : coPset_raw) : coPset_raw :=
   | coPNode b l r => coPNode' (negb b) (coPset_opp_raw l) (coPset_opp_raw r)
   end.
 
-Lemma coPset_singleton_wf p : coPset_wf (coPset_singleton_raw p).
-Proof. induction p; simpl; eauto. Qed.
-Lemma coPset_union_wf t1 t2 : coPset_wf t1 → coPset_wf t2 → coPset_wf (t1 ∪ t2).
-Proof. revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto. Qed.
+Lemma coPset_singleton_wf p : SIs_true (coPset_wf (coPset_singleton_raw p)).
+Proof. apply SIs_true_intro. induction p; simpl; eauto. Qed.
+Lemma coPset_union_wf t1 t2 :
+  SIs_true (coPset_wf t1) → SIs_true (coPset_wf t2) →
+  SIs_true (coPset_wf (t1 ∪ t2)).
+Proof.
+  intros Hwf1%SIs_true_elim Hwf2%SIs_true_elim.
+  apply SIs_true_intro. revert Hwf1 Hwf2.
+  revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto.
+Qed.
 Lemma coPset_intersection_wf t1 t2 :
-  coPset_wf t1 → coPset_wf t2 → coPset_wf (t1 ∩ t2).
-Proof. revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto. Qed.
-Lemma coPset_opp_wf t : coPset_wf (coPset_opp_raw t).
-Proof. induction t as [[]|[]]; simpl; eauto. Qed.
+  SIs_true (coPset_wf t1) → SIs_true (coPset_wf t2) →
+  SIs_true (coPset_wf (t1 ∩ t2)).
+Proof.
+  intros Hwf1%SIs_true_elim Hwf2%SIs_true_elim.
+  apply SIs_true_intro. revert Hwf1 Hwf2.
+  revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto.
+Qed.
+Lemma coPset_opp_wf t : SIs_true (coPset_wf (coPset_opp_raw t)).
+Proof. apply SIs_true_intro. induction t as [[]|[]]; simpl; eauto. Qed.
 Lemma coPset_elem_of_singleton p q : e_of p (coPset_singleton_raw q) ↔ p = q.
 Proof.
   split; [|by intros <-; induction p; simpl; rewrite ?coPset_elem_of_node].
@@ -150,22 +161,38 @@ Proof.
 Qed.
 
 (** * Packed together + set operations *)
-Definition coPset := { t | coPset_wf t }.
+Record coPset := CoPset {
+  coPset_car : coPset_raw;
+  coPset_prf : SIs_true (coPset_wf coPset_car);
+}.
+
+Lemma coPset_eq (X1 X2 : coPset) : X1 = X2 ↔ coPset_car X1 = coPset_car X2.
+Proof.
+  split; [by intros ->|intros].
+  destruct X1 as [t1 ?], X2 as [t2 ?]; by simplify_eq/=.
+Qed.
+Global Instance coPset_eq_dec : EqDecision coPset := λ X1 X2,
+  match coPset_raw_eq_dec (coPset_car X1) (coPset_car X2) with
+  | left H => left (proj2 (coPset_eq X1 X2) H)
+  | right H => right (H ∘ proj1 (coPset_eq X1 X2))
+  end.
 
 Global Instance coPset_singleton : Singleton positive coPset := λ p,
-  coPset_singleton_raw p ↾ coPset_singleton_wf _.
-Global Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
-Global Instance coPset_empty : Empty coPset := coPLeaf false ↾ I.
-Global Instance coPset_top : Top coPset := coPLeaf true ↾ I.
-Global Instance coPset_union : Union coPset := λ X Y,
-  let (t1,Ht1) := X in let (t2,Ht2) := Y in
-  (t1 ∪ t2) ↾ coPset_union_wf _ _ Ht1 Ht2.
-Global Instance coPset_intersection : Intersection coPset := λ X Y,
-  let (t1,Ht1) := X in let (t2,Ht2) := Y in
-  (t1 ∩ t2) ↾ coPset_intersection_wf _ _ Ht1 Ht2.
-Global Instance coPset_difference : Difference coPset := λ X Y,
-  let (t1,Ht1) := X in let (t2,Ht2) := Y in
-  (t1 ∩ coPset_opp_raw t2) ↾ coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _).
+  CoPset (coPset_singleton_raw p) (coPset_singleton_wf _).
+Global Instance coPset_elem_of : ElemOf positive coPset := λ p X,
+  e_of p (coPset_car X).
+Global Instance coPset_empty : Empty coPset := CoPset (coPLeaf false) stt.
+Global Instance coPset_top : Top coPset := CoPset (coPLeaf true) stt.
+Global Instance coPset_union : Union coPset :=
+  λ '(CoPset t1 Ht1) '(CoPset t2 Ht2),
+    CoPset (t1 ∪ t2) (coPset_union_wf _ _ Ht1 Ht2).
+Global Instance coPset_intersection : Intersection coPset :=
+  λ '(CoPset t1 Ht1) '(CoPset t2 Ht2),
+    CoPset (t1 ∩ t2) (coPset_intersection_wf _ _ Ht1 Ht2).
+Global Instance coPset_difference : Difference coPset :=
+  λ '(CoPset t1 Ht1) '(CoPset t2 Ht2),
+    CoPset (t1 ∩ coPset_opp_raw t2)
+           (coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _)).
 
 Global Instance coPset_top_set : TopSet positive coPset.
 Proof.
@@ -189,22 +216,22 @@ Global Hint Resolve coPset_top_subseteq : core.
 Global Instance coPset_leibniz : LeibnizEquiv coPset.
 Proof.
   intros X Y; rewrite set_equiv; intros HXY.
-  apply (sig_eq_pi _), coPset_eq; try apply @proj2_sig.
+  apply coPset_eq, coPset_wf_eq; [|apply SIs_true_elim, coPset_prf..].
   intros p; apply eq_bool_prop_intro, (HXY p).
 Qed.
-
 Global Instance coPset_elem_of_dec : RelDecision (∈@{coPset}).
 Proof. solve_decision. Defined.
 Global Instance coPset_equiv_dec : RelDecision (≡@{coPset}).
-Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
+Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Qed.
 Global Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
 Proof.
- refine (λ X Y, cast_if (decide (X ∩ Y = ∅)));
-  abstract (by rewrite disjoint_intersection_L).
+  refine (λ X Y, cast_if (decide (X ∩ Y = ∅)));
+   abstract (by rewrite disjoint_intersection_L).
 Defined.
 Global Instance mapset_subseteq_dec : RelDecision (⊆@{coPset}).
 Proof.
- refine (λ X Y, cast_if (decide (X ∪ Y = Y))); abstract (by rewrite subseteq_union_L).
+  refine (λ X Y, cast_if (decide (X ∪ Y = Y)));
+    abstract (by rewrite subseteq_union_L).
 Defined.
 
 (** * Finite sets *)
@@ -215,7 +242,7 @@ Fixpoint coPset_finite (t : coPset_raw) : bool :=
 Lemma coPset_finite_node b l r :
   coPset_finite (coPNode' b l r) = coPset_finite l && coPset_finite r.
 Proof. by destruct b, l as [[]|], r as [[]|]. Qed.
-Lemma coPset_finite_spec X : set_finite X ↔ coPset_finite (`X).
+Lemma coPset_finite_spec X : set_finite X ↔ coPset_finite (coPset_car X).
 Proof.
   destruct X as [t Ht].
   unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split.
@@ -234,7 +261,8 @@ Proof.
 Qed.
 Global Instance coPset_finite_dec (X : coPset) : Decision (set_finite X).
 Proof.
-  refine (cast_if (decide (coPset_finite (`X)))); by rewrite coPset_finite_spec.
+  refine (cast_if (decide (coPset_finite (coPset_car X))));
+    by rewrite coPset_finite_spec.
 Defined.
 
 (** * Pick element from infinite sets *)
@@ -252,7 +280,8 @@ Fixpoint coPpick_raw (t : coPset_raw) : option positive :=
      | Some i => Some (i~0) | None => (~1) <$> coPpick_raw r
      end
   end.
-Definition coPpick (X : coPset) : positive := default 1 (coPpick_raw (`X)).
+Definition coPpick (X : coPset) : positive :=
+  default 1 (coPpick_raw (coPset_car X)).
 
 Lemma coPpick_raw_elem_of t i : coPpick_raw t = Some i → e_of i t.
 Proof.
@@ -278,11 +307,15 @@ Fixpoint coPset_to_Pset_raw (t : coPset_raw) : Pmap_raw () :=
   | coPNode false l r => PNode' None (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
   | coPNode true l r => PNode (Some ()) (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
   end.
-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.
+Lemma coPset_to_Pset_wf t :
+  SIs_true (coPset_wf t) → SIs_true (Pmap_wf (coPset_to_Pset_raw t)).
+Proof.
+  intros Hwf%SIs_true_elim. apply SIs_true_intro.
+  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) (SIs_true_intro $ coPset_to_Pset_wf _ Ht)).
+  Mapset (PMap (coPset_to_Pset_raw t) (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].
@@ -298,8 +331,10 @@ Fixpoint Pset_to_coPset_raw (t : Pmap_raw ()) : coPset_raw :=
   | PNode None l r => coPNode false (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
   | PNode (Some _) l r => coPNode true (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
   end.
-Lemma Pset_to_coPset_wf t : Pmap_wf t → coPset_wf (Pset_to_coPset_raw t).
+Lemma Pset_to_coPset_wf t :
+  SIs_true (Pmap_wf t) → SIs_true (coPset_wf (Pset_to_coPset_raw t)).
 Proof.
+  intros Hwf%SIs_true_elim. apply SIs_true_intro. revert Hwf.
   induction t as [|[] l IHl r IHr]; simpl; rewrite ?andb_True; auto.
   - intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto.
   - destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r;
@@ -312,7 +347,7 @@ 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 _ (SIs_true_elim Ht).
+  CoPset (Pset_to_coPset_raw t) (Pset_to_coPset_wf _ 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).
@@ -329,7 +364,7 @@ Definition coPset_to_gset (X : coPset) : gset positive :=
 
 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 _ (SIs_true_elim Ht).
+  CoPset (Pset_to_coPset_raw t) (Pset_to_coPset_wf _ Ht).
 
 Lemma elem_of_coPset_to_gset X i : set_finite X → i ∈ coPset_to_gset X ↔ i ∈ X.
 Proof.
@@ -383,10 +418,10 @@ Fixpoint coPset_suffixes_raw (p : positive) : coPset_raw :=
   | p~0 => coPNode' false (coPset_suffixes_raw p) (coPLeaf false)
   | p~1 => coPNode' false (coPLeaf false) (coPset_suffixes_raw p)
   end.
-Lemma coPset_suffixes_wf p : coPset_wf (coPset_suffixes_raw p).
-Proof. induction p; simpl; eauto. Qed.
+Lemma coPset_suffixes_wf p : SIs_true (coPset_wf (coPset_suffixes_raw p)).
+Proof. apply SIs_true_intro. induction p; simpl; eauto. Qed.
 Definition coPset_suffixes (p : positive) : coPset :=
-  coPset_suffixes_raw p ↾ coPset_suffixes_wf _.
+  CoPset (coPset_suffixes_raw p) (coPset_suffixes_wf _).
 Lemma elem_coPset_suffixes p q : p ∈ coPset_suffixes q ↔ ∃ q', p = q' ++ q.
 Proof.
   unfold elem_of, coPset_elem_of; simpl; split.
@@ -414,14 +449,14 @@ Fixpoint coPset_r_raw (t : coPset_raw) : coPset_raw :=
   | coPNode b l r => coPNode' false (coPset_r_raw l) (coPset_r_raw r)
   end.
 
-Lemma coPset_l_wf t : coPset_wf (coPset_l_raw t).
-Proof. induction t as [[]|]; simpl; auto. Qed.
-Lemma coPset_r_wf t : coPset_wf (coPset_r_raw t).
-Proof. induction t as [[]|]; simpl; auto. Qed.
+Lemma coPset_l_wf t : SIs_true (coPset_wf (coPset_l_raw t)).
+Proof. apply SIs_true_intro. induction t as [[]|]; simpl; auto. Qed.
+Lemma coPset_r_wf t : SIs_true (coPset_wf (coPset_r_raw t)).
+Proof. apply SIs_true_intro.  induction t as [[]|]; simpl; auto. Qed.
 Definition coPset_l (X : coPset) : coPset :=
-  let (t,Ht) := X in coPset_l_raw t ↾ coPset_l_wf _.
+  let (t,Ht) := X in CoPset (coPset_l_raw t) (coPset_l_wf _).
 Definition coPset_r (X : coPset) : coPset :=
-  let (t,Ht) := X in coPset_r_raw t ↾ coPset_r_wf _.
+  let (t,Ht) := X in CoPset (coPset_r_raw t) (coPset_r_wf _).
 
 Lemma coPset_lr_disjoint X : coPset_l X ∩ coPset_r X = ∅.
 Proof.

theories/namespaces.v

@@ -36,7 +36,7 @@ Section namespace.
   Proof. intros N1 x1 N2 x2; rewrite !ndot_eq; naive_solver. Qed.
 
   Lemma nclose_nroot : ↑nroot = (⊤:coPset).
-  Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
+  Proof. by rewrite nclose_eq. Qed.
 
   Lemma nclose_subseteq N x : ↑N.@x ⊆ (↑N : coPset).
   Proof.

theories/pmap.v

@@ -267,7 +267,7 @@ Proof.
 Qed.
 
 (** Packed version and instance of the finite map type class *)
-Inductive Pmap (A : Type) : Type :=
+Record Pmap (A : Type) : Type :=
   PMap { pmap_car : Pmap_raw A; pmap_prf : SIs_true (Pmap_wf pmap_car) }.
 Global Arguments PMap {_} _ _ : assert.
 Global Arguments pmap_car {_} _ : assert.