Commit f9435245 authored by Robbert Krebbers's avatar Robbert Krebbers

Examples from MoSeL paper.

parent a181837b
Pipeline #9218 passed with stage
in 30 minutes and 25 seconds
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" : <affine> P
"H1" : Φ x
--------------------------------------∗
Φ x
1 subgoal
PROP : bi
A : Type
P : PROP
Φ, Ψ : A → PROP
x : A
============================
"HP" : <affine> 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" : <affine> Φ
--------------------------------------∗
⎡ P ∗ Q ⎤
1 subgoal
I : biIndex
PROP : bi
Φ : monPred I PROP
P, Q : PROP
============================
"H2" : ⎡ P ⎤
--------------------------------------□
"H1" : ⎡ P -∗ Q ⎤
"H3" : <affine> Φ
--------------------------------------∗
⎡ Q ⎤
(** 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) :
<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.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment