Exercise 8.6
Consider the following mathematical text:
‘If $k$, l and m are integers, $m$ being positive, then one says that $k$ is congruent to l modulo $m$ if $m$ divides $k−l$. We write $k ≡l(\mod m)$ to indicate that $k$ is congruent to $l$ modulo m$.
Hence $−3 ≡17(\mod 5)$, but not $−3 ≡−17(\mod 5)$.
If $k ≡l(\mod m)$ then also $l ≡k(\mod m)$.
$k ≡l(\mod m)$ if and only if there is an integer $u$ such that $k= l+um$.’
(a) Rewrite the texts in a formal form, as a list of definitions. Assume that $\mathbb{Z}$ is a type. Employ the flag format. Formalise $k ≡l(\mod m)$ as $eqv(k,l,m,u)$, with$u$ a proof that $m$ is positive.
(b) Indicate the scopes of all variables and constants introduced in the formal text.
(c) Identify all instantiations of the parameter lists introduced in the formal text and check that the type conditions are respected.
(a) The following is a flag-format formalisation of the text.
Note the author's solution has $\implies$ instead of $\iff$ for line (6).
(b) The scopes of the variables and constants are as follows:
- $k,l,m$ have local scope lines (2) to (6).
- $u$ has local scope lines (3) to (6).
- $v, p_1, p_2$ have global scope.
- $\textit{eqv}, q, r$ have global scope.
- $n$ has scope limited to the expression $(k=l+nm)$ at line (6).
(c) The instantiations of introduced parameter lists are as follows:
- line (5) $\textit{eqv}(k,l,m,u)$ is an identity instantiation.
- line (5) $\textit{eqv}(l,k,m,u)$ is not an identity instantiation. The type of $l$ and $k$ match the introduced types $\mathbb{Z}$. The type of $m$ is the expected $\mathbb{Z}$. The type of $u$ is $m>0$ as expected.
- line (6) $\textit{eqv}(k,l,m,u)$ is an identity instantiation.
- line (8) $\textit{eqv}(-3, 17, 5, v)$ has $-3, 17, 5$ of the expected type $\mathbb{Z}$ and $v$ is of type $m>0$ with $m=5$.
- line (9) $\textit{eqv}(-3, -17, 5, v)$ has $-3, -17, 5$ of the expected type $\mathbb{Z}$ and $v$ is of type $m>0$ with $m=5$.
