From 45c14ba9de92566c611280decdc3e8b43694f799 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 30 Aug 2020 09:07:54 +0200
Subject: [PATCH] Definition -> Lemma

---
 theories/base_logic/lib/fancy_updates.v   | 2 +-
 theories/bi/monpred.v                     | 8 ++++----
 theories/program_logic/total_weakestpre.v | 2 +-
 theories/program_logic/weakestpre.v       | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 32aea0268..a98674442 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -12,7 +12,7 @@ Definition uPred_fupd_def `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ
 Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
 Definition uPred_fupd := uPred_fupd_aux.(unseal).
 Arguments uPred_fupd {Σ _}.
-Definition uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
+Lemma uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
 Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
 
 Lemma uPred_fupd_mixin `{!invG Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 14c5d02d0..f6707af9c 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -746,7 +746,7 @@ Next Obligation. solve_proper. Qed.
 Definition monPred_bupd_aux : seal (@monPred_bupd_def). Proof. by eexists. Qed.
 Definition monPred_bupd := monPred_bupd_aux.(unseal).
 Arguments monPred_bupd {_}.
-Definition monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = monPred_bupd_def.
+Lemma monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = monPred_bupd_def.
 Proof. rewrite -monPred_bupd_aux.(seal_eq) //. Qed.
 
 Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
@@ -812,7 +812,7 @@ Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def).
 Proof. by eexists. Qed.
 Definition monPred_internal_eq := monPred_internal_eq_aux.(unseal).
 Arguments monPred_internal_eq {_}.
-Definition monPred_internal_eq_eq `{!BiInternalEq PROP} :
+Lemma monPred_internal_eq_eq `{!BiInternalEq PROP} :
   @internal_eq _ (@monPred_internal_eq _) = monPred_internal_eq_def.
 Proof. rewrite -monPred_internal_eq_aux.(seal_eq) //. Qed.
 
@@ -867,7 +867,7 @@ Next Obligation. solve_proper. Qed.
 Definition monPred_fupd_aux : seal (@monPred_fupd_def). Proof. by eexists. Qed.
 Definition monPred_fupd := monPred_fupd_aux.(unseal).
 Arguments monPred_fupd {_}.
-Definition monPred_fupd_eq `{BiFUpd PROP} : @fupd _ monPred_fupd = monPred_fupd_def.
+Lemma monPred_fupd_eq `{BiFUpd PROP} : @fupd _ monPred_fupd = monPred_fupd_def.
 Proof. rewrite -monPred_fupd_aux.(seal_eq) //. Qed.
 
 Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredI monPred_fupd.
@@ -905,7 +905,7 @@ Definition monPred_plainly_def `{BiPlainly PROP} P : monPred :=
 Definition monPred_plainly_aux : seal (@monPred_plainly_def). Proof. by eexists. Qed.
 Definition monPred_plainly := monPred_plainly_aux.(unseal).
 Arguments monPred_plainly {_}.
-Definition monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = monPred_plainly_def.
+Lemma monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = monPred_plainly_def.
 Proof. rewrite -monPred_plainly_aux.(seal_eq) //. Qed.
 
 Lemma monPred_plainly_mixin `{BiPlainly PROP} : BiPlainlyMixin monPredI monPred_plainly.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index dbba9257b..516043391 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -63,7 +63,7 @@ Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
 Definition twp' := twp_aux.(unseal).
 Arguments twp' {Λ Σ _}.
 Existing Instance twp'.
-Definition twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _.
+Lemma twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _.
 Proof. rewrite -twp_aux.(seal_eq) //. Qed.
 
 Section twp.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 44f06bd7c..8c2cb8f9a 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -50,7 +50,7 @@ Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
 Definition wp' := wp_aux.(unseal).
 Arguments wp' {Λ Σ _}.
 Existing Instance wp'.
-Definition wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _.
+Lemma wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _.
 Proof. rewrite -wp_aux.(seal_eq) //. Qed.
 
 Section wp.
-- 
GitLab