Verified Commit affd6603 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Also review Iris instances outside [frame_instances]

parent 9155503a
Pipeline #50960 canceled with stage
in 6 minutes and 12 seconds
......@@ -181,7 +181,7 @@ Section fractional.
Global Instance frame_fractional p R r Φ P q RES:
AsFractional R Φ r AsFractional P Φ q
FrameFractionalHyps p R Φ RES r q
Frame p R P RES.
Frame p R P RES. (* No explicit priority, as default prio > [frame_here]'s 1. *)
Proof.
rewrite /Frame=>-[HR _][->?]H.
revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0].
......
......@@ -284,7 +284,7 @@ Section proofmode_classes.
Global Instance frame_twp p s E e R Φ Ψ :
( v, Frame p R (Φ v) (Ψ v))
Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]).
Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]) | 2.
Proof. rewrite /Frame=> HR. rewrite twp_frame_l. apply twp_mono, HR. Qed.
Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E [{ Φ }]).
......
......@@ -366,7 +366,7 @@ Section proofmode_classes.
Global Instance frame_wp p s E e R Φ Ψ :
( v, Frame p R (Φ v) (Ψ v))
Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}).
Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}) | 2.
Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E {{ Φ }}).
......
......@@ -364,7 +364,7 @@ Qed.
(* Framing. *)
Global Instance frame_monPred_at_enter p i 𝓡 P 𝓠 :
FrameMonPredAt p i 𝓡 P 𝓠 Frame p 𝓡 (P i) 𝓠.
FrameMonPredAt p i 𝓡 P 𝓠 Frame p 𝓡 (P i) 𝓠 | 2.
Proof. intros. done. Qed.
Global Instance frame_monPred_at_here p P i j :
IsBiIndexRel i j FrameMonPredAt p j (P i) P emp | 0.
......
......@@ -73,7 +73,7 @@ Qed.
Global Instance array_cons_frame l dq v vs R Q :
Frame false R (l {dq} v (l + 1) ↦∗{dq} vs) Q
Frame false R (l ↦∗{dq} (v :: vs)) Q.
Frame false R (l ↦∗{dq} (v :: vs)) Q | 2.
Proof. by rewrite /Frame array_cons. Qed.
Lemma update_array l dq vs off v :
......
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