proofmode.v 5.52 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

5
Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
6
   (P  Q) - ( x, x = 0  x = 1)  (Q  P).
7
8
9
10
11
12
13
14
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.

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

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

58
Lemma demo_3 (M : ucmraT) (P1 P2 P3 : uPred M) :
59
  P1  P2  P3 -  P1   (P2   x, (P3  x = 0)  P3).
60
61
62
63
64
Proof. iIntros "($ & $ & H)". iFrame "H". iNext. by iExists 0. Qed.

Definition foo {M} (P : uPred M) := (P  P)%I.
Definition bar {M} : uPred M := ( P, foo P)%I.

65
Lemma demo_4 (M : ucmraT) : True - @bar M.
66
Proof. iIntros. iIntros (P) "HP". done. Qed.
67

68
Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
69
  ( z, P  z  y) - (P - (x,x)  (y,x)).
70
71
Proof.
  iIntros "H1 H2".
72
  iRewrite (uPred.internal_eq_sym x x with "[#]"); first done.
73
  iRewrite -("H1" $! _ with "[-]"); first done.
74
  done.
75
76
Qed.

77
Lemma demo_6 (M : ucmraT) (P Q : uPred M) :
78
79
  ( x y z : nat,
    x = plus 0 x  y = 0  z = 0  P   Q  foo (x  x))%I.
80
Proof.
81
  iIntros (a) "*".
82
  iIntros "#Hfoo **".
83
  by iIntros "# _".
84
Qed.
85

86
Lemma demo_7 (M : ucmraT) (P Q1 Q2 : uPred M) : P  (Q1  Q2) - P  Q1.
87
88
Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed.

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

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

Lemma demo_9 (M : ucmraT) (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
110
111
112
113
114
115
116
117
118

Lemma demo_10 (M : ucmraT) (P Q : uPred M) : P - Q - True.
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
120

Lemma demo_11 (M : ucmraT) (P Q R : uPred M) :
121
  (P - True - True - Q - R) - P - Q - R.
122
Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed.
123
124
125
126

(* Check coercions *)
Lemma demo_12 (M : ucmraT) (P : Z  uPred M) : ( x, P x) -  x, P x.
Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
127
128
129

Lemma demo_13 (M : ucmraT) (P : uPred M) : (|==> False) - |==> P.
Proof. iIntros. iAssert False%I with ">[-]" as "[]". done. Qed.
130
131
132

Lemma demo_14 (M : ucmraT) (P : uPred M) : False - P.
Proof. iIntros "H". done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
134
135
136
137
138
139
140

(* Check instantiation and dependent types *)
Lemma demo_15 (M : ucmraT) (P :  n, vec nat n  uPred M) :
  ( 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
142
143
144

Lemma demo_16 (M : ucmraT) (P Q R : uPred M) `{!PersistentP R} :
  P - Q - R - R  Q  P  R  False.
Proof. eauto with iFrame. Qed.
145
146
147
148

Lemma demo_17 (M : ucmraT) (P Q R : uPred M) `{!PersistentP R} :
  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
150
151
152
153
154
155

Lemma test_iNext_evar (M : ucmraT) (P : uPred M) :
  P - True.
Proof.
  iIntros "HP". iAssert ( _ -  P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
158
159
160
161
162
163

Lemma test_iNext_sep (M : ucmraT) (P Q : uPred M)
    (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.