From beebaa6ecb03512286e38e3e5c8357e9683df58d Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 13 Apr 2017 14:43:45 +0200 Subject: [PATCH] Reorganize proofmode tests. --- theories/tests/proofmode.v | 79 ++++++++++++++++++-------------------- 1 file changed, 38 insertions(+), 41 deletions(-) diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v index 0ec04c0d..d4584baa 100644 --- a/theories/tests/proofmode.v +++ b/theories/tests/proofmode.v @@ -4,8 +4,9 @@ Set Default Proof Using "Type". Section tests. Context {M : ucmraT}. -Lemma demo_0 (P Q : uPred M) : - □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P). +Implicit Types P Q R : uPred M. + +Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P). Proof. iIntros "#H #H2". (* should remove the disjunction "H" *) @@ -39,7 +40,7 @@ Proof. - done. Qed. -Lemma demo_2 (P1 P2 P3 P4 Q : uPred M) (P5 : nat → uPredC M): +Lemma demo_2 P1 P2 P3 P4 Q (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) ∧ @@ -57,17 +58,17 @@ Proof. * iSplitL "HQ". iAssumption. by iSplitL "H1". Qed. -Lemma demo_3 (P1 P2 P3 : uPred M) : +Lemma demo_3 P1 P2 P3 : P1 ∗ P2 ∗ P3 -∗ ▷ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3). Proof. iIntros "(\$ & \$ & H)". iFrame "H". iNext. by iExists 0. Qed. Definition foo (P : uPred M) := (P → P)%I. Definition bar : uPred M := (∀ P, foo P)%I. -Lemma demo_4 : True -∗ bar. +Lemma test_unfold_constants : True -∗ bar. Proof. iIntros. iIntros (P) "HP //". Qed. -Lemma demo_5 (x y : M) (P : uPred M) : +Lemma test_iRewrite (x y : M) P : (∀ z, P → z ≡ y) -∗ (P -∗ (x,x) ≡ (y,x)). Proof. iIntros "H1 H2". @@ -76,7 +77,7 @@ Proof. done. Qed. -Lemma demo_6 (P Q : uPred M) : +Lemma test_fast_iIntros P Q : (∀ x y z : nat, ⌜x = plus 0 x⌝ → ⌜y = 0⌝ → ⌜z = 0⌝ → P → □ Q → foo (x ≡ x))%I. Proof. @@ -85,29 +86,14 @@ Proof. iIntros "# _ //". Qed. -Lemma demo_7 (P Q1 Q2 : uPred M) : P ∗ (Q1 ∧ Q2) -∗ P ∗ Q1. +Lemma test_iDestruct_spatial_and P Q1 Q2 : P ∗ (Q1 ∧ Q2) -∗ P ∗ Q1. Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed. -Section iris. - Context `{invG Σ}. - Implicit Types E : coPset. - Implicit Types P Q : iProp Σ. - - Lemma demo_8 N E P Q R : - ↑N ⊆ E → - (True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ ▷ Q ={E}=∗ R. - Proof. - iIntros (?) "H HP HQ". - iApply ("H" with "[% //] [\$] [> HQ] [> //]"). - by iApply inv_alloc. - Qed. -End iris. - -Lemma demo_9 (x y z : M) : +Lemma test_iFrame_pure (x y z : M) : ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M). Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed. -Lemma demo_10 (P Q : uPred M) : P -∗ Q -∗ True. +Lemma test_iAssert_persistent P Q : P -∗ Q -∗ True. Proof. iIntros "HP HQ". iAssert True%I as "#_". { by iClear "HP HQ". } @@ -117,44 +103,43 @@ Proof. done. Qed. -Lemma demo_11 (P Q R : uPred M) : +Lemma test_iSpecialize_auto_frame P Q R : (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R. Proof. iIntros "H HP HQ". by iApply ("H" with "[\$]"). Qed. (* Check coercions *) -Lemma demo_12 (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x. +Lemma test_iExist_coercion (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x. Proof. iIntros "HP". iExists (0:nat). iApply ("HP" \$! (0:nat)). Qed. -Lemma demo_13 (P : uPred M) : (|==> False) -∗ |==> P. +Lemma test_iAssert_modality P : (|==> False) -∗ |==> P. Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed. -Lemma demo_14 (P : uPred M) : False -∗ P. +Lemma test_iAssumption_False P : False -∗ P. Proof. iIntros "H". done. Qed. (* Check instantiation and dependent types *) -Lemma demo_15 (P : ∀ n, vec nat n → uPred M) : +Lemma test_iSpecialize_dependent_type (P : ∀ n, vec nat n → uPred M) : (∀ n v, P n v) -∗ ∃ n v, P n v. Proof. iIntros "H". iExists _, [#10]. iSpecialize ("H" \$! _ [#10]). done. Qed. -Lemma demo_16 (P Q R : uPred M) `{!PersistentP R} : +Lemma test_eauto_iFramE P Q R `{!PersistentP R} : P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False. Proof. eauto with iFrame. Qed. -Lemma demo_17 (P Q R : uPred M) `{!PersistentP R} : +Lemma test_iCombine_persistent P Q R `{!PersistentP R} : P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False. Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed. -Lemma test_iNext_evar (P : uPred M) : - P -∗ True. +Lemma test_iNext_evar P : P -∗ True. Proof. iIntros "HP". iAssert (▷ _ -∗ ▷ P)%I as "?"; last done. iIntros "?". iNext. iAssumption. Qed. -Lemma test_iNext_sep1 (P Q : uPred M) +Lemma test_iNext_sep1 P Q (R1 := (P ∗ Q)%I) (R2 := (▷ P ∗ ▷ Q)%I) : (▷ P ∗ ▷ Q) ∗ R1 ∗ R2 -∗ ▷ (P ∗ Q) ∗ ▷ R1 ∗ R2. Proof. @@ -162,21 +147,33 @@ Proof. rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done. Qed. -Lemma test_iNext_sep2 (P Q : uPred M) : - ▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q). +Lemma test_iNext_sep2 P Q : ▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q). Proof. iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *) Qed. -Lemma test_frame_persistent (P Q : uPred M) : +Lemma test_iFrame_persistent (P Q : uPred M) : □ P -∗ Q -∗ □ (P ∗ P) ∗ (P ∧ Q ∨ Q). Proof. iIntros "#HP". iFrame "HP". iIntros "\$". Qed. -Lemma test_split_box (P Q : uPred M) : - □ P -∗ □ (P ∗ P). +Lemma test_iSplit_always P Q : □ P -∗ □ (P ∗ P). Proof. iIntros "#?". by iSplit. Qed. -Lemma test_specialize_persistent (P Q : uPred M) : +Lemma test_iSpecialize_persistent P Q : □ P -∗ (□ P -∗ Q) -∗ Q. Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed. End tests. + +Section more_tests. + Context `{invG Σ}. + Implicit Types P Q R : iProp Σ. + + Lemma test_masks N E P Q R : + ↑N ⊆ E → + (True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ ▷ Q ={E}=∗ R. + Proof. + iIntros (?) "H HP HQ". + iApply ("H" with "[% //] [\$] [> HQ] [> //]"). + by iApply inv_alloc. + Qed. +End more_tests. -- GitLab