proofmode.v 5.94 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 "[$]").
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 //". 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 73
  iRewrite (uPred.internal_eq_sym x x with "[# //]").
  iRewrite -("H1" $! _ with "[- //]").
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
  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 "[% //] [$] [> HQ] [> //]").
100
    by iApply inv_alloc.
101
  Qed.
102
End iris.
103 104

Lemma demo_9 (M : ucmraT) (x y z : M) :
105
   x  y  z - ( x   x  y  z : uPred M).
106
Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
107 108 109 110 111 112 113 114 115 116

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.
117 118

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

(* 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.
125 126

Lemma demo_13 (M : ucmraT) (P : uPred M) : (|==> False) - |==> P.
127
Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
128 129 130

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

(* 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
139 140 141 142

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.
143 144 145 146

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
147 148 149 150 151 152 153

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
154

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

Lemma test_iNext_sep2 (M : ucmraT) (P Q : uPred M) :
   P   Q -  (P  Q).
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
168 169 170 171

Lemma test_frame_persistent (M : ucmraT) (P Q : uPred M) :
   P - Q -  (P  P)  (P  Q  Q).
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
172 173 174 175

Lemma test_split_box (M : ucmraT) (P Q : uPred M) :
   P -  (P  P).
Proof. iIntros "#?". by iSplit. Qed.