proofmode.v 5.84 KB
 Robbert Krebbers committed Jun 30, 2016 1 ``````From iris.proofmode Require Import tactics. `````` 2 ``````From iris.base_logic.lib Require Import invariants. `````` Ralf Jung committed Jan 05, 2017 3 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Apr 11, 2016 4 `````` `````` Ralf Jung committed Apr 11, 2017 5 6 7 ``````Section tests. Context {M : ucmraT}. Lemma demo_0 (P Q : uPred M) : `````` Robbert Krebbers committed Dec 09, 2016 8 `````` □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P). `````` Robbert Krebbers committed May 02, 2016 9 10 11 12 13 14 15 16 ``````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. `````` Ralf Jung committed Apr 11, 2017 17 ``````Lemma demo_1 (P1 P2 P3 : nat → uPred M) : `````` 18 `````` (∀ (x y : nat) a b, `````` Robbert Krebbers committed Apr 11, 2016 19 `````` x ≡ y → `````` Robbert Krebbers committed Nov 03, 2016 20 21 22 `````` □ (uPred_ownM (a ⋅ b) -∗ (∃ y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ □ uPred_ownM c) -∗ □ ▷ (∀ z, P2 z ∨ True → P2 z) -∗ `````` Ralf Jung committed Nov 22, 2016 23 `````` ▷ (∀ n m : nat, P1 n → □ ((True ∧ P2 n) → □ (⌜n = n⌝ ↔ P3 n))) -∗ `````` 24 `````` ▷ ⌜x = 0⌝ ∨ ∃ x z, ▷ P3 (x + z) ∗ uPred_ownM b ∗ uPred_ownM (core b)))%I. `````` Robbert Krebbers committed Apr 11, 2016 25 ``````Proof. `````` Robbert Krebbers committed Aug 05, 2016 26 `````` iIntros (i [|j] a b ?) "!# [Ha Hb] H1 #H2 H3"; setoid_subst. `````` Robbert Krebbers committed Apr 11, 2016 27 28 `````` { iLeft. by iNext. } iRight. `````` Robbert Krebbers committed Jul 13, 2016 29 `````` iDestruct "H1" as (z1 z2 c) "(H1&_&#Hc)". `````` Robbert Krebbers committed May 02, 2016 30 `````` iPoseProof "Hc" as "foo". `````` Robbert Krebbers committed Jul 13, 2016 31 `````` iRevert (a b) "Ha Hb". iIntros (b a) "Hb {foo} Ha". `````` Robbert Krebbers committed May 24, 2016 32 `````` iAssert (uPred_ownM (a ⋅ core a)) with "[Ha]" as "[Ha #Hac]". `````` Robbert Krebbers committed Apr 11, 2016 33 `````` { by rewrite cmra_core_r. } `````` Robbert Krebbers committed Jun 30, 2016 34 `````` iIntros "{\$Hac \$Ha}". `````` Robbert Krebbers committed Apr 11, 2016 35 36 `````` iExists (S j + z1), z2. iNext. `````` Robbert Krebbers committed Mar 14, 2017 37 `````` iApply ("H3" \$! _ 0 with "[\$]"). `````` Robbert Krebbers committed May 02, 2016 38 `````` - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight. `````` Robbert Krebbers committed Apr 11, 2016 39 40 41 `````` - done. Qed. `````` Ralf Jung committed Apr 11, 2017 42 ``````Lemma demo_2 (P1 P2 P3 P4 Q : uPred M) (P5 : nat → uPredC M): `````` Robbert Krebbers committed Dec 09, 2016 43 44 45 `````` 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) ∧ `````` Robbert Krebbers committed May 31, 2016 46 `````` (P2 ∨ False) ∧ (False → P5 0). `````` Robbert Krebbers committed Apr 11, 2016 47 48 49 50 51 52 53 54 55 56 57 ``````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 58 59 ``````Qed. `````` Ralf Jung committed Apr 11, 2017 60 ``````Lemma demo_3 (P1 P2 P3 : uPred M) : `````` Robbert Krebbers committed Dec 09, 2016 61 `````` P1 ∗ P2 ∗ P3 -∗ ▷ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3). `````` Robbert Krebbers committed Apr 27, 2016 62 63 ``````Proof. iIntros "(\$ & \$ & H)". iFrame "H". iNext. by iExists 0. Qed. `````` Ralf Jung committed Apr 11, 2017 64 65 ``````Definition foo (P : uPred M) := (P → P)%I. Definition bar : uPred M := (∀ P, foo P)%I. `````` Robbert Krebbers committed Apr 27, 2016 66 `````` `````` Ralf Jung committed Apr 11, 2017 67 ``````Lemma demo_4 : True -∗ bar. `````` Robbert Krebbers committed Mar 14, 2017 68 ``````Proof. iIntros. iIntros (P) "HP //". Qed. `````` Robbert Krebbers committed May 02, 2016 69 `````` `````` Ralf Jung committed Apr 11, 2017 70 ``````Lemma demo_5 (x y : M) (P : uPred M) : `````` Robbert Krebbers committed Dec 09, 2016 71 `````` (∀ z, P → z ≡ y) -∗ (P -∗ (x,x) ≡ (y,x)). `````` Robbert Krebbers committed May 02, 2016 72 73 ``````Proof. iIntros "H1 H2". `````` Robbert Krebbers committed Mar 14, 2017 74 75 `````` iRewrite (uPred.internal_eq_sym x x with "[# //]"). iRewrite -("H1" \$! _ with "[- //]"). `````` Robbert Krebbers committed May 30, 2016 76 `````` done. `````` Robbert Krebbers committed May 02, 2016 77 78 ``````Qed. `````` Ralf Jung committed Apr 11, 2017 79 ``````Lemma demo_6 (P Q : uPred M) : `````` Robbert Krebbers committed Dec 09, 2016 80 81 `````` (∀ x y z : nat, ⌜x = plus 0 x⌝ → ⌜y = 0⌝ → ⌜z = 0⌝ → P → □ Q → foo (x ≡ x))%I. `````` Robbert Krebbers committed May 02, 2016 82 ``````Proof. `````` Robbert Krebbers committed Jul 13, 2016 83 `````` iIntros (a) "*". `````` Robbert Krebbers committed May 02, 2016 84 `````` iIntros "#Hfoo **". `````` Robbert Krebbers committed Mar 14, 2017 85 `````` iIntros "# _ //". `````` Robbert Krebbers committed May 02, 2016 86 ``````Qed. `````` Ralf Jung committed May 21, 2016 87 `````` `````` Ralf Jung committed Apr 11, 2017 88 ``````Lemma demo_7 (P Q1 Q2 : uPred M) : P ∗ (Q1 ∧ Q2) -∗ P ∗ Q1. `````` 89 90 ``````Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed. `````` Ralf Jung committed May 21, 2016 91 ``````Section iris. `````` Robbert Krebbers committed Oct 28, 2016 92 `````` Context `{invG Σ}. `````` Robbert Krebbers committed May 24, 2016 93 `````` Implicit Types E : coPset. `````` Robbert Krebbers committed Aug 05, 2016 94 `````` Implicit Types P Q : iProp Σ. `````` Ralf Jung committed May 21, 2016 95 `````` `````` 96 `````` Lemma demo_8 N E P Q R : `````` Robbert Krebbers committed Nov 22, 2016 97 `````` ↑N ⊆ E → `````` Robbert Krebbers committed Dec 09, 2016 98 `````` (True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ ▷ Q ={E}=∗ R. `````` Robbert Krebbers committed May 24, 2016 99 `````` Proof. `````` Robbert Krebbers committed Jul 13, 2016 100 `````` iIntros (?) "H HP HQ". `````` Robbert Krebbers committed Mar 14, 2017 101 `````` iApply ("H" with "[% //] [\$] [> HQ] [> //]"). `````` Robbert Krebbers committed Mar 14, 2017 102 `````` by iApply inv_alloc. `````` Robbert Krebbers committed May 24, 2016 103 `````` Qed. `````` Ralf Jung committed May 21, 2016 104 ``````End iris. `````` Robbert Krebbers committed Sep 19, 2016 105 `````` `````` Ralf Jung committed Apr 11, 2017 106 ``````Lemma demo_9 (x y z : M) : `````` Robbert Krebbers committed Dec 09, 2016 107 `````` ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M). `````` Robbert Krebbers committed Sep 19, 2016 108 ``````Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed. `````` Robbert Krebbers committed Dec 28, 2016 109 `````` `````` Ralf Jung committed Apr 11, 2017 110 ``````Lemma demo_10 (P Q : uPred M) : P -∗ Q -∗ True. `````` Robbert Krebbers committed Dec 28, 2016 111 112 113 114 115 116 117 118 ``````Proof. iIntros "HP HQ". iAssert True%I as "#_". { by iClear "HP HQ". } iAssert True%I with "[HP]" as "#_". { Fail iClear "HQ". by iClear "HP". } iAssert True%I as %_. { by iClear "HP HQ". } iAssert True%I with "[HP]" as %_. { Fail iClear "HQ". by iClear "HP". } done. Qed. `````` Robbert Krebbers committed Jan 22, 2017 119 `````` `````` Ralf Jung committed Apr 11, 2017 120 ``````Lemma demo_11 (P Q R : uPred M) : `````` Robbert Krebbers committed Jan 23, 2017 121 `````` (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R. `````` Robbert Krebbers committed Mar 14, 2017 122 ``````Proof. iIntros "H HP HQ". by iApply ("H" with "[\$]"). Qed. `````` Robbert Krebbers committed Feb 12, 2017 123 124 `````` (* Check coercions *) `````` Ralf Jung committed Apr 11, 2017 125 ``````Lemma demo_12 (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x. `````` Robbert Krebbers committed Feb 12, 2017 126 ``````Proof. iIntros "HP". iExists (0:nat). iApply ("HP" \$! (0:nat)). Qed. `````` Jacques-Henri Jourdan committed Feb 13, 2017 127 `````` `````` Ralf Jung committed Apr 11, 2017 128 ``````Lemma demo_13 (P : uPred M) : (|==> False) -∗ |==> P. `````` Robbert Krebbers committed Mar 14, 2017 129 ``````Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed. `````` Robbert Krebbers committed Feb 13, 2017 130 `````` `````` Ralf Jung committed Apr 11, 2017 131 ``````Lemma demo_14 (P : uPred M) : False -∗ P. `````` Robbert Krebbers committed Feb 13, 2017 132 ``````Proof. iIntros "H". done. Qed. `````` Robbert Krebbers committed Feb 13, 2017 133 134 `````` (* Check instantiation and dependent types *) `````` Ralf Jung committed Apr 11, 2017 135 ``````Lemma demo_15 (P : ∀ n, vec nat n → uPred M) : `````` Robbert Krebbers committed Feb 13, 2017 136 137 138 139 140 `````` (∀ n v, P n v) -∗ ∃ n v, P n v. Proof. iIntros "H". iExists _, [#10]. iSpecialize ("H" \$! _ [#10]). done. Qed. `````` Robbert Krebbers committed Feb 15, 2017 141 `````` `````` Ralf Jung committed Apr 11, 2017 142 ``````Lemma demo_16 (P Q R : uPred M) `{!PersistentP R} : `````` Robbert Krebbers committed Feb 15, 2017 143 144 `````` P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False. Proof. eauto with iFrame. Qed. `````` Robbert Krebbers committed Feb 21, 2017 145 `````` `````` Ralf Jung committed Apr 11, 2017 146 ``````Lemma demo_17 (P Q R : uPred M) `{!PersistentP R} : `````` Robbert Krebbers committed Feb 21, 2017 147 148 `````` P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False. Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed. `````` Ralf Jung committed Mar 10, 2017 149 `````` `````` Ralf Jung committed Apr 11, 2017 150 ``````Lemma test_iNext_evar (P : uPred M) : `````` Ralf Jung committed Mar 10, 2017 151 152 153 154 155 `````` P -∗ True. Proof. iIntros "HP". iAssert (▷ _ -∗ ▷ P)%I as "?"; last done. iIntros "?". iNext. iAssumption. Qed. `````` Robbert Krebbers committed Mar 11, 2017 156 `````` `````` Ralf Jung committed Apr 11, 2017 157 ``````Lemma test_iNext_sep1 (P Q : uPred M) `````` Robbert Krebbers committed Mar 11, 2017 158 159 160 161 162 163 `````` (R1 := (P ∗ Q)%I) (R2 := (▷ P ∗ ▷ Q)%I) : (▷ P ∗ ▷ Q) ∗ R1 ∗ R2 -∗ ▷ (P ∗ Q) ∗ ▷ R1 ∗ R2. Proof. iIntros "H". iNext. rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done. Qed. `````` Ralf Jung committed Mar 12, 2017 164 `````` `````` Ralf Jung committed Apr 11, 2017 165 ``````Lemma test_iNext_sep2 (P Q : uPred M) : `````` Ralf Jung committed Mar 12, 2017 166 167 168 169 `````` ▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q). Proof. iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *) Qed. `````` Robbert Krebbers committed Mar 15, 2017 170 `````` `````` Ralf Jung committed Apr 11, 2017 171 ``````Lemma test_frame_persistent (P Q : uPred M) : `````` Robbert Krebbers committed Mar 15, 2017 172 173 `````` □ P -∗ Q -∗ □ (P ∗ P) ∗ (P ∧ Q ∨ Q). Proof. iIntros "#HP". iFrame "HP". iIntros "\$". Qed. `````` Robbert Krebbers committed Mar 22, 2017 174 `````` `````` Ralf Jung committed Apr 11, 2017 175 ``````Lemma test_split_box (P Q : uPred M) : `````` Robbert Krebbers committed Mar 22, 2017 176 177 `````` □ P -∗ □ (P ∗ P). Proof. iIntros "#?". by iSplit. Qed. `````` Ralf Jung committed Apr 11, 2017 178 `````` `````` Robbert Krebbers committed Apr 13, 2017 179 180 181 ``````Lemma test_specialize_persistent (P Q : uPred M) : □ P -∗ (□ P -∗ Q) -∗ Q. Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed. `````` Ralf Jung committed Apr 11, 2017 182 ``End tests.``