Commit 4d1ef598 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Clean up basic defs on `stuckness`.

parent 8bccbcc9
...@@ -13,16 +13,14 @@ Notation irisG Λ Σ := (irisG' (state Λ) Σ). ...@@ -13,16 +13,14 @@ Notation irisG Λ Σ := (irisG' (state Λ) Σ).
Inductive stuckness := NotStuck | MaybeStuck. Inductive stuckness := NotStuck | MaybeStuck.
Definition stuckness_le (s1 s2 : stuckness) : bool := Definition stuckness_leb (s1 s2 : stuckness) : bool :=
match s1, s2 with match s1, s2 with
| MaybeStuck, NotStuck => false | MaybeStuck, NotStuck => false
| _, _ => true | _, _ => true
end. end.
Instance: PreOrder stuckness_le. Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
Proof. Instance stuckness_le_po : PreOrder stuckness_le.
split; first by case. move=>s1 s2 s3. by case: s1; case: s2; case: s3. Proof. split; by repeat intros []. Qed.
Qed.
Instance: SqSubsetEq stuckness := stuckness_le.
Definition stuckness_to_atomicity (s : stuckness) : atomicity := Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
if s is MaybeStuck then StronglyAtomic else WeaklyAtomic. if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
...@@ -45,7 +43,7 @@ Proof. ...@@ -45,7 +43,7 @@ Proof.
repeat (f_contractive || f_equiv); apply Hwp. repeat (f_contractive || f_equiv); apply Hwp.
Qed. Qed.
Definition wp_def `{irisG Λ Σ} s : Definition wp_def `{irisG Λ Σ} (s : stuckness) :
coPset expr Λ (val Λ iProp Σ) iProp Σ := fixpoint (wp_pre s). coPset expr Λ (val Λ iProp Σ) iProp Σ := fixpoint (wp_pre s).
Definition wp_aux : seal (@wp_def). by eexists. Qed. Definition wp_aux : seal (@wp_def). by eexists. Qed.
Definition wp := unseal wp_aux. Definition wp := unseal wp_aux.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment