atomic.v 3.52 KB
Newer Older
1
2
3
From iris.heap_lang Require Export lifting notation.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
Ralf Jung's avatar
Ralf Jung committed
4
From iris.heap_lang Require Import proofmode notation atomic_heap.
5
6
Set Default Proof Using "Type".

Ralf Jung's avatar
Ralf Jung committed
7
8
9
10
11
12
13
14
15
16
17
18
19
Section tests.
  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
  Import atomic_heap.notation.

  (* FIXME: removing the `val` type annotation breaks printing. *)
  Lemma test_awp_apply_without (Q : iProp Σ) (l : loc) v :
    Q - l  v - WP !#l {{ _, Q }}.
  Proof.
    iIntros "HQ Hl". awp_apply load_spec without "HQ". Show.
    iAaccIntro with "Hl"; eauto with iFrame.
  Qed.
End tests.

20
21
22
23
24
25
26
27
28
(* Test if AWP and the AU obtained from AWP print. *)
Section printing.
  Context `{!heapG Σ}.

  Definition code : expr := #().

  Lemma print_both_quant (P : val  iProp Σ) :
    <<<  x, P x >>> code @  <<<  y, P y, RET #() >>>.
  Proof.
29
    Show. iIntros (Φ) "AU". Show.
30
31
32
33
34
35
    iPoseProof (aupd_aacc with "AU") as "?". Show.
  Abort.

  Lemma print_first_quant l :
    <<<  x, l  x >>> code @  <<< l  x, RET #() >>>.
  Proof.
36
    Show. iIntros (Φ) "AU". Show.
37
38
39
40
41
42
    iPoseProof (aupd_aacc with "AU") as "?". Show.
  Abort.

  Lemma print_second_quant l :
    <<< l  #() >>> code @  <<<  y, l  y, RET #() >>>.
  Proof.
43
    Show. iIntros (Φ) "AU". Show.
44
45
46
47
48
49
    iPoseProof (aupd_aacc with "AU") as "?". Show.
  Abort.

  Lemma print_no_quant l :
    <<< l  #() >>> code @  <<< l  #(), RET #() >>>.
  Proof.
50
    Show. iIntros (Φ) "AU". Show.
51
52
53
54
55
56
57
58
    iPoseProof (aupd_aacc with "AU") as "?". Show.
  Abort.

  Check "Now come the long pre/post tests".

  Lemma print_both_quant_long l :
    <<<  x, l  x  l  x >>> code @  <<<  y, l  y, RET #() >>>.
  Proof.
59
    Show. iIntros (Φ) "AU". Show.
60
61
62
63
64
  Abort.

  Lemma print_both_quant_longpre l :
    <<<  x, l  x  l  x  l  x  l  x  l  x  l  x >>> code @  <<<  y, l  y, RET #() >>>.
  Proof.
65
    Show. iIntros (Φ) "AU". Show.
66
67
68
69
70
  Abort.

  Lemma print_both_quant_longpost l :
    <<<  xx, l  xx  l  xx  l  xx >>> code @  <<<  yyyy, l  yyyy  l  xx  l  xx  l  xx  l  xx  l  xx, RET #() >>>.
  Proof.
71
    Show. iIntros (Φ) "?". Show.
72
73
74
75
76
  Abort.

  Lemma print_first_quant_long l :
    <<<  x, l  x  l  x  l  x  l  x >>> code @  <<< l  x, RET #() >>>.
  Proof.
77
    Show. iIntros (Φ) "AU". Show.
78
79
80
81
82
  Abort.

  Lemma print_second_quant_long l x :
    <<< l  x  l  x  l  x  l  x  l  x  l  x >>> code @  <<<  y, l  y, RET #() >>>.
  Proof.
83
    Show. iIntros (Φ) "AU". Show.
84
85
86
87
88
  Abort.

  Lemma print_no_quant_long l x :
    <<< l  x  l  x  l  x  l  x  l  x  l  x >>> code @  <<< l  #(), RET #() >>>.
  Proof.
89
    Show. iIntros (Φ) "AU". Show.
90
91
92
93
94
  Abort.

  Lemma print_no_quant_longpre l xx yyyy :
    <<< l  xx  l  xx  l  xx  l  xx  l  xx  l  xx  l  xx >>> code @  <<< l  yyyy, RET #() >>>.
  Proof.
95
    Show. iIntros (Φ) "AU". Show.
96
97
98
99
100
  Abort.

  Lemma print_no_quant_longpost l xx yyyy :
    <<< l  xx  l  xx  l  xx >>> code @  <<< l  yyyy  l  xx  l  xx  l  xx  l  xx  l  xx  l  xx, RET #() >>>.
  Proof.
101
    Show. iIntros (Φ) "AU". Show.
102
103
  Abort.

Ralf Jung's avatar
Ralf Jung committed
104
105
106
107
108
109
110
111
  Check "Prettification".

  Lemma iMod_prettify (P : val  iProp Σ) :
    <<<  x, P x >>> !#0 @  <<<  y, P y, RET #() >>>.
  Proof.
    iIntros (Φ) "AU". iMod "AU". Show.
  Abort.

112
End printing.