pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-20 04:07:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge pull request #12 from ZiyaoWei/patch-2

Browse source 
Typo - invariant should be AnswerIs(n_0!)
This commit is contained in:
Adam Chlipala 2016-03-09 11:12:23 -05:00
commit 5ed670b5a6
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
frap_book.tex
View file

@ -873,7 +873,7 @@ Another important property of invariants formalizes the connection with weakenin
\end{theorem} \end{theorem}
Note that the larger $I'$ above may not be suitable to use in an inductive proof by Theorem \ref{invariant_induction}! Note that the larger $I'$ above may not be suitable to use in an inductive proof by Theorem \ref{invariant_induction}!
For instance, for factorial, we might define $I' = \mathcal \{\mathsf{AnswerIs}(n_0)\} \cup \{\mathsf{WithAccumulator}(n, a) \mid n, a \in \mathbb N\}$, clearly a superset of $I$. For instance, for factorial, we might define $I' = \mathcal \{\mathsf{AnswerIs}(n_0!)\} \cup \{\mathsf{WithAccumulator}(n, a) \mid n, a \in \mathbb N\}$, clearly a superset of $I$.
However, by forgetting everything that we know about intermediate $\mathsf{WithAccumulator}$ states, we will get stuck on the inductive step of the proof. However, by forgetting everything that we know about intermediate $\mathsf{WithAccumulator}$ states, we will get stuck on the inductive step of the proof.
Thus, what we call invariants here needn't also be \emph{inductive invariants}\index{inductive invariants}, and there may be slight terminology mismatches with other sources. Thus, what we call invariants here needn't also be \emph{inductive invariants}\index{inductive invariants}, and there may be slight terminology mismatches with other sources.