# Changeset 539 for Deliverables/D4.1/ITP-Paper/itp-2011.tex

Ignore:
Timestamp:
Feb 16, 2011, 5:10:33 PM (9 years ago)
Message:

 r538 \lstdefinelanguage{matita-ocaml} {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on}, {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to}, morekeywords={[2]whd,normalize,elim,cases,destruct}, morekeywords={[3]type,of,val,assert,let,function}, From hereonin, we typeset O'Caml source with blue and Matita source with red to distinguish between the two similar syntaxes. Matita's syntax is similar to that of O'Caml. The only subtlety is the use of \texttt{?} in an argument position, which denotes an argument that should be inferred automatically, if possible. \subsection{Development strategy} A function that checks whether an \texttt{addressing\_mode} is `morally' an \texttt{addressing\_mode\_tag} is provided, as follows: \begin{lstlisting} let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d ≝ let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d := match d with [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ] We also extend this check to vectors of \texttt{addressing\_mode\_tag}'s in the obvious manner: \begin{lstlisting} let rec is_in (n) (l: Vector addressing_mode_tag n) (A: addressing_mode) on l ≝ let rec is_in (n: nat) (l: Vector addressing_mode_tag n) (A: addressing_mode) on l := match l return $\lambda$m.$\lambda$_: Vector addressing_mode_tag m. bool with [ VEmpty $\Rightarrow$ false Here $\mathtt{\vee}$ is inclusive disjunction on the \texttt{bool} datatype. \begin{lstlisting} record subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝ record subaddressing_mode (n: nat) (l: Vector addressing_mode_tag (S n)): Type[0] := { subaddressing_modeel :> addressing_mode; % Have lemmas proving that if an element is a member of a sub, then it is a member of a superlist, and so on The final, missing component is a pair of type coercions from \texttt{addressing\_mode} to \texttt{subaddressing\_mode} and from \texttt{subaddressing\_mode} to \texttt{Type$\lbrack0\rbrack$}, respectively. The previous machinery allows us to state in the type of a function what addressing modes that function expects. The latter coercion is largely straightforward, however the former is not: \begin{lstlisting} coercion mk_subaddressing_mode: $\forall$n.  $\forall$l: Vector addressing_mode_tag (S n). $\forall$a: addressing_mode. $\forall$p: bool_to_Prop (is_in ? l a). subaddressing_mode n l := mk_subaddressing_mode on a: addressing_mode to subaddressing_mode ? ?. \end{lstlisting} Using this coercion opens a proof obligation wherein we must prove that the \texttt{addressing\_mode\_tag} in correspondence with the \texttt{addressing\_mode} is a member of the \texttt{Vector} of permissible \texttt{addressing\_mode\_tag}s. This impels us to state and prove a number of auxilliary lemmas. For instance, we prove that if an \texttt{addressing\_mode\_tag} is a member of a \texttt{Vector}, and we possess a supervector, then the same \texttt{addressing\_mode\_tag} is a member of this supervector. Without combining Matita's automation and lemmas such as these our approach becomes infeasible: type checking the main \texttt{execute1} function opens up over 200 proof obligations. The machinery just described allows us to state in the type of a function what addressing modes that function expects. For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}: \begin{lstlisting}