Commit 8bfac1ad authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 6c6f5755 126d54c3
From iris.program_logic Require Export model.
From iris.algebra Require Import iprod gmap.
From iris.proofmode Require Import classes.
Import uPred.
(** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
......@@ -145,3 +146,16 @@ Proof.
- apply cmra_transport_valid, ucmra_unit_valid.
- intros x; destruct inG_prf. by rewrite left_id.
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.proofmode Require Import weakestpre.
From iris.proofmode Require Import tactics.
Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
(e : expr Λ) (Φ : val Λ iProp Σ) : iProp Σ :=
......
......@@ -2,7 +2,7 @@ From iris.program_logic Require Export pviewshifts.
From iris.program_logic Require Export namespaces.
From iris.program_logic Require Import ownership.
From iris.algebra Require Import gmap.
From iris.proofmode Require Import pviewshifts.
From iris.proofmode Require Import tactics coq_tactics intro_patterns.
Import uPred.
(** Derived forms and lemmas about them. *)
......@@ -61,3 +61,29 @@ Proof.
iIntros "!==> {$HP} HP". iApply "Hclose"; auto.
Qed.
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 Import ownership.
From iris.algebra Require Export upred_big_op.
From iris.proofmode Require Import pviewshifts.
From iris.proofmode Require Import tactics.
Section lifting.
Context `{irisG Λ Σ}.
......
From iris.program_logic Require Export iris.
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 Σ)) :=
to_agree (Next (iProp_unfold P)).
......
From iris.program_logic Require Export iris.
From iris.program_logic Require Import ownership.
From iris.algebra Require Import upred_big_op gmap.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import tactics classes.
Import uPred.
Program Definition pvs_def `{irisG Λ Σ}
......@@ -136,3 +136,54 @@ Proof.
intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -pvs_sep.
Qed.
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.
From iris.program_logic Require Export pviewshifts.
From iris.program_logic Require Export invariants.
From iris.algebra Require Export sts.
From iris.proofmode Require Import invariants.
From iris.proofmode Require Import tactics.
Import uPred.
(** The CMRA we need. *)
......
From iris.program_logic Require Export invariants.
From iris.algebra Require Export gmap gset coPset.
From iris.proofmode Require Import invariants tactics.
From iris.proofmode Require Import tactics.
Import uPred.
Definition tlN : namespace := nroot .@ "tl".
......
From iris.program_logic Require Export pviewshifts.
From iris.proofmode Require Import pviewshifts invariants.
From iris.program_logic Require Export invariants.
From iris.proofmode Require Import tactics.
Definition vs `{irisG Λ Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
( (P |={E1,E2}=> Q))%I.
......
......@@ -2,7 +2,7 @@ From iris.program_logic Require Export pviewshifts.
From iris.program_logic Require Import ownership.
From iris.algebra Require Import upred_big_op.
From iris.prelude Require Export coPset.
From iris.proofmode Require Import tactics pviewshifts.
From iris.proofmode Require Import tactics classes.
Import uPred.
Definition wp_pre `{irisG Λ Σ}
......@@ -211,3 +211,32 @@ Lemma wp_wand_r E e Φ Ψ :
WP e @ E {{ Φ }} ( v, Φ v - Ψ v) WP e @ E {{ Ψ }}.
Proof. by rewrite comm wp_wand_l. Qed.
End wp.
(** Proofmode class instances *)
Section proofmode_classes.
Context `{irisG Λ Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
Global Instance frame_wp E e R Φ Ψ :
( v, Frame R (Φ v) (Ψ v)) Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
Global Instance is_except_last_wp E e Φ : IsExceptLast (WP e @ E {{ Φ }}).
Proof. by rewrite /IsExceptLast -{2}pvs_wp -except_last_pvs -pvs_intro. Qed.
Global Instance elim_vs_rvs_wp E e P Φ :
ElimVs (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
Proof. by rewrite /ElimVs (rvs_pvs E) pvs_frame_r wand_elim_r pvs_wp. Qed.
Global Instance elim_vs_pvs_wp E e P Φ :
ElimVs (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_wp. Qed.
(* lower precedence, if possible, it should always pick elim_vs_pvs_wp *)
Global Instance elim_vs_pvs_wp_atomic E1 E2 e P Φ :
atomic e
ElimVs (|={E1,E2}=> P) P
(WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
Proof. intros. by rewrite /ElimVs pvs_frame_r wand_elim_r wp_atomic. Qed.
End proofmode_classes.
......@@ -132,6 +132,10 @@ Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
(* FromSep *)
Global Instance from_sep_sep P1 P2 : FromSep (P1 P2) P1 P2 | 100.
Proof. done. Qed.
Global Instance from_sep_ownM (a b1 b2 : M) :
FromOp a b1 b2
FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. by rewrite /FromSep -ownM_op from_op. Qed.
Global Instance from_sep_always P Q1 Q2 :
FromSep P Q1 Q2 FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
......@@ -142,9 +146,6 @@ Global Instance from_sep_rvs P Q1 Q2 :
FromSep P Q1 Q2 FromSep (|=r=> P) (|=r=> Q1) (|=r=> Q2).
Proof. rewrite /FromSep=><-. apply rvs_sep. Qed.
Global Instance from_sep_ownM (a b : M) :
FromSep (uPred_ownM (a b)) (uPred_ownM a) (uPred_ownM b) | 99.
Proof. by rewrite /FromSep ownM_op. Qed.
Global Instance from_sep_big_sepM
`{Countable K} {A} (Φ Ψ1 Ψ2 : K A uPred M) m :
( k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x))
......@@ -160,6 +161,20 @@ Proof.
rewrite /FromSep=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
Qed.
(* FromOp *)
Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a b) a b.
Proof. by rewrite /FromOp. Qed.
Global Instance from_op_persistent {A : cmraT} (a : A) :
Persistent a FromOp a a a.
Proof. intros. by rewrite /FromOp -(persistent_dup a). Qed.
Global Instance from_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
FromOp a b1 b2 FromOp a' b1' b2'
FromOp (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed.
Global Instance from_op_Some {A : cmraT} (a : A) b1 b2 :
FromOp a b1 b2 FromOp (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed.
(* IntoOp *)
Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a b) a b.
Proof. by rewrite /IntoOp. Qed.
......
......@@ -39,6 +39,9 @@ Global Arguments into_and : clear implicits.
Lemma mk_into_and_sep p P Q1 Q2 : (P Q1 Q2) IntoAnd p P Q1 Q2.
Proof. rewrite /IntoAnd=>->. destruct p; auto using sep_and. Qed.
Class FromOp {A : cmraT} (a b1 b2 : A) := from_op : b1 b2 a.
Global Arguments from_op {_} _ _ _ {_}.
Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a b1 b2.
Global Arguments into_op {_} _ _ _ {_}.
......@@ -70,5 +73,8 @@ Global Arguments from_vs : clear implicits.
Class ElimVs (P P' : uPred M) (Q Q' : uPred M) :=
elim_vs : P (P' - Q') Q.
Arguments elim_vs _ _ _ _ {_}.
Global Arguments elim_vs _ _ _ _ {_}.
Lemma elim_vs_dummy P Q : ElimVs P P Q Q.
Proof. by rewrite /ElimVs wand_elim_r. Qed.
End classes.
......@@ -531,17 +531,9 @@ Proof.
by rewrite right_id assoc (into_wand R) always_if_elim wand_elim_r wand_elim_r.
Qed.
Class IntoAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
into_assert : R (P - Q) Q.
Global Arguments into_assert _ _ _ {_}.
Lemma into_assert_default P Q : IntoAssert P Q P.
Proof. by rewrite /IntoAssert wand_elim_r. Qed.
Global Instance to_assert_rvs P Q : IntoAssert P (|=r=> Q) (|=r=> P).
Proof. by rewrite /IntoAssert rvs_frame_r wand_elim_r rvs_trans. Qed.
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
envs_lookup_delete j Δ = Some (q, R, Δ')
IntoWand R P1 P2 IntoAssert P1 Q P1'
IntoWand R P1 P2 ElimVs P1' P1 Q Q
('(Δ1,Δ2) envs_split lr js Δ';
Δ2' envs_app false (Esnoc Enil j P2) Δ2;
Some (Δ1,Δ2')) = Some (Δ1,Δ2') (* does not preserve position of [j] *)
......@@ -553,7 +545,7 @@ Proof.
rewrite envs_lookup_sound // envs_split_sound //.
rewrite (envs_app_sound Δ2) //; simpl.
rewrite right_id (into_wand R) HP1 assoc -(comm _ P1') -assoc.
rewrite -(into_assert P1 Q); apply sep_mono_r, wand_intro_l.
rewrite -(elim_vs P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
by rewrite always_if_elim assoc !wand_elim_r.
Qed.
......@@ -614,11 +606,11 @@ Proof.
by rewrite -(idemp uPred_and Δ) {1}(persistentP Δ) {1}HP HPQ impl_elim_r.
Qed.
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
IntoAssert P Q R
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
ElimVs P' P Q Q
envs_split lr js Δ = Some (Δ1,Δ2)
envs_app false (Esnoc Enil j P) Δ2 = Some Δ2'
(Δ1 R) (Δ2' Q) Δ Q.
(Δ1 P') (Δ2' Q) Δ Q.
Proof.
intros ??? HP HQ. rewrite envs_split_sound //.
rewrite (envs_app_sound Δ2) //; simpl.
......
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export ghost_ownership.
Section ghost.
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 b :
FromSep (own γ (a b)) (own γ a) (own γ b) | 90.
Proof. by rewrite /FromSep own_op. Qed.
End ghost.
From iris.proofmode Require Export tactics pviewshifts.
From iris.program_logic Require Export invariants.
From iris.proofmode Require Import coq_tactics intro_patterns.
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.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics ghost_ownership.
From iris.program_logic Require Export pviewshifts.
Import uPred.
Section pvs.
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 to_assert_pvs E1 E2 P Q :
IntoAssert P (|={E1,E2}=> Q) (|={E1}=> P).
Proof. intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r pvs_trans. 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 pvs.
Hint Extern 2 (of_envs _ _) =>
match goal with |- _ |={_}=> _ => iVsIntro end.
......@@ -312,7 +312,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|match vs with
| false => apply into_assert_default
| false => apply elim_vs_dummy
| true => apply _ || fail "iSpecialize: cannot generate view shifted goal"
end
|env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
......@@ -1099,7 +1099,7 @@ Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac)
| [SGoal (SpecGoal ?vs ?lr ?Hs_frame ?Hs)] =>
eapply tac_assert with _ _ _ lr (Hs_frame ++ Hs) H Q _;
[match vs with
| false => apply into_assert_default
| false => apply elim_vs_dummy
| true => apply _ || fail "iAssert: cannot generate view shifted goal"
end
|env_cbv; reflexivity || fail "iAssert:" Hs "not found"
......@@ -1133,7 +1133,10 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
eapply (tac_rewrite _ Heq _ _ lr);
[env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
|let P := match goal with |- ?P _ => P end in
reflexivity || fail "iRewrite:" P "not an equality"
(* use ssreflect apply: which is better at dealing with unification
involving canonical structures. This is useful for the COFE canonical
structure in uPred_eq that it may have to infer. *)
apply: reflexivity || fail "iRewrite:" P "not an equality"
|iRewriteFindPred
|intros ??? ->; reflexivity|lazy beta; iClear Heq]).
......@@ -1146,7 +1149,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H)
[env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
|env_cbv; reflexivity || fail "iRewrite:" H "not found"
|let P := match goal with |- ?P _ => P end in
reflexivity || fail "iRewrite:" P "not an equality"
apply: reflexivity || fail "iRewrite:" P "not an equality"
|iRewriteFindPred
|intros ??? ->; reflexivity
|env_cbv; reflexivity|lazy beta; iClear Heq]).
......
From iris.proofmode Require Export classes pviewshifts.
From iris.proofmode Require Import coq_tactics.
From iris.program_logic Require Export weakestpre.
Import uPred.
Section weakestpre.
Context `{irisG Λ Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
Global Instance frame_wp E e R Φ Ψ :
( v, Frame R (Φ v) (Ψ v)) Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
Global Instance to_assert_wp E e P Φ :
IntoAssert P (WP e @ E {{ Ψ }}) (|={E}=> P).
Proof. intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r pvs_wp. Qed.
Global Instance is_except_last_wp E e Φ : IsExceptLast (WP e @ E {{ Φ }}).
Proof. by rewrite /IsExceptLast -{2}pvs_wp -except_last_pvs -pvs_intro. Qed.
Global Instance elim_vs_rvs_wp E e P Φ :
ElimVs (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
Proof. by rewrite /ElimVs (rvs_pvs E) pvs_frame_r wand_elim_r pvs_wp. Qed.
Global Instance elim_vs_pvs_wp E e P Φ :
ElimVs (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_wp. Qed.
(* lower precedence, if possible, it should always pick elim_vs_pvs_wp *)
Global Instance elim_vs_pvs_wp_atomic E1 E2 e P Φ :
atomic e
ElimVs (|={E1,E2}=> P) P
(WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
Proof. intros. by rewrite /ElimVs pvs_frame_r wand_elim_r wp_atomic. Qed.
End weakestpre.
From iris.program_logic Require Export hoare weakestpre pviewshifts ownership.
From iris.algebra Require Import upred_big_op.
From iris.prelude Require Export coPset.
From iris.proofmode Require Import tactics pviewshifts weakestpre.
From iris.proofmode Require Import tactics.
Import uPred.
Section atomic.
......@@ -42,7 +42,6 @@ Section atomic.
End atomic.
From iris.heap_lang Require Export lang proofmode notation.
From iris.proofmode Require Import invariants.
Section incr.
Context `{!heapG Σ} (N : namespace).
......
......@@ -5,7 +5,7 @@ under max can be found in `heap_lang/lib/counter.v`. *)
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.program_logic Require Export hoare.
From iris.proofmode Require Import invariants tactics.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import