Commit 6e10b9aa authored by Robbert Krebbers's avatar Robbert Krebbers

Generalize iTimeless tactic.

parent fe99f874
Pipeline #2391 passed with stage
......@@ -312,4 +312,7 @@ Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
Global Instance into_exist_always {A} P (Φ : A uPred M) :
IntoExist P Φ IntoExist ( P) (λ a, (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
Class TimelessElim (Q : uPred M) :=
timeless_elim `{!TimelessP P} R : (R Q) P (P - R) Q.
End classes.
......@@ -375,6 +375,16 @@ Proof.
by rewrite right_id always_and_sep_l' wand_elim_r HQ.
Qed.
Lemma tac_timeless Δ Δ' i p P Q :
TimelessElim Q
envs_lookup i Δ = Some (p, P)%I TimelessP P
envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ'
(Δ' Q) Δ Q.
Proof.
intros ???? HQ. rewrite envs_simple_replace_sound //; simpl.
rewrite always_if_later right_id. by apply timeless_elim.
Qed.
(** * Always *)
Lemma tac_always_intro Δ Q : envs_persistent Δ = true (Δ Q) Δ Q.
Proof. intros. by apply: always_intro. Qed.
......
......@@ -30,6 +30,12 @@ Global Instance into_wand_pvs E1 E2 R P Q :
IntoWand R P Q IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
Global Instance timeless_elim_pvs E1 E2 Q : TimelessElim (|={E1,E2}=> Q).
Proof.
intros P ? R HR. rewrite (pvs_timeless E1 P) pvs_frame_r.
by rewrite wand_elim_r HR pvs_trans; last set_solver.
Qed.
Class IsFSA {A} (P : iProp Λ Σ) (E : coPset)
(fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A iProp Λ Σ) := {
is_fsa : P ⊣⊢ fsa E Φ;
......@@ -48,6 +54,12 @@ Global Instance to_assert_pvs {A} P Q E (fsa : FSA Λ Σ A) fsaV Φ :
Proof.
intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r (is_fsa Q) fsa_pvs_fsa.
Qed.
Global Instance timeless_elim_fsa {A} Q E (fsa : FSA Λ Σ A) fsaV Φ :
IsFSA Q E fsa fsaV Φ TimelessElim Q.
Proof.
intros ? P ? R. rewrite (is_fsa Q) -{2}fsa_pvs_fsa. intros <-.
by rewrite (pvs_timeless _ P) pvs_frame_r wand_elim_r.
Qed.
Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2 (Δ Q) Δ |={E1,E2}=> Q.
Proof. intros -> ->. apply pvs_intro. Qed.
......@@ -74,26 +86,6 @@ Proof.
intros ? -> ??. rewrite (is_fsa Q) -fsa_pvs_fsa.
eapply tac_pvs_elim; set_solver.
Qed.
Lemma tac_pvs_timeless Δ Δ' E1 E2 i p P Q :
envs_lookup i Δ = Some (p, P)%I TimelessP P
envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ'
(Δ' ={E1,E2}=> Q) Δ ={E1,E2}=> Q.
Proof.
intros ??? HQ. rewrite envs_simple_replace_sound //; simpl.
rewrite always_if_later (pvs_timeless E1 (?_ P)%I) pvs_frame_r.
by rewrite right_id wand_elim_r HQ pvs_trans; last set_solver.
Qed.
Lemma tac_pvs_timeless_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P Q Φ :
IsFSA Q E fsa fsaV Φ
envs_lookup i Δ = Some (p, P)%I TimelessP P
envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ'
(Δ' fsa E Φ) Δ Q.
Proof.
intros ????. rewrite (is_fsa Q) -fsa_pvs_fsa.
eauto using tac_pvs_timeless.
Qed.
End pvs.
Tactic Notation "iPvsIntro" := apply tac_pvs_intro; first try fast_done.
......@@ -161,26 +153,5 @@ Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
iDestructHelp H as (fun H =>
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Tactic Notation "iTimeless" constr(H) :=
match goal with
| |- _ |={_,_}=> _ =>
eapply tac_pvs_timeless with _ H _ _;
[env_cbv; reflexivity || fail "iTimeless:" H "not found"
|let P := match goal with |- TimelessP ?P => P end in
apply _ || fail "iTimeless: " P "not timeless"
|env_cbv; reflexivity|simpl]
| |- _ =>
eapply tac_pvs_timeless_fsa with _ _ _ _ H _ _ _;
[let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
apply _ || fail "iTimeless: " P "not a pvs"
|env_cbv; reflexivity || fail "iTimeless:" H "not found"
|let P := match goal with |- TimelessP ?P => P end in
apply _ || fail "iTimeless: " P "not timeless"
|env_cbv; reflexivity|simpl]
end.
Tactic Notation "iTimeless" constr(H) "as" constr(Hs) :=
iTimeless H; iDestruct H as Hs.
Hint Extern 2 (of_envs _ _) =>
match goal with |- _ (|={_}=> _)%I => iPvsIntro end.
......@@ -501,6 +501,15 @@ Tactic Notation "iNext":=
|let P := match goal with |- FromLater ?P _ => P end in
apply _ || fail "iNext:" P "does not contain laters"|].
Tactic Notation "iTimeless" constr(H) :=
eapply tac_timeless with _ H _ _;
[let Q := match goal with |- TimelessElim ?Q => Q end in
apply _ || fail "iTimeless: cannot eliminate later in goal" Q
|env_cbv; reflexivity || fail "iTimeless:" H "not found"
|let P := match goal with |- TimelessP ?P => P end in
apply _ || fail "iTimeless: " P "not timeless"
|env_cbv; reflexivity|].
(** * Introduction tactic *)
Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" := first
[ (* (∀ _, _) *) apply tac_forall_intro; intros x
......
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