Commit afae72fd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

No longer put proof mode class instances in their own file.

parent 5f519f56
...@@ -116,15 +116,11 @@ tests/list_reverse.v ...@@ -116,15 +116,11 @@ tests/list_reverse.v
tests/tree_sum.v tests/tree_sum.v
tests/counter.v tests/counter.v
proofmode/coq_tactics.v proofmode/coq_tactics.v
proofmode/pviewshifts.v
proofmode/environments.v proofmode/environments.v
proofmode/intro_patterns.v proofmode/intro_patterns.v
proofmode/spec_patterns.v proofmode/spec_patterns.v
proofmode/sel_patterns.v proofmode/sel_patterns.v
proofmode/tactics.v proofmode/tactics.v
proofmode/notation.v proofmode/notation.v
proofmode/invariants.v
proofmode/weakestpre.v
proofmode/ghost_ownership.v
proofmode/classes.v proofmode/classes.v
proofmode/class_instances.v proofmode/class_instances.v
...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre adequacy. ...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre adequacy.
From iris.heap_lang Require Export heap. From iris.heap_lang Require Export heap.
From iris.program_logic Require Import auth ownership. From iris.program_logic Require Import auth ownership.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics weakestpre. From iris.proofmode Require Import tactics.
Definition heapΣ : gFunctors := #[authΣ heapUR; irisΣ heap_lang]. Definition heapΣ : gFunctors := #[authΣ heapUR; irisΣ heap_lang].
......
...@@ -2,7 +2,7 @@ From iris.heap_lang Require Export lifting. ...@@ -2,7 +2,7 @@ From iris.heap_lang Require Export lifting.
From iris.algebra Require Import upred_big_op gmap frac dec_agree. From iris.algebra Require Import upred_big_op gmap frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership. From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth. From iris.program_logic Require Import ownership auth.
From iris.proofmode Require Import weakestpre. From iris.proofmode Require Import tactics.
Import uPred. Import uPred.
(* TODO: The entire construction could be generalized to arbitrary languages that have (* TODO: The entire construction could be generalized to arbitrary languages that have
a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
......
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Import auth. From iris.program_logic Require Import auth.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
......
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics. From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl. From iris.algebra Require Import excl.
......
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics. From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl. From iris.algebra Require Import excl.
From iris.heap_lang.lib Require Import lock. From iris.heap_lang.lib Require Import lock.
......
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants. From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import auth gset. From iris.algebra Require Import auth gset.
From iris.heap_lang.lib Require Export lock. From iris.heap_lang.lib Require Export lock.
......
...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre. ...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ownership ectx_lifting. (* for ownP *) From iris.program_logic Require Import ownership ectx_lifting. (* for ownP *)
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics. From iris.heap_lang Require Import tactics.
From iris.proofmode Require Import weakestpre. From iris.proofmode Require Import tactics.
From iris.prelude Require Import fin_maps. From iris.prelude Require Import fin_maps.
Import uPred. Import uPred.
......
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics. From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export weakestpre. From iris.proofmode Require Export tactics.
From iris.heap_lang Require Export wp_tactics heap. From iris.heap_lang Require Export wp_tactics heap.
Import uPred. Import uPred.
......
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.algebra Require Import gmap auth agree gset coPset upred_big_op. From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
From iris.program_logic Require Import ownership. From iris.program_logic Require Import ownership.
From iris.proofmode Require Import tactics weakestpre. From iris.proofmode Require Import tactics.
Import uPred. Import uPred.
Record adequate {Λ} (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ Prop) := { Record adequate {Λ} (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ Prop) := {
......
From iris.program_logic Require Export pviewshifts. From iris.program_logic Require Export invariants.
From iris.algebra Require Export auth. From iris.algebra Require Export auth.
From iris.algebra Require Import gmap. From iris.algebra Require Import gmap.
From iris.proofmode Require Import invariants. From iris.proofmode Require Import tactics.
Import uPred. Import uPred.
(* The CMRA we need. *) (* The CMRA we need. *)
......
From iris.program_logic Require Export pviewshifts. From iris.program_logic Require Export invariants.
From iris.algebra Require Import auth gmap agree upred_big_op. From iris.algebra Require Import auth gmap agree upred_big_op.
From iris.proofmode Require Import tactics invariants. From iris.proofmode Require Import tactics.
Import uPred. Import uPred.
(** The CMRAs we need. *) (** The CMRAs we need. *)
......
From iris.program_logic Require Export invariants. From iris.program_logic Require Export invariants.
From iris.algebra Require Export frac. From iris.algebra Require Export frac.
From iris.proofmode Require Import invariants tactics. From iris.proofmode Require Import tactics.
Import uPred. Import uPred.
Class cinvG Σ := cinv_inG :> inG Σ fracR. Class cinvG Σ := cinv_inG :> inG Σ fracR.
......
(** Some derived lemmas for ectx-based languages *) (** Some derived lemmas for ectx-based languages *)
From iris.program_logic Require Export ectx_language weakestpre lifting. From iris.program_logic Require Export ectx_language weakestpre lifting.
From iris.program_logic Require Import ownership. From iris.program_logic Require Import ownership.
From iris.proofmode Require Import weakestpre. From iris.proofmode Require Import tactics.
Section wp. Section wp.
Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}. Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
......
From iris.program_logic Require Export model. From iris.program_logic Require Export model.
From iris.algebra Require Import iprod gmap. From iris.algebra Require Import iprod gmap.
From iris.proofmode Require Import classes.
Import uPred. Import uPred.
(** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors (** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
...@@ -145,3 +146,16 @@ Proof. ...@@ -145,3 +146,16 @@ Proof.
- apply cmra_transport_valid, ucmra_unit_valid. - apply cmra_transport_valid, ucmra_unit_valid.
- intros x; destruct inG_prf. by rewrite left_id. - intros x; destruct inG_prf. by rewrite left_id.
Qed. Qed.
(** Proofmode class instances *)
Section proofmode_classes.
Context `{inG Σ A}.
Implicit Types a b : A.
Global Instance into_and_own p γ a b1 b2 :
IntoOp a b1 b2 IntoAnd p (own γ a) (own γ b1) (own γ b2).
Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) own_op. Qed.
Global Instance from_sep_own γ a b1 b2 :
FromOp a b1 b2 FromSep (own γ a) (own γ b1) (own γ b2).
Proof. intros. by rewrite /FromSep -own_op from_op. Qed.
End proofmode_classes.
From iris.program_logic Require Export weakestpre viewshifts. From iris.program_logic Require Export weakestpre viewshifts.
From iris.proofmode Require Import weakestpre. From iris.proofmode Require Import tactics.
Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ) Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
(e : expr Λ) (Φ : val Λ iProp Σ) : iProp Σ := (e : expr Λ) (Φ : val Λ iProp Σ) : iProp Σ :=
......
...@@ -2,7 +2,7 @@ From iris.program_logic Require Export pviewshifts. ...@@ -2,7 +2,7 @@ From iris.program_logic Require Export pviewshifts.
From iris.program_logic Require Export namespaces. From iris.program_logic Require Export namespaces.
From iris.program_logic Require Import ownership. From iris.program_logic Require Import ownership.
From iris.algebra Require Import gmap. From iris.algebra Require Import gmap.
From iris.proofmode Require Import pviewshifts. From iris.proofmode Require Import tactics coq_tactics intro_patterns.
Import uPred. Import uPred.
(** Derived forms and lemmas about them. *) (** Derived forms and lemmas about them. *)
...@@ -61,3 +61,29 @@ Proof. ...@@ -61,3 +61,29 @@ Proof.
iIntros "!==> {$HP} HP". iApply "Hclose"; auto. iIntros "!==> {$HP} HP". iApply "Hclose"; auto.
Qed. Qed.
End inv. End inv.
Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
let Htmp := iFresh in
let patback := intro_pat.parse_one Hclose in
let pat := constr:(IList [[IName Htmp; patback]]) in
iVs (inv_open _ N with "[#]") as pat;
[idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
[solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
|tac Htmp].
Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestruct H as pat) Hclose.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestruct H as (x1) pat) Hclose.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestruct H as (x1 x2) pat) Hclose.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")"
constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestruct H as (x1 x2 x3) pat) Hclose.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestruct H as (x1 x2 x3 x4) pat) Hclose.
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ownership. From iris.program_logic Require Import ownership.
From iris.algebra Require Export upred_big_op. From iris.algebra Require Export upred_big_op.
From iris.proofmode Require Import pviewshifts. From iris.proofmode Require Import tactics.
Section lifting. Section lifting.
Context `{irisG Λ Σ}. Context `{irisG Λ Σ}.
......
From iris.program_logic Require Export iris. From iris.program_logic Require Export iris.
From iris.algebra Require Import gmap auth agree gset coPset upred_big_op. From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
From iris.proofmode Require Import ghost_ownership tactics. From iris.proofmode Require Import tactics.
Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) := Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
to_agree (Next (iProp_unfold P)). to_agree (Next (iProp_unfold P)).
......
From iris.program_logic Require Export iris. From iris.program_logic Require Export iris.
From iris.program_logic Require Import ownership. From iris.program_logic Require Import ownership.
From iris.algebra Require Import upred_big_op gmap. From iris.algebra Require Import upred_big_op gmap.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics classes.
Import uPred. Import uPred.
Program Definition pvs_def `{irisG Λ Σ} Program Definition pvs_def `{irisG Λ Σ}
...@@ -136,3 +136,54 @@ Proof. ...@@ -136,3 +136,54 @@ Proof.
intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -pvs_sep. intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -pvs_sep.
Qed. Qed.
End pvs. End pvs.
(** Proofmode class instances *)
Section proofmode_classes.
Context `{irisG Λ Σ}.
Implicit Types P Q : iProp Σ.
Global Instance from_pure_pvs E P φ : FromPure P φ FromPure (|={E}=> P) φ.
Proof. rewrite /FromPure. intros <-. apply pvs_intro. Qed.
Global Instance from_assumption_pvs E p P Q :
FromAssumption p P (|=r=> Q) FromAssumption p P (|={E}=> Q)%I.
Proof. rewrite /FromAssumption=>->. apply rvs_pvs. Qed.
Global Instance into_wand_pvs E1 E2 R P Q :
IntoWand R P Q IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
Global Instance from_sep_pvs E P Q1 Q2 :
FromSep P Q1 Q2 FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.
Global Instance or_split_pvs E1 E2 P Q1 Q2 :
FromOr P Q1 Q2 FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
Proof. rewrite /FromOr=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
Global Instance exists_split_pvs {A} E1 E2 P (Φ : A iProp Σ) :
FromExist P Φ FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
Proof.
rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
Global Instance frame_pvs E1 E2 R P Q :
Frame R P Q Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
Global Instance is_except_last_pvs E1 E2 P : IsExceptLast (|={E1,E2}=> P).
Proof. by rewrite /IsExceptLast except_last_pvs. Qed.
Global Instance from_vs_pvs E P : FromVs (|={E}=> P) P.
Proof. by rewrite /FromVs -rvs_pvs. Qed.
Global Instance elim_vs_rvs_pvs E1 E2 P Q :
ElimVs (|=r=> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
Proof. by rewrite /ElimVs (rvs_pvs E1) pvs_frame_r wand_elim_r pvs_trans. Qed.
Global Instance elim_vs_pvs_pvs E1 E2 E3 P Q :
ElimVs (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_trans. Qed.
End proofmode_classes.
Hint Extern 2 (coq_tactics.of_envs _ _) =>
match goal with |- _ |={_}=> _ => iVsIntro end.
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