pviewshifts.v 8.05 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 13 14 15
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
16
Global Instance or_split_pvs E1 E2 P Q1 Q2 :
17 18
  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
19
Global Instance exists_split_pvs {A} E1 E2 P (Φ : A  iProp Λ Σ) :
20
  FromExist P Φ  FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
Proof.
22
  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Robbert Krebbers's avatar
Robbert Krebbers committed
23
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
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
27 28 29
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
30

31
Class IsFSA {A} (P : iProp Λ Σ) (E : coPset)
Robbert Krebbers's avatar
Robbert Krebbers committed
32
    (fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A  iProp Λ Σ) := {
33 34
  is_fsa : P  fsa E Φ;
  is_fsa_is_fsa :> FrameShiftAssertion fsaV fsa;
Robbert Krebbers's avatar
Robbert Krebbers committed
35
}.
36 37 38
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
39
Proof. split. done. apply _. Qed.
40 41
Global Instance is_fsa_fsa {A} (fsa : FSA Λ Σ A) E Φ :
  FrameShiftAssertion fsaV fsa  IsFSA (fsa E Φ) E fsa fsaV Φ.
42
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
43

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

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

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

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

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

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

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

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

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 _ _ _;
172
       [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
173 174 175 176 177 178 179 180 181
        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.