proofmode.v 3.47 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.
23
  iIntros {i [|j] a b ?} "! [Ha Hb] H1 #H2 H3"; setoid_subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
24 25 26
  { iLeft. by iNext. }
  iRight.
  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 79 80
Proof.
  iIntros {a} "*".
  iIntros "#Hfoo **".
81
  by iIntros "# _".
82
Qed.
83 84 85

Section iris.
  Context {Λ : language} {Σ : iFunctor}.
86 87
  Implicit Types E : coPset.
  Implicit Types P Q : iProp Λ Σ.
88

89
  Lemma demo_7 E1 E2 E P :
90
    E1  E2  E  E1 
91
    (|={E1,E}=>  P) ={E2,E  E2  E1}=>  P.
92 93
  Proof.
    iIntros {? ?} "Hpvs".
94
    iPvs "Hpvs"; first set_solver.
95 96
    done.
  Qed.
97 98 99

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