From f9435245aed0c7055d7d8616b919dd5e0e09f382 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Fri, 1 Jun 2018 10:20:28 +0200 Subject: [PATCH] Examples from MoSeL paper. --- tests/mosel_paper.ref | 167 ++++++++++++++++++++++++++++++++++++++++++ tests/mosel_paper.v | 53 ++++++++++++++ 2 files changed, 220 insertions(+) create mode 100644 tests/mosel_paper.ref create mode 100644 tests/mosel_paper.v diff --git a/tests/mosel_paper.ref b/tests/mosel_paper.ref new file mode 100644 index 00000000..3031fbef --- /dev/null +++ b/tests/mosel_paper.ref @@ -0,0 +1,167 @@ +1 subgoal + + PROP : bi + A : Type + P : PROP + Φ, Ψ : A → PROP + ============================ + "HP" : P + "H" : ∃ a : A, Φ a ∨ Ψ a + --------------------------------------∗ + ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a + +2 subgoals + + PROP : bi + A : Type + P : PROP + Φ, Ψ : A → PROP + x : A + ============================ + "HP" : P + "H1" : Φ x + --------------------------------------∗ + ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a + + +subgoal 2 is: + "HP" : P +"H2" : Ψ x +--------------------------------------∗ +∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a + +1 subgoal + + PROP : bi + A : Type + P : PROP + Φ, Ψ : A → PROP + ============================ + "HP" : P + "H" : ∃ a : A, Φ a ∨ Ψ a + --------------------------------------∗ + ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a + +1 subgoal + + PROP : bi + A : Type + P : PROP + Φ, Ψ : A → PROP + ============================ + "H" : ∃ a : A, Φ a ∨ Ψ a + --------------------------------------∗ + ∃ x : A, Φ x ∨ Ψ x + +1 subgoal + + PROP : bi + A : Type + P : PROP + Φ, Ψ : A → PROP + x : A + ============================ + "HP" : P + "H1" : Φ x + --------------------------------------∗ + Φ x + +1 subgoal + + PROP : bi + A : Type + P : PROP + Φ, Ψ : A → PROP + x : A + ============================ + "HP" : P + "H2" : Ψ x + --------------------------------------∗ + P ∗ Ψ x + +1 subgoal + + PROP : bi + A : Type + P : PROP + Φ, Ψ : A → PROP + ============================ + "HP" : P + --------------------------------------□ + "H" : ∃ a : A, Φ a ∨ Ψ a + --------------------------------------∗ + ∃ a : A, Φ a ∨ P ∗ P ∗ Ψ a + +1 subgoal + + PROP : bi + A : Type + P : PROP + Φ, Ψ : A → PROP + x : A + ============================ + "HP" : P + --------------------------------------□ + "H2" : Ψ x + --------------------------------------∗ + P ∗ P ∗ Ψ x + +1 subgoal + + PROP : bi + A : Type + P, Q : PROP + ============================ + "HP" : P + "HQ" : Q + --------------------------------------□ + □ (P ∗ Q) + +1 subgoal + + I : biIndex + PROP : bi + Φ, Ψ : monPred I PROP + ============================ + "H1" : Φ + "H2" : Φ -∗ Ψ + --------------------------------------∗ + Ψ + +1 subgoal + + I : biIndex + PROP : bi + Φ, Ψ : monPred I PROP + ============================ + --------------------------------------∗ + ∀ i : I, Φ i ∗ (Φ -∗ Ψ) i -∗ Ψ i + +1 subgoal + + I : biIndex + PROP : bi + Φ : monPred I PROP + P, Q : PROP + ============================ + "H2" : ⎡ P ⎤ + --------------------------------------□ + "H1" : ⎡ P -∗ Q ⎤ + "H3" : Φ + --------------------------------------∗ + ⎡ P ∗ Q ⎤ + +1 subgoal + + I : biIndex + PROP : bi + Φ : monPred I PROP + P, Q : PROP + ============================ + "H2" : ⎡ P ⎤ + --------------------------------------□ + "H1" : ⎡ P -∗ Q ⎤ + "H3" : Φ + --------------------------------------∗ + ⎡ Q ⎤ + diff --git a/tests/mosel_paper.v b/tests/mosel_paper.v new file mode 100644 index 00000000..e5e08f8c --- /dev/null +++ b/tests/mosel_paper.v @@ -0,0 +1,53 @@ +(** 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. + iDestruct "H" as (x) "[H1|H2]". Show. + - iExists x. iLeft. iSplitL "HP"; iAssumption. + - iExists x. iRight. iSplitL "HP"; iAssumption. +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) : + 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 ⎤ -∗ Φ -∗ ⎡ P ∗ Q ⎤. +Proof. iIntros "H1 #H2 H3". Show. iFrame "H2". Show. iApply "H1". iAssumption. Qed. -- GitLab