proofmode.v 6.22 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
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
4

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

Lemma demo_0 P Q :  (P  Q) - ( x, x = 0  x = 1)  (Q  P).
10
Proof.
11
  iIntros "###H #H2".
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.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
43
Lemma demo_2 P1 P2 P3 P4 Q (P5 : nat  uPredC M):
44
45
46
  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) 
47
     (P2  False)  (False  P5 0).
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
50
51
52
53
54
55
56
57
58
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
59
60
Qed.

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

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

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

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

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

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

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

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
123
Lemma test_iAssumption_False P : False - P.
124
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
126

(* Check instantiation and dependent types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Lemma test_iSpecialize_dependent_type (P :  n, vec nat n  uPred M) :
Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
130
131
132
  ( 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
133

Robbert Krebbers's avatar
Robbert Krebbers committed
134
Lemma test_eauto_iFramE P Q R `{!PersistentP R} :
Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
  P - Q - R - R  Q  P  R  False.
Proof. eauto with iFrame. Qed.
137

Robbert Krebbers's avatar
Robbert Krebbers committed
138
Lemma test_iCombine_persistent P Q R `{!PersistentP R} :
139
140
  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
141

Robbert Krebbers's avatar
Robbert Krebbers committed
142
Lemma test_iNext_evar P : P - True.
Ralf Jung's avatar
Ralf Jung committed
143
144
145
146
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
147

Robbert Krebbers's avatar
Robbert Krebbers committed
148
Lemma test_iNext_sep1 P Q
Robbert Krebbers's avatar
Robbert Krebbers committed
149
150
151
152
153
154
    (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.
155

Robbert Krebbers's avatar
Robbert Krebbers committed
156
Lemma test_iNext_sep2 P Q :  P   Q -  (P  Q).
157
158
159
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
160

Robbert Krebbers's avatar
Robbert Krebbers committed
161
Lemma test_iFrame_persistent (P Q : uPred M) :
162
163
   P - Q -  (P  P)  (P  Q  Q).
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
164

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

Robbert Krebbers's avatar
Robbert Krebbers committed
168
Lemma test_iSpecialize_persistent P Q :
169
170
   P - ( P - Q) - Q.
Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
171
172
173
174
175
176

Lemma test_iLöb P : ( n, ^n P)%I.
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
Ralf Jung's avatar
Ralf Jung committed
177
End tests.
Robbert Krebbers's avatar
Robbert Krebbers committed
178
179
180
181
182
183
184
185
186
187
188
189
190
191

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.