proofmode.v 3.54 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.proofmode Require Import tactics.
2
From iris.proofmode Require Import pviewshifts 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
  True   (x y : nat) a b,
Robbert Krebbers's avatar
Robbert Krebbers committed
16 17 18
    x  y 
     (uPred_ownM (a  b) -
    ( y1 y2 c, P1 ((x + y1) + y2)  True   uPred_ownM c) -
19
      ( z, P2 z  True  P2 z) -
Robbert Krebbers's avatar
Robbert Krebbers 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)).
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) 
     (P2  False)  (False  P5 0).
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44 45 46 47 48 49 50 51 52 53
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
54 55
Qed.

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

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

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

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

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

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

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

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