From 89f21b85336474b4a173afc48df1526c1fb11edf Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 2 Feb 2020 17:16:19 -0500 Subject: [PATCH] First phase of update for Coq 8.10 --- .gitignore | 4 +++ CompilerCorrectness.v | 55 +++++++++++++++-------------- DeepAndShallowEmbeddings.v | 36 +++++++++---------- DeepAndShallowEmbeddings_template.v | 23 ++++++------ DependentInductiveTypes.v | 22 ++++++------ DependentInductiveTypes_template.v | 22 ++++++------ FrapWithoutSets.v | 2 +- ProofByReflection.v | 4 +-- ProofByReflection_template.v | 5 +-- Sets.v | 2 +- SharedMemory.v | 50 +++++++++++++------------- 11 files changed, 114 insertions(+), 111 deletions(-) diff --git a/.gitignore b/.gitignore index 3090ba6..7ff07ee 100644 --- a/.gitignore +++ b/.gitignore @@ -13,7 +13,11 @@ Makefile.coq Makefile.coq.conf *.glob *.v.d +*.coq.d +*.coqdeps.d *.vo +*.vok +*.vos frap.tgz .coq-native Deep.ml* diff --git a/CompilerCorrectness.v b/CompilerCorrectness.v index 862e13b..e9515b7 100644 --- a/CompilerCorrectness.v +++ b/CompilerCorrectness.v @@ -40,6 +40,7 @@ Inductive cmd := Coercion Const : nat >-> arith. Coercion Var : var >-> arith. +Declare Scope arith_scope. Infix "+" := Plus : arith_scope. Infix "-" := Minus : arith_scope. Infix "*" := Times : arith_scope. @@ -126,7 +127,7 @@ Inductive generate : valuation * cmd -> list (option nat) -> Prop := -> generate vc' ns -> generate vc (Some n :: ns). -Hint Constructors plug step0 cstep generate. +Hint Constructors plug step0 cstep generate : core. (* Notice that [generate] is defined so that, for any two of a starting state's * traces, one is a prefix of the other. The same wouldn't necessarily hold if @@ -178,8 +179,8 @@ Example month_boundaries_in_days := * because the program does not terminate, generating new output infinitely * often. *) -Hint Extern 1 (interp _ _ = _) => simplify; equality. -Hint Extern 1 (interp _ _ <> _) => simplify; equality. +Hint Extern 1 (interp _ _ = _) => simplify; equality : core. +Hint Extern 1 (interp _ _ <> _) => simplify; equality : core. Theorem first_few_values : generate ($0, month_boundaries_in_days) [Some 28; Some 56]. @@ -317,7 +318,7 @@ Proof. equality. Qed. -Hint Resolve peel_cseq. +Hint Resolve peel_cseq : core. Lemma plug_deterministic : forall v C c1 c2, plug C c1 c2 -> forall l vc1, step0 (v, c1) l vc1 @@ -499,7 +500,7 @@ Proof. induct 1; simplify; eauto. Qed. -Hint Resolve plug_cfoldExprs1. +Hint Resolve plug_cfoldExprs1 : core. (* The main correctness property! *) Theorem cfoldExprs_ok : forall v c, @@ -593,7 +594,7 @@ Proof. invert H4. Qed. -Hint Resolve silent_generate_fwd silent_generate_bwd generate_Skip. +Hint Resolve silent_generate_fwd silent_generate_bwd generate_Skip : core. (* You might have noticed that our old notion of simulation doesn't apply to the * new optimization. The reason is that, because the optimized program skips @@ -700,7 +701,7 @@ Section simulation_skipping. clear; induct 1; eauto. Qed. - Hint Resolve step_to_termination. + Hint Resolve step_to_termination : core. Lemma R_Skip : forall n vc1 v, R n vc1 (v, Skip) @@ -766,9 +767,9 @@ Section simulation_skipping. Qed. End simulation_skipping. -Hint Extern 1 (_ < _) => linear_arithmetic. -Hint Extern 1 (_ >= _) => linear_arithmetic. -Hint Extern 1 (_ <> _) => linear_arithmetic. +Hint Extern 1 (_ < _) => linear_arithmetic : core. +Hint Extern 1 (_ >= _) => linear_arithmetic : core. +Hint Extern 1 (_ <> _) => linear_arithmetic : core. (* We will need to do some bookkeeping of [n] values. This function is the * trick, as we only need to skip steps based on removing [If]s from the code. @@ -816,7 +817,7 @@ Proof. induct 1; simplify; eauto. Qed. -Hint Resolve plug_cfold1. +Hint Resolve plug_cfold1 : core. Lemma plug_samefold : forall C c1 c1', plug C c1 c1' @@ -828,7 +829,7 @@ Proof. f_equal; eauto. Qed. -Hint Resolve plug_samefold. +Hint Resolve plug_samefold : core. Lemma plug_countIfs : forall C c1 c1', plug C c1 c1' @@ -840,16 +841,16 @@ Proof. apply IHplug in H5; linear_arithmetic. Qed. -Hint Resolve plug_countIfs. +Hint Resolve plug_countIfs : core. Hint Extern 1 (interp ?e _ = _) => match goal with | [ H : cfoldArith e = _ |- _ ] => rewrite <- cfoldArith_ok; rewrite H - end. + end : core. Hint Extern 1 (interp ?e _ <> _) => match goal with | [ H : cfoldArith e = _ |- _ ] => rewrite <- cfoldArith_ok; rewrite H - end. + end : core. (* The final proof is fairly straightforward now. *) Lemma cfold_ok : forall v c, @@ -1118,7 +1119,7 @@ Section simulation_multiple. (* We won't comment on the other proof details, though they could be * interesting reading. *) - Hint Constructors generateN. + Hint Constructors generateN : core. Lemma generateN_fwd : forall sc vc ns, generateN sc vc ns @@ -1127,7 +1128,7 @@ Section simulation_multiple. induct 1; eauto. Qed. - Hint Resolve generateN_fwd. + Hint Resolve generateN_fwd : core. Lemma generateN_bwd : forall vc ns, generate vc ns @@ -1319,7 +1320,7 @@ Proof. first_order. Qed. -Hint Resolve agree_add agree_add_tempVar_fwd agree_add_tempVar_bwd agree_add_tempVar_bwd_prime agree_refl. +Hint Resolve agree_add agree_add_tempVar_fwd agree_add_tempVar_bwd agree_add_tempVar_bwd_prime agree_refl : core. (* And here are two more unremarkable lemmas. *) @@ -1332,7 +1333,7 @@ Proof. eauto 6. Qed. -Hint Resolve silent_csteps_front. +Hint Resolve silent_csteps_front : core. Lemma tempVar_contra : forall n1 n2, tempVar n1 = tempVar n2 @@ -1343,7 +1344,7 @@ Proof. first_order. Qed. -Hint Resolve tempVar_contra. +Hint Resolve tempVar_contra : core. Lemma self_prime_contra : forall s, (s ++ "'")%string = s -> False. @@ -1351,7 +1352,7 @@ Proof. induct s; simplify; equality. Qed. -Hint Resolve self_prime_contra. +Hint Resolve self_prime_contra : core. (* We've now proved all properties of [tempVar] that we need, so let's ask Coq * not to reduce applications of it anymore, to keep goals simpler. *) @@ -1559,7 +1560,7 @@ Proof. induct 1; bool; auto. Qed. -Hint Immediate noUnderscore_plug. +Hint Immediate noUnderscore_plug : core. Lemma silent_csteps_plug : forall C c1 c1', plug C c1 c1' @@ -1570,7 +1571,7 @@ Proof. induct 1; invert 1; eauto. Qed. -Hint Resolve silent_csteps_plug. +Hint Resolve silent_csteps_plug : core. Fixpoint flattenContext (C : context) : context := match C with @@ -1584,7 +1585,7 @@ Proof. induct 1; simplify; eauto. Qed. -Hint Resolve plug_flatten. +Hint Resolve plug_flatten : core. Lemma plug_total : forall c C, exists c', plug C c c'. Proof. @@ -1603,7 +1604,7 @@ Proof. eauto. Qed. -Hint Resolve plug_cstep. +Hint Resolve plug_cstep : core. Lemma step0_noUnderscore : forall v c l v' c', step0 (v, c) l (v', c') @@ -1615,7 +1616,7 @@ Proof. reflexivity. Qed. -Hint Resolve step0_noUnderscore. +Hint Resolve step0_noUnderscore : core. Fixpoint noUnderscoreContext (C : context) : bool := match C with @@ -1642,7 +1643,7 @@ Proof. rewrite H4, H3; reflexivity. Qed. -Hint Resolve noUnderscore_plug_context noUnderscore_plug_fwd. +Hint Resolve noUnderscore_plug_context noUnderscore_plug_fwd : core. (* Finally, the main correctness theorem. *) Lemma flatten_ok : forall v c, diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v index 71ae07f..29e89ea 100644 --- a/DeepAndShallowEmbeddings.v +++ b/DeepAndShallowEmbeddings.v @@ -14,12 +14,12 @@ Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 3 Definition heap := fmap nat nat. Definition assertion := heap -> Prop. -Hint Extern 1 (_ <= _) => linear_arithmetic. -Hint Extern 1 (@eq nat _ _) => linear_arithmetic. +Hint Extern 1 (_ <= _) => linear_arithmetic : core. +Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6). -Hint Rewrite max_l max_r using linear_arithmetic. +Hint Rewrite max_l max_r using linear_arithmetic : core. Ltac simp := repeat (simplify; subst; propositional; try match goal with @@ -493,16 +493,15 @@ Module Deep. cases (interp c h). eauto. Qed. - - (* We use Coq's *extraction* feature to produce OCaml versions of our deeply - * embedded programs. Then we can run them using OCaml intepreters, which are - * able to take advantage of the side effects built into OCaml, as a - * performance optimization. This command generates file "Deep.ml", which can - * be loaded along with "DeepInterp.ml" to run the generated code. Note how - * the latter file uses OCaml's built-in mutable hash-table type for efficient - * representation of program memories. *) - Extraction "Deep.ml" array_max increment_all. End Deep. +(* We use Coq's *extraction* feature to produce OCaml versions of our deeply + * embedded programs. Then we can run them using OCaml intepreters, which are + * able to take advantage of the side effects built into OCaml, as a + * performance optimization. This command generates file "Deep.ml", which can + * be loaded along with "DeepInterp.ml" to run the generated code. Note how + * the latter file uses OCaml's built-in mutable hash-table type for efficient + * representation of program memories. *) +Extraction "Deep.ml" Deep.array_max Deep.increment_all. (** * A slightly fancier deep embedding, adding unbounded loops *) @@ -836,10 +835,9 @@ Module Deeper. eapply invert_Return; eauto. simplify; auto. Qed. - - Extraction "Deeper.ml" index_of. End Deeper. +Extraction "Deeper.ml" Deeper.index_of. (** * Adding the possibility of program failure *) @@ -886,7 +884,7 @@ Module DeeperWithFail. | Stepped (h : heap) (c : cmd result) | Failed. - Implicit Arguments Failed [result]. + Arguments Failed {result}. Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result := match c with @@ -918,8 +916,6 @@ Module DeeperWithFail. end end. - Extraction "DeeperWithFail.ml" forever. - Inductive hoare_triple : assertion -> forall {result}, cmd result -> (result -> assertion) -> Prop := | HtReturn : forall P {result : Set} (v : result), hoare_triple P (Return v) (fun r h => P h /\ r = v) @@ -1216,7 +1212,7 @@ Module DeeperWithFail. reflexivity. Qed. - Hint Rewrite firstn_nochange fold_left_firstn using linear_arithmetic. + Hint Rewrite firstn_nochange fold_left_firstn using linear_arithmetic : core. (* Here's the soundness theorem for [heapfold], relying on a hypothesis of * soundness for [combine]. *) @@ -1274,7 +1270,7 @@ Module DeeperWithFail. apply IHls; linear_arithmetic. Qed. - Hint Resolve le_max. + Hint Resolve le_max : core. (* Finally, a short proof of [array_max], appealing mostly to the generic * proof of [heapfold] *) @@ -1291,3 +1287,5 @@ Module DeeperWithFail. auto. Qed. End DeeperWithFail. + +Extraction "DeeperWithFail.ml" DeeperWithFail.forever. diff --git a/DeepAndShallowEmbeddings_template.v b/DeepAndShallowEmbeddings_template.v index 5365fad..dec4c7b 100644 --- a/DeepAndShallowEmbeddings_template.v +++ b/DeepAndShallowEmbeddings_template.v @@ -9,12 +9,12 @@ Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 3 Definition heap := fmap nat nat. Definition assertion := heap -> Prop. -Hint Extern 1 (_ <= _) => linear_arithmetic. -Hint Extern 1 (@eq nat _ _) => linear_arithmetic. +Hint Extern 1 (_ <= _) => linear_arithmetic : core. +Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6). -Hint Rewrite max_l max_r using linear_arithmetic. +Hint Rewrite max_l max_r using linear_arithmetic : core. Ltac simp := repeat (simplify; subst; propositional; try match goal with @@ -396,10 +396,10 @@ Module Deep. cases (interp c h). eauto. Qed. - - Extraction "Deep.ml" array_max increment_all. End Deep. +Extraction "Deep.ml" Deep.array_max Deep.increment_all. + (** * A slightly fancier deep embedding, adding unbounded loops *) @@ -690,10 +690,9 @@ Module Deeper. eapply invert_Return; eauto. simplify; auto. Qed. - - Extraction "Deeper.ml" index_of. End Deeper. +Extraction "Deeper.ml" Deeper.index_of. (** * Adding the possibility of program failure *) @@ -731,7 +730,7 @@ Module DeeperWithFail. | Stepped (h : heap) (c : cmd result) | Failed. - Implicit Arguments Failed [result]. + Arguments Failed {result}. Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result := match c with @@ -763,8 +762,6 @@ Module DeeperWithFail. end end. - Extraction "DeeperWithFail.ml" forever. - Inductive hoare_triple : assertion -> forall {result}, cmd result -> (result -> assertion) -> Prop := | HtReturn : forall P {result : Set} (v : result), hoare_triple P (Return v) (fun r h => P h /\ r = v) @@ -1047,7 +1044,7 @@ Module DeeperWithFail. reflexivity. Qed. - Hint Rewrite firstn_nochange fold_left_firstn using linear_arithmetic. + Hint Rewrite firstn_nochange fold_left_firstn using linear_arithmetic : core. Theorem heapfold_ok : forall {A : Set} (init : A) combine (ls : list nat) (f : A -> nat -> A), @@ -1088,7 +1085,7 @@ Module DeeperWithFail. apply IHls; linear_arithmetic. Qed. - Hint Resolve le_max. + Hint Resolve le_max : core. Theorem array_max_ok : forall ls : list nat, {{ h ~> forall i, i < length ls -> h $! i = nth_default 0 ls i}} @@ -1097,3 +1094,5 @@ Module DeeperWithFail. Proof. Admitted. End DeeperWithFail. + +Extraction "DeeperWithFail.ml" DeeperWithFail.forever. diff --git a/DependentInductiveTypes.v b/DependentInductiveTypes.v index 9848008..28d7a69 100644 --- a/DependentInductiveTypes.v +++ b/DependentInductiveTypes.v @@ -1071,7 +1071,7 @@ Ltac substring := destruct N; simplify end; try linear_arithmetic; eauto; try equality. -Hint Resolve le_n_S. +Hint Resolve le_n_S : core. Lemma substring_le : forall s n m, length (substring n m s) <= m. @@ -1105,7 +1105,7 @@ Proof. induct s1; substring. Qed. -Hint Resolve length_emp append_emp substring_le substring_split length_app1. +Hint Resolve length_emp append_emp substring_le substring_split length_app1 : core. Lemma substring_app_fst : forall s2 s1 n, length s1 = n @@ -1151,7 +1151,7 @@ End sumbool_and. Infix "&&" := sumbool_and (at level 40, left associativity). -Hint Extern 1 (_ <= _) => linear_arithmetic. +Hint Extern 1 (_ <= _) => linear_arithmetic : core. Section split. Variables P1 P2 : string -> Prop. @@ -1217,7 +1217,7 @@ Section split. Defined. End split. -Implicit Arguments split [P1 P2]. +Arguments split [P1 P2]. (* And now, a few more boring lemmas. Rejoin at "BOREDOM VANQUISHED", if you * like. *) @@ -1253,7 +1253,7 @@ Proof. induct s; substring. Qed. -Hint Extern 1 (String _ _ = String _ _) => f_equal. +Hint Extern 1 (String _ _ = String _ _) => f_equal : core. Lemma substring_stack : forall s n2 m1 m2, m1 <= m2 @@ -1337,7 +1337,7 @@ Section dec_star. (* Some new lemmas and hints about the [star] type family are useful. Rejoin * at BOREDOM DEMOLISHED to skip the details. *) - Hint Constructors star. + Hint Constructors star : core. Lemma star_empty : forall s, length s = 0 @@ -1365,14 +1365,14 @@ Section dec_star. end. Qed. - Hint Resolve star_empty star_singleton star_app. + Hint Resolve star_empty star_singleton star_app : core. Variable s : string. Hint Extern 1 (exists i : nat, _) => match goal with | [ H : P (String _ ?S) |- _ ] => exists (length S); simplify - end. + end : core. Lemma star_inv : forall s, star P s @@ -1426,7 +1426,7 @@ Section dec_star. * an index into [s] that splits [s] into a nonempty prefix and a suffix, * such that the prefix satisfies [P] and the suffix satisfies [P']. *) - Hint Extern 1 (_ \/ _) => linear_arithmetic. + Hint Extern 1 (_ \/ _) => linear_arithmetic : core. Definition dec_star'' : forall l : nat, {exists l', S l' <= l @@ -1467,7 +1467,7 @@ Section dec_star. linear_arithmetic. Qed. - Hint Resolve star_length_contra star_length_flip substring_suffix_emp. + Hint Resolve star_length_contra star_length_flip substring_suffix_emp : core. (* The work of [dec_star''] is nested inside another linear search by * [dec_star'], which provides the final functionality we need, but for @@ -1507,7 +1507,7 @@ Proof. equality. Qed. -Hint Resolve app_cong. +Hint Resolve app_cong : core. (* With these helper functions completed, the implementation of our [matches] * function is refreshingly straightforward. *) diff --git a/DependentInductiveTypes_template.v b/DependentInductiveTypes_template.v index 715ecda..4ba65bb 100644 --- a/DependentInductiveTypes_template.v +++ b/DependentInductiveTypes_template.v @@ -487,7 +487,7 @@ Ltac substring := destruct N; simplify end; try linear_arithmetic; eauto; try equality. -Hint Resolve le_n_S. +Hint Resolve le_n_S : core. Lemma substring_le : forall s n m, length (substring n m s) <= m. @@ -521,7 +521,7 @@ Proof. induct s1; substring. Qed. -Hint Resolve length_emp append_emp substring_le substring_split length_app1. +Hint Resolve length_emp append_emp substring_le substring_split length_app1 : core. Lemma substring_app_fst : forall s2 s1 n, length s1 = n @@ -563,7 +563,7 @@ End sumbool_and. Infix "&&" := sumbool_and (at level 40, left associativity). -Hint Extern 1 (_ <= _) => linear_arithmetic. +Hint Extern 1 (_ <= _) => linear_arithmetic : core. Section split. Variables P1 P2 : string -> Prop. @@ -599,7 +599,7 @@ Section split. Defined. End split. -Implicit Arguments split [P1 P2]. +Arguments split [P1 P2]. (* And now, a few more boring lemmas. Rejoin at "BOREDOM VANQUISHED", if you * like. *) @@ -635,7 +635,7 @@ Proof. induct s; substring. Qed. -Hint Extern 1 (String _ _ = String _ _) => f_equal. +Hint Extern 1 (String _ _ = String _ _) => f_equal : core. Lemma substring_stack : forall s n2 m1 m2, m1 <= m2 @@ -715,7 +715,7 @@ Section dec_star. (* Some new lemmas and hints about the [star] type family are useful. Rejoin * at BOREDOM DEMOLISHED to skip the details. *) - Hint Constructors star. + Hint Constructors star : core. Lemma star_empty : forall s, length s = 0 @@ -743,14 +743,14 @@ Section dec_star. end. Qed. - Hint Resolve star_empty star_singleton star_app. + Hint Resolve star_empty star_singleton star_app : core. Variable s : string. Hint Extern 1 (exists i : nat, _) => match goal with | [ H : P (String _ ?S) |- _ ] => exists (length S); simplify - end. + end : core. Lemma star_inv : forall s, star P s @@ -789,7 +789,7 @@ Section dec_star. -> {P' (substring n' (length s - n') s)} + {~ P' (substring n' (length s - n') s)}. - Hint Extern 1 (_ \/ _) => linear_arithmetic. + Hint Extern 1 (_ \/ _) => linear_arithmetic : core. Definition dec_star'' : forall l : nat, {exists l', S l' <= l @@ -830,7 +830,7 @@ Section dec_star. linear_arithmetic. Qed. - Hint Resolve star_length_contra star_length_flip substring_suffix_emp. + Hint Resolve star_length_contra star_length_flip substring_suffix_emp : core. Definition dec_star' : forall n n' : nat, length s - n' <= n -> {star P (substring n' (length s - n') s)} @@ -863,7 +863,7 @@ Proof. equality. Qed. -Hint Resolve app_cong. +Hint Resolve app_cong : core. Definition matches : forall P (r : regexp P) s, {P s} + {~ P s}. refine (fix F P (r : regexp P) s : {P s} + {~ P s} := diff --git a/FrapWithoutSets.v b/FrapWithoutSets.v index fdad783..acbaa88 100644 --- a/FrapWithoutSets.v +++ b/FrapWithoutSets.v @@ -1,5 +1,5 @@ Require Import Eqdep String Arith Omega Program Sets Relations Map Var Invariant Bool ModelCheck. -Export String Arith Sets Relations Map Var Invariant Bool ModelCheck. +Export Ascii String Arith Sets Relations Map Var Invariant Bool ModelCheck. Require Import List. Export List ListNotations. Open Scope string_scope. diff --git a/ProofByReflection.v b/ProofByReflection.v index 7bee89c..9d2cf10 100644 --- a/ProofByReflection.v +++ b/ProofByReflection.v @@ -586,6 +586,8 @@ Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop := | Imp f1 f2 => formulaDenote atomics f1 -> formulaDenote atomics f2 end. +Require Import ListSet. + Section my_tauto. Variable atomics : asgn. @@ -593,8 +595,6 @@ Section my_tauto. * module of the standard library, which (unsurprisingly) presents a view of * lists as sets. *) - Require Import ListSet. - (* The [eq_nat_dec] below is a richly typed equality test on [nat]s. We'll * get to the ideas behind it in a later class. *) Definition add (s : set propvar) (v : propvar) := set_add eq_nat_dec v s. diff --git a/ProofByReflection_template.v b/ProofByReflection_template.v index 2075578..ac58e44 100644 --- a/ProofByReflection_template.v +++ b/ProofByReflection_template.v @@ -2,6 +2,7 @@ Require Import Frap. Set Implicit Arguments. Set Asymmetric Patterns. +Set Universe Polymorphism. (** * Proving Evenness *) @@ -272,11 +273,11 @@ Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop := | Imp f1 f2 => formulaDenote atomics f1 -> formulaDenote atomics f2 end. +Require Import ListSet. + Section my_tauto. Variable atomics : asgn. - Require Import ListSet. - Definition add (s : set propvar) (v : propvar) := set_add eq_nat_dec v s. Fixpoint allTrue (s : set propvar) : Prop := diff --git a/Sets.v b/Sets.v index 8a53bef..49bf1f6 100644 --- a/Sets.v +++ b/Sets.v @@ -35,7 +35,7 @@ Section set. End set. Infix "\in" := In (at level 70). -Notation "[ P ]" := (check P). +(*Notation "[ P ]" := (check P).*) Infix "\cup" := union (at level 40). Infix "\cap" := intersection (at level 40). Infix "\setminus" := minus (at level 40). diff --git a/SharedMemory.v b/SharedMemory.v index 2f77dbf..1b97263 100644 --- a/SharedMemory.v +++ b/SharedMemory.v @@ -13,8 +13,8 @@ Set Asymmetric Patterns. Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 30). Definition heap := fmap nat nat. -Hint Extern 1 (_ <= _) => linear_arithmetic. -Hint Extern 1 (@eq nat _ _) => linear_arithmetic. +Hint Extern 1 (_ <= _) => linear_arithmetic : core. +Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. (** * An object language with shared-memory concurrency *) @@ -203,7 +203,7 @@ Definition trsys_ofL (h : heap) (l : locks) (c : cmd) := {| (* Now we prove some basic facts; commentary resumes before [step_runLocal]. *) -Hint Constructors step stepL. +Hint Constructors step stepL : core. Lemma run_Return : forall h l r h' l' c, step^* (h, l, Return r) (h', l', c) @@ -265,7 +265,7 @@ Proof. eauto. Qed. -Hint Resolve StepBindRecur_star StepParRecur1_star StepParRecur2_star. +Hint Resolve StepBindRecur_star StepParRecur1_star StepParRecur2_star : core. Lemma runLocal_idem : forall c, runLocal (runLocal c) = runLocal c. Proof. @@ -722,7 +722,7 @@ Proof. first_order; eauto. Qed. -Hint Constructors summarize. +Hint Constructors summarize : core. (* The next two lemmas show that, once a summary is accurate for a command, it * remains accurate throughout the whole execution lifetime of the command. *) @@ -776,25 +776,25 @@ Inductive boundRunningTime : cmd -> nat -> Prop := (* Perhaps surprisingly, there exist commands that have no finite time bounds! * Mixed-embedding languages often have these counterintuitive properties. *) +Fixpoint scribbly (n : nat) : cmd := + match n with + | O => Return 0 + | S n' => _ <- Write n' 0; scribbly n' + end. + +Lemma scribbly_time : forall n m, + boundRunningTime (scribbly n) m + -> m >= n. +Proof. + induct n; invert 1; auto. + invert H2. + specialize (H4 n0). + apply IHn in H4. + linear_arithmetic. +Qed. + Theorem boundRunningTime_not_total : exists c, forall n, ~boundRunningTime c n. Proof. - Fixpoint scribbly (n : nat) : cmd := - match n with - | O => Return 0 - | S n' => _ <- Write n' 0; scribbly n' - end. - - Lemma scribbly_time : forall n m, - boundRunningTime (scribbly n) m - -> m >= n. - Proof. - induct n; invert 1; auto. - invert H2. - specialize (H4 n0). - apply IHn in H4. - linear_arithmetic. - Qed. - exists (n <- Read 0; scribbly n); propositional. invert H. specialize (H4 (S n2)). @@ -802,7 +802,7 @@ Proof. linear_arithmetic. Qed. -Hint Constructors boundRunningTime. +Hint Constructors boundRunningTime : core. (* Key property: taking a step of execution lowers the running-time bound. *) Lemma boundRunningTime_step : forall c n h l h' l', @@ -1029,7 +1029,7 @@ Inductive stepsi : nat -> heap * locks * cmd -> heap * locks * cmd -> Prop := -> stepsi i st2 st3 -> stepsi (S i) st1 st3. -Hint Constructors stepsi. +Hint Constructors stepsi : core. Theorem steps_stepsi : forall st1 st2, step^* st1 st2 @@ -1038,7 +1038,7 @@ Proof. induct 1; first_order; eauto. Qed. -Hint Constructors stepC. +Hint Constructors stepC : core. (* The next few lemmas are quite technical. Commentary resumes for * [translate_trace]. *)