Commit 51b15fdc authored by Robbert Krebbers's avatar Robbert Krebbers

No longer break now_True abstraction.

And make it Typeclasses Opaque to ensure that we indeed do not do
so using the proof mode.
parent c012a2f3
...@@ -339,6 +339,7 @@ Definition uPred_now_True {M} (P : uPred M) : uPred M := ▷ False ∨ P. ...@@ -339,6 +339,7 @@ Definition uPred_now_True {M} (P : uPred M) : uPred M := ▷ False ∨ P.
Notation "◇ P" := (uPred_now_True P) Notation "◇ P" := (uPred_now_True P)
(at level 20, right associativity) : uPred_scope. (at level 20, right associativity) : uPred_scope.
Instance: Params (@uPred_now_True) 1. Instance: Params (@uPred_now_True) 1.
Typeclasses Opaque uPred_now_True.
Class TimelessP {M} (P : uPred M) := timelessP : P P. Class TimelessP {M} (P : uPred M) := timelessP : P P.
Arguments timelessP {_} _ {_}. Arguments timelessP {_} _ {_}.
......
...@@ -52,11 +52,10 @@ Proof. ...@@ -52,11 +52,10 @@ Proof.
rewrite {1}wp_unfold /wp_pre. iIntros (Hstep) "[(Hw & HE & Hσ) [H|[_ H]]]". rewrite {1}wp_unfold /wp_pre. iIntros (Hstep) "[(Hw & HE & Hσ) [H|[_ H]]]".
{ iDestruct "H" as (v) "[% _]". apply val_stuck in Hstep; simplify_eq. } { iDestruct "H" as (v) "[% _]". apply val_stuck in Hstep; simplify_eq. }
rewrite pvs_eq /pvs_def. rewrite pvs_eq /pvs_def.
iVs ("H" $! σ1 with "Hσ [Hw HE]") as "[H|(Hw & HE & _ & H)]"; first by iFrame. iVs ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
{ iVsIntro; iNext. by iExFalso. }
iVsIntro; iNext. iVsIntro; iNext.
by iVs ("H" $! e2 σ2 ef with "[%] [Hw HE]") as "[?|($ & $ & $ & $)]"; iVs ("H" $! e2 σ2 ef with "[%] [Hw HE]")
[done|by iFrame|rewrite /uPred_now_True; eauto|]. as ">($ & $ & $ & $)"; try iFrame; eauto.
Qed. Qed.
Lemma wptp_step e1 t1 t2 σ1 σ2 Φ : Lemma wptp_step e1 t1 t2 σ1 σ2 Φ :
...@@ -84,8 +83,7 @@ Proof. ...@@ -84,8 +83,7 @@ Proof.
{ inversion_clear 1; iIntros "?"; eauto 10. } { inversion_clear 1; iIntros "?"; eauto 10. }
iIntros (Hsteps) "H". inversion_clear Hsteps as [|?? [t1' σ1']]. iIntros (Hsteps) "H". inversion_clear Hsteps as [|?? [t1' σ1']].
iVs (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq. iVs (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq.
iVsIntro; iNext; iVs "H" as "[?|?]"; first (iVsIntro; iNext; by iExFalso). iVsIntro; iNext; iVs "H" as ">?". by iApply IH.
by iApply IH.
Qed. Qed.
Instance rvs_iter_mono n : Proper (() ==> ()) (Nat.iter n (λ P, |=r=> P)%I). Instance rvs_iter_mono n : Proper (() ==> ()) (Nat.iter n (λ P, |=r=> P)%I).
...@@ -99,8 +97,7 @@ Proof. ...@@ -99,8 +97,7 @@ Proof.
intros. rewrite wptp_steps // (Nat_iter_S_r (S n)); apply rvs_iter_mono. intros. rewrite wptp_steps // (Nat_iter_S_r (S n)); apply rvs_iter_mono.
iDestruct 1 as (e2 t2') "(% & (Hw & HE & _) & H & _)"; simplify_eq. iDestruct 1 as (e2 t2') "(% & (Hw & HE & _) & H & _)"; simplify_eq.
iDestruct (wp_value_inv with "H") as "H". rewrite pvs_eq /pvs_def. iDestruct (wp_value_inv with "H") as "H". rewrite pvs_eq /pvs_def.
iVs ("H" with "[Hw HE]") as "[?|(_ & _ & $)]"; [by iFrame| |done]. iVs ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
iVsIntro; iNext; by iExFalso.
Qed. Qed.
Lemma wp_safe e σ Φ : Lemma wp_safe e σ Φ :
...@@ -108,8 +105,8 @@ Lemma wp_safe e σ Φ : ...@@ -108,8 +105,8 @@ Lemma wp_safe e σ Φ :
Proof. Proof.
rewrite wp_unfold /wp_pre. iIntros "[(Hw&HE&Hσ) [H|[_ H]]]". rewrite wp_unfold /wp_pre. iIntros "[(Hw&HE&Hσ) [H|[_ H]]]".
{ iDestruct "H" as (v) "[% _]"; eauto 10. } { iDestruct "H" as (v) "[% _]"; eauto 10. }
rewrite pvs_eq. iVs ("H" with "* Hσ [-]") as "[H|(?&?&%&?)]"; first by iFrame. rewrite pvs_eq. iVs ("H" with "* Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
iVsIntro; iNext; by iExFalso. eauto 10. eauto 10.
Qed. Qed.
Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ : Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
......
...@@ -49,9 +49,9 @@ Proof. ...@@ -49,9 +49,9 @@ Proof.
iDestruct "Hi" as % ?%elem_of_subseteq_singleton. iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
rewrite {1 4}(union_difference_L (nclose N) E) // ownE_op; last set_solver. rewrite {1 4}(union_difference_L (nclose N) E) // ownE_op; last set_solver.
rewrite {1 5}(union_difference_L {[ i ]} (nclose N)) // ownE_op; last set_solver. rewrite {1 5}(union_difference_L {[ i ]} (nclose N)) // ownE_op; last set_solver.
iIntros "(Hw & [HE $] & $)"; iVsIntro; iRight. iIntros "(Hw & [HE $] & $)"; iVsIntro; iApply now_True_intro.
iDestruct (ownI_open i P with "[Hw HE]") as "($ & $ & HD)"; first by iFrame. iDestruct (ownI_open i P with "[Hw HE]") as "($ & $ & HD)"; first by iFrame.
iIntros "HP [Hw $] !==>"; iRight. iApply ownI_close; by iFrame. iIntros "HP [Hw $] !==>"; iApply now_True_intro. iApply ownI_close; by iFrame.
Qed. Qed.
Lemma inv_open_timeless E N P `{!TimelessP P} : Lemma inv_open_timeless E N P `{!TimelessP P} :
......
...@@ -44,17 +44,17 @@ Lemma pvs_intro' E1 E2 P : E2 ⊆ E1 → ((|={E2,E1}=> True) -★ P) ={E1,E2}=> ...@@ -44,17 +44,17 @@ Lemma pvs_intro' E1 E2 P : E2 ⊆ E1 → ((|={E2,E1}=> True) -★ P) ={E1,E2}=>
Proof. Proof.
intros (E1''&->&?)%subseteq_disjoint_union_L. intros (E1''&->&?)%subseteq_disjoint_union_L.
rewrite pvs_eq /pvs_def ownE_op //; iIntros "H ($ & $ & HE) !==>". rewrite pvs_eq /pvs_def ownE_op //; iIntros "H ($ & $ & HE) !==>".
iApply now_True_intro. iApply "H". iIntros "[$ $] !==>". iRight; eauto. iApply now_True_intro. iApply "H".
iIntros "[$ $] !==>". by iApply now_True_intro.
Qed. Qed.
Lemma now_True_pvs E1 E2 P : (|={E1,E2}=> P) ={E1,E2}=> P. Lemma now_True_pvs E1 E2 P : (|={E1,E2}=> P) ={E1,E2}=> P.
Proof. Proof.
rewrite pvs_eq. iIntros "[?|H] [Hw HE]". rewrite pvs_eq. iIntros "H [Hw HE]". iTimeless "H". iApply "H"; by iFrame.
- rewrite /uPred_now_True; eauto.
- iApply "H"; by iFrame.
Qed. Qed.
Lemma rvs_pvs E P : (|=r=> P) ={E}=> P. Lemma rvs_pvs E P : (|=r=> P) ={E}=> P.
Proof. Proof.
rewrite pvs_eq /pvs_def. iIntros "H [$ $]". by rewrite -uPred.now_True_intro. rewrite pvs_eq /pvs_def. iIntros "H [$ $]"; iVs "H".
iVsIntro. by iApply now_True_intro.
Qed. Qed.
Lemma pvs_mono E1 E2 P Q : (P Q) (|={E1,E2}=> P) ={E1,E2}=> Q. Lemma pvs_mono E1 E2 P Q : (P Q) (|={E1,E2}=> P) ={E1,E2}=> Q.
Proof. Proof.
...@@ -64,18 +64,15 @@ Qed. ...@@ -64,18 +64,15 @@ Qed.
Lemma pvs_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P. Lemma pvs_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P.
Proof. Proof.
rewrite pvs_eq /pvs_def. iIntros "HP HwE". rewrite pvs_eq /pvs_def. iIntros "HP HwE".
iVs ("HP" with "HwE") as "[?|(Hw & HE & HP)]". iVs ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
- rewrite /uPred_now_True; eauto.
- iApply "HP"; by iFrame.
Qed. Qed.
Lemma pvs_mask_frame_r' E1 E2 Ef P : Lemma pvs_mask_frame_r' E1 E2 Ef P :
E1 Ef (|={E1,E2}=> E2 Ef P) ={E1 Ef,E2 Ef}=> P. E1 Ef (|={E1,E2}=> E2 Ef P) ={E1 Ef,E2 Ef}=> P.
Proof. Proof.
intros. rewrite pvs_eq /pvs_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)". intros. rewrite pvs_eq /pvs_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
iVs ("Hvs" with "[Hw HE1]") as "[?|($ & HE2 & HP)]"; first by iFrame. iVs ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
- rewrite /uPred_now_True; eauto. iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
- iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame. iVsIntro; iApply now_True_intro. by iApply "HP".
iVsIntro; iRight; by iApply "HP".
Qed. Qed.
Lemma pvs_frame_r E1 E2 P Q : (|={E1,E2}=> P) Q ={E1,E2}=> P Q. Lemma pvs_frame_r E1 E2 P Q : (|={E1,E2}=> P) Q ={E1,E2}=> P Q.
Proof. rewrite pvs_eq /pvs_def. by iIntros "[HwP $]". Qed. Proof. rewrite pvs_eq /pvs_def. by iIntros "[HwP $]". 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