proofmode.v 8.18 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.proofmode Require Import tactics.
2
From iris.base_logic.lib Require Import invariants.
3
From stdpp Require Import gmap.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5

Ralf Jung's avatar
Ralf Jung committed
6
7
Section tests.
Context {M : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
Implicit Types P Q R : uPred M.

Lemma demo_0 P Q :  (P  Q) - ( x, x = 0  x = 1)  (Q  P).
11
Proof.
12
  iIntros "###H #H2".
13
  (* should remove the disjunction "H" *)
14
  iDestruct "H" as "[#?|#?]"; last by iLeft.
15
16
17
18
  (* should keep the disjunction "H" because it is instantiated *)
  iDestruct ("H2" $! 10) as "[%|%]". done. done.
Qed.

Ralf Jung's avatar
Ralf Jung committed
19
Lemma demo_1 (P1 P2 P3 : nat  uPred M) :
20
  ( (x y : nat) a b,
Robbert Krebbers's avatar
Robbert Krebbers committed
21
    x  y 
22
23
24
     (uPred_ownM (a  b) -
    ( y1 y2 c, P1 ((x + y1) + y2)  True   uPred_ownM c) -
      ( z, P2 z  True  P2 z) -
Ralf Jung's avatar
Ralf Jung committed
25
     ( n m : nat, P1 n   ((True  P2 n)   (n = n  P3 n))) -
26
     x = 0   x z,  P3 (x + z)  uPred_ownM b  uPred_ownM (core b)))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
  iIntros (i [|j] a b ?) "!# [Ha Hb] H1 #H2 H3"; setoid_subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
  { iLeft. by iNext. }
  iRight.
31
  iDestruct "H1" as (z1 z2 c) "(H1&_&#Hc)".
32
  iPoseProof "Hc" as "foo".
33
  iRevert (a b) "Ha Hb". iIntros (b a) "Hb {foo} Ha".
34
  iAssert (uPred_ownM (a  core a)) with "[Ha]" as "[Ha #Hac]".
Robbert Krebbers's avatar
Robbert Krebbers committed
35
  { by rewrite cmra_core_r. }
36
  iIntros "{$Hac $Ha}".
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
  iExists (S j + z1), z2.
  iNext.
39
  iApply ("H3" $! _ 0 with "[$]").
40
  - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
43
  - done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
44
Lemma demo_2 P1 P2 P3 P4 Q (P5 : nat  uPredC M):
45
46
47
  P2  (P3  Q)  True  P1  P2  (P4  ( x:nat, P5 x  P3))  True -
    P1 - (True  True) -
  (((P2  False  P2  0 = 0)  P3)  Q  P1  True) 
48
     (P2  False)  (False  P5 0).
Robbert Krebbers's avatar
Robbert Krebbers committed
49
50
51
52
53
54
55
56
57
58
59
Proof.
  (* Intro-patterns do something :) *)
  iIntros "[H2 ([H3 HQ]&?&H1&H2'&foo&_)] ? [??]".
  (* To test destruct: can also be part of the intro-pattern *)
  iDestruct "foo" as "[_ meh]".
  repeat iSplit; [|by iLeft|iIntros "#[]"].
  iFrame "H2".
  (* split takes a list of hypotheses just for the LHS *)
  iSplitL "H3".
  * iFrame "H3". by iRight.
  * iSplitL "HQ". iAssumption. by iSplitL "H1".
Robbert Krebbers's avatar
Robbert Krebbers committed
60
61
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
62
Lemma demo_3 P1 P2 P3 :
63
  P1  P2  P3 -  P1   (P2   x, (P3  x = 0)  P3).
64
65
Proof. iIntros "($ & $ & H)". iFrame "H". iNext. by iExists 0. Qed.

Ralf Jung's avatar
Ralf Jung committed
66
67
Definition foo (P : uPred M) := (P  P)%I.
Definition bar : uPred M := ( P, foo P)%I.
68

Robbert Krebbers's avatar
Robbert Krebbers committed
69
Lemma test_unfold_constants : True - bar.
70
Proof. iIntros. iIntros (P) "HP //". Qed.
71

Robbert Krebbers's avatar
Robbert Krebbers committed
72
Lemma test_iRewrite (x y : M) P :
73
  ( z, P  z  y) - (P - (x,x)  (y,x)).
74
75
Proof.
  iIntros "H1 H2".
76
77
  iRewrite (uPred.internal_eq_sym x x with "[# //]").
  iRewrite -("H1" $! _ with "[- //]").
78
  done.
79
80
Qed.

81
Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P  Q  P  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
83
Proof. iIntros "H1 H2". by iFrame. Qed.

84
85
86
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ  ( φ   P   φ  ψ   P)%I.
Proof. iIntros (??) "H". auto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
87
Lemma test_fast_iIntros P Q :
88
89
  ( x y z : nat,
    x = plus 0 x  y = 0  z = 0  P   Q  foo (x  x))%I.
90
Proof.
91
  iIntros (a) "*".
92
  iIntros "#Hfoo **".
93
  iIntros "# _ //".
94
Qed.
95

96
97
98
99
Lemma test_very_fast_iIntros P :
   x y : nat,  x = y  - P - P.
Proof. by iIntros. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
100
Lemma test_iDestruct_spatial_and P Q1 Q2 : P  (Q1  Q2) - P  Q1.
101
102
Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
103
Lemma test_iFrame_pure (x y z : M) :
104
   x  y  z - ( x   x  y  z : uPred M).
105
Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
106

Robbert Krebbers's avatar
Robbert Krebbers committed
107
Lemma test_iAssert_persistent P Q : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
109
110
111
112
113
114
115
Proof.
  iIntros "HP HQ".
  iAssert True%I as "#_". { by iClear "HP HQ". }
  iAssert True%I with "[HP]" as "#_". { Fail iClear "HQ". by iClear "HP". }
  iAssert True%I as %_. { by iClear "HP HQ". }
  iAssert True%I with "[HP]" as %_. { Fail iClear "HQ". by iClear "HP". }
  done.
Qed.
116

Robbert Krebbers's avatar
Robbert Krebbers committed
117
Lemma test_iSpecialize_auto_frame P Q R :
118
  (P - True - True - Q - R) - P - Q - R.
119
Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
120
121

(* Check coercions *)
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Lemma test_iExist_coercion (P : Z  uPred M) : ( x, P x) -  x, P x.
123
Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
124

125
126
127
128
129
130
Lemma test_iExist_tc `{Collection A C} P : ( x1 x2 : gset positive, P - P)%I.
Proof. iExists {[ 1%positive ]}, . auto. Qed.

Lemma test_iSpecialize_tc P : ( x y z : gset positive, P) - P.
Proof. iIntros "H". iSpecialize ("H" $!  {[ 1%positive ]} ). done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
131
Lemma test_iAssert_modality P : (|==> False) - |==> P.
132
Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
133

Robbert Krebbers's avatar
Robbert Krebbers committed
134
Lemma test_iAssumption_False P : False - P.
135
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
137

(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
138
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  uPred M) :
Robbert Krebbers's avatar
Robbert Krebbers committed
139
140
141
142
143
  ( n v, P n v) -  n v, P n v.
Proof.
  iIntros "H". iExists _, [#10].
  iSpecialize ("H" $! _ [#10]). done.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
144

145
Lemma test_eauto_iFramE P Q R `{!Persistent R} :
Robbert Krebbers's avatar
Robbert Krebbers committed
146
147
  P - Q - R - R  Q  P  R  False.
Proof. eauto with iFrame. Qed.
148

149
Lemma test_iCombine_persistent P Q R `{!Persistent R} :
150
151
  P - Q - R - R  Q  P  R  False.
Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
152

Robbert Krebbers's avatar
Robbert Krebbers committed
153
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
154
155
156
157
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
158

Robbert Krebbers's avatar
Robbert Krebbers committed
159
Lemma test_iNext_sep1 P Q
Robbert Krebbers's avatar
Robbert Krebbers committed
160
161
162
163
164
165
    (R1 := (P  Q)%I) (R2 := ( P   Q)%I) :
  ( P   Q)  R1  R2 -  (P  Q)   R1  R2.
Proof.
  iIntros "H". iNext.
  rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
Qed.
166

Robbert Krebbers's avatar
Robbert Krebbers committed
167
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
168
169
170
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
171

Robbert Krebbers's avatar
Robbert Krebbers committed
172
173
174
175
Lemma test_iNext_quantifier (Φ : M  M  uPred M) :
  ( y,  x,  Φ x y) -  ( y,  x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
176
Lemma test_iFrame_persistent (P Q : uPred M) :
177
178
   P - Q -  (P  P)  (P  Q  Q).
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
179

180
Lemma test_iSplit_persistently P Q :  P -  (P  P).
181
Proof. iIntros "#?". by iSplit. Qed.
Ralf Jung's avatar
Ralf Jung committed
182

Robbert Krebbers's avatar
Robbert Krebbers committed
183
Lemma test_iSpecialize_persistent P Q :
184
185
   P - ( P - Q) - Q.
Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
187
188
189
190
191

Lemma test_iLöb P : ( n, ^n P)%I.
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
192

193
194
195
196
197
198
199
200
Lemma test_iInduction_wf (x : nat) P Q :
   P - Q -  (x + 0 = x)%nat .
Proof.
  iIntros "#HP HQ".
  iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
  rewrite (inj_iff S). by iApply ("IH" with "[%]"); first omega.
Qed.

201
202
203
204
205
206
207
208
209
210
211
Lemma test_iIntros_start_proof :
  (True : uPred M)%I.
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.

Lemma test_True_intros : (True : uPred M) - True.
Proof.
  iIntros "?". done.
Qed.
212
213
214
215
216
217
218
219
220
221
222
223

Lemma test_iPoseProof_let P Q :
  (let R := True%I in R  P  Q) 
  P  Q.
Proof.
  iIntros (help) "HP".
  iPoseProof (help with "[$HP]") as "?". done.
Qed.

Lemma test_iIntros_let P :
   Q, let R := True%I in P - R - Q - P  Q.
Proof. iIntros (Q R) "$ HR $". Qed.
224
225
226
227
228
229
230
231

Lemma test_iIntros_modalities P :
  (   x : nat,  x = 0  -  x = 0   False - P - P)%I.
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
232
233
234
235

Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
  x1 = x2  ( x2 = x3    x3  x4   P) -  x1 = x4   P.
Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
236
237
238
239
240
241
242

(* TODO: This test is broken in Coq 8.6. Should be restored once we drop Coq
8.6 support. See also issue #108. *)
(*
Lemma test_iIntros_pure : (⌜ ¬False ⌝ : uPred M)%I.
Proof. by iIntros (?). Qed.
*)
Ralf Jung's avatar
Ralf Jung committed
243
End tests.
Robbert Krebbers's avatar
Robbert Krebbers committed
244
245
246
247
248
249
250
251
252
253
254
255
256
257

Section more_tests.
  Context `{invG Σ}.
  Implicit Types P Q R : iProp Σ.

  Lemma test_masks  N E P Q R :
    N  E 
    (True - P - inv N Q - True - R) - P -  Q ={E}= R.
  Proof.
    iIntros (?) "H HP HQ".
    iApply ("H" with "[% //] [$] [> HQ] [> //]").
    by iApply inv_alloc.
  Qed.
End more_tests.