Commit 8a9de8a8 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'gen_proofmode' into janno/monfun

parents 5e0d1e32 cf4f1269
......@@ -42,7 +42,6 @@ opam:
build-coq.8.7.dev:
<<: *template
stage: build_more
variables:
OPAM_PINS: "coq version 8.7.dev"
artifacts:
......
......@@ -29,6 +29,7 @@ theories/bi/interface.v
theories/bi/derived_connectives.v
theories/bi/derived_laws.v
theories/bi/big_op.v
theories/bi/updates.v
theories/bi/bi.v
theories/bi/tactics.v
theories/bi/fractional.v
......
......@@ -42,9 +42,10 @@ Proof.
Qed.
(** * Derived rules *)
Global Instance bupd_mono' : Proper (() ==> ()) (@uPred_bupd M).
Global Instance bupd_mono' : Proper (() ==> ()) (@bupd _ (@uPred_bupd M)).
Proof. intros P Q; apply bupd_mono. Qed.
Global Instance bupd_flip_mono' : Proper (flip () ==> flip ()) (@uPred_bupd M).
Global Instance bupd_flip_mono' :
Proper (flip () ==> flip ()) (@bupd _ (@uPred_bupd M)).
Proof. intros P Q; apply bupd_mono. Qed.
Lemma bupd_frame_l R Q : (R |==> Q) == R Q.
Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
......@@ -61,7 +62,7 @@ Proof.
Qed.
Lemma except_0_bupd P : (|==> P) (|==> P).
Proof.
rewrite /sbi_except_0. apply or_elim; auto using bupd_mono, or_intro_r.
rewrite /sbi_except_0. apply or_elim; eauto using bupd_mono, or_intro_r.
by rewrite -bupd_intro -or_intro_l.
Qed.
......
......@@ -7,85 +7,64 @@ Set Default Proof Using "Type".
Export invG.
Import uPred.
Program Definition fupd_def `{invG Σ}
(E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
Definition uPred_fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
(wsat ownE E1 == (wsat ownE E2 P))%I.
Definition fupd_aux : seal (@fupd_def). by eexists. Qed.
Definition fupd := unseal fupd_aux.
Definition fupd_eq : @fupd = @fupd_def := seal_eq fupd_aux.
Arguments fupd {_ _} _ _ _%I.
Instance: Params (@fupd) 4.
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }=> Q") : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)%I
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=∗ Q") : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)
(at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
Notation "|={ E }=> Q" := (fupd E E Q)
(at level 99, E at level 50, Q at level 200,
format "|={ E }=> Q") : bi_scope.
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=∗ Q") : bi_scope.
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)
(at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
Definition uPred_fupd_aux `{invG Σ} : seal uPred_fupd_def. by eexists. Qed.
Instance uPred_fupd `{invG Σ} : FUpd (iProp Σ):= unseal uPred_fupd_aux.
Definition uPred_fupd_eq `{invG Σ} : fupd = uPred_fupd_def := seal_eq uPred_fupd_aux.
Section fupd.
Context `{invG Σ}.
Implicit Types P Q : iProp Σ.
Global Instance fupd_ne E1 E2 : NonExpansive (@fupd Σ _ E1 E2).
Proof. rewrite fupd_eq. solve_proper. Qed.
Global Instance fupd_proper E1 E2 : Proper (() ==> ()) (@fupd Σ _ E1 E2).
Global Instance fupd_ne E1 E2 : NonExpansive (fupd E1 E2).
Proof. rewrite uPred_fupd_eq. solve_proper. Qed.
Global Instance fupd_proper E1 E2 : Proper (() ==> ()) (fupd E1 E2).
Proof. apply ne_proper, _. Qed.
Lemma fupd_intro_mask E1 E2 P : E2 E1 P |={E1,E2}=> |={E2,E1}=> P.
Proof.
intros (E1''&->&?)%subseteq_disjoint_union_L.
rewrite fupd_eq /fupd_def ownE_op //.
rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
Qed.
Lemma except_0_fupd E1 E2 P : (|={E1,E2}=> P) ={E1,E2}= P.
Proof. rewrite fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed.
Proof. rewrite uPred_fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed.
Lemma bupd_fupd E P : (|==> P) ={E}= P.
Proof. rewrite fupd_eq /fupd_def. by iIntros ">? [$ $] !> !>". Qed.
Proof. rewrite uPred_fupd_eq. by iIntros ">? [$ $] !> !>". Qed.
Lemma fupd_mono E1 E2 P Q : (P Q) (|={E1,E2}=> P) |={E1,E2}=> Q.
Proof.
rewrite fupd_eq /fupd_def. iIntros (HPQ) "HP HwE".
rewrite -HPQ. by iApply "HP".
rewrite uPred_fupd_eq. iIntros (HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
Qed.
Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) |={E1,E3}=> P.
Proof.
rewrite fupd_eq /fupd_def. iIntros "HP HwE".
rewrite uPred_fupd_eq. iIntros "HP HwE".
iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
Qed.
Lemma fupd_mask_frame_r' E1 E2 Ef P :
E1 ## Ef (|={E1,E2}=> E2 ## Ef P) ={E1 Ef,E2 Ef}= P.
Proof.
intros. rewrite fupd_eq /fupd_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
intros. rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
iIntros "Hvs (Hw & HE1 &HEf)".
iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
iIntros "!> !>". by iApply "HP".
Qed.
Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) Q ={E1,E2}= P Q.
Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP $]". Qed.
Proof. rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros "[HwP $]". Qed.
Lemma fupd_plain' E1 E2 E2' P Q `{!Plain P} :
E1 E2
(Q ={E1, E2'}= P) - (|={E1, E2}=> Q) ={E1}= (|={E1, E2}=> Q) P.
Proof.
iIntros ((E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
rewrite fupd_eq /fupd_def ownE_op //. iIntros "H".
rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. iIntros "H".
iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
iAssert ( P)%I as "#HP".
{ by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
......@@ -94,16 +73,16 @@ Qed.
Lemma later_fupd_plain E P `{!Plain P} : ( |={E}=> P) ={E}= P.
Proof.
rewrite fupd_eq /fupd_def. iIntros "HP [Hw HE]".
rewrite uPred_fupd_eq /uPred_fupd_def. iIntros "HP [Hw HE]".
iAssert ( P)%I with "[-]" as "#$"; last by iFrame.
iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
Qed.
(** * Derived rules *)
Global Instance fupd_mono' E1 E2 : Proper (() ==> ()) (@fupd Σ _ E1 E2).
Global Instance fupd_mono' E1 E2 : Proper (() ==> ()) (fupd E1 E2).
Proof. intros P Q; apply fupd_mono. Qed.
Global Instance fupd_flip_mono' E1 E2 :
Proper (flip () ==> flip ()) (@fupd Σ _ E1 E2).
Proper (flip () ==> flip ()) (fupd E1 E2).
Proof. intros P Q; apply fupd_mono. Qed.
Lemma fupd_intro E P : P ={E}= P.
......
......@@ -45,7 +45,7 @@ Qed.
Lemma inv_alloc N E P : P ={E}= inv N P.
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
rewrite inv_eq /inv_def uPred_fupd_eq. iIntros "HP [Hw $]".
iMod (ownI_alloc ( (N : coPset)) P with "[$HP $Hw]")
as (i ?) "[$ ?]"; auto using fresh_inv_name.
Qed.
......@@ -53,7 +53,7 @@ Qed.
Lemma inv_alloc_open N E P :
N E (|={E, E∖↑N}=> inv N P (P ={E∖↑N, E}= True))%I.
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros (Sub) "[Hw HE]".
rewrite inv_eq /inv_def uPred_fupd_eq. iIntros (Sub) "[Hw HE]".
iMod (ownI_alloc_open ( (N : coPset)) P with "Hw")
as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
iAssert (ownE {[i]} ownE ( N {[i]}) ownE (E N))%I
......@@ -72,7 +72,7 @@ Qed.
Lemma inv_open E N P :
N E inv N P ={E,E∖↑N}= P ( P ={E∖↑N,E}= True).
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def; iDestruct 1 as (i) "[Hi #HiP]".
rewrite inv_eq /inv_def uPred_fupd_eq /uPred_fupd_def; iDestruct 1 as (i) "[Hi #HiP]".
iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
rewrite {1 4}(union_difference_L ( N) E) // ownE_op; last set_solver.
rewrite {1 5}(union_difference_L {[ i ]} ( N)) // ownE_op; last set_solver.
......
From iris.algebra Require Export cmra updates.
From iris.bi Require Export derived_connectives.
From iris.bi Require Export derived_connectives updates.
From stdpp Require Import finite.
Set Default Proof Using "Type".
Local Hint Extern 1 (_ _) => etrans; [eassumption|].
......@@ -328,16 +328,17 @@ Next Obligation.
apply uPred_mono with x'; eauto using cmra_includedN_l.
Qed.
Next Obligation. naive_solver. Qed.
Definition uPred_bupd_aux : seal (@uPred_bupd_def). by eexists. Qed.
Definition uPred_bupd {M} := unseal uPred_bupd_aux M.
Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := seal_eq uPred_bupd_aux.
Definition uPred_bupd_aux {M} : seal (@uPred_bupd_def M). by eexists. Qed.
Instance uPred_bupd {M} : BUpd (uPred M) := unseal uPred_bupd_aux.
Definition uPred_bupd_eq {M} :
@bupd _ uPred_bupd = @uPred_bupd_def M := seal_eq uPred_bupd_aux.
Module uPred_unseal.
Definition unseal_eqs :=
(uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq,
uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
uPred_cmra_valid_eq, uPred_bupd_eq).
uPred_cmra_valid_eq, @uPred_bupd_eq).
Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_emp; simpl;
unfold uPred_emp, bi_pure, bi_and, bi_or, bi_impl, bi_forall, bi_exist,
......@@ -566,12 +567,6 @@ Coercion uPred_valid {M} : uPred M → Prop := bi_valid.
(* Latest notation *)
Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
Notation "|==> Q" := (uPred_bupd Q)
(at level 99, Q at level 200, format "|==> Q") : bi_scope.
Notation "P ==∗ Q" := (P |==> Q)
(at level 99, Q at level 200, only parsing) : stdpp_scope.
Notation "P ==∗ Q" := (P - |==> Q)%I
(at level 99, Q at level 200, format "P ==∗ Q") : bi_scope.
Module uPred.
Include uPred_unseal.
......@@ -599,14 +594,15 @@ Qed.
Global Instance cmra_valid_proper {A : cmraT} :
Proper (() ==> ()) (@uPred_cmra_valid M A) := ne_proper _.
Global Instance bupd_ne : NonExpansive (@uPred_bupd M).
Global Instance bupd_ne : NonExpansive (@bupd _ (@uPred_bupd M)).
Proof.
intros n P Q HPQ.
unseal; split=> n' x; split; intros HP k yf ??;
destruct (HP k yf) as (x'&?&?); auto;
exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
Qed.
Global Instance bupd_proper : Proper (() ==> ()) (@uPred_bupd M) := ne_proper _.
Global Instance bupd_proper :
Proper (() ==> ()) (@bupd _ (@uPred_bupd M)) := ne_proper _.
(** BI instances *)
......
From iris.bi Require Export derived_laws big_op.
From iris.bi Require Export derived_laws big_op updates.
Set Default Proof Using "Type".
Module Import bi.
......
......@@ -530,4 +530,5 @@ Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed.
Lemma later_false_em P : P False ( False P).
Proof. eapply sbi_mixin_later_false_em, sbi_sbi_mixin. Qed.
End sbi_laws.
End bi.
From stdpp Require Import coPset.
From iris.bi Require Import interface.
Class BUpd (A : Type) : Type := bupd : A A.
Instance : Params (@bupd) 2.
Notation "|==> Q" := (bupd Q)
(at level 99, Q at level 200, format "|==> Q") : bi_scope.
Notation "P ==∗ Q" := (P |==> Q)
(at level 99, Q at level 200, only parsing) : stdpp_scope.
Notation "P ==∗ Q" := (P - |==> Q)%I
(at level 99, Q at level 200, format "P ==∗ Q") : bi_scope.
Class FUpd (A : Type) : Type := fupd : coPset coPset A A.
Instance: Params (@fupd) 4.
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }=> Q") : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)%I
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=∗ Q") : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)
(at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
Notation "|={ E }=> Q" := (fupd E E Q)
(at level 99, E at level 50, Q at level 200,
format "|={ E }=> Q") : bi_scope.
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=∗ Q") : bi_scope.
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)
(at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
......@@ -73,7 +73,7 @@ Lemma wp_step e1 σ1 e2 σ2 efs Φ :
world σ1 WP e1 {{ Φ }} == |==> (world σ2 WP e2 {{ Φ }} wptp efs).
Proof.
rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]".
rewrite (val_stuck e1 σ1 e2 σ2 efs) // fupd_eq /fupd_def.
rewrite (val_stuck e1 σ1 e2 σ2 efs) // uPred_fupd_eq.
iMod ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
iModIntro; iNext.
iMod ("H" $! e2 σ2 efs with "[%] [$Hw $HE]") as ">($ & $ & $ & $)"; auto.
......@@ -125,7 +125,7 @@ Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
Proof.
intros. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
iDestruct 1 as (e2 t2' ?) "((Hw & HE & _) & H & _)"; simplify_eq.
iDestruct (wp_value_inv with "H") as "H". rewrite fupd_eq /fupd_def.
iDestruct (wp_value_inv with "H") as "H". rewrite uPred_fupd_eq.
iMod ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
Qed.
......@@ -133,8 +133,8 @@ Lemma wp_safe e σ Φ :
world σ - WP e {{ Φ }} == is_Some (to_val e) reducible e σ⌝.
Proof.
rewrite wp_unfold /wp_pre. iIntros "(Hw&HE&Hσ) H".
destruct (to_val e) as [v|] eqn:?; [eauto 10|].
rewrite fupd_eq. iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; eauto 10 with iFrame.
destruct (to_val e) as [v|] eqn:?; [eauto 10|]. rewrite uPred_fupd_eq.
iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; eauto 10 with iFrame.
Qed.
Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
......@@ -157,7 +157,7 @@ Proof.
intros ?. rewrite wptp_steps // bupd_iter_frame_l laterN_later.
apply: bupd_iter_laterN_mono.
iIntros "[Hback H]"; iDestruct "H" as (e2' t2' ->) "[(Hw&HE&Hσ) _]".
rewrite fupd_eq.
rewrite uPred_fupd_eq.
iMod ("Hback" with "Hσ [$Hw $HE]") as "> (_ & _ & $)"; auto.
Qed.
End adequacy.
......@@ -172,14 +172,14 @@ Proof.
intros Hwp; split.
- intros t2 σ2 v2 [n ?]%rtc_nsteps.
eapply (soundness (M:=iResUR Σ) _ (S (S n))).
iMod wsat_alloc as (Hinv) "[Hw HE]".
rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "[HI Hwp]".
iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
- intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
eapply (soundness (M:=iResUR Σ) _ (S (S n))).
iMod wsat_alloc as (Hinv) "[Hw HE]".
rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "[HI Hwp]".
iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
Qed.
......@@ -194,8 +194,8 @@ Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ :
Proof.
intros Hwp [n ?]%rtc_nsteps.
eapply (soundness (M:=iResUR Σ) _ (S (S n))).
iMod wsat_alloc as (Hinv) "[Hw HE]".
rewrite {1}fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
rewrite {1}uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "(HIstate & Hwp & Hclose)".
iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
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