make sealing less heavy by using Qed and Sigma types rather than modules

heap_lang/heap.v

@@ -25,14 +25,11 @@ matching it against other forms of ownership. *)
 Definition heap_mapsto_def `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
   auth_own heap_name {[ l := Excl v ]}.
 (* Perform sealing *)
-Module Type HeapMapstoSig.
-  Parameter heap_mapsto : ∀ `{heapG Σ} (l : loc) (v: val), iPropG heap_lang Σ.
-  Axiom heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def.
-End HeapMapstoSig.
-Module Export HeapMapsto : HeapMapstoSig.
-  Definition heap_mapsto := @heap_mapsto_def.
-  Definition heap_mapsto_eq := Logic.eq_refl (@heap_mapsto).
-End HeapMapsto. 
+Definition heap_mapsto_aux : { x : _ & x = @heap_mapsto_def }.
+  exact (existT _ Logic.eq_refl). Qed.
+Definition heap_mapsto := projT1 heap_mapsto_aux.
+Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def := projT2 heap_mapsto_aux.
+Arguments heap_mapsto {_ _} _ _.
 
 Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
   ownP (of_heap h).

program_logic/auth.v

@@ -17,14 +17,11 @@ Proof. split; try apply _. apply: inGF_inG. Qed.
 Definition auth_own_def `{authG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
   own γ (◯ a).
 (* Perform sealing *)
-Module Type AuthOwnSig.
-  Parameter auth_own : ∀ `{authG Λ Σ A} (γ : gname) (a : A), iPropG Λ Σ.
-  Axiom auth_own_eq : @auth_own = @auth_own_def.
-End AuthOwnSig.
-Module Export AuthOwn : AuthOwnSig.
-  Definition auth_own := @auth_own_def.
-  Definition auth_own_eq := Logic.eq_refl (@auth_own).
-End AuthOwn. 
+Definition auth_own_aux : { x : _ & x = @auth_own_def }.
+  exact (existT _ Logic.eq_refl). Qed.
+Definition auth_own := projT1 auth_own_aux.
+Definition auth_own_eq : @auth_own = @auth_own_def := projT2 auth_own_aux.
+Arguments auth_own {_ _ _ _ _} _ _.
 
 (* TODO: Once we switched to RAs, it is no longer necessary to remember that a
      is constantly valid. *)

program_logic/saved_prop.v

@@ -11,16 +11,12 @@ Proof. apply: inGF_inG. Qed.
 Definition saved_prop_own_def `{savedPropG Λ Σ}
     (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
   own γ (to_agree (Next (iProp_unfold P))).
-(* Perform sealing. *)
-Module Type SavedPropOwnSig.
-  Parameter saved_prop_own : ∀ `{savedPropG Λ Σ} (γ : gname) (P : iPropG Λ Σ),
-    iPropG Λ Σ.
-  Axiom saved_prop_own_eq : @saved_prop_own = @saved_prop_own_def.
-End SavedPropOwnSig.
-Module Export SavedPropOwn : SavedPropOwnSig.
-  Definition saved_prop_own := @saved_prop_own_def.
-  Definition saved_prop_own_eq := Logic.eq_refl (@saved_prop_own).
-End SavedPropOwn. 
+(* Perform sealing *)
+Definition saved_prop_own_aux : { x : _ & x = @saved_prop_own_def }.
+  exact (existT _ Logic.eq_refl). Qed.
+Definition saved_prop_own := projT1 saved_prop_own_aux.
+Definition saved_prop_own_eq : @saved_prop_own = @saved_prop_own_def := projT2 saved_prop_own_aux.
+Arguments saved_prop_own {_ _ _} _ _.
 Instance: Params (@saved_prop_own) 4.
 
 Section saved_prop.

program_logic/sts.v

@@ -16,24 +16,22 @@ Proof. split; try apply _. apply: inGF_inG. Qed.
 Definition sts_ownS_def `{i : stsG Λ Σ sts} (γ : gname)
            (S : sts.states sts) (T : sts.tokens sts) : iPropG Λ Σ:=
   own γ (sts_frag S T).
+(* Perform sealing. *)
+Definition sts_ownS_aux : { x : _ & x = @sts_ownS_def }.
+  exact (existT _ Logic.eq_refl). Qed.
+Definition sts_ownS := projT1 sts_ownS_aux.
+Definition sts_ownS_eq : @sts_ownS = @sts_ownS_def := projT2 sts_ownS_aux.
+Arguments sts_ownS {_ _ _ _} _ _ _.
+
 Definition sts_own_def `{i : stsG Λ Σ sts} (γ : gname)
            (s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
   own γ (sts_frag_up s T).
 (* Perform sealing. *)
-Module Type StsOwnSig.
-  Parameter sts_ownS : ∀ `{i : stsG Λ Σ sts} (γ : gname)
-           (S : sts.states sts) (T : sts.tokens sts), iPropG Λ Σ.
-  Parameter sts_own : ∀ `{i : stsG Λ Σ sts} (γ : gname)
-           (s : sts.state sts) (T : sts.tokens sts), iPropG Λ Σ.
-  Axiom sts_ownS_eq : @sts_ownS = @sts_ownS_def.
-  Axiom sts_own_eq : @sts_own = @sts_own_def.
-End StsOwnSig.
-Module Export StsOwn : StsOwnSig.
-  Definition sts_ownS := @sts_ownS_def.
-  Definition sts_own := @sts_own_def.
-  Definition sts_ownS_eq := Logic.eq_refl (@sts_ownS_def).
-  Definition sts_own_eq := Logic.eq_refl (@sts_own_def).
-End StsOwn. 
+Definition sts_own_aux : { x : _ & x = @sts_own_def }.
+  exact (existT _ Logic.eq_refl). Qed.
+Definition sts_own := projT1 sts_own_aux.
+Definition sts_own_eq : @sts_own = @sts_own_def := projT2 sts_own_aux.
+Arguments sts_own {_ _ _ _} _ _ _.
 
 Definition sts_inv `{i : stsG Λ Σ sts} (γ : gname)
            (φ : sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=