% Chapter Template

% Main chapter title

\chapter{Correctness of Bit-coded Algorithm with Simplification}

\label{Bitcoded2} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX}

%Then we illustrate how the algorithm without bitcodes falls short for such aggressive 

%simplifications and therefore introduce our version of the bitcoded algorithm and 

%its correctness proof in 

%Chapter 3\ref{Chapter3}. 

%----------------------------------------------------------------------------------------

%	SECTION common identities

%----------------------------------------------------------------------------------------

\section{Common Identities In Simplification-Related Functions} 

Need to prove these before starting on the big correctness proof.

%-----------------------------------

%	SUBSECTION 

%-----------------------------------

\subsection{Idempotency of $\simp$}

\begin{equation}

	\simp \;r = \simp\; \simp \; r 

\end{equation}

This property means we do not have to repeatedly

apply simplification in each step, which justifies

our definition of $\blexersimp$.

It will also be useful in future proofs where properties such as 

closed forms are needed.

The proof is by structural induction on $r$.

%-----------------------------------

%	SUBSECTION 

%-----------------------------------

\subsection{Syntactic Equivalence Under $\simp$}

We prove that minor differences can be annhilated

by $\simp$.

For example,

\begin{center}

$\simp \;(\simpALTs\; (\map \;(\_\backslash \; x)\; (\distinct \; \mathit{rs}\; \phi))) = 

 \simp \;(\simpALTs \;(\distinct \;(\map \;(\_ \backslash\; x) \; \mathit{rs}) \; \phi))$

\end{center}

%----------------------------------------------------------------------------------------

%	SECTION corretness proof

%----------------------------------------------------------------------------------------

\section{Proof Technique of Correctness of Bit-coded Algorithm with Simplification}

The non-trivial part of proving the correctness of the algorithm with simplification

compared with not having simplification is that we can no longer use the argument 

in \cref{flex_retrieve}.

The function \retrieve needs the structure of the annotated regular expression to 

agree with the structure of the value, but simplification will always mess with the 

structure:

%TODO: after simp does not agree with each other: (a + 0) --> a v.s. Left(Char(a))