mirror of
https://github.com/achlipala/frap.git
synced 2024-11-10 00:07:51 +00:00
Revising before this week's lectures
This commit is contained in:
parent
45fa64d69e
commit
8fdc4e2cfd
5 changed files with 29 additions and 29 deletions
|
@ -19,8 +19,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 : core.
|
Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
|
||||||
Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
|
Local 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
|
||||||
|
@ -206,7 +206,7 @@ Module Import S <: SEP.
|
||||||
t.
|
t.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Hint Resolve split_empty_bwd' : core.
|
Local Hint Resolve split_empty_bwd' : core.
|
||||||
|
|
||||||
Theorem extra_lift : forall (P : Prop) p,
|
Theorem extra_lift : forall (P : Prop) p,
|
||||||
P
|
P
|
||||||
|
@ -502,7 +502,7 @@ Proof.
|
||||||
apply try_me_first_easy.
|
apply try_me_first_easy.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Hint Resolve try_ptsto_first : core.
|
Local Hint Resolve try_ptsto_first : core.
|
||||||
|
|
||||||
|
|
||||||
(** ** The nonzero shared counter *)
|
(** ** The nonzero shared counter *)
|
||||||
|
@ -837,7 +837,7 @@ Qed.
|
||||||
* book PDF for a sketch of the important technical devices and lemmas in this
|
* book PDF for a sketch of the important technical devices and lemmas in this
|
||||||
* proof. *)
|
* proof. *)
|
||||||
|
|
||||||
Hint Resolve himp_refl : core.
|
Local 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
|
||||||
|
@ -852,7 +852,7 @@ Proof.
|
||||||
rewrite IHhoare_triple; eauto.
|
rewrite IHhoare_triple; eauto.
|
||||||
Qed.
|
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,
|
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
|
||||||
|
|
|
@ -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 : core.
|
Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
|
||||||
Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
|
Local 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' : core.
|
Local Hint Resolve split_empty_bwd' : core.
|
||||||
|
|
||||||
Theorem extra_lift : forall (P : Prop) p,
|
Theorem extra_lift : forall (P : Prop) p,
|
||||||
P
|
P
|
||||||
|
@ -483,7 +483,7 @@ Proof.
|
||||||
apply try_me_first_easy.
|
apply try_me_first_easy.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Hint Resolve try_ptsto_first : core.
|
Local Hint Resolve try_ptsto_first : core.
|
||||||
|
|
||||||
|
|
||||||
(** ** The nonzero shared counter *)
|
(** ** The nonzero shared counter *)
|
||||||
|
@ -752,7 +752,7 @@ Qed.
|
||||||
|
|
||||||
(** * Soundness proof *)
|
(** * Soundness proof *)
|
||||||
|
|
||||||
Hint Resolve himp_refl : core.
|
Local 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
|
||||||
|
@ -767,7 +767,7 @@ Proof.
|
||||||
rewrite IHhoare_triple; eauto.
|
rewrite IHhoare_triple; eauto.
|
||||||
Qed.
|
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,
|
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
|
||||||
|
|
|
@ -327,7 +327,7 @@ Inductive RefineMethods {state1 state2} (R : state1 -> state2 -> Prop)
|
||||||
-> RefineMethods R (MethodsCons {| MethodName := name; MethodBody := f1 |} ms1)
|
-> RefineMethods R (MethodsCons {| MethodName := name; MethodBody := f1 |} ms1)
|
||||||
(MethodsCons {| MethodName := name; MethodBody := f2 |} ms2).
|
(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,
|
(* When does [adt2] refine [adt1]? When there exists a simulation relation,
|
||||||
* with respect to which the constructors and methods all satisfy the usual
|
* 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)
|
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. *)
|
(* Here is why the new implementation is correct. *)
|
||||||
Theorem split_counter_ok : adt_refine counter split_counter.
|
Theorem split_counter_ok : adt_refine counter split_counter.
|
||||||
|
@ -393,7 +393,7 @@ Proof.
|
||||||
subst; eauto.
|
subst; eauto.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Hint Immediate RefineMethods_refl : core.
|
Local Hint Immediate RefineMethods_refl : core.
|
||||||
|
|
||||||
Theorem refine_refl : forall names (adt1 : adt names),
|
Theorem refine_refl : forall names (adt1 : adt names),
|
||||||
adt_refine adt1 adt1.
|
adt_refine adt1 adt1.
|
||||||
|
@ -422,7 +422,7 @@ Proof.
|
||||||
first_order.
|
first_order.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Hint Resolve RefineMethods_trans : core.
|
Local Hint Resolve RefineMethods_trans : core.
|
||||||
|
|
||||||
Theorem refine_trans : forall names (adt1 adt2 adt3 : adt names),
|
Theorem refine_trans : forall names (adt1 adt2 adt3 : adt names),
|
||||||
adt_refine adt1 adt2
|
adt_refine adt1 adt2
|
||||||
|
@ -497,7 +497,7 @@ Proof.
|
||||||
simplify; subst; eauto.
|
simplify; subst; eauto.
|
||||||
Qed.
|
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]. *)
|
(* 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))
|
Theorem refine_method : forall state name (oldbody newbody : state -> nat -> comp (state * nat))
|
||||||
|
@ -553,7 +553,7 @@ Proof.
|
||||||
eauto.
|
eauto.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Hint Resolve RepChangeMethods_ok : core.
|
Local Hint Resolve RepChangeMethods_ok : core.
|
||||||
|
|
||||||
Theorem refine_rep : forall state1 state2 (absfunc : state2 -> state1)
|
Theorem refine_rep : forall state1 state2 (absfunc : state2 -> state1)
|
||||||
names (ms1 : methods state1 names) (ms2 : methods state2 names)
|
names (ms1 : methods state1 names) (ms2 : methods state2 names)
|
||||||
|
@ -688,7 +688,7 @@ Proof.
|
||||||
eauto.
|
eauto.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Hint Resolve CachingMethods_ok : core.
|
Local Hint Resolve CachingMethods_ok : core.
|
||||||
|
|
||||||
Theorem refine_cache : forall state name (func : state -> nat)
|
Theorem refine_cache : forall state name (func : state -> nat)
|
||||||
names (ms1 : methods state names) (ms2 : methods (state * nat) names)
|
names (ms1 : methods state names) (ms2 : methods (state * nat) names)
|
||||||
|
|
|
@ -187,7 +187,7 @@ Inductive RefineMethods {state1 state2} (R : state1 -> state2 -> Prop)
|
||||||
-> RefineMethods R (MethodsCons {| MethodName := name; MethodBody := f1 |} ms1)
|
-> RefineMethods R (MethodsCons {| MethodName := name; MethodBody := f1 |} ms1)
|
||||||
(MethodsCons {| MethodName := name; MethodBody := f2 |} ms2).
|
(MethodsCons {| MethodName := name; MethodBody := f2 |} ms2).
|
||||||
|
|
||||||
Hint Constructors RefineMethods : core.
|
Local Hint Constructors RefineMethods : core.
|
||||||
|
|
||||||
Record adt_refine {names} (adt1 adt2 : adt names) : Prop := {
|
Record adt_refine {names} (adt1 adt2 : adt names) : Prop := {
|
||||||
ArRel : AdtState adt1 -> AdtState adt2 -> 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)
|
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.
|
Theorem split_counter_ok : adt_refine counter split_counter.
|
||||||
Proof.
|
Proof.
|
||||||
|
@ -232,7 +232,7 @@ Proof.
|
||||||
subst; eauto.
|
subst; eauto.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Hint Immediate RefineMethods_refl : core.
|
Local Hint Immediate RefineMethods_refl : core.
|
||||||
|
|
||||||
Theorem refine_refl : forall names (adt1 : adt names),
|
Theorem refine_refl : forall names (adt1 : adt names),
|
||||||
adt_refine adt1 adt1.
|
adt_refine adt1 adt1.
|
||||||
|
@ -261,7 +261,7 @@ Proof.
|
||||||
first_order.
|
first_order.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Hint Resolve RefineMethods_trans : core.
|
Local Hint Resolve RefineMethods_trans : core.
|
||||||
|
|
||||||
Theorem refine_trans : forall names (adt1 adt2 adt3 : adt names),
|
Theorem refine_trans : forall names (adt1 adt2 adt3 : adt names),
|
||||||
adt_refine adt1 adt2
|
adt_refine adt1 adt2
|
||||||
|
@ -324,7 +324,7 @@ Proof.
|
||||||
simplify; subst; eauto.
|
simplify; subst; eauto.
|
||||||
Qed.
|
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))
|
Theorem refine_method : forall state name (oldbody newbody : state -> nat -> comp (state * nat))
|
||||||
names (ms1 ms2 : methods state names) constr,
|
names (ms1 ms2 : methods state names) constr,
|
||||||
|
@ -369,7 +369,7 @@ Proof.
|
||||||
eauto.
|
eauto.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Hint Resolve RepChangeMethods_ok : core.
|
Local Hint Resolve RepChangeMethods_ok : core.
|
||||||
|
|
||||||
Theorem refine_rep : forall state1 state2 (absfunc : state2 -> state1)
|
Theorem refine_rep : forall state1 state2 (absfunc : state2 -> state1)
|
||||||
names (ms1 : methods state1 names) (ms2 : methods state2 names)
|
names (ms1 : methods state1 names) (ms2 : methods state2 names)
|
||||||
|
@ -460,7 +460,7 @@ Proof.
|
||||||
eauto.
|
eauto.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Hint Resolve CachingMethods_ok : core.
|
Local Hint Resolve CachingMethods_ok : core.
|
||||||
|
|
||||||
Theorem refine_cache : forall state name (func : state -> nat)
|
Theorem refine_cache : forall state name (func : state -> nat)
|
||||||
names (ms1 : methods state names) (ms2 : methods (state * nat) names)
|
names (ms1 : methods state names) (ms2 : methods (state * nat) names)
|
||||||
|
|
|
@ -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))}}{
|
$$\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)}
|
\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)}}{}$$
|
$$\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)}}{}$$
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue