Commit f081f494 authored by Robbert Krebbers's avatar Robbert Krebbers

Type class for ⊤ to get overloaded notation for entire set.

parent 2392dc03
......@@ -131,12 +131,12 @@ Section proof.
saved_prop_own i Q (Q - R))%I.
Lemma newchan_spec (P : iProp) (Q : val iProp) :
( l, recv l P send l P - Q (LocV l)) wp coPset_all (newchan '()) Q.
( l, recv l P send l P - Q (LocV l)) wp (newchan '()) Q.
Proof.
Abort.
Lemma signal_spec l P (Q : val iProp) :
(send l P P Q '()) wp coPset_all (signal (LocV l)) Q.
(send l P P Q '()) wp (signal (LocV l)) Q.
Proof.
rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
apply exist_elim=>γ. wp_rec. (* FIXME wp_let *)
......@@ -167,12 +167,12 @@ Section proof.
Abort.
Lemma wait_spec l P (Q : val iProp) :
(recv l P (P - Q '())) wp coPset_all (wait (LocV l)) Q.
(recv l P (P - Q '())) wp (wait (LocV l)) Q.
Proof.
Abort.
Lemma split_spec l P1 P2 Q :
(recv l (P1 P2) (recv l P1 recv l P2 - Q '())) wp coPset_all Skip Q.
(recv l (P1 P2) (recv l P1 recv l P2 - Q '())) wp Skip Q.
Proof.
Abort.
......
......@@ -77,7 +77,7 @@ Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e Q :
( Q (LitV LitUnit) wp (Σ:=Σ) coPset_all e (λ _, True)) wp E (Fork e) Q.
( Q (LitV LitUnit) wp (Σ:=Σ) e (λ _, True)) wp E (Fork e) Q.
Proof.
rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
last by intros; inv_step; eauto.
......
......@@ -209,6 +209,9 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
Class Empty A := empty: A.
Notation "∅" := empty : C_scope.
Class Top A := top : A.
Notation "⊤" := top : C_scope.
Class Union A := union: A A A.
Instance: Params (@union) 2.
Infix "∪" := union (at level 50, left associativity) : C_scope.
......@@ -311,7 +314,7 @@ Instance: Params (@disjoint) 2.
Infix "⊥" := disjoint (at level 70) : C_scope.
Notation "(⊥)" := disjoint (only parsing) : C_scope.
Notation "( X ⊥.)" := (disjoint X) (only parsing) : C_scope.
Notation "(.⊥ X )" := (λ Y, Y X) (only parsing) : C_scope.
Notation "(.⊥ X )" := (λ Y, Y X) (only parsing) : C_scope.
Infix "⊥*" := (Forall2 ()) (at level 70) : C_scope.
Notation "(⊥*)" := (Forall2 ()) (only parsing) : C_scope.
Infix "⊥**" := (Forall2 (*)) (at level 70) : C_scope.
......
......@@ -6,7 +6,7 @@ From prelude Require Export prelude.
Record bset (A : Type) : Type := mkBSet { bset_car : A bool }.
Arguments mkBSet {_} _.
Arguments bset_car {_} _ _.
Definition bset_all {A} : bset A := mkBSet (λ _, true).
Instance bset_top {A} : Top (bset A) := mkBSet (λ _, true).
Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false).
Instance bset_singleton {A} `{ x y : A, Decision (x = y)} :
Singleton A (bset A) := λ x, mkBSet (λ y, bool_decide (y = x)).
......
......@@ -148,7 +148,7 @@ Instance coPset_singleton : Singleton positive coPset := λ p,
coPset_singleton_raw p coPset_singleton_wf _.
Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
Instance coPset_empty : Empty coPset := coPLeaf false I.
Definition coPset_all : coPset := coPLeaf true I.
Instance coPset_top : Top coPset := coPLeaf true I.
Instance coPset_union : Union coPset := λ X Y,
let (t1,Ht1) := X in let (t2,Ht2) := Y in
(t1 t2) coPset_union_wf _ _ Ht1 Ht2.
......
......@@ -6,7 +6,7 @@ From prelude Require Export prelude.
Record set (A : Type) : Type := mkSet { set_car : A Prop }.
Arguments mkSet {_} _.
Arguments set_car {_} _ _.
Definition set_all {A} : set A := mkSet (λ _, True).
Instance set_all {A} : Top (set A) := mkSet (λ _, True).
Instance set_empty {A} : Empty (set A) := mkSet (λ _, False).
Instance set_singleton {A} : Singleton A (set A) := λ x, mkSet (x =).
Instance set_elem_of {A} : ElemOf A (set A) := λ x X, set_car X x.
......
......@@ -14,16 +14,15 @@ Implicit Types Q : val Λ → iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
Transparent uPred_holds.
Notation wptp n := (Forall3 (λ e Q r, uPred_holds (wp coPset_all e Q) n r)).
Notation wptp n := (Forall3 (λ e Q r, uPred_holds (wp e Q) n r)).
Lemma wptp_le Qs es rs n n' :
{n'} (big_op rs) wptp n es Qs rs n' n wptp n' es Qs rs.
Proof. induction 2; constructor; eauto using uPred_weaken. Qed.
Lemma nsteps_wptp Qs k n tσ1 tσ2 rs1 :
nsteps step k tσ1 tσ2
1 < n wptp (k + n) (tσ1.1) Qs rs1
wsat (k + n) coPset_all (tσ1.2) (big_op rs1)
rs2 Qs', wptp n (tσ2.1) (Qs ++ Qs') rs2
wsat n coPset_all (tσ2.2) (big_op rs2).
wsat (k + n) (tσ1.2) (big_op rs1)
rs2 Qs', wptp n (tσ2.1) (Qs ++ Qs') rs2 wsat n (tσ2.2) (big_op rs2).
Proof.
intros Hsteps Hn; revert Qs rs1.
induction Hsteps as [|k ?? tσ3 [e1 σ1 e2 σ2 ef t1 t2 ?? Hstep] Hsteps IH];
......@@ -31,7 +30,7 @@ Proof.
{ by intros; exists rs, []; rewrite right_id_L. }
intros (Qs1&?&rs1&?&->&->&?&
(Q&Qs2&r&rs2&->&->&Hwp&?)%Forall3_cons_inv_l)%Forall3_app_inv_l ?.
destruct (wp_step_inv coPset_all Q e1 (k + n) (S (k + n)) σ1 r
destruct (wp_step_inv Q e1 (k + n) (S (k + n)) σ1 r
(big_op (rs1 ++ rs2))) as [_ Hwpstep]; eauto using values_stuck.
{ by rewrite right_id_L -big_op_cons Permutation_middle. }
destruct (Hwpstep e2 σ2 ef) as (r2&r2'&Hwsat&?&?); auto; clear Hwpstep.
......@@ -52,11 +51,11 @@ Proof.
by rewrite -Permutation_middle /= big_op_app.
Qed.
Lemma ht_adequacy_steps P Q k n e1 t2 σ1 σ2 r1 :
{{ P }} e1 @ coPset_all {{ Q }}
{{ P }} e1 @ {{ Q }}
nsteps step k ([e1],σ1) (t2,σ2)
1 < n wsat (k + n) coPset_all σ1 r1
1 < n wsat (k + n) σ1 r1
P (k + n) r1
rs2 Qs', wptp n t2 (Q :: Qs') rs2 wsat n coPset_all σ2 (big_op rs2).
rs2 Qs', wptp n t2 (Q :: Qs') rs2 wsat n σ2 (big_op rs2).
Proof.
intros Hht ????; apply (nsteps_wptp [Q] k n ([e1],σ1) (t2,σ2) [r1]);
rewrite /big_op ?right_id; auto.
......@@ -66,9 +65,9 @@ Proof.
Qed.
Lemma ht_adequacy_own Q e1 t2 σ1 m σ2 :
m
{{ ownP σ1 ownG m }} e1 @ coPset_all {{ Q }}
{{ ownP σ1 ownG m }} e1 @ {{ Q }}
rtc step ([e1],σ1) (t2,σ2)
rs2 Qs', wptp 2 t2 (Q :: Qs') rs2 wsat 2 coPset_all σ2 (big_op rs2).
rs2 Qs', wptp 2 t2 (Q :: Qs') rs2 wsat 2 σ2 (big_op rs2).
Proof.
intros Hv ? [k ?]%rtc_nsteps.
eapply ht_adequacy_steps with (r1 := (Res (Excl σ1) (Some m))); eauto; [|].
......@@ -87,7 +86,7 @@ Proof.
intros Hv ? Hs.
destruct (ht_adequacy_own (λ v', φ v')%I e (of_val v :: t2) σ1 m σ2)
as (rs2&Qs&Hwptp&?); auto.
{ by rewrite -(ht_mask_weaken E coPset_all). }
{ by rewrite -(ht_mask_weaken E ). }
inversion Hwptp as [|?? r ?? rs Hwp _]; clear Hwptp; subst.
apply wp_value_inv in Hwp; destruct (Hwp (big_op rs) 2 σ2) as [r' []]; auto.
by rewrite right_id_L.
......@@ -100,10 +99,10 @@ Lemma ht_adequacy_reducible E Q e1 e2 t2 σ1 m σ2 :
Proof.
intros Hv ? Hs [i ?]%elem_of_list_lookup He.
destruct (ht_adequacy_own Q e1 t2 σ1 m σ2) as (rs2&Qs&?&?); auto.
{ by rewrite -(ht_mask_weaken E coPset_all). }
destruct (Forall3_lookup_l (λ e Q r, wp coPset_all e Q 2 r) t2
{ by rewrite -(ht_mask_weaken E ). }
destruct (Forall3_lookup_l (λ e Q r, wp e Q 2 r) t2
(Q :: Qs) rs2 i e2) as (Q'&r2&?&?&Hwp); auto.
destruct (wp_step_inv coPset_all Q' e2 1 2 σ2 r2 (big_op (delete i rs2)));
destruct (wp_step_inv Q' e2 1 2 σ2 r2 (big_op (delete i rs2)));
rewrite ?right_id_L ?big_op_delete; auto.
Qed.
Theorem ht_adequacy_safe E Q e1 t2 σ1 m σ2 :
......
......@@ -23,7 +23,7 @@ Lemma ht_lift_step E1 E2
((P ={E2,E1}=> ownP σ1 P') e2 σ2 ef,
( φ e2 σ2 ef ownP σ2 P' ={E1,E2}=> Q1 e2 σ2 ef Q2 e2 σ2 ef)
{{ Q1 e2 σ2 ef }} e2 @ E2 {{ R }}
{{ Q2 e2 σ2 ef }} ef ?@ coPset_all {{ λ _, True }})
{{ Q2 e2 σ2 ef }} ef ?@ {{ λ _, True }})
{{ P }} e1 @ E2 {{ R }}.
Proof.
intros ?? Hsafe Hstep; apply (always_intro _ _), impl_intro_l.
......@@ -51,7 +51,7 @@ Lemma ht_lift_atomic_step
atomic e1
reducible e1 σ1
( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
( e2 σ2 ef, {{ φ e2 σ2 ef P }} ef ?@ coPset_all {{ λ _, True }})
( e2 σ2 ef, {{ φ e2 σ2 ef P }} ef ?@ {{ λ _, True }})
{{ ownP σ1 P }} e1 @ E {{ λ v, σ2 ef, ownP σ2 φ (of_val v) σ2 ef }}.
Proof.
intros ? Hsafe Hstep; set (φ' e σ ef := is_Some (to_val e) φ e σ ef).
......@@ -79,7 +79,7 @@ Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Q e1
( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef σ1 = σ2 φ e2 ef)
( e2 ef,
{{ φ e2 ef P }} e2 @ E {{ Q }}
{{ φ e2 ef P' }} ef ?@ coPset_all {{ λ _, True }})
{{ φ e2 ef P' }} ef ?@ {{ λ _, True }})
{{ (P P') }} e1 @ E {{ Q }}.
Proof.
intros ? Hsafe Hstep; apply (always_intro _ _), impl_intro_l.
......@@ -104,7 +104,7 @@ Lemma ht_lift_pure_det_step
to_val e1 = None
( σ1, reducible e1 σ1)
( σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' σ1 = σ2 e2 = e2' ef = ef')
({{ P }} e2 @ E {{ Q }} {{ P' }} ef ?@ coPset_all {{ λ _, True }})
({{ P }} e2 @ E {{ Q }} {{ P' }} ef ?@ {{ λ _, True }})
{{ (P P') }} e1 @ E {{ Q }}.
Proof.
intros ? Hsafe Hdet.
......
......@@ -15,7 +15,7 @@ Implicit Types σ : state Λ.
Implicit Types Q : val Λ iProp Λ Σ.
Transparent uPred_holds.
Notation wp_fork ef := (default True ef (flip (wp coPset_all) (λ _, True)))%I.
Notation wp_fork ef := (default True ef (flip (wp ) (λ _, True)))%I.
Lemma wp_lift_step E1 E2
(φ : expr Λ state Λ option (expr Λ) Prop) Q e1 σ1 :
......
......@@ -9,7 +9,7 @@ Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed.
Lemma nclose_nnil : nclose nnil = coPset_all.
Lemma nclose_nnil : nclose nnil = .
Proof. by apply (sig_eq_pi _). Qed.
Lemma encode_nclose N : encode N nclose N.
Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed.
......
......@@ -64,16 +64,14 @@ Section sts.
Proof. intros. by apply own_update, sts_update_frag_up. Qed.
Lemma sts_alloc N s :
φ s pvs N N ( γ, sts_ctx γ N φ
sts_own γ s (set_all sts.tok s)).
φ s pvs N N ( γ, sts_ctx γ N φ sts_own γ s ( sts.tok s)).
Proof.
eapply sep_elim_True_r.
{ apply (own_alloc (sts_auth s (set_all sts.tok s)) N).
{ apply (own_alloc (sts_auth s ( sts.tok s)) N).
apply sts_auth_valid; solve_elem_of. }
rewrite pvs_frame_l. apply pvs_strip_pvs.
rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
transitivity ( sts_inv γ φ
sts_own γ s (set_all sts.tok s))%I.
transitivity ( sts_inv γ φ sts_own γ s ( sts.tok s))%I.
{ rewrite /sts_inv -later_intro -(exist_intro s).
rewrite [(_ φ _)%I]comm -assoc. apply sep_mono_r.
by rewrite -own_op sts_op_auth_frag_up; last solve_elem_of. }
......
......@@ -28,7 +28,7 @@ CoInductive wp_pre {Λ Σ} (E : coPset)
0 < k < n E Ef =
wsat (S k) (E Ef) σ1 (r1 rf)
wp_go (E Ef) (wp_pre E Q)
(wp_pre coPset_all (λ _, True%I)) k rf e1 σ1)
(wp_pre (λ _, True%I)) k rf e1 σ1)
wp_pre E Q e1 n r1.
Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ)
(Q : val Λ iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Q e |}.
......@@ -102,7 +102,7 @@ Qed.
Lemma wp_step_inv E Ef Q e k n σ r rf :
to_val e = None 0 < k < n E Ef =
wp E e Q n r wsat (S k) (E Ef) σ (r rf)
wp_go (E Ef) (λ e, wp E e Q) (λ e, wp coPset_all e (λ _, True%I)) k rf e σ.
wp_go (E Ef) (λ e, wp E e Q) (λ e, wp e (λ _, True%I)) k rf e σ.
Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed.
Lemma wp_value' E Q v : Q v wp E (of_val v) Q.
......
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