From 19d9973e101fe9e8844671145e35bd9aae8b447b Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Tue, 28 Nov 2017 15:58:58 +0100
Subject: [PATCH] Prove `funbi_ofe` using `iso_ofe`.

---
 theories/bi/monfun.v | 31 ++++++++++++++++++++-----------
 1 file changed, 20 insertions(+), 11 deletions(-)

diff --git a/theories/bi/monfun.v b/theories/bi/monfun.v
index c9afd7084..6c7fb1af1 100644
--- a/theories/bi/monfun.v
+++ b/theories/bi/monfun.v
@@ -38,19 +38,28 @@ Proof.
   by rewrite {1}/dist /= /funbi_dist /=.
 Qed.
 
+Definition funbi_sig {I B} (P : funbi_ty I B):
+  sig (fun f : I -c> B => mono (bi_index_rel I) f) :=
+  exist _ (funbi_car P) (funbi_mono P).
+Definition sig_funbi {I : bi_index} {B : bi}
+           (P : sig (fun f : I -c> B => mono (bi_index_rel I) f)):
+  funbi_ty I B :=
+  FUN (proj1_sig P) (proj2_sig P).
+
+Lemma funbi_sig_equiv {I B}:
+  ∀ P Q : funbi_ty I B, P ≡ Q ↔ funbi_sig P ≡ funbi_sig Q.
+Proof. done. Qed.
+
+Lemma funbi_sig_dist {I B}:
+  ∀ n, ∀ P Q : funbi_ty I B, P ≡{n}≡ Q ↔ funbi_sig P ≡{n}≡ funbi_sig Q.
+Proof. done. Qed.
+
+Lemma funbi_sig_cancel {I B}:
+  ∀ P, @funbi_sig I B (sig_funbi P) ≡ P.
+Proof. intros [f M]. reflexivity. Qed.
 
 Definition funbi_ofe_mixin I B : OfeMixin (funbi_ty I B).
-Proof.
-  split.
-  - intros.
-    apply (mixin_equiv_dist _ ofe_fun_ofe_mixin).
-  - intros.
-    split.
-    + apply (mixin_dist_equivalence _ ofe_fun_ofe_mixin).
-    + repeat intro. by eapply (Equivalence_Symmetric).
-    + intros x y z H1 H2 ?. by eapply (Equivalence_Transitive), H2.
-  - intros. by apply (mixin_dist_S _ ofe_fun_ofe_mixin).
-Defined.
+Proof. by apply (iso_ofe_mixin funbi_sig funbi_sig_equiv funbi_sig_dist). Qed.
 
 Canonical Structure funbi_ofe I B := OfeT (funbi_ty I B) (funbi_ofe_mixin I B).
 
-- 
GitLab