proofmode.v 6.08 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
11
12
13
14
15
16
17
Proof.
  iIntros "#H #H2".
  (* should remove the disjunction "H" *)
  iDestruct "H" as "[?|?]"; last by iLeft.
  (* 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.

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

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
120
Lemma test_iAssumption_False P : False - P.
121
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
123

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

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

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

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

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

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

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

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

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

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
174
End tests.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
176
177
178
179
180
181
182
183
184
185
186
187
188

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.