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

Ralf Jung's avatar
Ralf Jung committed
5
Section tests.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
7
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

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

Robbert Krebbers's avatar
Robbert Krebbers committed
18
19
Lemma demo_2 P1 P2 P3 P4 Q (P5 : nat  PROP) `{!Affine P4, !Absorbing P2} :
  P2  (P3  Q)  True  P1  P2  (P4  ( x:nat, P5 x  P3))  emp -
20
21
    P1 - (True  True) -
  (((P2  False  P2  0 = 0)  P3)  Q  P1  True) 
22
     (P2  False)  (False  P5 0).
Robbert Krebbers's avatar
Robbert Krebbers committed
23
24
25
26
27
28
29
30
31
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".
Robbert Krebbers's avatar
Robbert Krebbers committed
32
33
  - iFrame "H3". iRight. auto.
  - iSplitL "HQ". iAssumption. by iSplitL "H1".
Robbert Krebbers's avatar
Robbert Krebbers committed
34
35
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
36
Lemma demo_3 P1 P2 P3 :
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
  P1  P2  P3 - P1   (P2   x, (P3  x = 0)  P3).
Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
39

Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
Definition foo (P : PROP) := (P - P)%I.
Definition bar : PROP := ( P, foo P)%I.
42

Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
Lemma test_unfold_constants : bar.
Proof. iIntros (P) "HP //". Qed.
45

Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
Lemma test_iRewrite {A : ofeT} (x y : A) P :
  ( z, P -  (z  y)) - (P - P  (x,x)  (y,x)).
48
49
Proof.
  iIntros "H1 H2".
Robbert Krebbers's avatar
Robbert Krebbers committed
50
  iRewrite (bi.internal_eq_sym x x with "[# //]").
51
  iRewrite -("H1" $! _ with "[- //]").
Robbert Krebbers's avatar
Robbert Krebbers committed
52
  auto.
53
54
Qed.

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

58
59
60
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ  ( φ   P   φ  ψ   P)%I.
Proof. iIntros (??) "H". auto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
61
Lemma test_fast_iIntros P Q :
62
63
  ( x y z : nat,
    x = plus 0 x  y = 0  z = 0  P   Q  foo (x  x))%I.
64
Proof.
65
  iIntros (a) "*".
66
  iIntros "#Hfoo **".
Robbert Krebbers's avatar
Robbert Krebbers committed
67
  iIntros "_ //".
68
Qed.
69

70
Lemma test_very_fast_iIntros P :
Robbert Krebbers's avatar
Robbert Krebbers committed
71
   x y : nat, ( x = y   P - P)%I.
72
73
Proof. by iIntros. Qed.

74
75
76
Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P - Q - R - Q.
Proof. iIntros "H1 H2 H3". iAssumption. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
77
Lemma test_iDestruct_spatial_and P Q1 Q2 : P  (Q1  Q2) - P  Q1.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Proof. iIntros "[H1 [H2 _]]". iFrame. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
79

Robbert Krebbers's avatar
Robbert Krebbers committed
80
Lemma test_iAssert_persistent P Q : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
82
83
84
85
86
87
88
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.
89

Robbert Krebbers's avatar
Robbert Krebbers committed
90
Lemma test_iSpecialize_auto_frame P Q R :
91
  (P - True - True - Q - R) - P - Q - R.
92
Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
93
94

(* Check coercions *)
Robbert Krebbers's avatar
Robbert Krebbers committed
95
Lemma test_iExist_coercion (P : Z  PROP) : ( x, P x) -  x, P x.
96
Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
97

98
99
100
101
102
103
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
104
105
106
107
108
109
110
111
112
113
Lemma test_iFrame_pure {A : ofeT} (φ : Prop) (y z : A) :
  φ   y  z - ( φ    φ   y  z : PROP).
Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.

Lemma test_iAssert_modality P :  False -  P.
Proof.
  iIntros "HF".
  iAssert ( False)%I with "[> -]" as %[].
  by iMod "HF".
Qed.
114

Robbert Krebbers's avatar
Robbert Krebbers committed
115
Lemma test_iAssumption_False P : False - P.
116
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
118

(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
119
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
120
121
122
123
124
  ( 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
125

Robbert Krebbers's avatar
Robbert Krebbers committed
126
127
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
  P - Q - R  R  Q  P  R  False.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
Proof. eauto with iFrame. Qed.
129

130
Lemma test_iCombine_persistent P Q R `{!Persistent R} :
Robbert Krebbers's avatar
Robbert Krebbers committed
131
  P - Q - R  R  Q  P  R  False.
132
Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
133

Robbert Krebbers's avatar
Robbert Krebbers committed
134
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
135
136
137
138
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
139

Robbert Krebbers's avatar
Robbert Krebbers committed
140
Lemma test_iNext_sep1 P Q
Robbert Krebbers's avatar
Robbert Krebbers committed
141
142
143
144
145
146
    (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.
147

Robbert Krebbers's avatar
Robbert Krebbers committed
148
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
149
150
151
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
152

Robbert Krebbers's avatar
Robbert Krebbers committed
153
Lemma test_iNext_quantifier {A} (Φ : A  A  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
154
155
156
  ( y,  x,  Φ x y) -  ( y,  x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
157
158
Lemma test_iFrame_persistent (P Q : PROP) :
   P - Q -  (P  P)  (P  Q  Q).
159
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
160

Robbert Krebbers's avatar
Robbert Krebbers committed
161
Lemma test_iSplit_persistently P Q :  P -  (P  P).
162
Proof. iIntros "#?". by iSplit. Qed.
Ralf Jung's avatar
Ralf Jung committed
163

Robbert Krebbers's avatar
Robbert Krebbers committed
164
Lemma test_iSpecialize_persistent P Q :  P - ( P  Q) - Q.
165
Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
167
168
169
170
171

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

173
Lemma test_iInduction_wf (x : nat) P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
174
   P - Q -  (x + 0 = x)%nat .
175
176
177
178
179
180
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.

181
Lemma test_iIntros_start_proof :
Robbert Krebbers's avatar
Robbert Krebbers committed
182
  (True : PROP)%I.
183
184
185
186
187
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
188
Lemma test_True_intros : (True : PROP) - True.
189
190
191
Proof.
  iIntros "?". done.
Qed.
192
193
194
195
196
197
198
199
200
201

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 :
Robbert Krebbers's avatar
Robbert Krebbers committed
202
203
   Q, let R := emp%I in P - R - Q - P  Q.
Proof. iIntros (Q R) "$ _ $". Qed.
204

Robbert Krebbers's avatar
Robbert Krebbers committed
205
206
Lemma test_iIntros_modalities `(!Absorbing P) :
  (    x : nat,  x = 0    x = 0  - False - P - P)%I.
207
208
209
210
211
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
Ralf Jung's avatar
Ralf Jung committed
212
End tests.