proofmode_monpred.v 7 KB
Newer Older
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1
From iris.proofmode Require Import tactics monpred.
2
From iris.base_logic.lib Require Import invariants.
Ralf Jung's avatar
Ralf Jung committed
3
Unset Printing Use Implicit Types. (* FIXME: remove once we drop support for Coq <=8.11. *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
4
5

Section tests.
6
  Context {I : biIndex} {PROP : bi}.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
7
8
9
  Local Notation monPred := (monPred I PROP).
  Local Notation monPredI := (monPredI I PROP).
  Implicit Types P Q R : monPred.
10
  Implicit Types 𝓟 𝓠 𝓡 : PROP.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
11
12
13
14
15
16
17
18
19
20
  Implicit Types i j : I.

  Lemma test0 P : P - P.
  Proof. iIntros "$". Qed.

  Lemma test_iStartProof_1 P : P - P.
  Proof. iStartProof. iStartProof. iIntros "$". Qed.
  Lemma test_iStartProof_2 P : P - P.
  Proof. iStartProof monPred. iStartProof monPredI. iIntros "$". Qed.
  Lemma test_iStartProof_3 P : P - P.
21
  Proof. iStartProof monPredI. iStartProof monPredI. iIntros "$". Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
22
  Lemma test_iStartProof_4 P : P - P.
23
  Proof. iStartProof monPredI. iStartProof monPred. iIntros "$". Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
24
25
26
27
  Lemma test_iStartProof_5 P : P - P.
  Proof. iStartProof PROP. iIntros (i) "$". Qed.
  Lemma test_iStartProof_6 P : P  P.
  Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "$". Qed.
28
  Lemma test_iStartProof_7 `{!BiInternalEq PROP} P : @{monPredI} P  P.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
29
30
  Proof. iStartProof PROP. done. Qed.

31
32
  Lemma test_intowand_1 P Q : (P - Q) - P - Q.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
33
34
    iStartProof PROP. iIntros (i) "HW". Show.
    iIntros (j ->) "HP". Show. by iApply "HW".
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
  Qed.
  Lemma test_intowand_2 P Q : (P - Q) - P - Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "[HP //]"). done.
  Qed.
  Lemma test_intowand_3 P Q : (P - Q) - P - Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "HP"). done.
  Qed.
  Lemma test_intowand_4 P Q : (P - Q) -  P -  Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP". by iApply "HW".
  Qed.
  Lemma test_intowand_5 P Q : (P - Q) -  P -  Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "HP"). done.
  Qed.
55

56
57
  Lemma test_apply_in_elim (P : monPredI) (i : I) : monPred_in i -  P i   P.
  Proof. iIntros. by iApply monPred_in_elim. Qed.
58
59
60
61
62
63
64
65
66

  Lemma test_iStartProof_forall_1 (Φ : nat  monPredI) :  n, Φ n - Φ n.
  Proof.
    iStartProof PROP. iIntros (n i) "$".
  Qed.
  Lemma test_iStartProof_forall_2 (Φ : nat  monPredI) :  n, Φ n - Φ n.
  Proof.
    iStartProof. iIntros (n) "$".
  Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
67
68
69
70
71

  Lemma test_embed_wand (P Q : PROP) : (P - Q) - P - Q : monPred.
  Proof.
    iIntros "H HP". by iApply "H".
  Qed.
72

Robbert Krebbers's avatar
Robbert Krebbers committed
73
  Lemma test_objectively P Q : <obj> emp - <obj> P - <obj> Q - <obj> (P  Q).
Ralf Jung's avatar
Ralf Jung committed
74
  Proof. iIntros "#? HP HQ". iModIntro. by iSplitL "HP". Qed.
75

76
  Lemma test_objectively_absorbing P Q R `{!Absorbing P} :
Robbert Krebbers's avatar
Robbert Krebbers committed
77
    <obj> emp - <obj> P - <obj> Q - R - <obj> (P  Q).
Ralf Jung's avatar
Ralf Jung committed
78
  Proof. iIntros "#? HP HQ HR". iModIntro. by iSplitL "HP". Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
79

80
  Lemma test_objectively_affine P Q R `{!Affine R} :
Robbert Krebbers's avatar
Robbert Krebbers committed
81
    <obj> emp - <obj> P - <obj> Q - R - <obj> (P  Q).
Ralf Jung's avatar
Ralf Jung committed
82
  Proof. iIntros "#? HP HQ HR". iModIntro. by iSplitL "HP". Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
83

84
85
  Lemma test_iModIntro_embed P `{!Affine Q} 𝓟 𝓠 :
     P - Q - ⎡𝓟⎤ - ⎡𝓠⎤ -  𝓟  𝓠 .
Ralf Jung's avatar
Ralf Jung committed
86
  Proof. iIntros "#H1 _ H2 H3". iModIntro. iFrame. Qed.
87

88
  Lemma test_iModIntro_embed_objective P `{!Objective Q} 𝓟 𝓠 :
89
     P - Q - ⎡𝓟⎤ - ⎡𝓠⎤ -   i, 𝓟  𝓠  Q i .
Ralf Jung's avatar
Ralf Jung committed
90
  Proof. iIntros "#H1 H2 H3 H4". iModIntro. Show. iFrame. Qed.
91

92
93
94
95
  Lemma test_iModIntro_embed_nested P 𝓟 𝓠 :
     P - ⎡◇ 𝓟⎤ - ⎡◇ 𝓠⎤ -   (𝓟  𝓠) .
  Proof. iIntros "#H1 H2 H3". iModIntro  _ %I. by iSplitL "H2". Qed.

96
97
  Lemma test_into_wand_embed 𝓟 𝓠 :
    (𝓟 -  𝓠) 
Ralf Jung's avatar
Ralf Jung committed
98
    ⎡𝓟⎤ @{monPredI}  ⎡𝓠⎤.
99
100
101
102
103
104
105
106
107
  Proof.
    iIntros (HPQ) "HP".
    iMod (HPQ with "[-]") as "$"; last by auto.
    iAssumption.
  Qed.

  (* This is a hack to avoid avoid coq bug #5735: sections variables ignore hint
     modes. So we assume the instances in a way that cannot be used by type
     class resolution, and then separately declare the instance as such. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
108
109
  Context (FU0 : BiFUpd PROP * unit).
  Instance FU : BiFUpd PROP := fst FU0.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
110
111
112

  Lemma test_apply_fupd_intro_mask E1 E2 P :
    E2  E1  P - |={E1,E2}=> |={E2,E1}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
  Proof. iIntros. by iApply @fupd_intro_mask. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
114
115
  Lemma test_apply_fupd_intro_mask_2 E1 E2 P :
    E2  E1  P - |={E1,E2}=> |={E2,E1}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
  Proof. iIntros. iFrame. by iApply @fupd_intro_mask'. Qed.
117
118
119
120
121
122
123

  Lemma test_iFrame_embed_persistent (P : PROP) (Q: monPred) :
    Q   P  Q  P  P.
  Proof.
    iIntros "[$ #HP]". iFrame "HP".
  Qed.

124
  Lemma test_iNext_Bi P :
125
     P @{monPredI}  P.
126
127
128
  Proof. iIntros "H". by iNext. Qed.

  (** Test monPred_at framing *)
129
130
131
132
  Lemma test_iFrame_monPred_at_wand (P Q : monPred) i :
    P i - (Q - P) i.
  Proof. iIntros "$". Show. Abort.

133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
  Program Definition monPred_id (R : monPred) : monPred :=
    MonPred (λ V, R V) _.
  Next Obligation. intros ? ???. eauto. Qed.

  Lemma test_iFrame_monPred_id (Q R : monPred) i :
    Q i  R i - (Q  monPred_id R) i.
  Proof.
    iIntros "(HQ & HR)". iFrame "HR". iAssumption.
  Qed.

  Lemma test_iFrame_rel P i j ij :
    IsBiIndexRel i ij  IsBiIndexRel j ij 
    P i - P j - P ij  P ij.
  Proof. iIntros (??) "HPi HPj". iFrame. Qed.

  Lemma test_iFrame_later_rel `{!BiAffine PROP} P i j :
    IsBiIndexRel i j 
     (P i) - ( P) j.
  Proof. iIntros (?) "?". iFrame. Qed.

  Lemma test_iFrame_laterN n P i :
    ^n (P i) - (^n P) i.
  Proof. iIntros "?". iFrame. Qed.

  Lemma test_iFrame_quantifiers P i :
    P i - ( _:(),  _:(), P) i.
  Proof. iIntros "?". iFrame. Show. iIntros ([]). iExists (). iEmpIntro. Qed.

  Lemma test_iFrame_embed (P : PROP) i :
    P - (embed (B:=monPredI) P) i.
  Proof. iIntros "$". Qed.

  (* Make sure search doesn't diverge on an evar *)
  Lemma test_iFrame_monPred_at_evar (P : monPred) i j :
    P i -  Q, (Q j).
  Proof. iIntros "HP". iExists _. Fail iFrame "HP". Abort.
169

170
End tests.
171
172
173
174
175

Section tests_iprop.
  Context {I : biIndex} `{!invG Σ}.

  Local Notation monPred := (monPred I (iPropI Σ)).
176
177
  Implicit Types P Q R : monPred.
  Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.
178

179
180
  Lemma test_iInv_0 N 𝓟 :
    embed (B:=monPred) (inv N (<pers> 𝓟)) ={}= ⎡▷ 𝓟⎤.
181
182
183
184
185
186
  Proof.
    iIntros "#H".
    iInv N as "#H2". Show.
    iModIntro. iSplit=>//. iModIntro. iModIntro; auto.
  Qed.

187
188
  Lemma test_iInv_0_with_close N 𝓟 :
    embed (B:=monPred) (inv N (<pers> 𝓟)) ={}= ⎡▷ 𝓟⎤.
189
190
191
192
193
194
  Proof.
    iIntros "#H".
    iInv N as "#H2" "Hclose". Show.
    iMod ("Hclose" with "H2").
    iModIntro. iModIntro. by iNext.
  Qed.
195
196
197
198
199
200
201
202

  Lemma test_iPoseProof `{inG Σ A} P γ (x y : A) :
    x ~~> y  P  own γ x == own γ y.
  Proof.
    iIntros (?) "[_ Hγ]".
    iPoseProof (own_update with "Hγ") as "H"; first done.
    by iMod "H".
  Qed.
203
End tests_iprop.