From 4d1ef598b7b1d18cc99e00a09d037c4f61a3e318 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 10 Jan 2018 15:57:49 -0800
Subject: [PATCH] Clean up basic defs on `stuckness`.

---
 theories/program_logic/weakestpre.v | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index e081ea449..06f590342 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -13,16 +13,14 @@ Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 
 Inductive stuckness := NotStuck | MaybeStuck.
 
-Definition stuckness_le (s1 s2 : stuckness) : bool :=
+Definition stuckness_leb (s1 s2 : stuckness) : bool :=
   match s1, s2 with
   | MaybeStuck, NotStuck => false
   | _, _ => true
   end.
-Instance: PreOrder stuckness_le.
-Proof.
-  split; first by case. move=>s1 s2 s3. by case: s1; case: s2; case: s3.
-Qed.
-Instance: SqSubsetEq stuckness := stuckness_le.
+Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
+Instance stuckness_le_po : PreOrder stuckness_le.
+Proof. split; by repeat intros []. Qed.
 
 Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
   if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
@@ -45,7 +43,7 @@ Proof.
   repeat (f_contractive || f_equiv); apply Hwp.
 Qed.
 
-Definition wp_def `{irisG Λ Σ} s :
+Definition wp_def `{irisG Λ Σ} (s : stuckness) :
   coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s).
 Definition wp_aux : seal (@wp_def). by eexists. Qed.
 Definition wp := unseal wp_aux.
-- 
GitLab