From e032ab4240adae3fa16f23547d6bc9da3ff03c42 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 4 Mar 2019 11:23:01 -0500 Subject: [PATCH 1/4] Update for Coq 8.9 --- .gitignore | 2 +- DeepAndShallowEmbeddings.v | 2 +- DeepAndShallowEmbeddings_template.v | 2 +- DependentInductiveTypes.v | 2 +- DependentInductiveTypes_template.v | 2 +- FrapWithoutSets.v | 2 +- SharedMemory.v | 34 ++++++++++++++--------------- 7 files changed, 23 insertions(+), 23 deletions(-) diff --git a/.gitignore b/.gitignore index 3090ba6..43c0b49 100644 --- a/.gitignore +++ b/.gitignore @@ -12,7 +12,7 @@ Makefile.coq Makefile.coq.conf *.glob -*.v.d +*.d *.vo frap.tgz .coq-native diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v index 71ae07f..f9bdb90 100644 --- a/DeepAndShallowEmbeddings.v +++ b/DeepAndShallowEmbeddings.v @@ -886,7 +886,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 diff --git a/DeepAndShallowEmbeddings_template.v b/DeepAndShallowEmbeddings_template.v index 5365fad..352d80c 100644 --- a/DeepAndShallowEmbeddings_template.v +++ b/DeepAndShallowEmbeddings_template.v @@ -731,7 +731,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 diff --git a/DependentInductiveTypes.v b/DependentInductiveTypes.v index 9848008..3f513d6 100644 --- a/DependentInductiveTypes.v +++ b/DependentInductiveTypes.v @@ -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. *) diff --git a/DependentInductiveTypes_template.v b/DependentInductiveTypes_template.v index 715ecda..464b53a 100644 --- a/DependentInductiveTypes_template.v +++ b/DependentInductiveTypes_template.v @@ -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. *) 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/SharedMemory.v b/SharedMemory.v index 2f77dbf..c460acc 100644 --- a/SharedMemory.v +++ b/SharedMemory.v @@ -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)). From ed64e05e38bf42705e132b99af21730765860e62 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 4 Mar 2019 11:26:06 -0500 Subject: [PATCH 2/4] Closes #27 --- frap_book.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/frap_book.tex b/frap_book.tex index e89e48c..5412798 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -810,7 +810,7 @@ In that sense, with this translation, we make progress toward efficient implemen \newcommand{\compile}[1]{{\left \lfloor #1 \right \rfloor}} Throughout this book, we will use notation $\compile{\ldots}$ for compilation, where the floor-based notation suggests \emph{moving downward} to a lower abstraction level. -Here is the compiler that concerns us now, where we write $\concat{s_1}{s_2}$ for concatenation of two stacks $s_1$ and $s_2$. +Here is the compiler that concerns us now, where we write $\concat{\overline{i_1}}{\overline{i_2}}$ for concatenation of two instruction sequences $\overline{i_1}$ and $\overline{i_2}$. \encoding \begin{eqnarray*} \compile{n} &=& \mathsf{PushConst}(n) \\ @@ -843,7 +843,7 @@ e \arrow{r}{\compile{\ldots}} \arrow{dr}{\denote{\ldots}} & \compile{e} \arrow{d As usual, we leave proof details for the associated Coq code, but the key insight of the proof is to strengthen the induction hypothesis via a lemma. \begin{lemma} - $\denote{\concat{\compile{e}}{\overline{i}}}(v, s) = \denote{\overline{i}}(v, \concat{\denote{e}v}{s})$. + $\denote{\concat{\compile{e}}{\overline{i}}}(v, s) = \denote{\overline{i}}(v, \push{\denote{e}v}{s})$. \end{lemma} We strengthen the statement by considering both an arbitrary initial stack $s$ and a sequence of extra instructions $\overline{i}$ to be run after $e$. From 93ef5add7a69eb8aacb5eacd37f91a5c4e104251 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 4 Mar 2019 11:28:37 -0500 Subject: [PATCH 3/4] Closes #28 --- frap_book.tex | 1 + 1 file changed, 1 insertion(+) diff --git a/frap_book.tex b/frap_book.tex index 5412798..081d499 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -1972,6 +1972,7 @@ One example, which we'll formalize in more detail shortly, would be to label eac \renewcommand{\O}[0]{\mathsf{O}} As an example, consider this formalization of even-odd analysis, whose proof of soundness is left as an exercise for the reader. +(While the treatment of subtraction may seem gratuitously imprecise, recall that we are working here with natural numbers and not integers, such that subtraction ``sticks'' at zero when the result would otherwise be negative.) \begin{eqnarray*} \mathbb D &=& \{\E, \O, \top\} \\ \mathcal C(n) &=& \textrm{$\E$ or $\O$, depending on parity of $n$} \\ From 958906a2e535d5460813a1aeba7548abafa7768b Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 8 Jan 2020 14:36:27 -0500 Subject: [PATCH 4/4] Clarify Cartesian-product operator --- frap_book.tex | 2 ++ 1 file changed, 2 insertions(+) diff --git a/frap_book.tex b/frap_book.tex index 081d499..02b0ab0 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -217,6 +217,8 @@ Such types can be defined by enumerating their \emph{constructor}\index{construc \mathsf{Times} &:& \mathsf{Exp} \times \mathsf{Exp} \to \mathsf{Exp} \end{eqnarray*} +Note that the ``$\times$'' here is not the multiplication operator of concrete syntax, but rather the Cartesian-product operator\index{Cartesian product} of set theory, to indicate a type of pairs! + Such a list of constructors defines the set $\mathsf{Exp}$ to contain exactly those terms that can be built up with the constructors. In inference-rule notation: \encoding