proofmode.v 3.58 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
3

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

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

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

57
Lemma demo_3 (M : ucmraT) (P1 P2 P3 : uPred M) :
58
  P1  P2  P3 -  P1   (P2   x, (P3  x = 0)  P3).
59 60 61 62 63
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.

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

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

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

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

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

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

Lemma demo_9 (M : ucmraT) (x y z : M) :
106
   x  y  z - ( x   x  y  z : uPred M).
107
Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed.