Commit f46394dc authored by Ralf Jung's avatar Ralf Jung
Browse files

make goal a bit more readable

parent 57b8c4f3
......@@ -28,7 +28,7 @@ Definition ex1_opt : function :=
Lemma ex1_sim_body fs ft : {fs,ft} ex1 ≥ᶠ ex1_opt.
Proof.
intros r es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
intros rf es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
destruct els as [|efs []]; [done| |done]. simpl in SUBSTs.
destruct elt as [|eft []]; [done| |done]. simpl in SUBSTt. simplify_eq.
......
......@@ -276,3 +276,8 @@ Lemma tmap_lookup_core_pub (pm: tmapUR) t h:
pm !! t Some (to_tagKindR tkPub, h)
core pm !! t Some (to_tagKindR tkPub, h).
Proof. intros Eq. rewrite lookup_core Eq /core /= core_id //. Qed.
(** Resources that we own. *)
Definition res_callState (c: call_id) (cs: call_state) : resUR :=
((ε, {[c := to_callStateR cs]}), ε).
......@@ -3,7 +3,7 @@ From stbor.sim Require Export local invariant.
Notation "r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) : Φ" :=
(sim_local_body wsat vrel_expr fs ft r n%nat es%E σs et%E σt Φ)
(at level 70, format "r ⊨{ n , fs , ft } ( es , σs ) ( et , σt ) : Φ").
(at level 70, format "'[hv' r ⊨{ n , fs , ft } '/ ' '[ ' ( es , σs ) ']' '/' ≥ '/ ' '[ ' ( et , σt ) ']' '/' : Φ ']'").
Notation "⊨{ fs , ft } f1 ≥ᶠ f2" :=
(sim_local_fun wsat vrel_expr fs ft end_call_sat f1 f2)
......
......@@ -806,7 +806,7 @@ Abort.
Lemma sim_body_init_call fs ft r n es et σs σt Φ :
let σs' := mkState σs.(shp) σs.(sst) (σs.(snc) :: σs.(scs)) σs.(snp) (S σs.(snc)) in
let σt' := mkState σt.(shp) σt.(sst) (σt.(snc) :: σt.(scs)) σt.(snp) (S σt.(snc)) in
let r' : resUR := ((ε, {[σt.(snc) := to_callStateR (csOwned )]}), ε) in
let r' : resUR := res_callState σt.(snc) (csOwned ) in
r r' {n,fs,ft} (es, σs') (et, σt') : Φ
r {n,fs,ft} (InitCall es, σs) (InitCall et, σt) : Φ.
Proof.
......
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