proofmode.v 3.21 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.proofmode Require Import tactics.
2
From iris.proofmode Require Import pviewshifts.
Robbert Krebbers's avatar
Robbert Krebbers committed
3

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

Robbert Krebbers's avatar
Robbert Krebbers committed
14
15
16
17
18
Lemma demo_1 (M : cmraT) (P1 P2 P3 : nat  uPred M) :
  True  ( (x y : nat) a b,
    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
21
22
     ( n m : nat, P1 n   ((True  P2 n)   (n = n  P3 n))) -
     (x = 0)   x z,  P3 (x + z)  uPred_ownM b  uPred_ownM (core b))).
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".
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
31
32
33
  iAssert (uPred_ownM (a  core a))%I as "[Ha #Hac]" with "[Ha]".
  { by rewrite cmra_core_r. }
  iFrame "Ha Hac".
  iExists (S j + z1), z2.
  iNext.
34
35
  iApply ("H3" $! _ 0 with "H1 ! [] !").
  - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
  - done.
Qed.

Lemma demo_2 (M : cmraT) (P1 P2 P3 P4 Q : uPred M) (P5 : nat  uPredC M):
    (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)).
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
56
57
Qed.

Lemma demo_3 (M : cmraT) (P1 P2 P3 : uPred M) :
  (P1  P2  P3)  ( P1   (P2   x, (P3  x = 0)  P3)).
58
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.

Lemma demo_4 (M : cmraT) : True  @bar M.
64
Proof. iIntros. iIntros {P} "HP". done. Qed.
65
66
67
68
69
70
71
72
73
74

Lemma demo_5 (M : cmraT) (x y : M) (P : uPred M) :
  ( z, P  z  y)  (P - (x,x)  (y,x)).
Proof.
  iIntros "H1 H2".
  iRewrite (uPred.eq_sym x x with "- !"). iApply uPred.eq_refl.
  iRewrite -("H1" $! _ with "- !"); first done.
  iApply uPred.eq_refl.
Qed.

75
Lemma demo_6 (M : cmraT) (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
86
87
88
89
90
91
92
93
94
95

Section iris.
  Context {Λ : language} {Σ : iFunctor}.

  Lemma demo_7 (E1 E2 E : coPset) (P : iProp Λ Σ) :
    E1  E2  E  E1 
    (|={E1,E}=>  P)  (|={E2,E  E2  E1}=>  P).
  Proof.
    iIntros {? ?} "Hpvs".
    iPvs "Hpvs"; first (split_and?; set_solver).
    done.
  Qed.
End iris.