Commit 34037c0f authored by Robbert Krebbers's avatar Robbert Krebbers

Simplify TimelessElim class.

parent 453a3791
Pipeline #2392 passed with stage
......@@ -314,5 +314,5 @@ Global Instance into_exist_always {A} P (Φ : A → uPred M) :
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.
timeless_elim `{!TimelessP P} : P (P - Q) Q.
End classes.
......@@ -382,7 +382,7 @@ Lemma tac_timeless Δ Δ' i p P Q :
(Δ' Q) Δ Q.
Proof.
intros ???? HQ. rewrite envs_simple_replace_sound //; simpl.
rewrite always_if_later right_id. by apply timeless_elim.
by rewrite always_if_later right_id HQ timeless_elim.
Qed.
(** * Always *)
......
......@@ -32,8 +32,8 @@ 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.
intros P ?. rewrite (pvs_timeless E1 P) pvs_frame_r.
by rewrite wand_elim_r pvs_trans; last set_solver.
Qed.
Class IsFSA {A} (P : iProp Λ Σ) (E : coPset)
......@@ -57,7 +57,7 @@ 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 <-.
intros ? P ?. rewrite (is_fsa Q) -{2}fsa_pvs_fsa.
by rewrite (pvs_timeless _ P) pvs_frame_r wand_elim_r.
Qed.
......
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