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

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

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

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

Ralf Jung's avatar
Ralf Jung committed
67
Lemma demo_4 : True - bar.
68
Proof. iIntros. iIntros (P) "HP //". Qed.
69

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

Ralf Jung's avatar
Ralf Jung committed
79
Lemma demo_6 (P Q : uPred M) :
80
81
  ( x y z : nat,
    x = plus 0 x  y = 0  z = 0  P   Q  foo (x  x))%I.
82
Proof.
83
  iIntros (a) "*".
84
  iIntros "#Hfoo **".
85
  iIntros "# _ //".
86
Qed.
87

Ralf Jung's avatar
Ralf Jung committed
88
Lemma demo_7 (P Q1 Q2 : uPred M) : P  (Q1  Q2) - P  Q1.
89
90
Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed.

91
Section iris.
92
  Context `{invG Σ}.
93
  Implicit Types E : coPset.
94
  Implicit Types P Q : iProp Σ.
95

96
  Lemma demo_8 N E P Q R :
97
    N  E 
98
    (True - P - inv N Q - True - R) - P -  Q ={E}= R.
99
  Proof.
100
    iIntros (?) "H HP HQ".
101
    iApply ("H" with "[% //] [$] [> HQ] [> //]").
102
    by iApply inv_alloc.
103
  Qed.
104
End iris.
105

Ralf Jung's avatar
Ralf Jung committed
106
Lemma demo_9 (x y z : M) :
107
   x  y  z - ( x   x  y  z : uPred M).
108
Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
109

Ralf Jung's avatar
Ralf Jung committed
110
Lemma demo_10 (P Q : uPred M) : P - Q - True.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
112
113
114
115
116
117
118
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.
119

Ralf Jung's avatar
Ralf Jung committed
120
Lemma demo_11 (P Q R : uPred M) :
121
  (P - True - True - Q - R) - P - Q - R.
122
Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
123
124

(* Check coercions *)
Ralf Jung's avatar
Ralf Jung committed
125
Lemma demo_12 (P : Z  uPred M) : ( x, P x) -  x, P x.
126
Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
127

Ralf Jung's avatar
Ralf Jung committed
128
Lemma demo_13 (P : uPred M) : (|==> False) - |==> P.
129
Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
130

Ralf Jung's avatar
Ralf Jung committed
131
Lemma demo_14 (P : uPred M) : False - P.
132
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
134

(* Check instantiation and dependent types *)
Ralf Jung's avatar
Ralf Jung committed
135
Lemma demo_15 (P :  n, vec nat n  uPred M) :
Robbert Krebbers's avatar
Robbert Krebbers committed
136
137
138
139
140
  ( 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
141

Ralf Jung's avatar
Ralf Jung committed
142
Lemma demo_16 (P Q R : uPred M) `{!PersistentP R} :
Robbert Krebbers's avatar
Robbert Krebbers committed
143
144
  P - Q - R - R  Q  P  R  False.
Proof. eauto with iFrame. Qed.
145

Ralf Jung's avatar
Ralf Jung committed
146
Lemma demo_17 (P Q R : uPred M) `{!PersistentP R} :
147
148
  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
149

Ralf Jung's avatar
Ralf Jung committed
150
Lemma test_iNext_evar (P : uPred M) :
Ralf Jung's avatar
Ralf Jung committed
151
152
153
154
155
  P - True.
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
156

Ralf Jung's avatar
Ralf Jung committed
157
Lemma test_iNext_sep1 (P Q : uPred M)
Robbert Krebbers's avatar
Robbert Krebbers committed
158
159
160
161
162
163
    (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.
164

Ralf Jung's avatar
Ralf Jung committed
165
Lemma test_iNext_sep2 (P Q : uPred M) :
166
167
168
169
   P   Q -  (P  Q).
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
170

Ralf Jung's avatar
Ralf Jung committed
171
Lemma test_frame_persistent (P Q : uPred M) :
172
173
   P - Q -  (P  P)  (P  Q  Q).
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
174

Ralf Jung's avatar
Ralf Jung committed
175
Lemma test_split_box (P Q : uPred M) :
176
177
   P -  (P  P).
Proof. iIntros "#?". by iSplit. Qed.
Ralf Jung's avatar
Ralf Jung committed
178

179
180
181
Lemma test_specialize_persistent (P Q : uPred M) :
   P - ( P - Q) - Q.
Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
Ralf Jung's avatar
Ralf Jung committed
182
End tests.