pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge branch 'master' of github.com:achlipala/frap

Browse source
This commit is contained in:
Adam Chlipala 2020-04-29 16:06:34 -04:00
commit 1c91cf3d5c
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
ConcurrentSeparationLogic_template.v
View file

@ -9,8 +9,8 @@ Set Asymmetric Patterns.
Notation heap := (fmap nat nat). Notation heap := (fmap nat nat).
Notation locks := (set nat). Notation locks := (set nat).
Hint Extern 1 (_ <= _) => linear_arithmetic. Hint Extern 1 (_ <= _) => linear_arithmetic : core.
Hint Extern 1 (@eq nat _ _) => linear_arithmetic. Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
Ltac simp := repeat (simplify; subst; propositional; Ltac simp := repeat (simplify; subst; propositional;
try match goal with try match goal with
@ -187,7 +187,7 @@ Module Import S <: SEP.
t. t.
Qed. Qed.
Hint Resolve split_empty_bwd'. Hint Resolve split_empty_bwd' : core.
Theorem extra_lift : forall (P : Prop) p, Theorem extra_lift : forall (P : Prop) p,
P P
@ -469,7 +469,7 @@ Proof.
apply try_me_first_easy. apply try_me_first_easy.
Qed. Qed.
Hint Resolve try_ptsto_first. Hint Resolve try_ptsto_first : core.
(** ** The nonzero shared counter *) (** ** The nonzero shared counter *)
@ -740,7 +740,7 @@ Qed.
(** * Soundness proof *) (** * Soundness proof *)
Hint Resolve himp_refl. Hint Resolve himp_refl : core.
Lemma invert_Return : forall linvs {result : Set} (r : result) P Q, Lemma invert_Return : forall linvs {result : Set} (r : result) P Q,
hoare_triple linvs P (Return r) Q hoare_triple linvs P (Return r) Q
@ -755,7 +755,7 @@ Proof.
rewrite IHhoare_triple; eauto. rewrite IHhoare_triple; eauto.
Qed. Qed.
Hint Constructors hoare_triple. Hint Constructors hoare_triple : core.
Lemma invert_Bind : forall linvs {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q, Lemma invert_Bind : forall linvs {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q,
hoare_triple linvs P (Bind c1 c2) Q hoare_triple linvs P (Bind c1 c2) Q