proofmode.v 6.93 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.

Robbert Krebbers's avatar
Robbert Krebbers committed
81
82
83
Lemma test_iIntros_persistent P Q `{!PersistentP Q} : (P  Q  P  Q)%I.
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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
99
Lemma test_iFrame_pure (x y z : M) :
100
   x  y  z - ( x   x  y  z : uPred M).
101
Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
102

Robbert Krebbers's avatar
Robbert Krebbers committed
103
Lemma test_iAssert_persistent P Q : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
106
107
108
109
110
111
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.
112

Robbert Krebbers's avatar
Robbert Krebbers committed
113
Lemma test_iSpecialize_auto_frame P Q R :
114
  (P - True - True - Q - R) - P - Q - R.
115
Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
116
117

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

121
122
123
124
125
126
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
127
Lemma test_iAssert_modality P : (|==> False) - |==> P.
128
Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
129

Robbert Krebbers's avatar
Robbert Krebbers committed
130
Lemma test_iAssumption_False P : False - P.
131
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
133

(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
134
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  uPred M) :
Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
137
138
139
  ( 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
140

Robbert Krebbers's avatar
Robbert Krebbers committed
141
Lemma test_eauto_iFramE P Q R `{!PersistentP R} :
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
  P - Q - R - R  Q  P  R  False.
Proof. eauto with iFrame. Qed.
144

Robbert Krebbers's avatar
Robbert Krebbers committed
145
Lemma test_iCombine_persistent P Q R `{!PersistentP R} :
146
147
  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
148

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

Robbert Krebbers's avatar
Robbert Krebbers committed
155
Lemma test_iNext_sep1 P Q
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
158
159
160
161
    (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.
162

Robbert Krebbers's avatar
Robbert Krebbers committed
163
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
164
165
166
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
167

Robbert Krebbers's avatar
Robbert Krebbers committed
168
169
170
171
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
172
Lemma test_iFrame_persistent (P Q : uPred M) :
173
174
   P - Q -  (P  P)  (P  Q  Q).
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
175

Robbert Krebbers's avatar
Robbert Krebbers committed
176
Lemma test_iSplit_always P Q :  P -  (P  P).
177
Proof. iIntros "#?". by iSplit. Qed.
Ralf Jung's avatar
Ralf Jung committed
178

Robbert Krebbers's avatar
Robbert Krebbers committed
179
Lemma test_iSpecialize_persistent P Q :
180
181
   P - ( P - Q) - Q.
Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
183
184
185
186
187

Lemma test_iLöb P : ( n, ^n P)%I.
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
188
189
190
191
192
193
194
195
196
197
198
199

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.
Ralf Jung's avatar
Ralf Jung committed
200
End tests.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
202
203
204
205
206
207
208
209
210
211
212
213
214

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.