Commit 6e11695f authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Improve tactics a bit.

parent 4a91ae92
......@@ -151,7 +151,7 @@ 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. iIntros "_ $". auto. (* TODO : improve. *)
ram_apply rule_get_ro. auto with iFrame.
Qed.
(* detailed proof (to keep somewhere for debugging):
......@@ -294,11 +294,13 @@ Proof using.
xletfun => F HF.
ram_apply_let (rule_box_twice (fun (x:int) => (x + n)%Z) n).
{ intros. xdef'. xletapp rule_box_get => m ->.
ram_apply rule_add. { iModIntro. auto. } } (* TODO : improve. *)
ram_apply rule_add. { iIntros "?".
iSplitR. iModIntro. auto. auto with iFrame. } } (* TODO : improve. *)
{ 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.
iIntros "$ !>". auto 10. (* TODO: improve. *)
iIntros "$". auto 10 with iFrame. (* TODO: improve. *)
Qed.
......@@ -1887,7 +1887,8 @@ Hint Extern 1 (Frame _ (RO _) (ROFrame _ ?Q) _) =>
lazymatch Q with
| normally _ => fail
| _ => simple eapply @frame_roframe_ro_lr
end.
end
: typeclass_instances.
(* 2nd step: we try to frame on the LHS. *)
Instance frame_roframe_l p (R P P' Q S : hprop) :
......@@ -1913,28 +1914,29 @@ Qed.
(** Setup iModIntro to work with normally. *)
Lemma modality_normally_mixin :
modality_mixin normally MIEnvId (MIEnvForall Normal).
modality_mixin normally MIEnvId
(MIEnvTransform (λ P Q : hprop, TCAnd (TCEq P Q) (Normal P))).
Proof.
split; simpl; intros.
- by intros h [-> ?].
- by apply normally_intro.
split; simpl.
- by intros P h [-> ?].
- by intros P Q [-> ?]; apply normally_intro.
- by rewrite normally_hempty.
- by f_equiv.
- by rewrite normally_hstar.
- by intros P Q ?; f_equiv.
- by intros P Q; rewrite normally_hstar.
Qed.
Definition modality_normally :=
Modality _ modality_normally_mixin.
Instance from_modal_normally P :
FromModal modality_normally (normally P) (normally P) P.
Proof. by rewrite /FromModal. Qed.
(* Low priority to force annotation. *)
Instance from_modal_abs_normally P :
FromModal modality_normally (<absorb> normally P) (<absorb> normally P) P.
FromModal modality_normally (normally P) (<absorb> normally P) P | 100.
Proof. by rewrite /FromModal -bi.absorbingly_intro. Qed.
(** A bit of automation for ROFrame and normally. *)
Hint Extern 2 (envs_entails _ (ROFrame _ _)) => progress iFrame : iFrame.
Hint Extern 2 (envs_entails _ (<absorb> ROFrame _ _)) => progress iFrame : iFrame.
Hint Extern 0 (envs_entails _ (ROFrame \[_] _)) => iSplitR.
Hint Extern 0 (envs_entails _ (ROFrame _ \[_])) => iSplitL.
......@@ -1942,11 +1944,9 @@ Hint Extern 0 (envs_entails _ (ROFrame \[] _)) => iSplitR.
Hint Extern 0 (envs_entails _ (ROFrame _ \[])) => iSplitL.
Hint Extern 0 (envs_entails _ (ROFrame emp%I _)) => iSplitR.
Hint Extern 0 (envs_entails _ (ROFrame _ emp%I)) => iSplitL.
Hint Extern 0 (envs_entails _ (<absorb> ROFrame _ _)) => iSplit.
Hint Extern 0 (envs_entails _ (normally _)) => iModIntro (normally _).
Hint Extern 0 (envs_entails _ (<absorb> normally _)) =>
iModIntro (<absorb> normally _)%I.
Hint Extern 0 (envs_entails _ (<absorb> normally _)) => iModIntro (normally _)%I.
(** [PrepareHProp] stuff. *)
......
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