Commit 15c4ffc0 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Better FromModal instance for <absorb>normally P.

parent 996a7db5
......@@ -151,7 +151,7 @@ Arguments RO_Box_fold : clear implicits.
(* ---------------------------------------------------------------------- *)
(** Get operation *)
(*
(*
let get p =
! (!p)
*)
......@@ -168,14 +168,14 @@ Lemma rule_box_get : forall p n,
Proof using.
intros. xdef. xchanges (RO_Box_unfold p) ;=> q.
xletapp rule_get_ro => ? ->.
ram_apply rule_get_ro. auto with iFrame.
ram_apply rule_get_ro. auto 10 with iFrame.
Qed.
(* ---------------------------------------------------------------------- *)
(** Box up2 operation *)
(*
(*
let up2 f p =
let q = !p in
q := f !q + f !q
......@@ -244,9 +244,9 @@ Proof using.
xletfun => F HF.
ram_apply_let (rule_box_up2 (fun (x:int) => (x + n)%Z) n).
{ intros. xdef. xletapp rule_box_get => m ->.
ram_apply rule_add. { auto with iFrame. } }
ram_apply rule_add. { auto 10 with iFrame. } }
{ iIntros "Hq Hp". iDestruct (Box_fold with "[$Hq $Hp]") as "$".
auto with iFrame. }
unlock. xpull=> u /= _. apply rule_htop_post. ram_apply rule_box_get.
math_rewrite (2 * (n + n) = 4 * n)%Z. auto with iFrame.
math_rewrite (2 * (n + n) = 4 * n)%Z. auto 10 with iFrame.
Qed.
......@@ -1871,8 +1871,8 @@ Instance from_modal_normally P :
Proof. by rewrite /FromModal. Qed.
(* Low priority to force annotation. *)
Instance from_modal_abs_normally P :
FromModal modality_normally (normally P) (<absorb> normally P) P | 100.
Proof. by rewrite /FromModal -bi.absorbingly_intro. Qed.
FromModal modality_normally (normally P) (<absorb> normally P) (<absorb> P) | 100.
Proof. by rewrite /FromModal /= /bi_absorbingly normally_hstar normally_erase. Qed.
(** Frame instances *)
......
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