pviewshifts.v 7.12 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9
From iris.proofmode Require Import coq_tactics spec_patterns.
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export pviewshifts.
Import uPred.

Section pvs.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.

10 11
Global Instance from_pure_pvs E P φ : FromPure P φ  FromPure (|={E}=> P) φ.
Proof. intros ??. by rewrite -pvs_intro (from_pure P). Qed.
12 13 14 15 16 17
Global Instance from_assumption_pvs E p P Q :
  FromAssumption p P Q  FromAssumption p P (|={E}=> Q)%I.
Proof. rewrite /FromAssumption=>->. apply pvs_intro. Qed.
Global Instance from_sep_pvs E P Q1 Q2 :
  FromSep P Q1 Q2  FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
Global Instance or_split_pvs E1 E2 P Q1 Q2 :
19 20
  FromOr P Q1 Q2  FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
Proof. rewrite /FromOr=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
Global Instance exists_split_pvs {A} E1 E2 P (Φ : A  iProp Λ Σ) :
22
  FromExist P Φ  FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
Proof.
24
  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Robbert Krebbers's avatar
Robbert Krebbers committed
25
Qed.
26 27
Global Instance frame_pvs E1 E2 R P Q :
  Frame R P Q  Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
28
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
29 30 31
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
32

33 34
Global Instance timeless_elim_pvs E1 E2 Q : TimelessElim (|={E1,E2}=> Q).
Proof.
35 36
  intros P ?. rewrite (pvs_timeless E1 P) pvs_frame_r.
  by rewrite wand_elim_r pvs_trans; last set_solver.
37 38
Qed.

39
Class IsFSA {A} (P : iProp Λ Σ) (E : coPset)
Robbert Krebbers's avatar
Robbert Krebbers committed
40
    (fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A  iProp Λ Σ) := {
41 42
  is_fsa : P  fsa E Φ;
  is_fsa_is_fsa :> FrameShiftAssertion fsaV fsa;
Robbert Krebbers's avatar
Robbert Krebbers committed
43
}.
44 45 46
Global Arguments is_fsa {_} _ _ _ _ _ {_}.
Global Instance is_fsa_pvs E P :
  IsFSA (|={E}=> P)%I E pvs_fsa True (λ _, P).
Robbert Krebbers's avatar
Robbert Krebbers committed
47
Proof. split. done. apply _. Qed.
48 49
Global Instance is_fsa_fsa {A} (fsa : FSA Λ Σ A) E Φ :
  FrameShiftAssertion fsaV fsa  IsFSA (fsa E Φ) E fsa fsaV Φ.
50
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
51

52
Global Instance to_assert_pvs {A} P Q E (fsa : FSA Λ Σ A) fsaV Φ :
53
  IsFSA Q E fsa fsaV Φ  IntoAssert P Q (|={E}=> P).
54
Proof.
55
  intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r (is_fsa Q) fsa_pvs_fsa.
56
Qed.
57 58 59
Global Instance timeless_elim_fsa {A} Q E (fsa : FSA Λ Σ A) fsaV Φ :
  IsFSA Q E fsa fsaV Φ  TimelessElim Q.
Proof.
60
  intros ? P ?. rewrite (is_fsa Q) -{2}fsa_pvs_fsa.
61 62
  by rewrite (pvs_timeless _ P) pvs_frame_r wand_elim_r.
Qed.
63

64
Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2  (Δ  Q)  Δ  |={E1,E2}=> Q.
65
Proof. intros -> ->. apply pvs_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
66

67 68 69 70
Lemma tac_pvs_elim Δ Δ' E1 E2 E3 i p P' E1' E2' P Q :
  envs_lookup i Δ = Some (p, P')  P' = (|={E1',E2'}=> P)%I 
  (E1' = E1  E2' = E2  E2  E1  E3
   E2 = E2'  E1  E1'  E2'  E1  E1'  E1'  E1  E2'  E1'  E3) 
Robbert Krebbers's avatar
Robbert Krebbers committed
71
  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' 
72
  (Δ' ={E2,E3}=> Q)  Δ ={E1,E3}=> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
Proof.
74 75 76 77
  intros ? -> HE ? HQ. rewrite envs_replace_sound //; simpl.
  rewrite always_if_elim right_id pvs_frame_r wand_elim_r HQ.
  destruct HE as [(?&?&?)|(?&?&?&?)]; subst; first (by apply pvs_trans).
  etrans; [eapply pvs_mask_frame'|apply pvs_trans]; auto; set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
78 79
Qed.

80 81
Lemma tac_pvs_elim_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P' P Q Φ :
  envs_lookup i Δ = Some (p, P')  P' = (|={E}=> P)%I 
82
  IsFSA Q E fsa fsaV Φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
83
  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' 
84
  (Δ'  fsa E Φ)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Proof.
86
  intros ? -> ??. rewrite (is_fsa Q) -fsa_pvs_fsa.
Robbert Krebbers's avatar
Robbert Krebbers committed
87 88 89 90
  eapply tac_pvs_elim; set_solver.
Qed.
End pvs.

91
Tactic Notation "iPvsIntro" := apply tac_pvs_intro; first try fast_done.
Robbert Krebbers's avatar
Robbert Krebbers committed
92 93 94 95

Tactic Notation "iPvsCore" constr(H) :=
  match goal with
  | |- _  |={_,_}=> _ =>
96
    eapply tac_pvs_elim with _ _ H _ _ _ _ _;
Robbert Krebbers's avatar
Robbert Krebbers committed
97
      [env_cbv; reflexivity || fail "iPvs:" H "not found"
98 99
      |let P := match goal with |- ?P = _ => P end in
       reflexivity || fail "iPvs:" H ":" P "not a pvs with the right mask"
100 101 102 103 104
      |first
         [left; split_and!;
            [reflexivity|reflexivity|try (rewrite (idemp_L ()); reflexivity)]
         |right; split; first reflexivity]
      |env_cbv; reflexivity|]
Robbert Krebbers's avatar
Robbert Krebbers committed
105
  | |- _ =>
106
    eapply tac_pvs_elim_fsa with _ _ _ _ H _ _ _ _;
Robbert Krebbers's avatar
Robbert Krebbers committed
107
      [env_cbv; reflexivity || fail "iPvs:" H "not found"
108 109
      |let P := match goal with |- ?P = _ => P end in
       reflexivity || fail "iPvs:" H ":" P "not a pvs with the right mask"
110
      |let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
111
       apply _ || fail "iPvs:" P "not a pvs"
Robbert Krebbers's avatar
Robbert Krebbers committed
112 113 114 115
      |env_cbv; reflexivity|simpl]
  end.

Tactic Notation "iPvs" open_constr(H) :=
116
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as "?").
Robbert Krebbers's avatar
Robbert Krebbers committed
117
Tactic Notation "iPvs" open_constr(H) "as" constr(pat) :=
118
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as pat).
119
Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1) ")"
Robbert Krebbers's avatar
Robbert Krebbers committed
120
    constr(pat) :=
121 122 123 124 125 126 127 128 129
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as ( x1 ) pat).
Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) ")" constr(pat) :=
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as ( x1 x2 ) pat).
Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as ( x1 x2 x3 ) pat).
Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
Robbert Krebbers's avatar
Robbert Krebbers committed
130
    constr(pat) :=
131
  iDestructHelp H as (fun H =>
132 133
    iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 ) pat).
Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
134
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
135
    simple_intropattern(x5) ")" constr(pat) :=
136
  iDestructHelp H as (fun H =>
137 138
    iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 ) pat).
Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
139
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
140
    simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
141
  iDestructHelp H as (fun H =>
142 143
    iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 ) pat).
Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
144
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
145
    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
Robbert Krebbers's avatar
Robbert Krebbers committed
146
    constr(pat) :=
147
  iDestructHelp H as (fun H =>
148 149
    iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
150 151
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
152
    simple_intropattern(x8) ")" constr(pat) :=
153
  iDestructHelp H as (fun H =>
154
    iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
155

156 157
Hint Extern 2 (of_envs _  _) =>
  match goal with |- _  (|={_}=> _)%I => iPvsIntro end.