First phase of update for Coq 8.10

This commit is contained in:
Adam Chlipala 2020-02-02 17:16:19 -05:00
parent e92a697e33
commit 89f21b8533
11 changed files with 114 additions and 111 deletions

4
.gitignore vendored
View file

@ -13,7 +13,11 @@ Makefile.coq
Makefile.coq.conf Makefile.coq.conf
*.glob *.glob
*.v.d *.v.d
*.coq.d
*.coqdeps.d
*.vo *.vo
*.vok
*.vos
frap.tgz frap.tgz
.coq-native .coq-native
Deep.ml* Deep.ml*

View file

@ -40,6 +40,7 @@ Inductive cmd :=
Coercion Const : nat >-> arith. Coercion Const : nat >-> arith.
Coercion Var : var >-> arith. Coercion Var : var >-> arith.
Declare Scope arith_scope.
Infix "+" := Plus : arith_scope. Infix "+" := Plus : arith_scope.
Infix "-" := Minus : arith_scope. Infix "-" := Minus : arith_scope.
Infix "*" := Times : arith_scope. Infix "*" := Times : arith_scope.
@ -126,7 +127,7 @@ Inductive generate : valuation * cmd -> list (option nat) -> Prop :=
-> generate vc' ns -> generate vc' ns
-> generate vc (Some n :: 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 (* 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 * 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 * because the program does not terminate, generating new output infinitely
* often. *) * often. *)
Hint Extern 1 (interp _ _ = _) => simplify; equality. Hint Extern 1 (interp _ _ = _) => simplify; equality : core.
Hint Extern 1 (interp _ _ <> _) => simplify; equality. Hint Extern 1 (interp _ _ <> _) => simplify; equality : core.
Theorem first_few_values : Theorem first_few_values :
generate ($0, month_boundaries_in_days) [Some 28; Some 56]. generate ($0, month_boundaries_in_days) [Some 28; Some 56].
@ -317,7 +318,7 @@ Proof.
equality. equality.
Qed. Qed.
Hint Resolve peel_cseq. Hint Resolve peel_cseq : core.
Lemma plug_deterministic : forall v C c1 c2, plug C c1 c2 Lemma plug_deterministic : forall v C c1 c2, plug C c1 c2
-> forall l vc1, step0 (v, c1) l vc1 -> forall l vc1, step0 (v, c1) l vc1
@ -499,7 +500,7 @@ Proof.
induct 1; simplify; eauto. induct 1; simplify; eauto.
Qed. Qed.
Hint Resolve plug_cfoldExprs1. Hint Resolve plug_cfoldExprs1 : core.
(* The main correctness property! *) (* The main correctness property! *)
Theorem cfoldExprs_ok : forall v c, Theorem cfoldExprs_ok : forall v c,
@ -593,7 +594,7 @@ Proof.
invert H4. invert H4.
Qed. 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 (* 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 * new optimization. The reason is that, because the optimized program skips
@ -700,7 +701,7 @@ Section simulation_skipping.
clear; induct 1; eauto. clear; induct 1; eauto.
Qed. Qed.
Hint Resolve step_to_termination. Hint Resolve step_to_termination : core.
Lemma R_Skip : forall n vc1 v, Lemma R_Skip : forall n vc1 v,
R n vc1 (v, Skip) R n vc1 (v, Skip)
@ -766,9 +767,9 @@ Section simulation_skipping.
Qed. Qed.
End simulation_skipping. End simulation_skipping.
Hint Extern 1 (_ < _) => linear_arithmetic. Hint Extern 1 (_ < _) => linear_arithmetic : core.
Hint Extern 1 (_ >= _) => linear_arithmetic. Hint Extern 1 (_ >= _) => linear_arithmetic : core.
Hint Extern 1 (_ <> _) => linear_arithmetic. Hint Extern 1 (_ <> _) => linear_arithmetic : core.
(* We will need to do some bookkeeping of [n] values. This function is the (* 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. * 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. induct 1; simplify; eauto.
Qed. Qed.
Hint Resolve plug_cfold1. Hint Resolve plug_cfold1 : core.
Lemma plug_samefold : forall C c1 c1', Lemma plug_samefold : forall C c1 c1',
plug C c1 c1' plug C c1 c1'
@ -828,7 +829,7 @@ Proof.
f_equal; eauto. f_equal; eauto.
Qed. Qed.
Hint Resolve plug_samefold. Hint Resolve plug_samefold : core.
Lemma plug_countIfs : forall C c1 c1', Lemma plug_countIfs : forall C c1 c1',
plug C c1 c1' plug C c1 c1'
@ -840,16 +841,16 @@ Proof.
apply IHplug in H5; linear_arithmetic. apply IHplug in H5; linear_arithmetic.
Qed. Qed.
Hint Resolve plug_countIfs. Hint Resolve plug_countIfs : core.
Hint Extern 1 (interp ?e _ = _) => Hint Extern 1 (interp ?e _ = _) =>
match goal with match goal with
| [ H : cfoldArith e = _ |- _ ] => rewrite <- cfoldArith_ok; rewrite H | [ H : cfoldArith e = _ |- _ ] => rewrite <- cfoldArith_ok; rewrite H
end. end : core.
Hint Extern 1 (interp ?e _ <> _) => Hint Extern 1 (interp ?e _ <> _) =>
match goal with match goal with
| [ H : cfoldArith e = _ |- _ ] => rewrite <- cfoldArith_ok; rewrite H | [ H : cfoldArith e = _ |- _ ] => rewrite <- cfoldArith_ok; rewrite H
end. end : core.
(* The final proof is fairly straightforward now. *) (* The final proof is fairly straightforward now. *)
Lemma cfold_ok : forall v c, 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 (* We won't comment on the other proof details, though they could be
* interesting reading. *) * interesting reading. *)
Hint Constructors generateN. Hint Constructors generateN : core.
Lemma generateN_fwd : forall sc vc ns, Lemma generateN_fwd : forall sc vc ns,
generateN sc vc ns generateN sc vc ns
@ -1127,7 +1128,7 @@ Section simulation_multiple.
induct 1; eauto. induct 1; eauto.
Qed. Qed.
Hint Resolve generateN_fwd. Hint Resolve generateN_fwd : core.
Lemma generateN_bwd : forall vc ns, Lemma generateN_bwd : forall vc ns,
generate vc ns generate vc ns
@ -1319,7 +1320,7 @@ Proof.
first_order. first_order.
Qed. 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. *) (* And here are two more unremarkable lemmas. *)
@ -1332,7 +1333,7 @@ Proof.
eauto 6. eauto 6.
Qed. Qed.
Hint Resolve silent_csteps_front. Hint Resolve silent_csteps_front : core.
Lemma tempVar_contra : forall n1 n2, Lemma tempVar_contra : forall n1 n2,
tempVar n1 = tempVar n2 tempVar n1 = tempVar n2
@ -1343,7 +1344,7 @@ Proof.
first_order. first_order.
Qed. Qed.
Hint Resolve tempVar_contra. Hint Resolve tempVar_contra : core.
Lemma self_prime_contra : forall s, Lemma self_prime_contra : forall s,
(s ++ "'")%string = s -> False. (s ++ "'")%string = s -> False.
@ -1351,7 +1352,7 @@ Proof.
induct s; simplify; equality. induct s; simplify; equality.
Qed. 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 (* 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. *) * not to reduce applications of it anymore, to keep goals simpler. *)
@ -1559,7 +1560,7 @@ Proof.
induct 1; bool; auto. induct 1; bool; auto.
Qed. Qed.
Hint Immediate noUnderscore_plug. Hint Immediate noUnderscore_plug : core.
Lemma silent_csteps_plug : forall C c1 c1', Lemma silent_csteps_plug : forall C c1 c1',
plug C c1 c1' plug C c1 c1'
@ -1570,7 +1571,7 @@ Proof.
induct 1; invert 1; eauto. induct 1; invert 1; eauto.
Qed. Qed.
Hint Resolve silent_csteps_plug. Hint Resolve silent_csteps_plug : core.
Fixpoint flattenContext (C : context) : context := Fixpoint flattenContext (C : context) : context :=
match C with match C with
@ -1584,7 +1585,7 @@ Proof.
induct 1; simplify; eauto. induct 1; simplify; eauto.
Qed. Qed.
Hint Resolve plug_flatten. Hint Resolve plug_flatten : core.
Lemma plug_total : forall c C, exists c', plug C c c'. Lemma plug_total : forall c C, exists c', plug C c c'.
Proof. Proof.
@ -1603,7 +1604,7 @@ Proof.
eauto. eauto.
Qed. Qed.
Hint Resolve plug_cstep. Hint Resolve plug_cstep : core.
Lemma step0_noUnderscore : forall v c l v' c', Lemma step0_noUnderscore : forall v c l v' c',
step0 (v, c) l (v', c') step0 (v, c) l (v', c')
@ -1615,7 +1616,7 @@ Proof.
reflexivity. reflexivity.
Qed. Qed.
Hint Resolve step0_noUnderscore. Hint Resolve step0_noUnderscore : core.
Fixpoint noUnderscoreContext (C : context) : bool := Fixpoint noUnderscoreContext (C : context) : bool :=
match C with match C with
@ -1642,7 +1643,7 @@ Proof.
rewrite H4, H3; reflexivity. rewrite H4, H3; reflexivity.
Qed. Qed.
Hint Resolve noUnderscore_plug_context noUnderscore_plug_fwd. Hint Resolve noUnderscore_plug_context noUnderscore_plug_fwd : core.
(* Finally, the main correctness theorem. *) (* Finally, the main correctness theorem. *)
Lemma flatten_ok : forall v c, Lemma flatten_ok : forall v c,

View file

@ -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 heap := fmap nat nat.
Definition assertion := heap -> Prop. Definition assertion := heap -> Prop.
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.
Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6). 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; Ltac simp := repeat (simplify; subst; propositional;
try match goal with try match goal with
@ -493,16 +493,15 @@ Module Deep.
cases (interp c h). cases (interp c h).
eauto. eauto.
Qed. 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. 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 *) (** * A slightly fancier deep embedding, adding unbounded loops *)
@ -836,10 +835,9 @@ Module Deeper.
eapply invert_Return; eauto. eapply invert_Return; eauto.
simplify; auto. simplify; auto.
Qed. Qed.
Extraction "Deeper.ml" index_of.
End Deeper. End Deeper.
Extraction "Deeper.ml" Deeper.index_of.
(** * Adding the possibility of program failure *) (** * Adding the possibility of program failure *)
@ -886,7 +884,7 @@ Module DeeperWithFail.
| Stepped (h : heap) (c : cmd result) | Stepped (h : heap) (c : cmd result)
| Failed. | Failed.
Implicit Arguments Failed [result]. Arguments Failed {result}.
Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result := Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result :=
match c with match c with
@ -918,8 +916,6 @@ Module DeeperWithFail.
end end
end. end.
Extraction "DeeperWithFail.ml" forever.
Inductive hoare_triple : assertion -> forall {result}, cmd result -> (result -> assertion) -> Prop := Inductive hoare_triple : assertion -> forall {result}, cmd result -> (result -> assertion) -> Prop :=
| HtReturn : forall P {result : Set} (v : result), | HtReturn : forall P {result : Set} (v : result),
hoare_triple P (Return v) (fun r h => P h /\ r = v) hoare_triple P (Return v) (fun r h => P h /\ r = v)
@ -1216,7 +1212,7 @@ Module DeeperWithFail.
reflexivity. reflexivity.
Qed. 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 (* Here's the soundness theorem for [heapfold], relying on a hypothesis of
* soundness for [combine]. *) * soundness for [combine]. *)
@ -1274,7 +1270,7 @@ Module DeeperWithFail.
apply IHls; linear_arithmetic. apply IHls; linear_arithmetic.
Qed. Qed.
Hint Resolve le_max. Hint Resolve le_max : core.
(* Finally, a short proof of [array_max], appealing mostly to the generic (* Finally, a short proof of [array_max], appealing mostly to the generic
* proof of [heapfold] *) * proof of [heapfold] *)
@ -1291,3 +1287,5 @@ Module DeeperWithFail.
auto. auto.
Qed. Qed.
End DeeperWithFail. End DeeperWithFail.
Extraction "DeeperWithFail.ml" DeeperWithFail.forever.

View file

@ -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 heap := fmap nat nat.
Definition assertion := heap -> Prop. Definition assertion := heap -> Prop.
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.
Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6). 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; Ltac simp := repeat (simplify; subst; propositional;
try match goal with try match goal with
@ -396,10 +396,10 @@ Module Deep.
cases (interp c h). cases (interp c h).
eauto. eauto.
Qed. Qed.
Extraction "Deep.ml" array_max increment_all.
End Deep. End Deep.
Extraction "Deep.ml" Deep.array_max Deep.increment_all.
(** * A slightly fancier deep embedding, adding unbounded loops *) (** * A slightly fancier deep embedding, adding unbounded loops *)
@ -690,10 +690,9 @@ Module Deeper.
eapply invert_Return; eauto. eapply invert_Return; eauto.
simplify; auto. simplify; auto.
Qed. Qed.
Extraction "Deeper.ml" index_of.
End Deeper. End Deeper.
Extraction "Deeper.ml" Deeper.index_of.
(** * Adding the possibility of program failure *) (** * Adding the possibility of program failure *)
@ -731,7 +730,7 @@ Module DeeperWithFail.
| Stepped (h : heap) (c : cmd result) | Stepped (h : heap) (c : cmd result)
| Failed. | Failed.
Implicit Arguments Failed [result]. Arguments Failed {result}.
Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result := Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result :=
match c with match c with
@ -763,8 +762,6 @@ Module DeeperWithFail.
end end
end. end.
Extraction "DeeperWithFail.ml" forever.
Inductive hoare_triple : assertion -> forall {result}, cmd result -> (result -> assertion) -> Prop := Inductive hoare_triple : assertion -> forall {result}, cmd result -> (result -> assertion) -> Prop :=
| HtReturn : forall P {result : Set} (v : result), | HtReturn : forall P {result : Set} (v : result),
hoare_triple P (Return v) (fun r h => P h /\ r = v) hoare_triple P (Return v) (fun r h => P h /\ r = v)
@ -1047,7 +1044,7 @@ Module DeeperWithFail.
reflexivity. reflexivity.
Qed. 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 Theorem heapfold_ok : forall {A : Set} (init : A) combine
(ls : list nat) (f : A -> nat -> A), (ls : list nat) (f : A -> nat -> A),
@ -1088,7 +1085,7 @@ Module DeeperWithFail.
apply IHls; linear_arithmetic. apply IHls; linear_arithmetic.
Qed. Qed.
Hint Resolve le_max. Hint Resolve le_max : core.
Theorem array_max_ok : forall ls : list nat, Theorem array_max_ok : forall ls : list nat,
{{ h ~> forall i, i < length ls -> h $! i = nth_default 0 ls i}} {{ h ~> forall i, i < length ls -> h $! i = nth_default 0 ls i}}
@ -1097,3 +1094,5 @@ Module DeeperWithFail.
Proof. Proof.
Admitted. Admitted.
End DeeperWithFail. End DeeperWithFail.
Extraction "DeeperWithFail.ml" DeeperWithFail.forever.

View file

@ -1071,7 +1071,7 @@ Ltac substring :=
destruct N; simplify destruct N; simplify
end; try linear_arithmetic; eauto; try equality. 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, Lemma substring_le : forall s n m,
length (substring n m s) <= m. length (substring n m s) <= m.
@ -1105,7 +1105,7 @@ Proof.
induct s1; substring. induct s1; substring.
Qed. 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, Lemma substring_app_fst : forall s2 s1 n,
length s1 = n length s1 = n
@ -1151,7 +1151,7 @@ End sumbool_and.
Infix "&&" := sumbool_and (at level 40, left associativity). Infix "&&" := sumbool_and (at level 40, left associativity).
Hint Extern 1 (_ <= _) => linear_arithmetic. Hint Extern 1 (_ <= _) => linear_arithmetic : core.
Section split. Section split.
Variables P1 P2 : string -> Prop. Variables P1 P2 : string -> Prop.
@ -1217,7 +1217,7 @@ Section split.
Defined. Defined.
End split. End split.
Implicit Arguments split [P1 P2]. Arguments split [P1 P2].
(* And now, a few more boring lemmas. Rejoin at "BOREDOM VANQUISHED", if you (* And now, a few more boring lemmas. Rejoin at "BOREDOM VANQUISHED", if you
* like. *) * like. *)
@ -1253,7 +1253,7 @@ Proof.
induct s; substring. induct s; substring.
Qed. Qed.
Hint Extern 1 (String _ _ = String _ _) => f_equal. Hint Extern 1 (String _ _ = String _ _) => f_equal : core.
Lemma substring_stack : forall s n2 m1 m2, Lemma substring_stack : forall s n2 m1 m2,
m1 <= m2 m1 <= m2
@ -1337,7 +1337,7 @@ Section dec_star.
(* Some new lemmas and hints about the [star] type family are useful. Rejoin (* Some new lemmas and hints about the [star] type family are useful. Rejoin
* at BOREDOM DEMOLISHED to skip the details. *) * at BOREDOM DEMOLISHED to skip the details. *)
Hint Constructors star. Hint Constructors star : core.
Lemma star_empty : forall s, Lemma star_empty : forall s,
length s = 0 length s = 0
@ -1365,14 +1365,14 @@ Section dec_star.
end. end.
Qed. Qed.
Hint Resolve star_empty star_singleton star_app. Hint Resolve star_empty star_singleton star_app : core.
Variable s : string. Variable s : string.
Hint Extern 1 (exists i : nat, _) => Hint Extern 1 (exists i : nat, _) =>
match goal with match goal with
| [ H : P (String _ ?S) |- _ ] => exists (length S); simplify | [ H : P (String _ ?S) |- _ ] => exists (length S); simplify
end. end : core.
Lemma star_inv : forall s, Lemma star_inv : forall s,
star P 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, * 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']. *) * 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, Definition dec_star'' : forall l : nat,
{exists l', S l' <= l {exists l', S l' <= l
@ -1467,7 +1467,7 @@ Section dec_star.
linear_arithmetic. linear_arithmetic.
Qed. 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 (* The work of [dec_star''] is nested inside another linear search by
* [dec_star'], which provides the final functionality we need, but for * [dec_star'], which provides the final functionality we need, but for
@ -1507,7 +1507,7 @@ Proof.
equality. equality.
Qed. Qed.
Hint Resolve app_cong. Hint Resolve app_cong : core.
(* With these helper functions completed, the implementation of our [matches] (* With these helper functions completed, the implementation of our [matches]
* function is refreshingly straightforward. *) * function is refreshingly straightforward. *)

View file

@ -487,7 +487,7 @@ Ltac substring :=
destruct N; simplify destruct N; simplify
end; try linear_arithmetic; eauto; try equality. 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, Lemma substring_le : forall s n m,
length (substring n m s) <= m. length (substring n m s) <= m.
@ -521,7 +521,7 @@ Proof.
induct s1; substring. induct s1; substring.
Qed. 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, Lemma substring_app_fst : forall s2 s1 n,
length s1 = n length s1 = n
@ -563,7 +563,7 @@ End sumbool_and.
Infix "&&" := sumbool_and (at level 40, left associativity). Infix "&&" := sumbool_and (at level 40, left associativity).
Hint Extern 1 (_ <= _) => linear_arithmetic. Hint Extern 1 (_ <= _) => linear_arithmetic : core.
Section split. Section split.
Variables P1 P2 : string -> Prop. Variables P1 P2 : string -> Prop.
@ -599,7 +599,7 @@ Section split.
Defined. Defined.
End split. End split.
Implicit Arguments split [P1 P2]. Arguments split [P1 P2].
(* And now, a few more boring lemmas. Rejoin at "BOREDOM VANQUISHED", if you (* And now, a few more boring lemmas. Rejoin at "BOREDOM VANQUISHED", if you
* like. *) * like. *)
@ -635,7 +635,7 @@ Proof.
induct s; substring. induct s; substring.
Qed. Qed.
Hint Extern 1 (String _ _ = String _ _) => f_equal. Hint Extern 1 (String _ _ = String _ _) => f_equal : core.
Lemma substring_stack : forall s n2 m1 m2, Lemma substring_stack : forall s n2 m1 m2,
m1 <= m2 m1 <= m2
@ -715,7 +715,7 @@ Section dec_star.
(* Some new lemmas and hints about the [star] type family are useful. Rejoin (* Some new lemmas and hints about the [star] type family are useful. Rejoin
* at BOREDOM DEMOLISHED to skip the details. *) * at BOREDOM DEMOLISHED to skip the details. *)
Hint Constructors star. Hint Constructors star : core.
Lemma star_empty : forall s, Lemma star_empty : forall s,
length s = 0 length s = 0
@ -743,14 +743,14 @@ Section dec_star.
end. end.
Qed. Qed.
Hint Resolve star_empty star_singleton star_app. Hint Resolve star_empty star_singleton star_app : core.
Variable s : string. Variable s : string.
Hint Extern 1 (exists i : nat, _) => Hint Extern 1 (exists i : nat, _) =>
match goal with match goal with
| [ H : P (String _ ?S) |- _ ] => exists (length S); simplify | [ H : P (String _ ?S) |- _ ] => exists (length S); simplify
end. end : core.
Lemma star_inv : forall s, Lemma star_inv : forall s,
star P 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)}
+ {~ 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, Definition dec_star'' : forall l : nat,
{exists l', S l' <= l {exists l', S l' <= l
@ -830,7 +830,7 @@ Section dec_star.
linear_arithmetic. linear_arithmetic.
Qed. 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 Definition dec_star' : forall n n' : nat, length s - n' <= n
-> {star P (substring n' (length s - n') s)} -> {star P (substring n' (length s - n') s)}
@ -863,7 +863,7 @@ Proof.
equality. equality.
Qed. Qed.
Hint Resolve app_cong. Hint Resolve app_cong : core.
Definition matches : forall P (r : regexp P) s, {P s} + {~ P s}. Definition matches : forall P (r : regexp P) s, {P s} + {~ P s}.
refine (fix F P (r : regexp P) s : {P s} + {~ P s} := refine (fix F P (r : regexp P) s : {P s} + {~ P s} :=

View file

@ -1,5 +1,5 @@
Require Import Eqdep String Arith Omega Program Sets Relations Map Var Invariant Bool ModelCheck. 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. Require Import List.
Export List ListNotations. Export List ListNotations.
Open Scope string_scope. Open Scope string_scope.

View file

@ -586,6 +586,8 @@ Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop :=
| Imp f1 f2 => formulaDenote atomics f1 -> formulaDenote atomics f2 | Imp f1 f2 => formulaDenote atomics f1 -> formulaDenote atomics f2
end. end.
Require Import ListSet.
Section my_tauto. Section my_tauto.
Variable atomics : asgn. Variable atomics : asgn.
@ -593,8 +595,6 @@ Section my_tauto.
* module of the standard library, which (unsurprisingly) presents a view of * module of the standard library, which (unsurprisingly) presents a view of
* lists as sets. *) * lists as sets. *)
Require Import ListSet.
(* The [eq_nat_dec] below is a richly typed equality test on [nat]s. We'll (* 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. *) * get to the ideas behind it in a later class. *)
Definition add (s : set propvar) (v : propvar) := set_add eq_nat_dec v s. Definition add (s : set propvar) (v : propvar) := set_add eq_nat_dec v s.

View file

@ -2,6 +2,7 @@ Require Import Frap.
Set Implicit Arguments. Set Implicit Arguments.
Set Asymmetric Patterns. Set Asymmetric Patterns.
Set Universe Polymorphism.
(** * Proving Evenness *) (** * Proving Evenness *)
@ -272,11 +273,11 @@ Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop :=
| Imp f1 f2 => formulaDenote atomics f1 -> formulaDenote atomics f2 | Imp f1 f2 => formulaDenote atomics f1 -> formulaDenote atomics f2
end. end.
Require Import ListSet.
Section my_tauto. Section my_tauto.
Variable atomics : asgn. Variable atomics : asgn.
Require Import ListSet.
Definition add (s : set propvar) (v : propvar) := set_add eq_nat_dec v s. Definition add (s : set propvar) (v : propvar) := set_add eq_nat_dec v s.
Fixpoint allTrue (s : set propvar) : Prop := Fixpoint allTrue (s : set propvar) : Prop :=

2
Sets.v
View file

@ -35,7 +35,7 @@ Section set.
End set. End set.
Infix "\in" := In (at level 70). Infix "\in" := In (at level 70).
Notation "[ P ]" := (check P). (*Notation "[ P ]" := (check P).*)
Infix "\cup" := union (at level 40). Infix "\cup" := union (at level 40).
Infix "\cap" := intersection (at level 40). Infix "\cap" := intersection (at level 40).
Infix "\setminus" := minus (at level 40). Infix "\setminus" := minus (at level 40).

View file

@ -13,8 +13,8 @@ Set Asymmetric Patterns.
Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 30). Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 30).
Definition heap := fmap nat nat. Definition heap := fmap nat 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.
(** * An object language with shared-memory concurrency *) (** * 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]. *) (* 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, Lemma run_Return : forall h l r h' l' c,
step^* (h, l, Return r) (h', l', c) step^* (h, l, Return r) (h', l', c)
@ -265,7 +265,7 @@ Proof.
eauto. eauto.
Qed. 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. Lemma runLocal_idem : forall c, runLocal (runLocal c) = runLocal c.
Proof. Proof.
@ -722,7 +722,7 @@ Proof.
first_order; eauto. first_order; eauto.
Qed. Qed.
Hint Constructors summarize. Hint Constructors summarize : core.
(* The next two lemmas show that, once a summary is accurate for a command, it (* 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. *) * 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! (* Perhaps surprisingly, there exist commands that have no finite time bounds!
* Mixed-embedding languages often have these counterintuitive properties. *) * 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. Theorem boundRunningTime_not_total : exists c, forall n, ~boundRunningTime c n.
Proof. 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. exists (n <- Read 0; scribbly n); propositional.
invert H. invert H.
specialize (H4 (S n2)). specialize (H4 (S n2)).
@ -802,7 +802,7 @@ Proof.
linear_arithmetic. linear_arithmetic.
Qed. Qed.
Hint Constructors boundRunningTime. Hint Constructors boundRunningTime : core.
(* Key property: taking a step of execution lowers the running-time bound. *) (* Key property: taking a step of execution lowers the running-time bound. *)
Lemma boundRunningTime_step : forall c n h l h' l', 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 i st2 st3
-> stepsi (S i) st1 st3. -> stepsi (S i) st1 st3.
Hint Constructors stepsi. Hint Constructors stepsi : core.
Theorem steps_stepsi : forall st1 st2, Theorem steps_stepsi : forall st1 st2,
step^* st1 st2 step^* st1 st2
@ -1038,7 +1038,7 @@ Proof.
induct 1; first_order; eauto. induct 1; first_order; eauto.
Qed. Qed.
Hint Constructors stepC. Hint Constructors stepC : core.
(* The next few lemmas are quite technical. Commentary resumes for (* The next few lemmas are quite technical. Commentary resumes for
* [translate_trace]. *) * [translate_trace]. *)