From 25c5e64debdb9fe4f4da85c220efb5571389e9c5 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Mon, 24 Jun 2019 19:38:21 +0200
Subject: [PATCH] Prove sigT_equivI is admissible (fix #250)

---
 theories/algebra/ofe.v         |  2 --
 theories/bi/derived_laws_sbi.v | 19 +++++++++++++++++++
 2 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index cfe0d6106..923fa2097 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1359,8 +1359,6 @@ Section sigT.
 
   Global Instance existT_proper_2 a : Proper ((≡) ==> (≡)) (@existT A P a).
   Proof. apply ne_proper, _. Qed.
-  (* XXX Which do you prefer? *)
-  (* Proof. move => ?? Heq. apply (existT_proper eq_refl Heq). Qed. *)
 
   Implicit Types (c : chain sigTO).
 
diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index a9883b41d..fe60dc3a7 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -84,6 +84,25 @@ Qed.
 Lemma sig_equivI {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
 Proof. apply (anti_symm _). apply sig_eq. apply f_equiv, _. Qed.
 
+Section sigT_equivI.
+Import EqNotations.
+
+Lemma sigT_equivI {A : Type} {P : A → ofeT} (x y : sigT P) :
+  x ≡ y ⊣⊢
+  ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y.
+Proof.
+  apply (anti_symm _).
+  - apply (internal_eq_rewrite' x y (λ y,
+             ∃ eq : projT1 x = projT1 y,
+               rew eq in projT2 x ≡ projT2 y))%I;
+        [| done | exact: (exist_intro' _ _ eq_refl) ].
+    move => n [a pa] [b pb] [/=]; intros -> => /= Hab.
+    apply exist_ne => ?. by rewrite Hab.
+  - apply exist_elim. move: x y => [a pa] [b pb] /=. intros ->; simpl.
+    apply f_equiv, _.
+Qed.
+End sigT_equivI.
+
 Lemma discrete_fun_equivI {A} {B : A → ofeT} (f g : discrete_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof.
   apply (anti_symm _); auto using fun_ext.
-- 
GitLab