proofmode.v 3.51 KB
 Robbert Krebbers committed Apr 11, 2016 1 ``````From iris.proofmode Require Import tactics. `````` Robbert Krebbers committed May 24, 2016 2 ``````From iris.proofmode Require Import pviewshifts invariants. `````` Robbert Krebbers committed Apr 11, 2016 3 `````` `````` Robbert Krebbers committed May 02, 2016 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 committed Apr 11, 2016 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) -★ `````` Robbert Krebbers committed May 02, 2016 19 `````` □ ▷ (∀ z, P2 z ∨ True → P2 z) -★ `````` Robbert Krebbers committed Apr 11, 2016 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. `````` Robbert Krebbers committed May 02, 2016 23 `````` iIntros {i [|j] a b ?} "! [Ha Hb] H1 #H2 H3"; setoid_subst. `````` Robbert Krebbers committed Apr 11, 2016 24 25 26 `````` { iLeft. by iNext. } iRight. iDestruct "H1" as {z1 z2 c} "(H1&_&#Hc)". `````` Robbert Krebbers committed May 02, 2016 27 `````` iPoseProof "Hc" as "foo". `````` Robbert Krebbers committed Apr 26, 2016 28 `````` iRevert {a b} "Ha Hb". iIntros {b a} "Hb {foo} Ha". `````` Robbert Krebbers committed May 24, 2016 29 `````` iAssert (uPred_ownM (a ⋅ core a)) with "[Ha]" as "[Ha #Hac]". `````` Robbert Krebbers committed Apr 11, 2016 30 31 32 33 `````` { by rewrite cmra_core_r. } iFrame "Ha Hac". iExists (S j + z1), z2. iNext. `````` Robbert Krebbers committed May 24, 2016 34 `````` iApply ("H3" \$! _ 0 with "H1 []"). `````` Robbert Krebbers committed May 02, 2016 35 `````` - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight. `````` Robbert Krebbers committed Apr 11, 2016 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 committed Apr 20, 2016 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)). `````` Robbert Krebbers committed Apr 27, 2016 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. `````` Robbert Krebbers committed May 02, 2016 64 ``````Proof. iIntros. iIntros {P} "HP". done. Qed. `````` Robbert Krebbers committed May 02, 2016 65 66 67 68 69 `````` Lemma demo_5 (M : cmraT) (x y : M) (P : uPred M) : (∀ z, P → z ≡ y) ⊢ (P -★ (x,x) ≡ (y,x)). Proof. iIntros "H1 H2". `````` Robbert Krebbers committed May 24, 2016 70 71 `````` iRewrite (uPred.eq_sym x x with "[#]"). iApply uPred.eq_refl. iRewrite -("H1" \$! _ with "[#]"); first done. `````` Robbert Krebbers committed May 02, 2016 72 73 74 `````` iApply uPred.eq_refl. Qed. `````` Robbert Krebbers committed May 02, 2016 75 ``````Lemma demo_6 (M : cmraT) (P Q : uPred M) : `````` Robbert Krebbers committed May 06, 2016 76 77 `````` True ⊢ (∀ x y z : nat, x = plus 0 x → y = 0 → z = 0 → P → □ Q → foo (x ≡ x)). `````` Robbert Krebbers committed May 02, 2016 78 79 80 ``````Proof. iIntros {a} "*". iIntros "#Hfoo **". `````` Robbert Krebbers committed May 06, 2016 81 `````` by iIntros "# _". `````` Robbert Krebbers committed May 02, 2016 82 ``````Qed. `````` Ralf Jung committed May 21, 2016 83 84 85 `````` Section iris. Context {Λ : language} {Σ : iFunctor}. `````` Robbert Krebbers committed May 24, 2016 86 87 `````` Implicit Types E : coPset. Implicit Types P Q : iProp Λ Σ. `````` Ralf Jung committed May 21, 2016 88 `````` `````` Robbert Krebbers committed May 24, 2016 89 `````` Lemma demo_7 E1 E2 E P : `````` Ralf Jung committed May 21, 2016 90 91 92 93 `````` E1 ⊆ E2 → E ⊆ E1 → (|={E1,E}=> ▷ P) ⊢ (|={E2,E ∪ E2 ∖ E1}=> ▷ P). Proof. iIntros {? ?} "Hpvs". `````` Robbert Krebbers committed May 24, 2016 94 `````` iPvs "Hpvs"; first set_solver. `````` Ralf Jung committed May 21, 2016 95 96 `````` done. Qed. `````` Robbert Krebbers committed May 24, 2016 97 98 99 100 101 102 103 104 105 106 107 `````` Lemma demo_8 N E P Q R : nclose N ⊆ E → (True -★ P -★ inv N Q -★ True -★ R) ⊢ (P -★ ▷ Q -★ |={E}=> R). Proof. iIntros {?} "H HP HQ". iApply ("H" with "[#] HP =>[HQ] =>"). - done. - by iApply inv_alloc. - by iPvsIntro. Qed. `````` Ralf Jung committed May 21, 2016 108 ``End iris.``