Commit a12e05c2 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

WIP

parent d0a65bdf
......@@ -843,6 +843,27 @@ Section option.
apply cmra_core_idemp' in Hx'. setoid_subst.
by apply cmra_included_core_reflexive with y.
Qed.
Lemma option_includedN n mx my :
mx {n} my mx = None x y, mx = Some x my = Some y
(x {n} y x {n} y).
Proof.
split.
- intros [mz Hmz].
destruct mx as [x|]; [right|by left].
destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
destruct mz as [z|]; inversion_clear Hmz; split_and?; auto; setoid_subst.
left. exists z. auto.
- intros [->|(x&y&->&->&[(z&Hz)|Hxy])]; try (by exists my; destruct my; constructor).
by exists (Some z); constructor.
exists None. constructor. done.
Qed.
Lemma option_includedN_Some {_:TotalCore A} n x y :
Some x {n} Some y -> x {n} y.
Proof.
intros [[z|]Hz]; inversion_clear Hz.
- exists z; auto.
- exists (core' x). by rewrite cmra_core'_r.
Qed.
End option.
Instance option_fmap_cmra_monotone {A B : cmraT} (f: A B) `{!CMRAMonotone f} :
......
......@@ -9,7 +9,7 @@ Record uPred (M : cmraT) : Type := IProp {
uPred_ne n x1 x2 : uPred_holds n x1 x1 {n} x2 uPred_holds n x2;
uPred_le n1 n2 x :
uPred_holds n1 x n2 n1 {n2} x uPred_holds n2 x;
uPred_weaken n x1 x2 :
uPred_weaken n x1 x2 :
uPred_holds n x1 x1 x2 {n} x2 uPred_holds n x2
}.
Arguments uPred_holds {_} _ _ _ : simpl never.
......
......@@ -18,7 +18,7 @@ Implicit Types m : iGst Λ Σ.
Notation wptp n := (Forall3 (λ e Φ r, uPred_holds (wp e Φ) n r)).
Lemma wptp_le Φs es rs n n' :
{n'} (big_op rs) wptp n es Φs rs n' n wptp n' es Φs rs.
Proof. induction 2; constructor; eauto using uPred_weaken. Qed.
Proof. induction 2; constructor; eauto using uPred_le. Qed.
Lemma nsteps_wptp Φs k n tσ1 tσ2 rs1 :
nsteps step k tσ1 tσ2
1 < n wptp (k + n) (tσ1.1) Φs rs1
......@@ -51,7 +51,7 @@ Proof.
{ rewrite /option_list right_id_L.
apply Forall3_app, Forall3_cons; eauto using wptp_le.
rewrite wp_eq.
apply uPred_weaken with (k + n) r2; eauto using cmra_included_l. }
eauto using uPred_weaken, uPred_le, cmra_included_l. }
by rewrite -Permutation_middle /= big_op_app.
Qed.
Lemma wp_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 :
......@@ -74,9 +74,9 @@ Lemma wp_adequacy_own Φ e1 t2 σ1 m σ2 :
rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 wsat 2 σ2 (big_op rs2).
Proof.
intros Hv ? [k ?]%rtc_nsteps.
eapply wp_adequacy_steps with (r1 := (Res (Excl σ1) m)); eauto; [|].
eapply wp_adequacy_steps with (r1 := (Res (Some (Excl σ1)) m)); eauto; [|].
{ by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
uPred.unseal; exists (Res (Excl σ1) ), (Res m); split_and?.
uPred.unseal; exists (Res (Some (Excl σ1)) ), (Res m); split_and?.
- by rewrite Res_op ?left_id ?right_id.
- rewrite /ownP; uPred.unseal; rewrite /uPred_holds //=.
- by apply ownG_spec.
......
......@@ -59,7 +59,7 @@ Section auth.
φ a (|={E}=> γ, auth_ctx γ N φ auth_own γ a).
Proof.
iIntros {??} "Hφ". rewrite /auth_own /auth_ctx.
iPvs (own_alloc (Auth (Excl a) a)) as {γ} "Hγ"; first done.
iPvs (own_alloc (Auth (Some (Excl a)) a)) as {γ} "Hγ"; first done.
iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
iPvs (inv_alloc N _ (auth_inv γ φ) with "-[Hγ']"); first done.
{ iNext. iExists a. by iFrame "Hφ". }
......
......@@ -25,6 +25,7 @@ Proof.
- apply cmra_transport_valid, cmra_unit_valid.
- intros x; rewrite /empty /inG_empty; destruct inG_prf. by rewrite left_id.
- apply _.
- apply _.
Qed.
(** * Properties of own *)
......
......@@ -63,16 +63,21 @@ Lemma ownI_spec n r i P :
Proof.
intros (?&?&?). rewrite /ownI; uPred.unseal.
rewrite /uPred_holds/=res_includedN/= singleton_includedN; split.
- intros [(P'&Hi&HP) _]; rewrite Hi.
- intros [(P'&Hi&HP%option_includedN_Some) _]; rewrite Hi.
apply Some_dist, symmetry, agree_valid_includedN; last done.
by apply lookup_validN with (wld r) i.
- intros ?; split_and?; try apply cmra_unit_leastN; eauto.
Qed.
Lemma ownP_spec n r σ : {n} r (ownP σ) n r pst r Excl σ.
Lemma ownP_spec n r σ : {n} r (ownP σ) n r pst r Some (Excl σ).
Proof.
intros (?&?&?). rewrite /ownP; uPred.unseal.
rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
rewrite (timeless_iff n). naive_solver (apply cmra_unit_leastN).
intros (?&Hpst&?). rewrite /ownP; uPred.unseal.
rewrite /uPred_holds /= res_includedN /= option_includedN.
split.
- intro HH. revert HH Hpst. intros [_[[|(x&y&Hx&->&[[z Hz]|Hxy])]_]]. done.
by destruct x, z; inversion Hz.
apply (@timeless_iff _ _ _ _) in Hxy. by inversion Hx; setoid_subst.
- intros Hr. inversion Hr. split_and?; try apply cmra_unit_leastN.
right. do 2 eexists. split_and?; eauto. setoid_subst. auto.
Qed.
Lemma ownG_spec n r m : (ownG m) n r m {n} gst r.
Proof.
......
......@@ -18,11 +18,12 @@ Next Obligation.
intros Λ Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *.
apply HP; auto. by rewrite (dist_le _ _ _ _ Hr); last lia.
Qed.
Next Obligation.
intros Λ Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst.
Next Obligation. repeat intro; auto. Qed.
Next Obligation. simpl.
intros Λ Σ E1 E2 P n r1 r2 HP [r3 ?] ? rf k Ef σ ?? Hws; setoid_subst.
destruct (HP (r3rf) k Ef σ) as (r'&?&Hws'); rewrite ?(assoc op); auto.
exists (r' r3); rewrite -assoc; split; last done.
apply uPred_weaken with k r'; eauto using cmra_included_l.
apply uPred_weaken with r'; eauto using cmra_included_l.
Qed.
Definition pvs_aux : { x | x = @pvs_def }. by eexists. Qed.
......@@ -62,7 +63,7 @@ Proof. apply ne_proper, _. Qed.
Lemma pvs_intro E P : P |={E}=> P.
Proof.
rewrite pvs_eq. split=> n r ? HP rf k Ef σ ???; exists r; split; last done.
apply uPred_weaken with n r; eauto.
apply uPred_le with n; auto.
Qed.
Lemma pvs_mono E1 E2 P Q : P Q (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof.
......@@ -75,7 +76,7 @@ Proof.
rewrite pvs_eq uPred.timelessP_spec=> HP.
uPred.unseal; split=>-[|n] r ? HP' rf k Ef σ ???; first lia.
exists r; split; last done.
apply HP, uPred_weaken with n r; eauto using cmra_validN_le.
apply HP, uPred_le with n; eauto using cmra_validN_le.
Qed.
Lemma pvs_trans E1 E2 E3 P :
E2 E1 E3 (|={E1,E2}=> |={E2,E3}=> P) (|={E1,E3}=> P).
......@@ -96,7 +97,7 @@ Proof.
destruct (HP (r2 rf) k Ef σ) as (r'&?&?); eauto.
{ by rewrite assoc -(dist_le _ _ _ _ Hr); last lia. }
exists (r' r2); split; last by rewrite -assoc.
exists r', r2; split_and?; auto; apply uPred_weaken with n r2; auto.
exists r', r2; split_and?; auto; apply uPred_le with n; auto.
Qed.
Lemma pvs_openI i P : ownI i P (|={{[i]},}=> P).
Proof.
......@@ -105,17 +106,17 @@ Proof.
destruct (wsat_open k Ef σ (r rf) i P) as (rP&?&?); auto.
{ rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. }
exists (rP r); split; last by rewrite (left_id_L _ _) -assoc.
eapply uPred_weaken with (S k) rP; eauto using cmra_included_l.
eapply uPred_weaken with rP; eauto using cmra_included_l.
Qed.
Lemma pvs_closeI i P : (ownI i P P) (|={,{[i]}}=> True).
Proof.
rewrite pvs_eq. uPred.unseal; split=> -[|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia.
exists ; split; [done|].
rewrite left_id; apply wsat_close with P r.
- apply ownI_spec, uPred_weaken with (S n) r; auto.
- apply ownI_spec, uPred_le with (S n); auto.
- set_solver +HE.
- by rewrite -(left_id_L () Ef).
- apply uPred_weaken with n r; auto.
- apply uPred_le with n; auto.
Qed.
Lemma pvs_ownG_updateP E m (P : iGst Λ Σ Prop) :
m ~~>: P ownG m (|={E}=> m', P m' ownG m').
......@@ -131,7 +132,7 @@ Proof.
rewrite pvs_eq. intros ?; rewrite /ownI; uPred.unseal.
split=> -[|n] r ? HP rf [|k] Ef σ ???; try lia.
destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto.
{ apply uPred_weaken with n r; eauto. }
{ apply uPred_le with n; eauto. }
exists (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ).
split; [|done]. by exists i; split; rewrite /uPred_holds /=.
Qed.
......
......@@ -38,11 +38,14 @@ Next Obligation.
intros rf k Ef σ1 ?; rewrite -(dist_le _ _ _ _ Hr); naive_solver.
Qed.
Next Obligation.
intros Λ Σ E e Φ n1 n2 r1 r2; revert Φ E e n2 r1 r2.
induction n1 as [n1 IH] using lt_wf_ind; intros Φ E e n2 r1 r1'.
intros Λ Σ E e Φ n1 n2 r [|n1' r1 e1 ? Hgo]; constructor; eauto using uPred_le.
Qed.
Next Obligation.
intros Λ Σ E e Φ n r1 r2; revert Φ E e r1 r2.
induction n as [n IH] using lt_wf_ind; intros Φ E e r1 r1'.
destruct 1 as [|n1 r1 e1 ? Hgo].
- constructor; eauto using uPred_weaken.
- intros [rf' Hr] ??; constructor; [done|intros rf k Ef σ1 ???].
- intros [rf' Hr] ?; constructor; [done|intros rf k Ef σ1 ???].
destruct (Hgo (rf' rf) k Ef σ1) as [Hsafe Hstep];
rewrite ?assoc -?Hr; auto; constructor; [done|].
intros e2 σ2 ef ?; destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
......@@ -194,7 +197,7 @@ Proof.
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
exists (r2 rR), r2'; split_and?; auto.
- by rewrite -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR).
- apply IH; eauto using uPred_weaken.
- apply IH; eauto using uPred_le.
Qed.
Lemma wp_frame_step_r E E1 E2 e Φ R :
to_val e = None E E1 E2 E1
......
......@@ -36,7 +36,10 @@ Next Obligation.
by rewrite (dist_le _ _ _ _ Hr1); last omega.
Qed.
Next Obligation.
intros wp E e1 Φ n1 n2 r1 ? Hwp [r2 ?] ?? rf k Ef σ1 ???; setoid_subst.
intros wp E e1 Φ n1 n2 r1 Hwp ?? rf k Ef σ1 ???; setoid_subst; auto.
Qed.
Next Obligation.
intros wp E e1 Φ n r1 ? Hwp [r2 ?] ? rf k Ef σ1 ???; setoid_subst.
destruct (Hwp (r2 rf) k Ef σ1) as [Hval Hstep]; rewrite ?assoc; auto.
split.
- intros v Hv. destruct (Hval v Hv) as [r3 [??]].
......
......@@ -3,7 +3,7 @@ From iris.program_logic Require Import model saved_prop.
Module ModelTest. (* Make sure we got the notations right. *)
Definition iResTest {Λ : language} {Σ : iFunctor}
(w : iWld Λ Σ) (p : iPst Λ) (g : iGst Λ Σ) : iRes Λ Σ := Res w p g.
(w : iWld Λ Σ) (p : option (iPst Λ)) (g : iGst Λ Σ) : iRes Λ Σ := Res w p g.
End ModelTest.
Module SavedPropTest.
......
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