From 8fdc4e2cfd20ea580d2180c645f841c4d9ece4ce Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 10 May 2021 10:45:34 -0400 Subject: [PATCH] Revising before this week's lectures --- ConcurrentSeparationLogic.v | 12 ++++++------ ConcurrentSeparationLogic_template.v | 12 ++++++------ ProgramDerivation.v | 16 ++++++++-------- ProgramDerivation_template.v | 16 ++++++++-------- frap_book.tex | 2 +- 5 files changed, 29 insertions(+), 29 deletions(-) diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v index 6415b91..d0223e0 100644 --- a/ConcurrentSeparationLogic.v +++ b/ConcurrentSeparationLogic.v @@ -19,8 +19,8 @@ Set Asymmetric Patterns. Notation heap := (fmap nat nat). Notation locks := (set nat). -Hint Extern 1 (_ <= _) => linear_arithmetic : core. -Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. +Local Hint Extern 1 (_ <= _) => linear_arithmetic : core. +Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. Ltac simp := repeat (simplify; subst; propositional; try match goal with @@ -206,7 +206,7 @@ Module Import S <: SEP. t. Qed. - Hint Resolve split_empty_bwd' : core. + Local Hint Resolve split_empty_bwd' : core. Theorem extra_lift : forall (P : Prop) p, P @@ -502,7 +502,7 @@ Proof. apply try_me_first_easy. Qed. -Hint Resolve try_ptsto_first : core. +Local Hint Resolve try_ptsto_first : core. (** ** The nonzero shared counter *) @@ -837,7 +837,7 @@ Qed. * book PDF for a sketch of the important technical devices and lemmas in this * proof. *) -Hint Resolve himp_refl : core. +Local Hint Resolve himp_refl : core. Lemma invert_Return : forall linvs {result : Set} (r : result) P Q, hoare_triple linvs P (Return r) Q @@ -852,7 +852,7 @@ Proof. rewrite IHhoare_triple; eauto. Qed. -Hint Constructors hoare_triple : core. +Local Hint Constructors hoare_triple : core. Lemma invert_Bind : forall linvs {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q, hoare_triple linvs P (Bind c1 c2) Q diff --git a/ConcurrentSeparationLogic_template.v b/ConcurrentSeparationLogic_template.v index 3f9d7cb..4e06763 100644 --- a/ConcurrentSeparationLogic_template.v +++ b/ConcurrentSeparationLogic_template.v @@ -9,8 +9,8 @@ Set Asymmetric Patterns. Notation heap := (fmap nat nat). Notation locks := (set nat). -Hint Extern 1 (_ <= _) => linear_arithmetic : core. -Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. +Local Hint Extern 1 (_ <= _) => linear_arithmetic : core. +Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. Ltac simp := repeat (simplify; subst; propositional; try match goal with @@ -187,7 +187,7 @@ Module Import S <: SEP. t. Qed. - Hint Resolve split_empty_bwd' : core. + Local Hint Resolve split_empty_bwd' : core. Theorem extra_lift : forall (P : Prop) p, P @@ -483,7 +483,7 @@ Proof. apply try_me_first_easy. Qed. -Hint Resolve try_ptsto_first : core. +Local Hint Resolve try_ptsto_first : core. (** ** The nonzero shared counter *) @@ -752,7 +752,7 @@ Qed. (** * Soundness proof *) -Hint Resolve himp_refl : core. +Local Hint Resolve himp_refl : core. Lemma invert_Return : forall linvs {result : Set} (r : result) P Q, hoare_triple linvs P (Return r) Q @@ -767,7 +767,7 @@ Proof. rewrite IHhoare_triple; eauto. Qed. -Hint Constructors hoare_triple : core. +Local Hint Constructors hoare_triple : core. Lemma invert_Bind : forall linvs {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q, hoare_triple linvs P (Bind c1 c2) Q diff --git a/ProgramDerivation.v b/ProgramDerivation.v index 0575b30..52c9c1d 100644 --- a/ProgramDerivation.v +++ b/ProgramDerivation.v @@ -327,7 +327,7 @@ Inductive RefineMethods {state1 state2} (R : state1 -> state2 -> Prop) -> RefineMethods R (MethodsCons {| MethodName := name; MethodBody := f1 |} ms1) (MethodsCons {| MethodName := name; MethodBody := f2 |} ms2). -Hint Constructors RefineMethods : core. +Local Hint Constructors RefineMethods : core. (* When does [adt2] refine [adt1]? When there exists a simulation relation, * with respect to which the constructors and methods all satisfy the usual @@ -360,7 +360,7 @@ Definition split_counter := ADT { and method "value"[[self, _]] = ret (self, fst self + snd self) }. -Hint Extern 1 (@eq nat _ _) => simplify; linear_arithmetic : core. +Local Hint Extern 1 (@eq nat _ _) => simplify; linear_arithmetic : core. (* Here is why the new implementation is correct. *) Theorem split_counter_ok : adt_refine counter split_counter. @@ -393,7 +393,7 @@ Proof. subst; eauto. Qed. -Hint Immediate RefineMethods_refl : core. +Local Hint Immediate RefineMethods_refl : core. Theorem refine_refl : forall names (adt1 : adt names), adt_refine adt1 adt1. @@ -422,7 +422,7 @@ Proof. first_order. Qed. -Hint Resolve RefineMethods_trans : core. +Local Hint Resolve RefineMethods_trans : core. Theorem refine_trans : forall names (adt1 adt2 adt3 : adt names), adt_refine adt1 adt2 @@ -497,7 +497,7 @@ Proof. simplify; subst; eauto. Qed. -Hint Resolve ReplaceMethod_ok : core. +Local Hint Resolve ReplaceMethod_ok : core. (* It is OK to replace a method body if the new refines the old as a [comp]. *) Theorem refine_method : forall state name (oldbody newbody : state -> nat -> comp (state * nat)) @@ -553,7 +553,7 @@ Proof. eauto. Qed. -Hint Resolve RepChangeMethods_ok : core. +Local Hint Resolve RepChangeMethods_ok : core. Theorem refine_rep : forall state1 state2 (absfunc : state2 -> state1) names (ms1 : methods state1 names) (ms2 : methods state2 names) @@ -627,7 +627,7 @@ Definition derived_counter : sig (adt_refine counter). refine_finish. Defined. - + Eval simpl in proj1_sig derived_counter. @@ -688,7 +688,7 @@ Proof. eauto. Qed. -Hint Resolve CachingMethods_ok : core. +Local Hint Resolve CachingMethods_ok : core. Theorem refine_cache : forall state name (func : state -> nat) names (ms1 : methods state names) (ms2 : methods (state * nat) names) diff --git a/ProgramDerivation_template.v b/ProgramDerivation_template.v index f7e368f..3d92482 100644 --- a/ProgramDerivation_template.v +++ b/ProgramDerivation_template.v @@ -187,7 +187,7 @@ Inductive RefineMethods {state1 state2} (R : state1 -> state2 -> Prop) -> RefineMethods R (MethodsCons {| MethodName := name; MethodBody := f1 |} ms1) (MethodsCons {| MethodName := name; MethodBody := f2 |} ms2). -Hint Constructors RefineMethods : core. +Local Hint Constructors RefineMethods : core. Record adt_refine {names} (adt1 adt2 : adt names) : Prop := { ArRel : AdtState adt1 -> AdtState adt2 -> Prop; @@ -214,7 +214,7 @@ Definition split_counter := ADT { and method "value"[[self, _]] = ret (self, fst self + snd self) }. -Hint Extern 1 (@eq nat _ _) => simplify; linear_arithmetic : core. +Local Hint Extern 1 (@eq nat _ _) => simplify; linear_arithmetic : core. Theorem split_counter_ok : adt_refine counter split_counter. Proof. @@ -232,7 +232,7 @@ Proof. subst; eauto. Qed. -Hint Immediate RefineMethods_refl : core. +Local Hint Immediate RefineMethods_refl : core. Theorem refine_refl : forall names (adt1 : adt names), adt_refine adt1 adt1. @@ -261,7 +261,7 @@ Proof. first_order. Qed. -Hint Resolve RefineMethods_trans : core. +Local Hint Resolve RefineMethods_trans : core. Theorem refine_trans : forall names (adt1 adt2 adt3 : adt names), adt_refine adt1 adt2 @@ -324,7 +324,7 @@ Proof. simplify; subst; eauto. Qed. -Hint Resolve ReplaceMethod_ok : core. +Local Hint Resolve ReplaceMethod_ok : core. Theorem refine_method : forall state name (oldbody newbody : state -> nat -> comp (state * nat)) names (ms1 ms2 : methods state names) constr, @@ -369,7 +369,7 @@ Proof. eauto. Qed. -Hint Resolve RepChangeMethods_ok : core. +Local Hint Resolve RepChangeMethods_ok : core. Theorem refine_rep : forall state1 state2 (absfunc : state2 -> state1) names (ms1 : methods state1 names) (ms2 : methods state2 names) @@ -405,7 +405,7 @@ Ltac refine_finish := apply refine_refl. Definition derived_counter : sig (adt_refine counter). Admitted. - + Eval simpl in proj1_sig derived_counter. @@ -460,7 +460,7 @@ Proof. eauto. Qed. -Hint Resolve CachingMethods_ok : core. +Local Hint Resolve CachingMethods_ok : core. Theorem refine_cache : forall state name (func : state -> nat) names (ms1 : methods state names) (ms2 : methods (state * nat) names) diff --git a/frap_book.tex b/frap_book.tex index a36019b..0305d0f 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -5377,7 +5377,7 @@ $$\begin{array}{rrcl} $$\infer{\smallstep{(h, l, x \leftarrow c_1; c_2(x))}{(h', l', x \leftarrow c'_1; c_2(x))}}{ \smallstep{(h, l, c_1)}{(h', l', c'_1)} } -\quad \infer{\smallstep{(h, l, x \leftarrow \mt{Return} \; v; c_2(x))}{(h, k, c_2(v))}}{}$$ +\quad \infer{\smallstep{(h, l, x \leftarrow \mt{Return} \; v; c_2(x))}{(h, l, c_2(v))}}{}$$ $$\infer{\smallstep{(h, l, \mt{Loop} \; i \; f)}{(h, l, x \leftarrow f(i); \mt{match} \; x \; \mt{with} \; \mt{Done}(a) \Rightarrow \mt{Return} \; a \mid \mt{Again}(a) \Rightarrow \mt{Loop} \; a \; f)}}{}$$