mosel_paper.v 2.23 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14
(** 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.proofmode Require Import tactics monpred.
From iris.bi Require Import monpred.

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.
15 16 17
  iDestruct "H" as (x) "[H1|H2]".
  - Show. iExists x. iLeft. iSplitL "HP"; iAssumption.
  - Show. iExists x. iRight. iSplitL "HP"; iAssumption.
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 46 47 48 49 50 51 52 53
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.