From 81f69ae4942ec93cf53a703b81b55d369cc71702 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sat, 6 Jul 2019 17:58:15 +0200
Subject: [PATCH 1/4] sigT_equiv_proj1: make implicits consistent with
 sigT_dist_proj1

---
 theories/algebra/ofe.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 32275bc2b..8873dac58 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1323,7 +1323,7 @@ Section sigT.
       reflexivity _.
 
   Definition sigT_dist_proj1 n {x y} : x ≡{n}≡ y → projT1 x = projT1 y := proj1_ex.
-  Definition sigT_equiv_proj1 x y : x ≡ y → projT1 x = projT1 y := λ H, proj1_ex (H 0).
+  Definition sigT_equiv_proj1 {x y} : x ≡ y → projT1 x = projT1 y := λ H, proj1_ex (H 0).
 
   Definition sigT_ofe_mixin : OfeMixin (sigT P).
   Proof.
-- 
GitLab


From d19db86ea2f28b3c108776e728fa9cac898caf43 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 7 Jul 2019 01:56:14 +0200
Subject: [PATCH 2/4] Move sigT_equiv_eq_alt earlier (unchanged)

---
 theories/algebra/ofe.v | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 8873dac58..1075bf7e8 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1342,6 +1342,17 @@ Section sigT.
 
   Canonical Structure sigTO : ofeT := OfeT (sigT P) sigT_ofe_mixin.
 
+  Lemma sigT_equiv_eq_alt `{!∀ a b : A, ProofIrrel (a = b)} x1 x2 :
+    x1 ≡ x2 ↔
+    ∃ eq : projT1 x1 = projT1 x2, rew eq in projT2 x1 ≡ projT2 x2.
+  Proof.
+    setoid_rewrite equiv_dist; setoid_rewrite sigT_dist_eq; split => Heq.
+    - move: (Heq 0) => [H0eq1 _].
+      exists H0eq1 => n. move: (Heq n) => [] Hneq1.
+      by rewrite (proof_irrel H0eq1 Hneq1).
+    - move: Heq => [Heq1 Heqn2] n. by exists Heq1.
+  Qed.
+
   (** [existT] is "non-expansive" — general, dependently-typed statement. *)
   Lemma existT_ne n {i1 i2} {v1 : P i1} {v2 : P i2} :
     ∀ (eq : i1 = i2), (rew f_equal P eq in v1 ≡{n}≡ v2) →
@@ -1374,17 +1385,6 @@ Section sigT.
   Lemma sigT_chain_const_proj1 c n : projT1 (c n) = projT1 (c 0).
   Proof. refine (sigT_dist_proj1 _ (chain_cauchy c 0 n _)). lia. Qed.
 
-  Lemma sigT_equiv_eq_alt `{!∀ a b : A, ProofIrrel (a = b)} x1 x2 :
-    x1 ≡ x2 ↔
-    ∃ eq : projT1 x1 = projT1 x2, rew eq in projT2 x1 ≡ projT2 x2.
-  Proof.
-    setoid_rewrite equiv_dist; setoid_rewrite sigT_dist_eq; split => Heq.
-    - move: (Heq 0) => [H0eq1 _].
-      exists H0eq1 => n. move: (Heq n) => [] Hneq1.
-      by rewrite (proof_irrel H0eq1 Hneq1).
-    - move: Heq => [Heq1 Heqn2] n. by exists Heq1.
-  Qed.
-
   (* For this COFE construction we need UIP (Uniqueness of Identity Proofs)
     on [A] (i.e. [∀ x y : A, ProofIrrel (x = y)]. UIP is most commonly obtained
     from decidable equality (by Hedberg’s theorem, see
-- 
GitLab


From 933cadbcbe69140ad6b71baf76f6d9c6f97d2011 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 7 Jul 2019 01:59:09 +0200
Subject: [PATCH 3/4] =?UTF-8?q?sigTO:=20eq=20=E2=86=A6=20Heq?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/algebra/ofe.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 1075bf7e8..32e131a8c 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1301,7 +1301,7 @@ Section sigT.
     on the first component.
   *)
   Instance sigT_dist : Dist (sigT P) := λ n x1 x2,
-    ∃ eq : projT1 x1 = projT1 x2, rew eq in projT2 x1 ≡{n}≡ projT2 x2.
+    ∃ Heq : projT1 x1 = projT1 x2, rew Heq in projT2 x1 ≡{n}≡ projT2 x2.
 
   (**
     Usually we'd give a direct definition, and show it equivalent to
@@ -1319,7 +1319,7 @@ Section sigT.
       reflexivity _.
 
   Definition sigT_dist_eq x1 x2 n : (x1 ≡{n}≡ x2) ↔
-    ∃ eq : projT1 x1 = projT1 x2, (rew eq in projT2 x1) ≡{n}≡ projT2 x2 :=
+    ∃ Heq : projT1 x1 = projT1 x2, (rew Heq in projT2 x1) ≡{n}≡ projT2 x2 :=
       reflexivity _.
 
   Definition sigT_dist_proj1 n {x y} : x ≡{n}≡ y → projT1 x = projT1 y := proj1_ex.
@@ -1344,7 +1344,7 @@ Section sigT.
 
   Lemma sigT_equiv_eq_alt `{!∀ a b : A, ProofIrrel (a = b)} x1 x2 :
     x1 ≡ x2 ↔
-    ∃ eq : projT1 x1 = projT1 x2, rew eq in projT2 x1 ≡ projT2 x2.
+    ∃ Heq : projT1 x1 = projT1 x2, rew Heq in projT2 x1 ≡ projT2 x2.
   Proof.
     setoid_rewrite equiv_dist; setoid_rewrite sigT_dist_eq; split => Heq.
     - move: (Heq 0) => [H0eq1 _].
@@ -1355,14 +1355,14 @@ Section sigT.
 
   (** [existT] is "non-expansive" — general, dependently-typed statement. *)
   Lemma existT_ne n {i1 i2} {v1 : P i1} {v2 : P i2} :
-    ∀ (eq : i1 = i2), (rew f_equal P eq in v1 ≡{n}≡ v2) →
+    ∀ (Heq : i1 = i2), (rew f_equal P Heq in v1 ≡{n}≡ v2) →
       existT i1 v1 ≡{n}≡ existT i2 v2.
   Proof. intros ->; simpl. exists eq_refl => /=. done. Qed.
 
   Lemma existT_proper {i1 i2} {v1 : P i1} {v2 : P i2} :
-    ∀ (eq : i1 = i2), (rew f_equal P eq in v1 ≡ v2) →
+    ∀ (Heq : i1 = i2), (rew f_equal P Heq in v1 ≡ v2) →
       existT i1 v1 ≡ existT i2 v2.
-  Proof. intros eq Heq n. apply (existT_ne n eq), equiv_dist, Heq. Qed.
+  Proof. intros Heq Heqv n. apply (existT_ne n Heq), equiv_dist, Heqv. Qed.
 
   (** [existT] is "non-expansive" — non-dependently-typed version. *)
   Global Instance existT_ne_2 a : NonExpansive (@existT A P a).
-- 
GitLab


From 5be0feac715e0e5f5db406c9825dbfd517474fdd Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 7 Jul 2019 02:00:28 +0200
Subject: [PATCH 4/4] projT1, projT2: add instance/lemmas for NonExpansive and
 Proper.

---
 theories/algebra/ofe.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 32e131a8c..ffaa9239f 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1353,6 +1353,26 @@ Section sigT.
     - move: Heq => [Heq1 Heqn2] n. by exists Heq1.
   Qed.
 
+  (** [projT1] is non-expansive and proper. *)
+  Global Instance projT1_ne : NonExpansive (projT1 : sigTO → leibnizO A).
+  Proof. solve_proper. Qed.
+
+  Global Instance projT1_proper : Proper ((≡) ==> (≡)) (projT1 : sigTO → leibnizO A).
+  Proof. apply ne_proper, projT1_ne. Qed.
+
+  (** [projT2] is "non-expansive"; the properness lemma [projT2_ne] requires UIP. *)
+  Lemma projT2_ne n (x1 x2 : sigTO) (Heq : x1 ≡{n}≡ x2) :
+    rew (sigT_dist_proj1 n Heq) in projT2 x1 ≡{n}≡ projT2 x2.
+  Proof. by destruct Heq. Qed.
+
+  Lemma projT2_proper `{!∀ a b : A, ProofIrrel (a = b)} (x1 x2 : sigTO) (Heqs : x1 ≡ x2):
+    rew (sigT_equiv_proj1 Heqs) in projT2 x1 ≡ projT2 x2.
+  Proof.
+    move: x1 x2 Heqs => [a1 x1] [a2 x2] Heqs.
+    case: (proj1 (sigT_equiv_eq_alt _ _) Heqs) => /=. intros ->.
+    rewrite (proof_irrel (sigT_equiv_proj1 Heqs) eq_refl) /=. done.
+  Qed.
+
   (** [existT] is "non-expansive" — general, dependently-typed statement. *)
   Lemma existT_ne n {i1 i2} {v1 : P i1} {v2 : P i2} :
     ∀ (Heq : i1 = i2), (rew f_equal P Heq in v1 ≡{n}≡ v2) →
-- 
GitLab