From 064690ea744ed2c5798c5bdc60201879e3c97b01 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 7 Oct 2020 14:41:57 +0200
Subject: [PATCH] =?UTF-8?q?add=20iff=20lemma=20for=20'=E2=9C=93=20(to=5Fag?=
 =?UTF-8?q?ree=20a=20=E2=8B=85=20to=5Fagree=20b)'?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/algebra/agree.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 7ace47cea..ac7a14d3e 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -244,6 +244,19 @@ Proof. by intros ?%agree_op_inv%(inj to_agree). Qed.
 Lemma to_agree_op_inv_L `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) → a = b.
 Proof. by intros ?%to_agree_op_inv%leibniz_equiv. Qed.
 
+Lemma to_agree_op_validN a b n : ✓{n} (to_agree a ⋅ to_agree b) ↔ a ≡{n}≡ b.
+Proof.
+  split; first by apply to_agree_op_invN.
+  intros ->. rewrite agree_idemp //.
+Qed.
+Lemma to_agree_op_valid a b : ✓ (to_agree a ⋅ to_agree b) ↔ a ≡ b.
+Proof.
+  split; first by apply to_agree_op_inv.
+  intros ->. rewrite agree_idemp //.
+Qed.
+Lemma to_agree_op_valid_L `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) ↔ a = b.
+Proof. rewrite to_agree_op_valid. by fold_leibniz. Qed.
+
 (** Internalized properties *)
 Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢@{uPredI M} (a ≡ b).
 Proof.
-- 
GitLab