Commit af27e338 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use a type class for monotone uPred predicates.

parent e393429d
...@@ -5,9 +5,9 @@ Import uPred. ...@@ -5,9 +5,9 @@ Import uPred.
(** Least and greatest fixpoint of a monotone function, defined entirely inside (** Least and greatest fixpoint of a monotone function, defined entirely inside
the logic. *) the logic. *)
Class BIMonoPred {M A} (F : (A uPred M) (A uPred M)) :=
Definition uPred_mono_pred {M A} (F : (A uPred M) (A uPred M)) := bi_mono_pred Φ Ψ : (( x, Φ x - Ψ x) x, F Φ x - F Ψ x)%I.
Φ Ψ, (( x, Φ x Ψ x) x, F Φ x F Ψ x)%I. Arguments bi_mono_pred {_ _ _ _} _ _.
Definition uPred_least_fixpoint {M A} (F : (A uPred M) (A uPred M)) Definition uPred_least_fixpoint {M A} (F : (A uPred M) (A uPred M))
(x : A) : uPred M := (x : A) : uPred M :=
...@@ -18,13 +18,12 @@ Definition uPred_greatest_fixpoint {M A} (F : (A → uPred M) → (A → uPred M ...@@ -18,13 +18,12 @@ Definition uPred_greatest_fixpoint {M A} (F : (A → uPred M) → (A → uPred M
( Φ, ( x, Φ x F Φ x) Φ x)%I. ( Φ, ( x, Φ x F Φ x) Φ x)%I.
Section least. Section least.
Context {M : ucmraT}. Context {M A} (F : (A uPred M) (A uPred M)) `{!BIMonoPred F}.
Context {A} (F : (A uPred M) (A uPred M)) (Hmono : uPred_mono_pred F).
Lemma least_fixpoint_unfold_2 x : F (uPred_least_fixpoint F) x uPred_least_fixpoint F x. Lemma least_fixpoint_unfold_2 x : F (uPred_least_fixpoint F) x uPred_least_fixpoint F x.
Proof. Proof.
iIntros "HF" (Φ) "#Hincl". iIntros "HF" (Φ) "#Hincl".
iApply "Hincl". iApply (Hmono _ Φ); last done. iApply "Hincl". iApply (bi_mono_pred _ Φ); last done.
iIntros "!#" (y) "Hy". iApply "Hy". done. iIntros "!#" (y) "Hy". iApply "Hy". done.
Qed. Qed.
...@@ -32,7 +31,7 @@ Section least. ...@@ -32,7 +31,7 @@ Section least.
uPred_least_fixpoint F x F (uPred_least_fixpoint F) x. uPred_least_fixpoint F x F (uPred_least_fixpoint F) x.
Proof. Proof.
iIntros "HF". iApply "HF". iIntros "!#" (y) "Hy". iIntros "HF". iApply "HF". iIntros "!#" (y) "Hy".
iApply Hmono; last done. iIntros "!#" (z) "?". iApply bi_mono_pred; last done. iIntros "!#" (z) "?".
by iApply least_fixpoint_unfold_2. by iApply least_fixpoint_unfold_2.
Qed. Qed.
...@@ -48,13 +47,13 @@ Section least. ...@@ -48,13 +47,13 @@ Section least.
End least. End least.
Section greatest. Section greatest.
Context {M : ucmraT} {A} (F : (A uPred M) (A uPred M)) (Hmono : uPred_mono_pred F). Context {M A} (F : (A uPred M) (A uPred M)) `{!BIMonoPred F}.
Lemma greatest_fixpoint_unfold_1 x : Lemma greatest_fixpoint_unfold_1 x :
uPred_greatest_fixpoint F x F (uPred_greatest_fixpoint F) x. uPred_greatest_fixpoint F x F (uPred_greatest_fixpoint F) x.
Proof. Proof.
iDestruct 1 as (Φ) "[#Hincl HΦ]". iDestruct 1 as (Φ) "[#Hincl HΦ]".
iApply (Hmono Φ (uPred_greatest_fixpoint F)). iApply (bi_mono_pred Φ (uPred_greatest_fixpoint F)).
- iIntros "!#" (y) "Hy". iExists Φ. auto. - iIntros "!#" (y) "Hy". iExists Φ. auto.
- by iApply "Hincl". - by iApply "Hincl".
Qed. Qed.
...@@ -63,7 +62,7 @@ Section greatest. ...@@ -63,7 +62,7 @@ Section greatest.
F (uPred_greatest_fixpoint F) x uPred_greatest_fixpoint F x. F (uPred_greatest_fixpoint F) x uPred_greatest_fixpoint F x.
Proof. Proof.
iIntros "HF". iExists (F (uPred_greatest_fixpoint F)). iIntros "HF". iExists (F (uPred_greatest_fixpoint F)).
iIntros "{$HF} !#" (y) "Hy". iApply (Hmono with "[] Hy"). iIntros "{$HF} !#" (y) "Hy". iApply (bi_mono_pred with "[] Hy").
iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1. iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
Qed. Qed.
......
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