From 52d7d27542914b2f89e88c6b440ea48d71755f66 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Feb 2016 00:39:33 +0100
Subject: [PATCH] Tweak sealing stuff.

* Use sig instead of sigT: the proof is a Prop after all
* Tweak implicit arguments
* Shorten proof of sigma
---
 heap_lang/heap.v           |  9 ++++-----
 program_logic/auth.v       |  8 +++-----
 program_logic/saved_prop.v | 10 +++++-----
 program_logic/sts.v        | 24 ++++++++++--------------
 4 files changed, 22 insertions(+), 29 deletions(-)

diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 2bf1994a9..d31ec3f44 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -25,11 +25,10 @@ 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 *)
-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_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
+Definition heap_mapsto {Σ h} := proj1_sig heap_mapsto_aux Σ h.
+Definition heap_mapsto_eq :
+  @heap_mapsto = @heap_mapsto_def := proj2_sig heap_mapsto_aux.
 
 Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
   ownP (of_heap h).
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 90d5d6e45..15f435ff5 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -16,11 +16,9 @@ Proof. split; try apply _. apply: inGF_inG. Qed.
 Definition auth_own_def `{authG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
   own γ (◯ a).
 (* Perform sealing *)
-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 {_ _ _ _ _} _ _.
+Definition auth_own_aux : { x | x = @auth_own_def }. by eexists. Qed.
+Definition auth_own {Λ Σ A Ae a} := proj1_sig auth_own_aux Λ Σ A Ae a.
+Definition auth_own_eq : @auth_own = @auth_own_def := proj2_sig auth_own_aux.
 
 Definition auth_inv `{authG Λ Σ A}
     (γ : gname) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 56f63df96..b7254b591 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -12,11 +12,11 @@ Definition saved_prop_own_def `{savedPropG Λ Σ}
     (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
   own γ (to_agree (Next (iProp_unfold P))).
 (* 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 {_ _ _} _ _.
+Definition saved_prop_own_aux : { x | x = @saved_prop_own_def }. by eexists. Qed.
+Definition saved_prop_own {Λ Σ s} := proj1_sig saved_prop_own_aux Λ Σ s.
+Definition saved_prop_own_eq :
+  @saved_prop_own = @saved_prop_own_def := proj2_sig saved_prop_own_aux.
+
 Instance: Params (@saved_prop_own) 4.
 
 Section saved_prop.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index edc2938d4..8c9480ab5 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -14,30 +14,26 @@ Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
 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 Λ Σ:=
+    (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_ownS_aux : { x | x = @sts_ownS_def }. by eexists. Qed.
+Definition sts_ownS {Λ Σ sts i} := proj1_sig sts_ownS_aux Λ Σ sts i.
+Definition sts_ownS_eq : @sts_ownS = @sts_ownS_def := proj2_sig sts_ownS_aux.
 
 Definition sts_own_def `{i : stsG Λ Σ sts} (γ : gname)
-           (s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
+    (s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
   own γ (sts_frag_up s T).
 (* Perform sealing. *)
-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_own_aux : { x | x = @sts_own_def }. by eexists. Qed.
+Definition sts_own {Λ Σ sts i} := proj1_sig sts_own_aux Λ Σ sts i.
+Definition sts_own_eq : @sts_own = @sts_own_def := proj2_sig sts_own_aux.
 
 Definition sts_inv `{i : stsG Λ Σ sts} (γ : gname)
-           (φ : sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
+    (φ : sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
   (∃ s, own γ (sts_auth s ∅) ★ φ s)%I.
 Definition sts_ctx `{i : stsG Λ Σ sts} (γ : gname)
-           (N : namespace) (φ: sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
+    (N : namespace) (φ: sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
   inv N (sts_inv γ φ).
 
 Instance: Params (@sts_inv) 5.
-- 
GitLab