Commit 4a91ae92 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Solve admits.

parent 94cd4223
...@@ -124,6 +124,9 @@ Lemma RO_Box_fold : forall p q n, ...@@ -124,6 +124,9 @@ Lemma RO_Box_fold : forall p q n,
RO (p ~~~> q \* q ~~~> n) ==> RO (p ~> Box n). RO (p ~~~> q \* q ~~~> n) ==> RO (p ~> Box n).
Proof using. iIntros (???) "?". xunfold Box. by iExists _. Qed. Proof using. iIntros (???) "?". xunfold Box. by iExists _. Qed.
Instance Box_normal : forall p n, Normal (p ~> Box n).
Proof. xunfold Box. apply _. Qed.
Arguments Box_fold : clear implicits. Arguments Box_fold : clear implicits.
Arguments Box_unfold : clear implicits. Arguments Box_unfold : clear implicits.
Arguments RO_Box_unfold : clear implicits. Arguments RO_Box_unfold : clear implicits.
...@@ -148,8 +151,8 @@ Lemma rule_box_get : forall p n, ...@@ -148,8 +151,8 @@ Lemma rule_box_get : forall p n,
Proof using. Proof using.
intros. xdef. xchanges (RO_Box_unfold p) ;=> q. intros. xdef. xchanges (RO_Box_unfold p) ;=> q.
xletapp rule_get_ro => ? ->. xletapp rule_get_ro => ? ->.
ram_apply rule_get_ro. admit. (* TODO: complete proof *) ram_apply rule_get_ro. iIntros "_ $". auto. (* TODO : improve. *)
Admitted. Qed.
(* detailed proof (to keep somewhere for debugging): (* detailed proof (to keep somewhere for debugging):
intros. xdef. xchange (RO_Box_unfold p). xpull ;=> q. intros. xdef. xchange (RO_Box_unfold p). xpull ;=> q.
...@@ -291,14 +294,11 @@ Proof using. ...@@ -291,14 +294,11 @@ Proof using.
xletfun => F HF. xletfun => F HF.
ram_apply_let (rule_box_twice (fun (x:int) => (x + n)%Z) n). ram_apply_let (rule_box_twice (fun (x:int) => (x + n)%Z) n).
{ intros. xdef'. xletapp rule_box_get => m ->. { intros. xdef'. xletapp rule_box_get => m ->.
ram_apply rule_add. { iIntros. admit. (* todo *) } } ram_apply rule_add. { iModIntro. auto. } } (* TODO : improve. *)
{ iIntros "Hq Hp". iDestruct (Box_fold with "[$Hq $Hp]") as "$". { iIntros "Hq Hp". iDestruct (Box_fold with "[$Hq $Hp]") as "$".
auto with iFrame. } auto with iFrame. }
unlock. xpull=> u /= _. ram_apply rule_box_get. unlock. xpull=> u /= _. apply rule_htop_post. ram_apply rule_box_get.
math_rewrite (2 * (n + n) = 4 * n)%Z.
assert (forall x, Normal (p ~> Box x)). admit. iIntros "$ !>". auto 10. (* TODO: improve. *)
math_rewrite (2 * (n + n) = 4 * n)%Z.
iIntros "$".
admit.
Qed. Qed.
...@@ -1719,12 +1719,6 @@ Qed. ...@@ -1719,12 +1719,6 @@ Qed.
Instance RO_affine P : Affine P Affine (RO P). Instance RO_affine P : Affine P Affine (RO P).
Proof. rewrite /Affine=>->. by rewrite RO_empty. Qed. Proof. rewrite /Affine=>->. by rewrite RO_empty. Qed.
(* This is probably true, but not trivial to prove and not very usefull: *)
(* Instance ROFrame_persistent (P Q : hprop) : *)
(* Persistent P Persistent Q Persistent (ROFrame P Q). *)
(* Instance ROFrame_affine (P Q : hprop) : *)
(* Affine P Affine Q Affine (ROFrame P Q). *)
(** Into/From instances for RO, normally and ROFrame. *) (** Into/From instances for RO, normally and ROFrame. *)
Instance normally_from_pure (P : hprop) (φ : Prop) : Instance normally_from_pure (P : hprop) (φ : Prop) :
...@@ -1878,16 +1872,22 @@ Proof. unfold FrameOrWand. iIntros "[? H]". by iApply "H". Qed. ...@@ -1878,16 +1872,22 @@ Proof. unfold FrameOrWand. iIntros "[? H]". by iApply "H". Qed.
(* 1st step: if we are tying to frame an RO, we first see if it is (* 1st step: if we are tying to frame an RO, we first see if it is
needed on the LHS. If so, then we also make it available on the needed on the LHS. If so, then we also make it available on the
RHS. *) RHS. We do this only if the RHS is not of the form [normally P],
Instance frame_roframe_ro_lr p (R P P' Q Q' S : hprop) : because otherwise we cannot get rid of this RO permission. *)
Lemma frame_roframe_ro_lr p (R P P' Q Q' S : hprop) :
DupFrameRO R P P' FrameOrWand (RO R) Q Q' DupFrameRO R P P' FrameOrWand (RO R) Q Q'
MakeROFrame P' Q' S Frame p (RO R) (ROFrame P Q) S | 1. MakeROFrame P' Q' S Frame p (RO R) (ROFrame P Q) S.
Proof. Proof.
rewrite /Frame /DupFrameRO /FrameOrWand /MakeROFrame rewrite /Frame /DupFrameRO /FrameOrWand /MakeROFrame
bi.affinely_persistently_if_elim=><- <- ->. bi.affinely_persistently_if_elim=><- <- ->.
assert (HR:=@RO_duplicatable R). unfold duplicatable in HR. rewrite {1}HR. assert (HR:=@RO_duplicatable R). unfold duplicatable in HR. rewrite {1}HR.
by rewrite /bi_sep /= hstar_assoc ROFrame_frame_r ROFrame_frame_l. by rewrite /bi_sep /= hstar_assoc ROFrame_frame_r ROFrame_frame_l.
Qed. Qed.
Hint Extern 1 (Frame _ (RO _) (ROFrame _ ?Q) _) =>
lazymatch Q with
| normally _ => fail
| _ => simple eapply @frame_roframe_ro_lr
end.
(* 2nd step: we try to frame on the LHS. *) (* 2nd step: we try to frame on the LHS. *)
Instance frame_roframe_l p (R P P' Q S : hprop) : Instance frame_roframe_l p (R P P' Q S : hprop) :
...@@ -1929,6 +1929,10 @@ Instance from_modal_normally P : ...@@ -1929,6 +1929,10 @@ Instance from_modal_normally P :
FromModal modality_normally (normally P) (normally P) P. FromModal modality_normally (normally P) (normally P) P.
Proof. by rewrite /FromModal. Qed. Proof. by rewrite /FromModal. Qed.
Instance from_modal_abs_normally P :
FromModal modality_normally (<absorb> normally P) (<absorb> normally P) P.
Proof. by rewrite /FromModal -bi.absorbingly_intro. Qed.
(** A bit of automation for ROFrame and normally. *) (** A bit of automation for ROFrame and normally. *)
Hint Extern 2 (envs_entails _ (ROFrame _ _)) => progress iFrame : iFrame. Hint Extern 2 (envs_entails _ (ROFrame _ _)) => progress iFrame : iFrame.
...@@ -1938,8 +1942,11 @@ Hint Extern 0 (envs_entails _ (ROFrame \[] _)) => iSplitR. ...@@ -1938,8 +1942,11 @@ Hint Extern 0 (envs_entails _ (ROFrame \[] _)) => iSplitR.
Hint Extern 0 (envs_entails _ (ROFrame _ \[])) => iSplitL. Hint Extern 0 (envs_entails _ (ROFrame _ \[])) => iSplitL.
Hint Extern 0 (envs_entails _ (ROFrame emp%I _)) => iSplitR. Hint Extern 0 (envs_entails _ (ROFrame emp%I _)) => iSplitR.
Hint Extern 0 (envs_entails _ (ROFrame _ emp%I)) => iSplitL. 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 _ (normally _)) => iModIntro (normally _).
Hint Extern 0 (envs_entails _ (<absorb> normally _)) =>
iModIntro (<absorb> normally _)%I.
(** [PrepareHProp] stuff. *) (** [PrepareHProp] stuff. *)
...@@ -1947,24 +1954,35 @@ Instance prepare_hprop_normally (P Q : hprop) : ...@@ -1947,24 +1954,35 @@ Instance prepare_hprop_normally (P Q : hprop) :
PrepareHProp P Q PrepareHProp (normally P) (normally Q). PrepareHProp P Q PrepareHProp (normally P) (normally Q).
Proof. by unfold PrepareHProp=>->. Qed. Proof. by unfold PrepareHProp=>->. Qed.
Instance prepare_hprop_hstar (P P' Q Q' : hprop) : Instance prepare_hprop_ROFrame (P P' Q Q' : hprop) :
PrepareHProp P P' PrepareHProp Q Q' PrepareHProp P P' PrepareHProp Q Q'
PrepareHProp (ROFrame P Q) (ROFrame P' Q'). PrepareHProp (ROFrame P Q) (ROFrame P' Q').
Proof. by rewrite /PrepareHProp=>-> ->. Qed. Proof. by rewrite /PrepareHProp=>-> ->. Qed.
(** Tactics *) (** Tactics *)
Lemma rule_ramified_frame_read_only_locked : forall t H Q H' Q', Lemma rule_ramified_frame_read_only_absorb : forall t H Q H' Q',
triple t H' Q' ->
H ==> (<absorb> ROFrame H' (normally (Q' \---* Q)))%I ->
triple t H Q.
Proof using.
intros t H Q H' Q' Ht HH. eapply rule_consequence; first last; [done| |].
eapply rule_htop_pre, rule_ramified_frame_read_only;
[eassumption|iIntros "?"; iAssumption].
iIntros "H". by iDestruct (HH with "H") as ">$".
Qed.
Lemma rule_ramified_frame_read_only_absorb_locked : forall t H Q H' Q',
triple t H' Q' -> triple t H' Q' ->
H ==> ROFrame H' (normally (locked Q' \---* Q)) -> H ==> (<absorb> ROFrame H' (normally (locked Q' \---* Q)))%I ->
triple t H Q. triple t H Q.
Proof using. unlock. apply rule_ramified_frame_read_only. Qed. Proof using. unlock. apply rule_ramified_frame_read_only_absorb. Qed.
Ltac ram_apply lem := Ltac ram_apply lem :=
lazymatch goal with lazymatch goal with
| |- triple _ _ ?Q => | |- triple _ _ ?Q =>
(is_evar Q; eapply rule_ramified_frame_read_only_locked) || (is_evar Q; eapply rule_ramified_frame_read_only_absorb_locked) ||
eapply rule_ramified_frame_read_only eapply rule_ramified_frame_read_only_absorb
end; [eapply lem|iPrepare]. end; [eapply lem|iPrepare].
Lemma rule_let_ramified_frame_read_only_locked : forall x t1 t2 H1 H Q1 Q Q', Lemma rule_let_ramified_frame_read_only_locked : forall x t1 t2 H1 H Q1 Q Q',
......
...@@ -2371,6 +2371,11 @@ Hint Extern 1 (PrepareHProp (_ \* emp%I)%I _) => ...@@ -2371,6 +2371,11 @@ Hint Extern 1 (PrepareHProp (_ \* emp%I)%I _) =>
Hint Extern 1 (PrepareHProp (_ emp) _) => Hint Extern 1 (PrepareHProp (_ emp) _) =>
simple apply prepare_hprop_hstar_hemp : typeclass_instances. simple apply prepare_hprop_hstar_hemp : typeclass_instances.
Instance prepare_hprop_absorbingly (P Q : hprop) :
PrepareHProp P Q PrepareHProp (<absorb> P) (<absorb> Q).
Proof. by unfold PrepareHProp=>->. Qed.
Lemma tac_prepare Δ (P Q : hprop) : Lemma tac_prepare Δ (P Q : hprop) :
PrepareHProp P Q PrepareHProp P Q
envs_entails Δ Q envs_entails Δ Q
......
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