Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL
Formal verification of cyber-physical and robotic systems requires that we can accurately model physical quantities that exist in the real-world. The use of explicit units in such quantities can allow a higher degree of rigour, since we can ensure compatibility of quantities in calculations. At the same time, improper use of units can be a barrier to safety and therefore it is highly desirable to have automated sanity checking in physical calculations. In this paper, we contribute a mechanisation of the International System of Quantities (ISQ) and the associated SI unit system in Isabelle/HOL. We show how Isabelle can be used to provide a type system for physical quantities, and automated proof support. Quantities are parameterised by dimension types, which correspond to base vectors, and thus only quantities of the same dimension can be equated. Since the underlying "algebra of quantities" induces congruences on quantity and SI types, specific tactic support is developed to capture these. Our construction is validated by a test-set of known equivalences between both quantities and SI units. Moreover, the presented theory can be used for type-safe conversions between the SI system and others, like the British Imperial System (BIS).
\section{Introduction}
\input{sec/intro}


\section{Related Work}
\label{sec:related}
\input{sec/related}

\section{Dimensions}
\label{sec:dimensions}
\input{sec/dimensions}

\section{Physical Quantities and Measurement}
\label{sec:quantities}
\input{sec/quantities}

\section{Unit Systems and the SI}
\label{sec:units}
\input{sec/units}

\section{Unit Conversions and Non-SI Systems}
\label{sec:conversions}
\input{sec/conversions}

\section{Conclusions}
\label{sec:conclusions}
\input{sec/conclusions}

\bibliographystyle{IEEEtran}



\subsection{Universe of Dimensions}

We begin by defining the dimension universe, the core operators for constructing dimensions, and their properties. If we assume there are $n \in \nat$ base quantities, then a dimension has the form $d_1^{\vec{x}_1} \cdot d_2^{\vec{x}_2} \cdots d_n^{\vec{x}_n}$, a product of dimension symbols ($d_i$) each raised to a power drawn from the vector $\vec{x}$. The encoding of the dimension vector $\vec{x}$ in Isabelle is shown below.

\begin{definition}[Dimension Vectors]
$$\textbf{typedef}~(N, I)~\textit{dimvec} = (\textit{UNIV} :: (I::enum) \Rightarrow N)$$
\end{definition}

\noindent The \textbf{typedef} command in Isabelle/HOL introduces a new type characterised by a non-empty subset of an existing type. In this case, we introduce a new type \textit{dimvec} with two parameters $N$ and $I$. We choose the set $UNIV$ of all total functions from $I$ to $N$ as the characteristic set. In future type definitions, we will use \textbf{typedef} to further restrict the subset. 

Conceptually, a dimension vector is simply a total function from an enumerable index type $I$, for the possible dimensions, to a numeric type $N$, which should minimally form a ring (e.g. $\num$). The enumerable ($enum$) sort constraint ($I :: enum$) requires that $I$ is isomorphic to a list of values, and is thus also a finite type. In the ISQ we have $I = \{\mathbf{L}, \mathbf{M}, \mathbf{T}, \mathbf{I}, \Theta, \mathbf{N}, \mathbf{J}\}$, for example.

Next, we define the core dimension constructors. For simplicity, we present these as functions using $\lambda$-terms, but they are technically defined using the lifting package~\cite{Huffman13Lifting}.

\begin{definition}[Dimension Constructors]
  $$\mathbf{1} \defs (\lambda i.~ 0) \quad \textbf{b}(i) \defs \mathbf{1}(i \mapsto 1)$$
  $$\vec{x} \cdot \vec{y} \defs (\lambda i.~ \vec{x}(i) + \vec{y}(i)) \quad \vec{x}^{-1} \defs (\lambda i.~ - \vec{x}(i))$$
\end{definition}
\noindent Here, $\mathbf{1}$ denotes a null dimension, which does not map to any physical quantity. It can characterise dimensionless quantities, such as mathematical constants ($\pi$, $e$, etc.) and functions.

The function $\textbf{b}(i)$, for $i \in I$, constructs a \emph{base dimension} from the base quantity $i$ by updating the mapping for $i$ in $\mathbf{1}$ to have the power $1$. A base dimension has exactly one entry in the vector mapping to 1, with the others all 0. We also define a predicate $\textit{is-BaseDim} :: (N, I)~\textit{dimvec} \Rightarrow \mathbb{B}$, which determines whether a dimension vector corresponds to a base dimension.

A product of two dimensions ($\vec{x} \cdot \vec{y})$ simply pointwise sums together all of the powers, and an inverse ($\vec{x}^{-1}$) negates each of the powers. We can also now obtain division using the usual definition: $\vec{x} / \vec{y} \defs \vec{x} \cdot \vec{y}^{-1}$. With these definitions, we can prove the following group theorem:

\begin{theorem} If $(N, +, 0, -)$ forms an abelian group then also $((N, I)\textit{dimvec}, \cdot, \mathbf{1}, {}^{-1})$ forms an abelian group.
\end{theorem}
\noindent The abelian group laws can therefore be used to equationally rewrite dimension expressions, which is automated using Isabelle's simplifier.

Another avenue to efficient proof for dimensions is provided through the Isabelle code generator~\cite{Haftman2010-CodeGen}. Since the set of base quantities $I$ is enumerable, we can always convert a dimension vector to a list of $N$, and vice-versa. We achieve this using a function \textit{mk-dimvec}, which converts a list of $N$ with length $|\!I\!|$ to a dimension vector in $N$.

\begin{definition}[Converting Lists to Dimensions] $ $ %
\label{def:list-to-dim}

\vspace{1ex}
  \noindent
  $$
  
  \textit{mk-dvec}(ds) \defs \left(\begin{array}{l} \mathbf{if}~ (length(ds) = ~|\!I\!|) \\
                                       \mathbf{then}~ (\lambda d.~ ds(\textit{enum-ind}(d))) ~\mathbf{else}~ \mathbf{1}\end{array}\right)
  $$
\end{definition}
\noindent Since $I$ is enumerable, every dimension can be assigned a natural number, which also denotes its position in the underlying list. The function $\textit{enum-ind} :: (I\!::\!enum) \Rightarrow \nat$ extracts this positional index of a value in an enumerable type. For ISQ, we have $\textit{enum-ind}(\mathbf{L}) = 0$ and $\textit{enum-ind}(\mathbf{T}) = 2$, for example. We can then construct a dimension from a list $ds$ simply by looking up the value at the enumeration index.

Every possible dimension can be constructed using \textit{mk-dvec}, and so we can use it as a so-called ``code datatype'' for the Isabelle code generator. Dimensions are then encoded in SML or Haskell as an algebraic datatype with a single constructor corresponding to \textit{mk-dvec}, for example:

\begin{alltt}
 \textbf{datatype} ('a, 'b) dimvec = Mk_dimvec of 'a list
\end{alltt}

\noindent We then prove code equation theorems for the group operators, which are homomorphism laws, and enable efficient execution:

\begin{theorem} For a dimension vector space $(N, I)~dimvec$, with $|\!xs\!| \,=\, |\!ys\!| \,=\, |\!I\!|$, the following code equations hold:
\begin{align*}
  \mathbf{1} &= \textit{mk-dvec}\,(\textit{replicate}\,|\!I\!|\,0) \\
  \textit{mk-dvec}(xs) \cdot \textit{mk-dvec}(ys) &= map~(\lambda (x, y).\, x + y)~(zip~xs~ys) \\
  (\textit{mk-dvec}(xs))^n &= \textit{mk-dvec}~(map~(\lambda x.\, n \cdot x)~xs \\
  (\textit{mk-dvec}(xs))^{-1} &= \textit{mk-dvec}~(map~(\lambda x.\, - x)~xs
\end{align*}
\end{theorem}
\noindent These theorems give concrete definitional equations for the executable functions on the datatype. The null dimension is a list of $0$ powers of length $|\!I\!|$. Multiplication of two equilength lists $xs$ and $ys$ is pairwise addition of each element. Raising to the $n$th power multiplies each list element by $n$. Taking the inverse power negates each element. With such equations we can perform efficient dimension arithmetic on dimensions constructed from lists.

Dimensions in the ISQ are represented using the concrete dimension index type \textit{sdim}:

\begin{definition}[ISQ Base Quantities]
\label{def:isq-base-quant}
\begin{align*}
\textbf{datatype}~ sdim &= Length | Mass | Time | Current \\
                        &| Temperature | Amount | Intensity \\[1ex]
\textbf{type-synonym}~ Dimension &= (\num, sdim)~dimvec
\end{align*}
\end{definition}
\noindent
It suffices to show that \textit{sdim} is enumerable, using a type class instantiation, and then we can create a specific type synonym \textit{Dimension}, for dimension vectors in the ISQ. For convenience, we then define dimension vectors for each of the base quantities, for example $\mathbf{L} \defs \mathbf{b}(Length)$.

\subsection{Dimension Types}
\label{sec:dim-types}

Having defined our dimension universe, the next step is to characterise the family of dimension types. These dimension types will be used to parameterise our quantities, and ensure only quantities of the type dimension may be compared. We avoid the need for dependent types by first introducing a type class for dimension types.

\begin{definition}[Dimension Type Classes] $ $ %

\vspace{1ex}

$\begin{array}{l}
\textbf{class}~\textit{dim-type} = unitary~ + \\
~~ \textbf{fixes}~\textit{dim-ty-sem} :: \mathcal{D}~itself \Rightarrow Dimension \\[2ex]
\textbf{class}~\textit{basedim-type} = \textit{dim-type}~ + \\
~~ \textbf{assumes}~ \textit{is-BaseDim}\!: \textit{is-BaseDim}(QD(\mathcal{D}))
\end{array} 
$

\end{definition}
\noindent A type class characterises a family of types that each implement a given function signature with certain properties, such as algebraic structures like monoids and groups. The \textbf{class} command introduces a type class with a given name, potentially extending existing classes. The \textbf{fixes} subcommand declares a new typed symbol in the signature, and \textbf{assumes} introduces a property of the symbols in the signature.

The \textit{dim-type} class characterises a $unitary$ type $\mathcal{D}$ (i.e. a type with cardinality 1) and associates it to a particular dimension. The type $\mathcal{D}~itself$ represents a type as a value in Isabelle/HOL. Thus, \textit{dim-ty-sem} can be seen as a function from types inhabiting the \textit{dim-type} class to particular dimensions, as shown in Figure~\ref{fig:dim-mapping}. We can use the syntactic constructor $TYPE(\alpha)$ to obtain a value of type $\alpha~itself$, for a particular type $\alpha$. This effectively introduces an isomorphism between dimensions at the value level and the type level. For convenience, we introduce the notation $QD(\mathcal{D}) \defs \textit{dim-ty-sem}~\textit{TYPE}(\mathcal{D})$, which obtains the dimension of a given dimension type. The class \textit{basedim-type} further specialises \textit{dim-type} by requiring that the mapped dimension is a base dimension.

We use these classes to capture the set of type constructors for dimension types. First we construct types to denote the base dimensions, as unitary types. For example, we define the type length as below:
$$\textbf{typedef}~Length = (UNIV :: unit~set)$$
which exploits the fact that a type definition generates a fresh type name from a set
(in this case, the set that just contains the only element of the \textit{unit} type).
Though there is a seeming clash with the \textit{Length} constructor introduced in \cref{def:isq-base-quant}, these names inhabit different name spaces. \textit{Length} here is a ``tag type'' whose members do not convey information, but  represent dimension types syntactically.

We define seven such types, one for each of the ISQ base quantities, and also a further special type called \textbf{1}, which corresponds to a dimensionless quantity. Each of the base dimensions instantiates the \textit{basedim-type} class by mapping to the corresponding dimension symbol introduced in the previous section, such that, for example, $QD(Length) = Length$.

Next, we introduce the arithmetic operators for dimensions at the type level. The product and inverse type constructors are defined as shown below:
\begin{align*}
    &\textbf{typedef}~(\mathcal{D}_1\!::\!\textit{dim-ty},\mathcal{D}_2\!::\!\textit{dim-ty})~\textit{DimTimes} = (\textit{UNIV} :: unit set) \\
    &\textbf{typedef}~(\mathcal{D}\!::\!\textit{dim-ty})~DimInv = (\textit{UNIV} :: unit set)
\end{align*}
They are similarly tag types, but the parameters must inhabit the \textit{dim-ty} class. This ensures that the dimension types are closed under products and inverse. Using these type constructors, and the base dimension types, we can inductively define algebraic dimensions at the type level. We assign the type constructors the following implementations of \textit{dim-ty-sem}:
\begin{definition}[Semantic Interpretation of Dimension Types] \label{def:sem-dim} 
\begin{align*}
    \textit{dim-ty-sem}(d :: (\mathcal{D}_1, \mathcal{D}_2)~\textit{DimTimes}) &= QD(\mathcal{D}_1) \cdot QD(\mathcal{D}_2) \\
    \textit{dim-ty-sem}(d :: (\mathcal{D})~\textit{DimInv}) &= QD(\mathcal{D})^{-1}
\end{align*}
\end{definition}
These link together the type constructors and the underlying dimension operators. The semantics of a \textit{DimTimes} type calculates the underlying value-level dimension of each parameter $\mathcal{D}_1$ and $\mathcal{D}_2$, and multiplies them together. The \textit{DimInv} type similarly calculates the dimension and then takes the inverse. We give these type constructors the usual mathematical syntax, so that we can write dimension types like $\mathbf{M} \cdot \mathbf{L}$ and $\mathbf{T}^{-1}$. We also define a type synonym for division, namely $(\mathcal{D}_1, \mathcal{D}_2)~\textit{DimDiv} \defs \mathcal{D}_1 \cdot \mathcal{D}_2^{-1}$, and give it the usual syntax. Moreover, we define a fixed number of powers and inverse powers at the type level, such as $\mathcal{D}^{-3} = (\mathcal{D} \cdot \mathcal{D} \cdot \mathcal{D})^{-1}$.

We can now also create the set of derived dimensions specified in the ISQ using type synonyms. For example, we define $\textit{Velocity} \defs \mathbf{L} \cdot \mathbf{T}^{-1}$ and $\textit{Pressure} \defs \mathbf{L}^{-1} \cdot \mathbf{M} \cdot \mathbf{T}^{-1}$, which provides a terminology of dimensions for use in formal specifications. We show further example in Figure~\ref{fig:derived-dimensions}, which also demonstrates the mathematical syntax for dimensions implemented in Isabelle/HOL.

\begin{figure}[t]
  \centering
  \includegraphics[width=.6\linewidth]{figures/Derived_Dimensions.png}

  \caption{Derived dimension type expressions in Isabelle/HOL}
  \label{fig:derived-dimensions}

  \vspace{-1ex}
\end{figure}

\subsection{Dimension Normalisation}
\label{sec:dim-norm}

Unlike dimensions at the value level, dimension types with different syntactic forms are incomparable, because they are distinct type expressions. For example, it is intuitively a fact that $\mathbf{L} \cdot \mathbf{T}^{-1} \cdot \mathbf{T} = \mathbf{L}$, which can be proved using the group laws. However, at the type level $\mathbf{L} \cdot \mathbf{T}^{-1} \cdot \mathbf{T}$ and $\mathbf{L}$ are different type expressions, and no built-in normalisation is available in Isabelle. As a result, we need to implement our own normalisation function, $\textit{normalise}(\mathcal{D})$, for ISQ dimensions in Isabelle/ML, so that quantities over dimensions with distinct syntactic forms can be related. Our normalisation function evaluates the dimension vector of a dimension expression, and then uses this to produce a normal form.

We implement dimension type evaluation using the ML function $\textit{typ-to-dim} :: typ \Rightarrow int~list$. It converts types formed of the base dimensions and dimension arithmetic operators into a dimension vector list, using the representation given in \cref{def:list-to-dim}. For example, $\textit{typ-to-dim}(\mathbf{L}) = [1, 0, 0, 0, 0, 0, 0]$ and $\textit{typ-to-dim}(\mathcal{D}^{-1}) = map~(\lambda x.\, - x)~(\textit{typ-to-dim}(x))$.

Having evaluated the dimension expression, we can use it to construct the normal form. This is an ordered dimension expression of the form $\mathbf{L}^{\vec{x}_1} \cdot \mathbf{M}^{\vec{x}_2} \cdot \mathbf{T}^{\vec{x}_3} \cdots \mathbf{J}^{\vec{x}_7}$, except that we omit terms where $\vec{x}_i = 0$. If every such term is $0$, then the function produces the dimensionless quantity, $\mathbf{1}$. As an example, $\textit{normalise}(\mathbf{T}^4 \cdot \mathbf{L}^{-2} \cdot \mathbf{M}^{-1} \cdot \mathbf{I}^2 \cdot \mathbf{M})$ yields the dimension type $\mathbf{L}^{-2} \cdot \mathbf{T}^4 \cdot \mathbf{I}^2$. This normalisation function is used later in this paper to facilitate coercion between quantities with distinct dimension expressions.


\subsection{Quantity Universe and Measurement Systems}
\label{sec:quant-univ}

We specify our quantity universe as a record with fields for the magnitude and dimension of the quantity.

\begin{definition}[Quantity Universe]
$$\begin{array}{rl}
  \textbf{record}~ (N, I\!::\!enum)\, Quantity =&\hspace{-1.5ex} mag\!::\!N\ \\ &\hspace{-1.5ex} dim\!::\!(int, I)\,dimvec
\end{array}$$
\end{definition}

\noindent The \textit{Quantity} type is parametric over a numeric type $N$ (e.g. $\mathbb{Q}$, $\mathbb{R}$), which should form a field, and the dimension index type $I$. The magnitude is then a number in $N$, and a dimension vector in over $I$. We can now specify the core arithmetic operators on quantities. For convenience of presentation, we use tuple syntax $(x, \mathcal{D})$, though in Isabelle the record fields are used.

\begin{definition}[Quantity Arithmetic Operators] \label{def:quant-arith}
  \begin{align*}
    0 &\defs (0, \mathbf{1}) \\
    1 &\defs (1, \mathbf{1}) \\
    (x, \mathcal{D}_1) \cdot (y, \mathcal{D}_2) &= (x \cdot y, \mathcal{D}_1 \cdot \mathcal{D}_2) \\
    (x, \mathcal{D})^{-1} &= (x^{-1}, \mathcal{D}^{-1}) \\
    (x, \mathcal{D}_1) / (y, \mathcal{D}_2) &= (x / y, \mathcal{D}_1 / \mathcal{D}_2) \\
    (x, \mathcal{D}) + (y, \mathcal{D}) &= (x + y, \mathcal{D}) \\
    (x, \mathcal{D}) - (y, \mathcal{D}) &= (x - y, \mathcal{D}) \\
    (x, \mathcal{D}_1) \le (y, \mathcal{D}_2) &\iff (x \le y \land \mathcal{D}_1 = \mathcal{D}_2)
  \end{align*}
\end{definition}

\noindent The arithmetic operators are overloaded in Isabelle/HOL, which is why they can validly appear on both sides of these equations. The ``0'' and ``1'' quantities are specified as dimensionless quantities with magnitude 0 and 1, respectively. Multiplication, inverse, and division are total operations that simply distribute through the pair. When multiplying two quantities, we need to multiply both the magnitudes and dimensions. For example, $(7, \mathbf{L}\cdot\mathbf{T}^{-1}) \cdot (2, \mathbf{T}) = (14, \mathbf{L})$. In contrast, addition and subtraction are partial operators that may be applied only when the two quantities have the same dimension. In Isabelle/HOL, the value of an addition or subtraction for different quantities of different dimensions is unspecified. Finally, the order on quantities is simply the order on the magnitudes, but with the requirement that the two dimensions are equal.

Quantities as formalised so far specify the form of dimension, but not the system of units being employed. For this, we extend the \textit{Quantity} type to create ``measurement systems'':

\begin{definition}[Measurement Systems]
$$
\begin{array}{l}
\textbf{record} (N, I\!::\!enum, \mathcal{S}\!::\!\textit{unit-system})~\textit{Measurement-System} \\
  \quad = (N, I)~Quantity + \textit{unit-sys} :: \mathcal{S}
\end{array}
$$  
\end{definition}

\noindent We extend the \textit{Quantity} record with an additional field \textit{unit-sys}. A measurement system is a quantity that specifies the system of units being used via an additional type parameter $\mathcal{S}$, which must inhabit the type class \textit{unit-system}. A unit system type is a unitary type that effectively allows us to tag quantities. This allows us to distinguish quantities using different systems of units, and so prevent improper mixing.

For example, the presence of the \textit{SI} tag means that a quantity of length is fundamentally measured in metres, whereas the presence of a tag such as \textit{BIS} may indicate that length is measured in yards. Later, we will use these to facilitate type-safe conversions between different unit systems.

All the arithmetic operators can be straightforwardly lifted to measurement systems. Since all such functions are monomorphic (e.g. of type $\alpha \Rightarrow \alpha \Rightarrow \alpha$), mixing of systems is avoided by construction.


\subsection{Dimension Typed Quantities}

Having defined our universe for quantities, we next enrich this representation with type-level dimensions. For expediency, we assume that all such quantities also have a measurement system attached. Moreover, we focus on quantities with dimensions from the ISQ.

\begin{definition}[Quantity Type]
$$
\begin{array}{l}
\textbf{typedef}~ (N, \mathcal{D}\!::\!\textit{dim-type}, \mathcal{S}::\textit{unit-system})~\textit{QuantT} \\ 
\quad = \{x :: (N, sdim, S)~\textit{Measurement-System}.~~ dim(x) = QD(\mathcal{D})\} 
\end{array}
$$
\end{definition}
\noindent The $(N, \mathcal{D}, \mathcal{S})~\textit{QuantT}$ type represents a quantity with numeric type $N$, dimension type $\mathcal{D}$, and unit system $\mathcal{S}$. The type definition introduces an invariant that requires that the dimension of the underlying quantity $x$ agrees with the one specified in the dimension type. At this level, we use \textit{sdim} as the concrete interpretation of dimensions, as this is required by the \textit{dim-type} class. For convenience, we introduce the type syntax $N[\mathcal{D}, \mathcal{S}]$ to stand for $(N, \mathcal{D}, \mathcal{S})~\textit{QuantT}$. Our \textbf{typedef} also induces two functions for converting between typed and untyped quantitities: $\textit{fromQ} :: N[\mathcal{D}, \mathcal{S}] \Rightarrow (N, \textit{sdim}, \mathcal{S})~\textit{Measurement-System}$ and \textit{toQ} in the opposite direction.

Lifting of arithmetic operators $x + y$ and $x - y$ is straightforward for typed quantities, since they are monomorphic and only defined when the dimensions of $x$ and $y$ agree. We can then easily show that typed quantities form an additive abelian group. We also define a scalar multiplication $\textit{scaleQ} :: N \Rightarrow N[\mathcal{D}, \mathcal{S}] \Rightarrow N[\mathcal{D}, \mathcal{S}]$, with notation $n \mathop{*_\qsub} x$, which scales a quantity by a given number without changing the dimension. We can then show that typed quantities form an additive abelian group, and a real vector space, with $(\mathop{*_\qsub})$ as the scalar multiplication operator.

Things are more involved when dealing with general multiplication and division, since these need to perform dimension arithmetic at the type level. For example, if we have quantities $x :: \mathbb{R}[\mathbf{I}, SI]$ and $y :: \mathbb{R}[\mathbf{T}, SI]$, then multiplication of $x$ and $y$ is well-defined, and should have the type $\mathbb{R}[\mathbf{I}\cdot\mathbf{T}, SI]$. As a result, we introduce bespoke functions, $qtimes$, $qinverse$, and $qdivide$. We first give the types for these functions:
\begin{align*}
  qtimes &:: N[\mathcal{D}_1, \mathcal{S}] \Rightarrow N[\mathcal{D}_2, \mathcal{S}] \Rightarrow N[\mathcal{D}_1 \cdot \mathcal{D}_2, \mathcal{S}] \\
  qinverse &:: N[\mathcal{D}, \mathcal{S}] \Rightarrow N[\mathcal{D}^{-1}, \mathcal{S}] \\
  qdivide &:: N[\mathcal{D}_1, \mathcal{S}] \Rightarrow N[\mathcal{D}_2, \mathcal{S}] \Rightarrow N[\mathcal{D}_1 / \mathcal{D}_2, \mathcal{S}]
\end{align*}
\noindent The first function multiplies two quantities, with the same measurement system, and ``multiplies'' the dimension types using the type constructors introduced in \S\ref{sec:dim-types}. Technically, no multiplication computation takes place, but rather a type constructor denoting multiplication is inserted. Similarly, \textit{qinverse} represents the inverse of the parametrised dimension, and \textit{qdivide} stands for a division. What is achieved here is analogous to dependent types, though we require additional machinery for normalising dimension types (cf. \S\ref{sec:dim-norm}).

The definitions of \textit{qtimes} and \textit{qinverse} are obtained simply by lifting of the corresponding functions on quantities in Definition~\ref{def:quant-arith}, which is technically achieved using the \emph{lifting} package~\cite{Huffman13Lifting}. In order to do this we need to prove that the invariant of the \textit{QuantT} type is satisfied, which involves showing that the family of typed quantities is closed under the two functions. For \textit{qmult}, we need to prove that $dim(x \cdot y) = QD(\mathcal{D}_1 \cdot \mathcal{D}_2)$, whenever $dim(x) = QD(\mathcal{D}_1)$ and $dim(y) = QD(\mathcal{D}_2)$, which follows simply through Definitions \ref{def:sem-dim} and \ref{def:quant-arith}. For convenience, we give these functions the usual notation of $x \bullet y$, $x^{-1}$, and $x / y$, but in Isabelle we embolden the operators to syntactically distinguish them. With \textit{qtimes} and \textit{qinverse}, we can also define positive and negative powers, such as $x^{-2} = (x \bullet x)^{-1}$.

Equality ($x = y$) in HOL is a homogeneous function of type $\alpha \to \alpha \to \mathbb{B}$; therefore, it cannot be used to compare objects of different types. Consequently, it cannot be used to compare quantities whose dimension types have different syntactic forms (e.g. $\mathbf{L} \cdot \mathbf{T}^{-1} \cdot \mathbf{T}$ and $\mathbf{L}$). This motivates a definition of \emph{heterogeneous (in)equality} for quantities:
\begin{align*}
  \textit{qequiv} &:: N[\mathcal{D}_1, \mathcal{S}] \Rightarrow N[\mathcal{D}_2, \mathcal{S}] \Rightarrow \mathbb{B} \\
  \textit{qless-eq} &:: N[\mathcal{D}_1, \mathcal{S}] \Rightarrow N[\mathcal{D}_2, \mathcal{S}] \Rightarrow \mathbb{B}
\end{align*}

\noindent These functions are defined simply by lifting the functions $(=)$ and $(\le)$ on the underlying quantities. They ignore the dimension types, but the underlying dimensions must nevertheless be the same as per the definitions in \S\ref{sec:quant-univ}. We give these functions the notation $x \cong y$ and $x \lesssim y$, respectively. Relation $(\cong)$ forms an equivalence relation, and $(\lesssim)$ forms a preorder. Moreover, $(\cong)$ is a congruence relation for $(\bullet)$, $({}^{-1})$, and $(\mathop{*_\qsub})$.


\subsection{Proof Support}

We implement an interpretation-based proof strategy for typed quantity (in)equalities, which allows us to split a conjecture into two parts: (1) equality of the magnitudes; and (2) equivalence of the dimensions. This is supported by a function $\textit{magQ} :: N[\mathcal{D}, \mathcal{S}] \Rightarrow N$, with syntax $\qsem{-}$, which extracts the magnitude from a typed quantity. We can calculate magnitudes using interpretation laws, like the ones below:
  $$\qsem{x + y} = \qsem{x} + \qsem{y} \quad \qsem{x \bullet y} = \qsem{x} \cdot \qsem{y}$$
\noindent Such laws derive directly from the definition of the quantity operators in Definition~\ref{def:quant-arith}. The equation for addition implicitly makes use of the fact that $x$ and $y$ have the same dimension, and so addition is well-defined in the quantity universe. We then have the following transfer theorems, for the case of two quantitites with the same (syntactic) dimensions:
\begin{theorem}[Quantity Transfer Laws]
  $$x = y \iff (\qsem{x} = \qsem{y}) \qquad x \le y \iff (\qsem{x} \le \qsem{y})$$
\end{theorem}
\noindent In both cases, we need not check the equivalence of the dimensions as by construction we know that $x$ and $y$ have the same type, and so also have the same dimensions. It is sufficient simply to check the relation holds of the underlying magnitudes. For our heterogeneous (in)equality relations, we have the following transfer theorems:
\begin{theorem}[Heterogeneous Transfer Laws] Given quantities $x :: N[\mathcal{D}_1, \mathcal{S}]$ and $y :: N[\mathcal{D}_2, \mathcal{S}]$, we have
  $$x \cong y \iff \left(\qsem{x} = \qsem{y} \land QD(\mathcal{D}_1) = QD(\mathcal{D}_2)\right).$$ 
\end{theorem}
\noindent We can then prove heterogeneous equalities by calculation of the underlying magnitudes and dimensions, and use of the numeric and dimensions laws. We supply a proof method called \textit{si-simp}, which uses the simplifier to perform transfer and interpretation, and additionally invokes field simplification laws. An additional method called \textit{si-calc} also compiles dimension vectors (cf. Definition~\ref{def:list-to-dim}) using the code generator, and can thus efficiently prove dimension equalities. We can, for example, prove the following algebraic laws automatically:
\begin{theorem}[Quantity Algebraic Laws]
  \begin{align*}
    a \mathop{*_\qsub} (x + y) &= (a \mathop{*_\qsub} x) + (a \mathop{*_\qsub} y) \\
    x \bullet y &\cong y \bullet x \\
    (x \bullet y)^{-1} &\cong x^{-1} \bullet y^{-1}
  \end{align*}
\end{theorem}

  
\subsection{Coercion and Dimension Normalisation}

The need for heterogeneous quantity relations ($\cong$, $\lesssim$) can be avoided by the use of coercions to convert between two syntactic representations of the same dimension. Moreover, we can use Isabelle's sophisticated syntax and checking pipeline to normalise dimensions, and so automatically coerce quantities to a normal form. This improves the usability of the library, since the usual relations $(=)$ and $(\le)$ can be used directly.

We implement a function $\textit{dnorm} :: N[\mathcal{D}_1, \mathcal{S}] \Rightarrow N[\mathcal{D}_2, \mathcal{S}]$, which can convert between quantities with different dimension forms. In order to use it effectively, it is necessary to know the target dimension $\mathcal{D}_2$ in advance. It is defined below:
$$\textit{dnorm}(x) \defs (\mathbf{if}~QD(\mathcal{D}_1) = QD(\mathcal{D}_2)~\mathbf{then}~toQ~(\,fromQ(x))~\mathbf{else}~0)$$
The function checks whether the source and target dimensions ($\mathcal{D}_1$ and $\mathcal{D}_2$) are the same. If they agree, then it performs the coercion by erasing the types with \textit{fromQ} and reinstating the new dimension type with \textit{toQ}. Otherwise, it returns a valid quantity of the target dimension, but with magnitude $0$. For example, if we have $x :: \mathbb{R}[\mathbf{L} \cdot \mathbf{T}^{-1} \cdot \mathbf{T}, SI]$, then we can use $\textit{dnorm}(x) :: \mathbb{R}[\mathbf{L}, SI]$ to obtain a quantity with an equivalent dimension, since $QD(\mathbf{L} \cdot \mathbf{T}^{-1} \cdot \mathbf{T}) = QD(\mathbf{L})$. In general, for two equivalent quantities $x \cong y$, we have it that $\textit{dnorm}(x) = y$.

Next, we extend Isabelle's checking pipeline to allow dimension normalisation, so that $\mathcal{D}_2$ can be automatically calculated. We do this by implementing an SML function \textit{check-quant}, which takes a term and enriches it with dimension information. Whenever it encounters an instance of $\textit{dnorm}(t)$, it extracts the type of $t$, which should be $N[\mathcal{D}, \mathcal{S}]$. This being the case, we enrich the instance of \textit{dnorm} to have the type $N[\mathcal{D}, \mathcal{S}] \Rightarrow N[\textit{normalise}(\mathcal{D}), \mathcal{S}]$.

We then insert \textit{check-quant} into Isabelle's term checking pipeline. Technically, this is achieved using an Isabelle/ML API function called \texttt{Syntax\_Phases.term\_check}, which allow us to add a new phase into the term checking process. In this case, we add it after type inference has occurred so that we can use the unnormalised dimension type expression as an input to \textit{check-quant}.

The soundness of this transformation does not depend on the correctness of \textit{normalise}, since if an incorrect dimension is calculated, \textit{dnorm} will return 0. Nevertheless, the effect is to achieve something akin to dependent types, but in a first-order polymorphic type system.



2023-02-16T02:12:43.000
2302
2302.07629
en
https://arxiv.org/abs/2302.07629
Formal verification of cyber-physical and robotic systems requires that we can accurately model physical quantities that exist in the real-world. The use of explicit units in such quantities can allow a higher degree of rigour, since we can ensure compatibility of quantities in calculations. At the same time, improper use of units can be a barrier to safety and therefore it is highly desirable to have automated sanity checking in physical calculations. In this paper, we contribute a mechanisation of the International System of Quantities (ISQ) and the associated SI unit system in Isabelle/HOL. We show how Isabelle can be used to provide a type system for physical quantities, and automated proof support. Quantities are parameterised by dimension types, which correspond to base vectors, and thus only quantities of the same dimension can be equated. Since the underlying "algebra of quantities" induces congruences on quantity and SI types, specific tactic support is developed to capture these. Our construction is validated by a test-set of known equivalences between both quantities and SI units. Moreover, the presented theory can be used for type-safe conversions between the SI system and others, like the British Imperial System (BIS).
Logic in Computer Science (cs.LO)
Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL
Qwen/Qwen-72B
1. YES
2. YES