pviewshifts.v 8.09 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 12
Global Instance to_assumption_pvs E p P Q :
  ToAssumption p P Q  ToAssumption p P (|={E}=> Q)%I.
Proof. rewrite /ToAssumption=>->. apply pvs_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14 15 16 17 18 19 20 21 22 23
Global Instance sep_split_pvs E P Q1 Q2 :
  SepSplit P Q1 Q2  SepSplit (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
Proof. rewrite /SepSplit=><-. apply pvs_sep. Qed.
Global Instance or_split_pvs E1 E2 P Q1 Q2 :
  OrSplit P Q1 Q2  OrSplit (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
Proof. rewrite /OrSplit=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
Global Instance exists_split_pvs {A} E1 E2 P (Φ : A  iProp Λ Σ) :
  ExistSplit P Φ  ExistSplit (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
Proof.
  rewrite /ExistSplit=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
24 25
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
26 27
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
Global Instance to_wand_pvs E1 E2 R P Q :
28
  ToWand R P Q  ToWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
29 30 31 32
Proof. rewrite /ToWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.

Class FSASplit {A} (P : iProp Λ Σ) (E : coPset)
    (fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A  iProp Λ Σ) := {
33
  fsa_split : fsa E Φ  P;
34
  fsa_split_is_fsa :> FrameShiftAssertion fsaV fsa;
Robbert Krebbers's avatar
Robbert Krebbers committed
35 36 37 38 39
}.
Global Arguments fsa_split {_} _ _ _ _ _ {_}.
Global Instance fsa_split_pvs E P :
  FSASplit (|={E}=> P)%I E pvs_fsa True (λ _, P).
Proof. split. done. apply _. Qed.
40 41 42
Global Instance fsa_split_fsa {A} (fsa : FSA Λ Σ A) E Φ :
  FrameShiftAssertion fsaV fsa  FSASplit (fsa E Φ) E fsa fsaV Φ.
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
43

44 45 46 47 48 49 50
Global Instance to_assert_pvs {A} P Q E (fsa : FSA Λ Σ A) fsaV Φ :
  FSASplit Q E fsa fsaV Φ  ToAssert P Q (|={E}=> P).
Proof.
  intros.
  by rewrite /ToAssert pvs_frame_r wand_elim_r -(fsa_split Q) fsa_pvs_fsa.
Qed.

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

54 55 56 57
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
58
  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' 
59
  (Δ' ={E2,E3}=> Q)  Δ ={E1,E3}=> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Proof.
61 62 63 64
  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
65 66
Qed.

67 68 69
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 
  FSASplit Q E fsa fsaV Φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
70
  envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' 
71
  (Δ'  fsa E Φ)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Proof.
73
  intros ? -> ??. rewrite -(fsa_split Q) -fsa_pvs_fsa.
Robbert Krebbers's avatar
Robbert Krebbers committed
74 75 76 77 78 79
  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 Δ' 
80
  (Δ' ={E1,E2}=> Q)  Δ ={E1,E2}=> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82
Proof.
  intros ??? HQ. rewrite envs_simple_replace_sound //; simpl.
83 84
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86 87 88 89 90
Qed.

Lemma tac_pvs_timeless_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P Q Φ :
  FSASplit Q E fsa fsaV Φ 
  envs_lookup i Δ = Some (p,  P)%I  TimelessP P 
  envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ' 
91
  (Δ'  fsa E Φ)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
92 93 94 95 96 97
Proof.
  intros ????. rewrite -(fsa_split Q) -fsa_pvs_fsa.
  eauto using tac_pvs_timeless.
Qed.
End pvs.

98
Tactic Notation "iPvsIntro" := apply tac_pvs_intro; first try fast_done.
Robbert Krebbers's avatar
Robbert Krebbers committed
99 100 101 102

Tactic Notation "iPvsCore" constr(H) :=
  match goal with
  | |- _  |={_,_}=> _ =>
103
    eapply tac_pvs_elim with _ _ H _ _ _ _ _;
Robbert Krebbers's avatar
Robbert Krebbers committed
104
      [env_cbv; reflexivity || fail "iPvs:" H "not found"
105 106
      |let P := match goal with |- ?P = _ => P end in
       reflexivity || fail "iPvs:" H ":" P "not a pvs with the right mask"
107 108 109 110 111
      |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
112
  | |- _ =>
113
    eapply tac_pvs_elim_fsa with _ _ _ _ H _ _ _ _;
Robbert Krebbers's avatar
Robbert Krebbers committed
114
      [env_cbv; reflexivity || fail "iPvs:" H "not found"
115 116
      |let P := match goal with |- ?P = _ => P end in
       reflexivity || fail "iPvs:" H ":" P "not a pvs with the right mask"
Robbert Krebbers's avatar
Robbert Krebbers committed
117
      |let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
118
       apply _ || fail "iPvs:" P "not a pvs"
Robbert Krebbers's avatar
Robbert Krebbers committed
119 120 121 122
      |env_cbv; reflexivity|simpl]
  end.

Tactic Notation "iPvs" open_constr(H) :=
123
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as "?").
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Tactic Notation "iPvs" open_constr(H) "as" constr(pat) :=
125
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
126 127
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1) "}"
    constr(pat) :=
128
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
129 130
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) "}" constr(pat) :=
131
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
132 133
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
134
  iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 x3 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
135 136 137
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
    constr(pat) :=
138
  iDestructHelp H as (fun H =>
139
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
140 141 142
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) "}" constr(pat) :=
143
  iDestructHelp H as (fun H =>
144
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
145 146 147
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
148
  iDestructHelp H as (fun H =>
149
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
150 151 152 153
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
    constr(pat) :=
154
  iDestructHelp H as (fun H =>
155
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
156 157 158 159
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
    simple_intropattern(x8) "}" constr(pat) :=
160
  iDestructHelp H as (fun H =>
161
    iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182

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 |- FSASplit ?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.