proofmode.v 5.97 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
Lemma test_fast_iIntros P Q :
81
82
  ( x y z : nat,
    x = plus 0 x  y = 0  z = 0  P   Q  foo (x  x))%I.
83
Proof.
84
  iIntros (a) "*".
85
  iIntros "#Hfoo **".
86
  iIntros "# _ //".
87
Qed.
88

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.