Add more recursive rules

1 files changed, 22 insertions, 12 deletions

diff --git a/main.tex b/main.tex
index 74eeb57..5fe26c7 100644
--- a/main.tex
+++ b/main.tex
@@ -220,54 +220,64 @@ based on what they evaluate to. For case I think that would end up being a three
 \YH{To add to that, I used to have both in the Coq code, but commented the recursive definition out, and now only have the inductive definition, which is basically what I copy pasted here.} \JW{Fair enough. Whatever you think ends up being the easiest to read and understand, really. There's something to be said for staying close to the Coq definitions anyway.}
 
 \begin{align}
-    \text{stmntrun}\ f\ s\ \mathtt{Vskip} &= s \\
-    \text{stmntrun}\ f\ s_0\ (\mathtt{Vseq}\ \mathit{st}_1\ \mathit{st}_2) &= \text{stmntrun}\ f\
-    (\text{stmntrun}\ f\ s_0\ \mathit{st}_1)\ \mathit{st}_2
+    \text{srun}\ f\ s\ \mathtt{Vskip} &= \mathtt{Some}\ s\\
+    \text{srun}\ f\ s_0\ (\mathtt{Vseq}\ \mathit{st}_1\ \mathit{st}_2) &= \text{srun}\ f\
+    (\text{srun}\ f\ s_0\ \mathit{st}_1)\ \mathit{st}_2\\
+  \text{srun}\ f\ s\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf}) &= \begin{cases}
+    \text{srun}\ f\ s_{0}\ \mathit{stf},& \text{erun}\ f\ \Gamma_{0}\ c = 0\\
+    \text{srun}\ f\ s_{0}\ \mathit{stt},& \text{otherwise}
+  \end{cases}\\
+  \text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ \mathit{def}) &= \begin{cases}
+    \text{srun}\ f\ s_{0}\ sc,& \text{erun}\ f\ \Gamma_{0}\ me = \text{erun}\ f\ \Gamma_{0}\ e\\
+    \text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ cs\ \mathit{def}),& \text{otherwise}
+  \end{cases}\\
+  \text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ []\ (\mathtt{Some}\ st)) &= \text{srun}\ f\ s_{0}\ st\\
+  \text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ []\ \mathtt{None}) &= \mathtt{None}
 \end{align}
 
 \begin{equation}
   \label{eq:1}
-  \inferrule[Skip]{ }{\text{stmntrun}\ f\ s\ \mathtt{Vskip} = s}
+  \inferrule[Skip]{ }{\text{srun}\ f\ s\ \mathtt{Vskip} = s}
 \end{equation}
 
 \begin{equation}
   \label{eq:4}
-  \inferrule[Seq]{\text{stmntrun}\ f\ s_{0}\ \mathit{st}_{1}\ s_{1} \\ \text{stmntrun}\ f\ s_{1}\ \mathit{st}_{2}\ s_{2}}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vseq}\ \mathit{st}_{1}\ \mathit{st}_{2})\ s_{2}}
+  \inferrule[Seq]{\text{srun}\ f\ s_{0}\ \mathit{st}_{1}\ s_{1} \\ \text{srun}\ f\ s_{1}\ \mathit{st}_{2}\ s_{2}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vseq}\ \mathit{st}_{1}\ \mathit{st}_{2})\ s_{2}}
 \end{equation}
 
 \begin{equation}
   \label{eq:2}
-  \inferrule[CondTrue]{\text{exprrun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \text{valToB}\ v_{c} = \mathtt{true} \\ \text{stmntrun}\ f\ s_{0}\ \mathit{stt}\ s_{1}}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf})\ s_{1}}
+  \inferrule[CondTrue]{\text{erun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \text{valToB}\ v_{c} = \mathtt{true} \\ \text{srun}\ f\ s_{0}\ \mathit{stt}\ s_{1}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf})\ s_{1}}
 \end{equation}
 
 \begin{equation}
   \label{eq:3}
-  \inferrule[CondFalse]{\text{exprrun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \text{valToB}\ v_{c} = \mathtt{false} \\ \text{stmntrun}\ f\ s_{0}\ \mathit{stf}\ s_{1}}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf})\ s_{1}}
+  \inferrule[CondFalse]{\text{erun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \text{valToB}\ v_{c} = \mathtt{false} \\ \text{srun}\ f\ s_{0}\ \mathit{stf}\ s_{1}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf})\ s_{1}}
 \end{equation}
 
 \begin{equation}
   \label{eq:5}
-  \inferrule[CaseNoMatch]{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ cs\ def)\ s_{1} \\ \text{exprrun}\ f\ \Gamma_{0}\ me\ mve \\ \text{exprrun}\ f\ \Gamma_{0}\ e\ ve \\ mve \neq ve}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ def)\ s_{1}}
+  \inferrule[CaseNoMatch]{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ cs\ \mathit{def})\ s_{1} \\ \text{erun}\ f\ \Gamma_{0}\ me\ mve \\ \text{erun}\ f\ \Gamma_{0}\ e\ ve \\ mve \neq ve}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ \mathit{def})\ s_{1}}
 \end{equation}
 
 \begin{equation}
   \label{eq:6}
-  \inferrule[CaseMatch]{\text{stmntrun}\ f\ s_{0}\ sc\ s_{1} \\ \text{exprrun}\ f\ \Gamma_{0}\ e\ ve \\ \text{exprrun}\ f\ \Gamma_{0}\ me\ mve \\ mve = ve}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ def)\ s_{1}}
+  \inferrule[CaseMatch]{\text{srun}\ f\ s_{0}\ sc\ s_{1} \\ \text{erun}\ f\ \Gamma_{0}\ e\ ve \\ \text{erun}\ f\ \Gamma_{0}\ me\ mve \\ mve = ve}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ \mathit{def})\ s_{1}}
 \end{equation}
 
 \begin{equation}
   \label{eq:7}
-  \inferrule[CaseDefault]{\text{stmntrun}\ f\ s_{0}\ st\ s_{1}}{\text{stmntrun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ []\ (\mathtt{Some}\ st))\ s_{1}}
+  \inferrule[CaseDefault]{\text{srun}\ f\ s_{0}\ st\ s_{1}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ []\ (\mathtt{Some}\ st))\ s_{1}}
 \end{equation}
 
 \begin{equation}
   \label{eq:8}
-  \inferrule[Blocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{exprrun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{stmntrun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vblock}\ \mathit{lhs}\ \mathit{rhs})\ (\Gamma ! n \rightarrow v_{\mathit{rhs}}, \Delta)}
+  \inferrule[Blocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{erun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{srun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vblock}\ \mathit{lhs}\ \mathit{rhs})\ (\Gamma ! n \rightarrow v_{\mathit{rhs}}, \Delta)}
 \end{equation}
 
 \begin{equation}
   \label{eq:9}
-  \inferrule[Nonblocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{exprrun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{stmntrun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vnonblock}\ \mathit{lhs}\ \mathit{rhs}) = (\Gamma, \Delta ! n \rightarrow v_{\mathit{rhs}})}
+  \inferrule[Nonblocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{erun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{srun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vnonblock}\ \mathit{lhs}\ \mathit{rhs}) = (\Gamma, \Delta ! n \rightarrow v_{\mathit{rhs}})}
 \end{equation}
 
 \section{Proof}