Changeset 1024 for src

Ignore:
Timestamp:
Jun 21, 2011, 12:27:02 PM (9 years ago)
Message:

tidied explanation of proof

File:
1 edited

Legend:

Unmodified
 r1023 For instance, to apply a coercion to force $\lambda x.M : A \to B$ to have type $\forall x:A.\Sigma y:B.P~x~y$, the system looks for a coercion from $M: B$ to $\Sigma y:B.P~x~y$ in a context augmented with $x:A$. This is significant when the coercion opens a proof obligation, as the user will be presented with multiple, but simpler proof obligations in the correct context. In this way, Matita supports the proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated than that of Coq. In this way, Matita supports the proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated with the system than that of Coq. % ---------------------------------------------------------------------------- % This is a tempting approach to the proof, but ultimately the wrong approach. In particular, to expand a pseudo instruction we need to know the address at which the expanded instructions will be located, for instance to determine if a short jump is possible. That address is a function of the \emph{object code} generated for the pseudo-instructions already visited. Thus we need to assemble each pseduto instruction down to object code before moving to the next one and this must be eventually reflected on the proof of correctness. Therefore we will have lemmas for the \texttt{assembly1} function and for the composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly1}, but not for \texttt{expand\_pseudo\_instruction} alone. In particular, to expand a pseudoinstruction we need to know the address at which the expanded instructions will be located, for instance to determine if a short jump is possible. That address is a function of the \emph{machine code} generated for the pseudoinstructions already expanded. Thus, we must assemble each psedutoinstruction into machine code before moving on, and this must be eventually reflected in the proof of correctness. Therefore we will have lemmas proving correctness for the \texttt{assembly1} function, and for the composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly1}, but not for \texttt{expand\_pseudo\_instruction} alone. % ---------------------------------------------------------------------------- %