mosel_paper.v 2.25 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
(** This file contains the examples from the paper:

MoSeL: A General, Extensible Modal Framework for Interactive Proofs in
Separation Logic
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti,
Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
ICFP 2018 *)
From iris.bi Require Import monpred.
9
From iris.proofmode Require Import tactics monpred.
Robbert Krebbers's avatar
Robbert Krebbers committed
10

11
12
Unset Mangle Names.

Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
15
16
Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A  PROP) :
  P  ( a, Φ a  Ψ a) -  a, (P  Φ a)  (P  Ψ a).
Proof.
  iIntros "[HP H]". Show.
17
18
19
  iDestruct "H" as (x) "[H1|H2]".
  - Show. iExists x. iLeft. iSplitL "HP"; iAssumption.
  - Show. iExists x. iRight. iSplitL "HP"; iAssumption.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
46
47
48
49
50
51
52
53
54
55
Qed.
Lemma example {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A  PROP) :
P  ( a, Φ a  Ψ a) -  a, (P  Φ a)  (P  Ψ a).
Proof.
  iIntros "[HP H]". Show.
  iFrame "HP". Show.
  iAssumption.
Qed.

Lemma example_2 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A  PROP) :
  <affine> P  ( a, Φ a  Ψ a) -  a, Φ a  (P  Ψ a).
Proof.
  iIntros "[HP H]". iDestruct "H" as (x) "[H1|H2]".
  - iExists x. iLeft. Show. iAssumption.
  - iExists x. iRight. Show. iSplitL "HP"; iAssumption.
Qed.

Lemma example_3 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A  PROP) :
   P  ( a, Φ a  Ψ a) -  a, Φ a  (P  P  Ψ a).
Proof.
  iIntros "[#HP H]". Show. iDestruct "H" as (x) "[H1|H2]".
  - iExists x. iLeft. iAssumption.
  - iExists x. iRight. Show. iSplitR; [|iSplitR]; iAssumption.
Qed.
Lemma example_4 {PROP : bi} {A : Type} (P Q : PROP) :  P   Q -  (P  Q).
Proof. iIntros "[#HP #HQ]". Show. iModIntro. iSplitL; iAssumption. Qed.

Lemma example_monpred {I PROP} (Φ Ψ : monPred I PROP) : Φ  (Φ - Ψ)  Ψ.
Proof. iIntros "[H1 H2]". Show. iApply "H2". iAssumption. Qed.

Lemma example_monpred_model {I PROP} (Φ Ψ : monPred I PROP) : Φ  (Φ - Ψ)  Ψ.
Proof. iStartProof PROP. Show. iIntros (i) "[H1 H2]". iApply "H2". iAssumption. Qed.

Lemma example_monpred_2 {I PROP} (Φ : monPred I PROP) (P Q : PROP) :
   P - Q  -   P  - <affine> Φ -  P  Q .
Proof. iIntros "H1 #H2 H3". Show. iFrame "H2". Show. iApply "H1". iAssumption. Qed.