atomic.v 3.52 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2 3
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Export lifting notation.
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.