Commit c012a2f3 authored by Robbert Krebbers's avatar Robbert Krebbers

Generalize iTimeless to deal with now_True hypotheses.

parent 34f9f865
......@@ -327,11 +327,21 @@ 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.
(* IsTrueNow *)
(* IntoNowTrue *)
Global Instance into_now_True_now_True P : IntoNowTrue ( P) P.
Proof. done. Qed.
Global Instance into_now_True_timeless P : TimelessP P IntoNowTrue ( P) P.
Proof. done. Qed.
(* IsNowTrue *)
Global Instance is_now_True_now_True P : IsNowTrue ( P).
Proof. by rewrite /IsNowTrue now_True_idemp. Qed.
Global Instance is_now_True_later P : IsNowTrue ( P).
Proof. by rewrite /IsNowTrue now_True_later. Qed.
Global Instance is_now_True_rvs P : IsNowTrue P IsNowTrue (|=r=> P).
Proof.
rewrite /IsNowTrue=> HP. by rewrite -{2}HP -now_True_rvs -(now_True_intro P).
Qed.
(* FromViewShift *)
Global Instance from_vs_rvs P : FromVs (|=r=> P) P.
......
......@@ -55,6 +55,9 @@ Class IntoExist {A} (P : uPred M) (Φ : A → uPred M) :=
into_exist : P x, Φ x.
Global Arguments into_exist {_} _ _ {_}.
Class IntoNowTrue (P Q : uPred M) := into_now_True : P Q.
Global Arguments into_now_True : clear implicits.
Class IsNowTrue (Q : uPred M) := is_now_True : Q Q.
Global Arguments is_now_True : clear implicits.
......
......@@ -375,15 +375,15 @@ Proof.
by rewrite right_id always_and_sep_l' wand_elim_r HQ.
Qed.
Lemma tac_timeless Δ Δ' i p P Q :
Lemma tac_timeless Δ Δ' i p P P' Q :
IsNowTrue Q
envs_lookup i Δ = Some (p, P)%I TimelessP P
envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ'
envs_lookup i Δ = Some (p, P) IntoNowTrue P 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 HQ -{2}(is_now_True Q).
by rewrite (timelessP (?p P)) now_True_frame_r wand_elim_r.
rewrite right_id HQ -{2}(is_now_True Q).
by rewrite (into_now_True P) -now_True_always_if now_True_frame_r wand_elim_r.
Qed.
(** * Always *)
......
......@@ -496,11 +496,11 @@ Tactic Notation "iNext":=
apply _ || fail "iNext:" P "does not contain laters"|].
Tactic Notation "iTimeless" constr(H) :=
eapply tac_timeless with _ H _ _;
eapply tac_timeless with _ H _ _ _;
[let Q := match goal with |- IsNowTrue ?Q => Q end in
apply _ || fail "iTimeless: cannot remove later of timeless hypothesis in goal" Q
|env_cbv; reflexivity || fail "iTimeless:" H "not found"
|let P := match goal with |- TimelessP ?P => P end in
|let P := match goal with |- IntoNowTrue ?P _ => P end in
apply _ || fail "iTimeless:" P "not timeless"
|env_cbv; reflexivity|].
......
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