proofmode.v 11 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) "? {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
Proof. iIntros "[H [? _]]". by iFrame. Qed.
102

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". iFrame (Hv) "Hxy". Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
106

107 108 109 110 111 112
Lemma test_iFrame_disjunction_1 P1 P2 Q1 Q2 :
   P1 - Q2 - P2 - (P1  P2  False  P2)  (Q1  Q2).
Proof. iIntros "#HP1 HQ2 HP2". iFrame "HP1 HQ2 HP2". Qed.
Lemma test_iFrame_disjunction_2 P : P - (True  True)  P.
Proof. iIntros "HP". iFrame "HP". auto. Qed.

113 114 115 116 117 118 119
Lemma test_iFrame_conjunction_1 P Q :
  P - Q - (P  Q)  (P  Q).
Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
Lemma test_iFrame_conjunction_2 P Q :
  P - Q - (P  P)  (Q  Q).
Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
120
Lemma test_iAssert_persistent P Q : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
121 122 123 124 125 126 127 128
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.
129

Robbert Krebbers's avatar
Robbert Krebbers committed
130
Lemma test_iSpecialize_auto_frame P Q R :
131
  (P - True - True - Q - R) - P - Q - R.
132
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
133 134

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

138 139 140 141 142 143
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
144
Lemma test_iAssert_modality P : (|==> False) - |==> P.
145
Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
146

Robbert Krebbers's avatar
Robbert Krebbers committed
147
Lemma test_iAssumption_False P : False - P.
148
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
149 150

(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
151
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  uPred M) :
Robbert Krebbers's avatar
Robbert Krebbers committed
152 153 154 155 156
  ( 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
157

Robbert Krebbers's avatar
Robbert Krebbers committed
158
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
Robbert Krebbers's avatar
Robbert Krebbers committed
159
  P - Q - R - R  Q  P  R  False.
160
Proof. eauto 10 with iFrame. Qed.
161

162
Lemma test_iCombine_persistent P Q R `{!Persistent R} :
163 164
  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
165

Robbert Krebbers's avatar
Robbert Krebbers committed
166
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
167 168 169 170
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
171

Robbert Krebbers's avatar
Robbert Krebbers committed
172
Lemma test_iNext_sep1 P Q
Robbert Krebbers's avatar
Robbert Krebbers committed
173 174 175 176 177 178
    (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.
179

Robbert Krebbers's avatar
Robbert Krebbers committed
180
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
181 182 183
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
184

Robbert Krebbers's avatar
Robbert Krebbers committed
185 186 187 188
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
189
Lemma test_iFrame_persistent (P Q : uPred M) :
190 191
   P - Q -  (P  P)  (P  Q  Q).
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
192

193
Lemma test_iSplit_persistently P Q :  P -  (P  P).
194
Proof. iIntros "#?". by iSplit. Qed.
Ralf Jung's avatar
Ralf Jung committed
195

Robbert Krebbers's avatar
Robbert Krebbers committed
196
Lemma test_iSpecialize_persistent P Q :
197 198
   P - ( P - Q) - Q.
Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
199 200 201 202 203 204

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

206 207 208 209 210 211 212 213
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.

214 215 216 217 218 219 220 221 222 223 224
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.
225 226 227 228 229 230 231 232 233 234 235 236

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.
237 238 239 240 241 242 243 244

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.
245 246 247 248

Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
  x1 = x2  ( x2 = x3    x3  x4   P) -  x1 = x4   P.
Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
249

Robbert Krebbers's avatar
Robbert Krebbers committed
250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_1 (φ : Prop) :
  φ  ( _ : φ, False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_forall_nondep_2 (φ : Prop) :
  φ  ( _ : φ, False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_forall_nondep_3 (φ : Prop) :
  φ  ( _ : φ, False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_forall_nondep_4 (φ : Prop) :
  φ  ( _ : φ, False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.

Lemma test_pure_impl_1 (φ : Prop) :
  φ  (⌜φ⌝  False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_pure_impl_2 (φ : Prop) :
  φ  (⌜φ⌝  False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_pure_impl_3 (φ : Prop) :
  φ  (⌜φ⌝  False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_pure_impl_4 (φ : Prop) :
  φ  (⌜φ⌝  False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.

Lemma test_forall_nondep_impl2 (φ : Prop) P :
  φ  P - ( _ : φ, P - False : uPred M) - False.
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Lemma test_pure_impl2 (φ : Prop) P :
  φ  P - (⌜φ⌝  P - False : uPred M) - False.
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
294 295 296 297 298 299 300
Lemma test_iNext_laterN_later P n :  ^n P  ^n  P.
Proof. iIntros "H". iNext. by iNext. Qed.
Lemma test_iNext_later_laterN P n : ^n  P   ^n P.
Proof. iIntros "H". iNext. by iNext. Qed.
Lemma test_iNext_laterN_laterN P n1 n2 :  ^n1 ^n2 P  ^n1 ^n2  P.
Proof. iIntros "H". iNext. iNext. by iNext. Qed.

301 302 303 304 305 306 307
Lemma test_iEval x y :  (y + x)%nat = 1  -  S (x + y) = 2%nat  : uPred M.
Proof.
  iIntros (H).
  iEval (rewrite (Nat.add_comm x y) // H).
  done.
Qed.

308 309 310 311 312 313
(* 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
314
End tests.
Robbert Krebbers's avatar
Robbert Krebbers committed
315 316 317 318 319 320 321 322 323 324 325 326 327 328

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.