Commit 78dedb27 authored by Ralf Jung's avatar Ralf Jung

make fixpoints simpl never

parent 67325634
......@@ -14,11 +14,13 @@ Local Existing Instance bi_mono_pred_ne.
Definition bi_least_fixpoint {PROP : bi} {A : ofeT}
(F : (A PROP) (A PROP)) (x : A) : PROP :=
( Φ : A -n> PROP, <pers> ( x, F Φ x - Φ x) Φ x)%I.
tc_opaque ( Φ : A -n> PROP, <pers> ( x, F Φ x - Φ x) Φ x)%I.
Arguments bi_least_fixpoint : simpl never.
Definition bi_greatest_fixpoint {PROP : bi} {A : ofeT}
(F : (A PROP) (A PROP)) (x : A) : PROP :=
( Φ : A -n> PROP, <pers> ( x, Φ x - F Φ x) Φ x)%I.
tc_opaque ( Φ : A -n> PROP, <pers> ( x, Φ x - F Φ x) Φ x)%I.
Arguments bi_greatest_fixpoint : simpl never.
Section least.
Context {PROP : bi} {A : ofeT} (F : (A PROP) (A PROP)) `{!BiMonoPred F}.
......@@ -28,7 +30,7 @@ Section least.
Lemma least_fixpoint_unfold_2 x : F (bi_least_fixpoint F) x bi_least_fixpoint F x.
Proof.
iIntros "HF" (Φ) "#Hincl".
rewrite /bi_least_fixpoint /=. iIntros "HF" (Φ) "#Hincl".
iApply "Hincl". iApply (bi_mono_pred _ Φ with "[#]"); last done.
iIntros "!#" (y) "Hy". iApply ("Hy" with "[# //]").
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