From 73a733bb9f1aaef6c28bfe120361ba87b34455b8 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 5 Jun 2020 19:00:04 +0100 Subject: Add more recursive rules --- main.tex | 34 ++++++++++++++++++++++------------ 1 file changed, 22 insertions(+), 12 deletions(-) (limited to 'main.tex') 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} -- cgit