Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
From iris.algebra Require Import frac.
From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic lib.fancy_updates.
Section base_logic_tests.
Context {M : ucmra}.
Implicit Types P Q R : uPred M.
(* Test scopes for bupd *)
Definition use_bupd_uPred (n : nat) : uPred M :=
□ |==> ∃ m : nat , ⌜ n = 2 ⌝.
Definition use_plainly_uPred (n : nat) : uPred M :=
■ |==> ∃ m : nat , ⌜ n = 2 ⌝.
(* Test scopes inside big-ops *)
Definition big_op_scope_uPred_1 (xs : list nat) : uPred M :=
[∗ list] _ ↦ x ∈ xs, True.
Definition big_op_scope_uPred_2 (xs : list nat) : uPred M :=
[∗ list] x; y ∈ xs; xs, True.
Definition big_op_scope_uPred_3 (m : gmap nat nat) : uPred M :=
[∗ map] _ ↦ x ∈ m, True.
Definition big_op_scope_uPred_4 (m : gmap nat nat) : uPred M :=
[∗ map] x; y ∈ m; m, True.
End base_logic_tests.
Section iris_tests.
Context `{!invG Σ}.
Implicit Types P Q R : iProp Σ.
(* Test scopes for bupd and fupd *)
Definition use_bupd_iProp (n : nat) : iProp Σ :=
□ |==> ∃ m : nat , ⌜ n = 2 ⌝.
Definition use_fupd_iProp (n : nat) : iProp Σ :=
□ |={⊤}=> ∃ m : nat , ⌜ n = 2 ⌝.
(* Test scopes inside big-ops *)
Definition big_op_scope_iProp_1 (xs : list nat) : iProp Σ :=
[∗ list] _ ↦ x ∈ xs, True.
Definition big_op_scope_iProp_2 (xs : list nat) : iProp Σ :=
[∗ list] x; y ∈ xs; xs, True.
Definition big_op_scope_iProp_3 (m : gmap nat nat) : iProp Σ :=
[∗ map] _ ↦ x ∈ m, True.
Definition big_op_scope_iProp_4 (m : gmap nat nat) : iProp Σ :=
[∗ map] x; y ∈ m; m, True.
End iris_tests.