%include thesis.fmt
%include catch.fmt

%format /# = "/"
%format === = =
%format lhs = "\mathrm{LHS}"
%format rhs = "\mathrm{RHS}"

\newcommand{\eq}{$\equiv$ \{}
\newcommand{\im}{$\Leftarrow$ \{}

% the lemmas
\newcommand{\lemSat}{C1}
\newcommand{\lemSatTri}{C2}
\newcommand{\lemMPAny}{MP1}
\newcommand{\lemMPMerge}{MP2}
\newcommand{\lemElem}{A1}
\newcommand{\lemSatE}{A2}
\newcommand{\lemPrecondError}{A3}
\newcommand{\lemPrecond}{A4}
\newcommand{\lemPrePost}{A5}
\newcommand{\lemPre}{A6}
\newcommand{\lemRed}{A7}
\newcommand{\lemReduce}{A8}

\newcommand{\define}[1]{\subsection*{Lemma #1}}
\newcommand{\case}[1]{\paragraph{Case:} #1 \smallskip}
\newcommand{\csp}{\hspace{2mm}\textbf{;} \hspace{2mm}}
\newcommand{\lemma}[1]{Lemma #1}
\newcommand{\lemmap}{Soundness Theorem}


\hsdef{\begin{comment}
k,f,c,v,i,on,xs_i,x,ys_i,s,a,ws,c',ms_1,ms_2,e,h
vs,xs,y,as,ys,cs,rhs,lhs,g,f_lhd,f_rhd,ks
\end{comment}}
\begin{comment}
\h{.*}\begin{code}
import Prelude hiding (($),(/))
import Data.List

infixr 1  $
infix 0  ==>
infix 0  ===
($) :: (a -> b) -> a -> b
class Implies a where (==>) :: a -> a -> Bool
(===) :: a -> a -> ()

instance Implies Bool
instance Implies (Prop a)

type FuncName = String
type CtorName = String
type VarName = String

freeVars :: Expr -> [String]
body   :: FuncName  -> Expr
args   :: FuncName  -> [VarName]
var    :: VarName   -> Maybe (Expr, Selector)
ctors  :: CtorName  -> [CtorName]
arity :: String -> Int
type Selector  =  (CtorName, Int)
isRec :: Selector -> Bool

precond   :: FuncName -> Prop (Sat VarName)
prePost   :: FuncName -> Constraint -> Prop (Sat VarName)
pre ::  Expr -> Prop (Sat Expr)
reduce    :: Prop (Sat Expr) -> Prop (Sat VarName)
red :: Expr -> Constraint -> Prop (Sat VarName)
substP :: Eq alpha => [(alpha,beta)] -> Prop (Sat alpha) -> Prop (Sat beta)

data Sat alpha = Sat alpha Constraint
instance Eq a => Eq (Sat a)

(-<)  :: alpha -> [CtorName] -> Prop (Sat alpha)
(|>)  :: Selector -> Constraint -> Constraint
(<|)  :: CtorName -> Constraint -> Prop (Sat Int)

data Prop alpha
instance Eq a => Eq (Prop a)

propAnd, propOr           :: Prop alpha -> Prop alpha -> Prop alpha
propAnds, propOrs         :: [Prop alpha] -> Prop alpha
propMap                   :: (alpha -> Prop beta) -> Prop alpha -> Prop beta
propTrue, propFalse       :: Prop alpha
propBool                  :: Bool -> Prop alpha
propLit                   :: alpha -> Prop alpha
propIsTrue :: Prop () -> Bool
propTaut :: (alpha -> Bool) -> Prop alpha -> Bool


-- variable substitution, replacing free variables
class SubstVar a where (/) :: a -> ([VarName],[Expr]) -> a
instance SubstVar Expr
instance SubstVar Alt
instance SubstVar a => SubstVar [a]
instance SubstVar a => SubstVar (Sat a)
instance SubstVar a => SubstVar (Prop a)

-- equality substitution, replacing items
class SubstRep a b c | a c -> b, c b -> a, a b -> c where (/#) :: a -> b -> c
instance SubstRep (Prop (Sat a)) ([a], [b]) (Prop (Sat b))
instance SubstRep VarName ([VarName], [Expr]) Expr

instance Eq Value
instance Eq Expr

alt :: Alt -> Prop (Sat a)
pre' :: String -> [Expr] -> Prop (Sat Expr)
sub :: ([VarName],[Expr])
\end{code}

\begin{code}
-- for BP
anys :: String -> Constraint
instance Eq Constraint
\end{code}

\h{.mp}\begin{code}
-- for MP
type Constraint = [Val]
data Val = [Pattern] :* [Pattern] | Any deriving Eq
data Pattern = Pattern CtorName [Val] deriving Eq
complete :: CtorName -> Pattern
nonRecs :: CtorName -> [Int]
merge :: [Pattern] -> [Pattern] -> [Pattern]
non :: [Int]
rec :: [Int]
\end{code}
\end{comment}


\chapter{Soundness of Pattern-Match Analysis}
\label{chp:proof}

This appendix shows that the algorithms and constraint languages presented in Chapter \ref{chp:catch} are sound -- if Catch informs the user that a program is safe, then that program is guaranteed not to call |error|. \S\ref{secP:style} describes the style of proof and \S\ref{secP:evaluator} defines an evaluator for expressions. \S\ref{secP:theorem} states the soundness theorem, along with necessary side conditions. \S\ref{secP:constraint} gives two lemmas that constraint languages must satisfy, and shows they hold for BP-constraints and MP-constraints. \S\ref{secP:general_lemmas} gives eight lemmas, mainly about the constraint operations. \S\ref{secP:proof} gives the proof of soundness and \S\ref{secP:summary} discusses the results.


\section{Proof-Style and Notation}
\label{secP:style}

Proofs in this appendix are detailed outlines based on equational reasoning. They make use of induction, application of equational laws, case analysis and inlining of function definitions. When performing case analysis we ignore the possibility of $\bot{}$ as a Haskell value, which is valid provided all expressions within the proof do not result in $\bot{}$. The proofs are structured as a series of rewrites, either preserving equality (marked with $\equiv$), or implying the previous statement (marked with $\Leftarrow$). Some expressions may refer to locally bound definitions, which we do not show until necessary. All the properties are boolean valued expressions, typically implications.

In order to reduce the size of some of the intermediate expressions, we have replaced one side of an implication with either |lhs| or |rhs|, designating either the left-hand side or right-hand side. We also make heavy use of the function composition and function application operators, namely |(.)| and |($)|. These can be read with the translations:

\ignore\begin{code}
(f . g) x  = f $ g x = f (g x)
\end{code}


\section{Evaluator}
\label{secP:evaluator}

\begin{figure}
\ind{Value}\ind{Bottom}\ind{Expr}\ind{Make}\ind{Call}\ind{Var}\ind{Sel}\ind{Case}\ind{Alt}\ind{eval}
\h{.*}\begin{code}
data Value  =  Value CtorName [Value]
            |  Bottom

data Expr  =  Make CtorName [Expr]  -- Constructor application
           |  Call FuncName [Expr]  -- Function application
           |  Var  VarName          -- Function variable
           |  Sel  Expr Selector    -- Case alternative variable
           |  Case Expr [Alt]       -- Case expression

data Alt = Alt CtorName [VarName] Expr

eval :: Expr -> Value
eval (Sel x (c,i)  )  |  c == c' = xs !! i
    where Value c' xs = eval x
eval (Make c  xs   )  =  Value c (map eval xs)
eval (Call f  xs   )  |  f == "error"  = Bottom
                      |  otherwise     = eval $ body f / (args f, xs)
eval (Case x as    )  =  case eval x of
    Value c xs -> head [eval y | Alt c' vs y <- as, c == c']
    Bottom -> Bottom
\end{code}
\caption{Evaluator for expressions.}
\label{figP:eval}
\end{figure}

We start with an evaluator for a Core expression language defined in Figure \ref{figP:eval}. The value |Bottom| corresponds to program failure, \textit{not} divergence. The |Expr| data type represents the first-order Core language described in \S\ref{secC:catch_core}. We have introduced |Sel|, which represents variables bound in case alternatives. For the algorithms presented previously, the |Sel| expression contains the information returned by the |var| function. While evaluating a |Sel| expression we know that we are beneath a |Case| on the same expression |x|, and that |x| evaluates to the constructor mentioned in the selector. The |Alt| constructor has a list of variables which are unnecessary because selectors are used instead of local variable names -- but they are retained to allow direct use of the algorithms from Chapter \ref{chp:catch}.

There is no case in |eval| for |Var|, and the behaviour of |eval| with free variables is undefined. The |Call| equation will replace any free variables in the body of a function with the supplied arguments.

We make use of |(/)|, which we have redefined as a substitution operator -- we write |x / (vs,ys)| to denote replacing the free variables |vs| in |x| with |ys|. We use |(/)| instead of |substP| in the proofs, where |substP (zip vs ys) x === x /# (vs,ys)|.

\begin{figure}
\ind{isBottom}\ind{valCtor}\ind{satE'}\ind{satE}\ind{sat'}\ind{sat}
\h{.*}\begin{code}
isBottom :: Value -> Bool
isBottom Bottom = True
isBottom (Value c xs) = any isBottom xs

valCtor :: Value -> Maybe CtorName
valCtor (Value c xs) = Just c
valCtor Bottom = Nothing

satE' :: Prop (Sat Expr) -> Bool
satE' = propTaut satE

satE :: Sat Expr -> Bool
satE (Sat x k) = sat (Sat (eval x) k)

sat' :: Prop (Sat Value) -> Bool
sat' = propTaut sat

sat :: Sat Value -> Bool
sat (Sat Bottom        k) = True
sat (Sat (Value c xs)  k) = sat' $ (c <| k) /# ([0..],xs)
\end{code}
\caption{Auxiliary functions.}
\label{figP:auxiliary}
\end{figure}

We also make use of a number of auxiliaries defined in Figure \ref{figP:auxiliary}. The |sat| function tests whether a value satisfies a constraint, using the |(<||)| operator from the constraint language. The |satE| function tests whether the result of evaluating an expression satisfies a constraint. The |sat'| and |satE'| functions operate over a proposition.

\section{Soundness Theorem}
\label{secP:theorem}

We wish to prove that our analysis is sound, as previously discussed in \S\ref{secC:soundness}. Our analysis is sound if for any expression |e|, provided the precondition of |e| is calculated to be true, then the evaluation of |e| will not result in $\bot{}$. Using the definitions from \S\ref{secP:evaluator} we can express this theorem as:

\h{expr}\begin{code}
satE' $ pre e ==> not $ isBottom $ eval e
\end{code}

In order to evaluate an expression to normal form, it is necessary for the expression to be closed and for evaluation of the expression to terminate. Therefore we prove that provided the expression |e| can be evaluated to normal form, and that both |e| and the program under analysis are first-order Core as described in \S\ref{secC:catch_core}, the above theorem is true. The above restrictions allow us to assume that all constructors have the correct arity, and that there are no free variables. We will prove this result in \ref{secP:proof}.

%subst comment a = "\hspace{-5mm}\mbox{\textit{" a "\}}}"

\section{Constraint Lemmas}
\label{secP:constraint}

We shall need the following two lemmas about each constraint language:

\define{\lemSat}

\h{expr}\begin{code}
sat' (Value c xs -< cs) ==> c `elem` cs
\end{code}

\define{\lemSatTri}

\h{expr}\begin{code}
sat $ Sat (Value c xs) ((c,i) |> k) ==> sat $ Sat (xs !! i) k
\end{code}

Both lemmas are given in \S\ref{secC:constraint_semantics}, as properties. These properties require the |(-<)| and |(||>)| operators to be consistent with |sat|. The |sat| function is defined in terms of |(<||)|, and therefore all three operators must be consistent with each other. We prove them for the BP-constraint and MP-constraint systems in \S\ref{secP:bp} and \S\ref{secP:mp}. Since RE-constraints do not scale sufficiently, we do not recommend their use, and have not attempted to prove these lemmas for them.

\subsection{BP-Constraint Lemmas}
\label{secP:bp}

\begin{figure}
\begin{code}
data Constraint  =  Any
                 |  Con CtorName [Constraint]

a -< xs = propOrs [propLit (a `Sat` anys x) | x <- xs]
    where anys x = Con x (replicate (arity x) Any)

(c,i) |> k = Con c  [  if i == j then k else Any
                    |  j <- [0..arity c - 1]]

c <| Any         =  propTrue
c <| Con c_2 xs  =  propBool (c_2 == c) `propAnd` propAnds (map propLit (zipWith Sat [0..] xs))
\end{code}
\caption{BP-Constraint operations.}
\label{figP:bp}
\end{figure}

Since BP-constraints are presented piecemeal throughout \S\ref{secC:manipulate}, we present all the relevant definitions in Figure \ref{figP:bp}.

\define{\lemSat\ (BP)}

\h{exprlist}\begin{code}
sat' (Value c xs -< cs) ==> c `elem` cs
    -- \eq inline |(-<)|
sat' $ propOrs [propLit (Value c xs `Sat` anys c') | c' <- cs] ==> c `elem` cs
    -- \eq inline |sat'|
any (\c' -> sat $ Value c xs `Sat` anys c') cs ==> c `elem` cs
    -- \eq inline |sat|
any (\c' -> sat' $ (c <| anys c') /# ([0..],xs)) cs ==> c `elem` cs
    -- \eq inline |anys|
any (\c' -> sat' $ (c <| Con c' (replicate (arity c') Any)) /#
    ([0..],xs)) cs ==> c `elem` cs
    -- \eq inline | <|| |
any (\c' -> sat' $ (propBool (c' == c) `propAnd`
    propAnds (map propLit (zipWith Sat [0..] (replicate (arity c') Any))))
    /# ([0..],xs)) cs ==> c `elem` cs
    -- \eq inline |(/)|
any (\c' -> sat' $ (propBool (c' == c) `propAnd`
    propAnds (map propLit (zipWith Sat [0..] (replicate (arity c') Any)
    /# ([0..],xs))))) cs ==> c `elem` cs
    -- \eq inline |sat'|
any (\c' -> (c' == c) && all sat (zipWith Sat [0..] (replicate (arity c') Any)
    /# ([0..],xs))) cs ==> c `elem` cs
    -- \im weaken implication
any (\c' -> c' == c) cs ==> c `elem` cs
    -- \eq simplify
any (== c) cs ==> c `elem` cs
    -- \eq definition of |elem|
c `elem` cs ==> c `elem` cs
    -- \eq tautology
True
\end{code}

\define{\lemSatTri\ (BP)}

\h{expr}\begin{code}
sat $ Sat (Value c xs) ((c,i) |> k) ==> sat $ Sat (xs !! i) k
\end{code}

\case{|k === Any|}

\h{exprlist}\begin{code}
sat $ Sat (Value c xs) ((c,i) |> k) ==> sat $ Sat (xs !! i) k
    -- \eq |k === Any|
sat $ Sat (Value c xs) ((c,i) |> Any) ==> sat $ Sat (xs !! i) Any
    -- \eq inline |sat| on RHS
sat $ Sat (Value c xs) ((c,i) |> Any) ==> sat $ Sat (xs !! i) Any
\end{code}

\case{|k === Any| \csp |xs !! i === Bottom|}

\h{exprlist}\begin{code}
sat $ Sat (Value c xs) ((c,i) |> Any) ==> sat $ Sat (xs !! i) Any
    -- \eq |xs !! i === Bottom|
sat $ Sat (Value c xs) ((c,i) |> Any) ==> sat $ Sat Bottom Any
    -- \eq inline |sat| on RHS
sat $ Sat (Value c xs) ((c,i) |> Any) ==> True
    -- \eq implication
True
\end{code}

\case{|k === Any| \csp |xs !! i === Value c' ys|}

\h{exprlist}\begin{code}
sat $ Sat (Value c xs) ((c,i) |> Any) ==> sat $ Sat (xs !! i) Any
    -- \eq |xs !! i === Value c' ys|
sat $ Sat (Value c xs) ((c,i) |> Any) ==> sat $ Sat (Value c' ys) Any
    -- \eq inline |sat| on RHS
sat $ Sat (Value c xs) ((c,i) |> Any) ==> sat' $ (c' <| Any) /# ([0..],ys)
    -- \eq inline | <|| |
sat $ Sat (Value c xs) ((c,i) |> Any) ==> sat' $ propTrue /# ([0..],ys)
    -- \eq inline |(/)| on RHS
sat $ Sat (Value c xs) ((c,i) |> Any) ==> sat' propTrue
    -- \eq inline |sat'| on RHS
sat $ Sat (Value c xs) ((c,i) |> Any) ==> True
    -- \eq implication
True
\end{code}

\case{|k === Con c' ys|}

\h{exprlist}\begin{code}
sat $ Sat (Value c xs) ((c,i) |> k) ==> sat $ Sat (xs !! i) k
    -- \eq |k === Con c' ys|
sat $ Sat (Value c xs) ((c,i) |> Con c' ys) ==> sat $ Sat (xs !! i) (Con c' ys)
    -- \eq inline |sat| on LHS
sat' $ (c <| ((c,i) |> Con c' ys)) /# ([0..],xs) ==> rhs
    -- \eq inline | ||> |
sat' $ (c <| (Con c [if i == j then (Con c' ys) else Any | j <- [0..arity c - 1]]))
    /# ([0..],xs) ==> rhs
    -- \eq inline | <|| |
sat' $ (propBool (c == c) `propAnd` propAnds (map propLit (zipWith Sat [0..]
    [if i == j then (Con c' ys) else Any | j <- [0..arity c - 1]])))
    /# ([0..],xs) ==> rhs
    -- \eq inline |c == c|
sat' $ (propTrue `propAnd` propAnds (map propLit (zipWith Sat [0..]
    [if i == j then (Con c' ys) else Any | j <- [0..arity c - 1]])))
    /# ([0..],xs) ==> rhs
    -- \eq inline |propAnd|
sat' $ (propAnds (map propLit (zipWith Sat [0..]
    [if i == j then (Con c' ys) else Any | j <- [0..arity c - 1]])))
    /# ([0..],xs) ==> rhs
    -- \eq inline |(/)|
sat' $ propAnds $ map propLit $ zipWith Sat [0..]
    [if i == j then (Con c' ys) else Any | j <- [0..arity c - 1]]
    /# ([0..],xs) ==> rhs
    -- \eq inline |sat'|
all sat $ zipWith Sat [0..]
    [if i == j then (Con c' ys) else Any | j <- [0..arity c - 1]]
    /# ([0..],xs) ==> rhs
    -- \eq inline |(/)|
all sat $ zipWith Sat xs
    [if i == j then (Con c' ys) else Any | j <- [0..arity c - 1]] ==> rhs
    -- \im weaken LHS
sat $ zipWith Sat xs
    [if i == j then (Con c' ys) else Any | j <- [0..arity c - 1]] !! i ==> rhs
    -- \eq inline |(!!)|
sat $ Sat (xs !! i) (Con c' ys) ==> rhs
    -- \eq restore RHS
sat $ Sat (xs !! i) (Con c' ys) ==> sat $ Sat (xs !! i) (Con c' ys)
    -- \eq tautology
True
\end{code}


\subsection{MP-Constraint Lemmas}
\label{secP:mp}

The proofs in this section appeal to definitions in Figure \ref{figC:enumeration}. To perform some of these proofs, we will rely on two auxiliary lemmas about MP-constraints.

\define{\lemMPAny}

\h{.mp expr}\begin{code}
sat (Sat (Value c xs) ks) == any (\k -> sat $ Sat (Value c xs) [k]) ks
\end{code}

We argue as follows:

\h{.mp exprlist}\begin{code}
sat (Sat (Value c xs) ks) == any (\k -> sat $ Sat (Value c xs) [k]) ks
    -- \eq inline |sat|
sat' ((c <| ks) /# ([0..],xs)) == rhs
    -- \eq inline | <|| |
sat' (propOrs (map f ks) /# ([0..],xs)) == rhs
    -- \eq inline |(/)|
sat' (propOrs (map f ks /# ([0..],xs))) == rhs
    -- \eq inline |sat'|
any sat' (map f ks /# ([0..],xs)) == rhs
    -- \eq inline |(/)|
any sat' (map ((/# ([0..],xs)) . f) ks) == rhs
    -- \eq combine |any| and |map|
any (sat' . (/# ([0..],xs)) . f) ks == rhs
    -- \eq insert |k|
any (\k -> sat' $ f k /# ([0..],xs)) ks == rhs
    -- \eq insert RHS
any (\k -> sat' $ f k /# ([0..],xs)) ks == any (\k -> sat $ Sat (Value c xs) [k]) ks
    -- \eq unwrap common parts
sat' (f k /# ([0..],xs)) == sat (Sat (Value c xs) [k])
    -- \eq inline |sat|
lhs == sat' ((c <| [k]) /# ([0..],xs))
    -- \eq inline | <|| |
lhs == sat' (propOrs (map f [k]) /# ([0..],xs))
    -- \eq inline |map|
lhs == sat' (propOrs [f k] /# ([0..],xs))
    -- \eq inline |propOrs|
sat' (f k /# ([0..],xs)) == sat' (f k /# ([0..],xs))
    -- \eq tautology
True
\end{code}

\define{\lemMPMerge}

\h{.mp expr}\begin{code}
sat $ Sat (Value c xs) [merge ms_1 ms_2 :* merge ms_1 ms_2] ==>
    sat $ Sat (Value c xs) [ms_1 :* ms_2]
\end{code}

We have \textit{not} proved this lemma, as we suspect the proof is very long. Instead we have used Lazy SmallCheck \cite{lazysmallcheck} to test the property. Lazy SmallCheck exhaustively tests properties up to some depth of input values. Here is the property we have tested, along with the invariants on values:

\h{.mp}\begin{code}
prop :: (Value, [Pattern], [Pattern]) -> Bool
prop (v,ms1,ms2) =
        validValue v && validPatterns ms1 && validPatterns ms2 &&
        sat (Sat v [ms :* ms]) ==> sat (Sat v [ms1 :* ms2])
    where ms = merge ms1 ms2

validValue Bottom        = True
validValue (Value c xs)  = arity c == length xs && all validValue xs

validVal Any           = True
validVal (ms1 :* ms2)  = validPatterns ms1 && validPatterns ms2

validPatterns = all validPattern
validPattern (Pattern c xs) = fields c == length xs && all validVal xs

fields c = length [isRec (c,i) | i <- [0..arity c - 1]]
\end{code}

We check that values and patterns are well-formed using |validValue| and |validPatterns|. These functions both check that the arity of constructors are correct, and that patterns have an appropriate number of non-recursive fields. We have defined depth so that the length-constrained list structure present in both values and patterns \textit{does not} count towards the depth of a structure. For example, the following is a |Value| structure of depth 3:

\h{expr}\begin{code}
Value "(,)"
    [Value ":"
        [Value "True" []
        ,Value "[]" []]
    ,Value "Nothing" []]
\end{code}

Testing all values and patterns up to depth 4 (446,105,404 tests) no counter-example is found. These tests represent 692,363,920,494,602 possible inputs. We do not believe it is feasible to test this property at a greater depth, but depth 4 gives us reasonable confidence that the property is indeed true.


\define{\lemSat\ (MP)}

\h{.mp exprlist}\begin{code}
sat' (Value c xs -< cs) ==> c `elem` cs
    -- \eq inline |(-<)|
sat' $ propLit $ Sat (Value c xs)
    [map complete cs :* map complete (ctors (head cs)) | not (null cs)] ==> c `elem` cs
\end{code}

\case{|cs === []|}

\h{.mp exprlist}\begin{code}
sat' $ propLit $ Sat (Value c xs)
    [map complete cs :* map complete (ctors (head cs)) | not (null cs)] ==> c `elem` cs
    -- \eq |cs === []|
sat' $ propLit $ Sat (Value c xs)
    [map complete [] :* map complete (ctors (head [])) | not (null [])] ==> c `elem` []
    -- \eq inline |null|
sat' $ propLit $ Sat (Value c xs)
    [map complete [] :* map complete (ctors (head [])) | not True] ==> c `elem` []
    -- \eq inline |not|
sat' $ propLit $ Sat (Value c xs)
    [map complete [] :* map complete (ctors (head [])) | False] ==> c `elem` []
    -- \eq reduce list comprehension
sat' $ propLit $ Sat (Value c xs) [] ==> c `elem` []
    -- \eq inline |elem|
sat' $ propLit $ Sat (Value c xs) [] ==> False
    -- \eq inline |sat'|
sat $ Sat (Value c xs) [] ==> False
    -- \eq \lemma{\lemMPAny}
any (\k -> sat $ Sat (Value c xs) [k]) [] ==> False
    -- \eq inline |any|
False ==> False
    -- \eq tautology
True
\end{code}

\case{|cs /= []|}

\h{.mp exprlist}\begin{code}
sat' $ propLit $ Sat (Value c xs)
    [map complete cs :* map complete (ctors (head cs)) | not (null cs)] ==> c `elem` cs
    -- \eq |null cs == False|
sat' $ propLit $ Sat (Value c xs)
    [map complete cs :* map complete (ctors (head cs)) | not False] ==> c `elem` cs
    -- \eq inline |not|
sat' $ propLit $ Sat (Value c xs)
    [map complete cs :* map complete (ctors (head cs)) | True] ==> c `elem` cs
    -- \eq simplify list comprehension
sat' $ propLit $ Sat (Value c xs)
    [map complete cs :* map complete (ctors (head cs))] ==> c `elem` cs
    -- \eq inline |sat'|
sat $ Sat (Value c xs)
    [map complete cs :* map complete (ctors (head cs))] ==> c `elem` cs
    -- \eq inline |sat|
sat' $ (c <| [map complete cs :* map complete (ctors (head cs))])
    /# ([0..],xs) ==> c `elem` cs
    -- \eq inline | <|| |
sat' $ (propOrs $ map f [map complete cs :* map complete (ctors (head cs))])
    /# ([0..],xs) ==> c `elem` cs
    -- \eq inline |map|
sat' $ (propOrs [f $ map complete cs :* map complete (ctors (head cs))])
    /# ([0..],xs) ==> c `elem` cs
    -- \eq inline |propOr|
sat' $ (f $ map complete cs :* map complete (ctors (head cs)))
    /# ([0..],xs) ==> c `elem` cs
    -- \eq inline |f|
sat' $ propOrs [propAnds $ map propLit $ g vs_1 | Pattern c_1 vs_1 <- map complete cs, c_1 == c]
    /# ([0..],xs) ==> c `elem` cs
    -- \eq inline |(/)|
sat' $ propOrs [propAnds $ map propLit $ g vs_1 /# ([0..],xs) |
    Pattern c_1 vs_1 <- map complete cs, c_1 == c] ==> c `elem` cs
    -- \eq inline |sat'|
or [sat' $ propAnds $ map propLit $ g vs_1 /# ([0..],xs) |
    Pattern c_1 vs_1 <- map complete cs, c_1 == c] ==> c `elem` cs
    -- \eq move the guard
or [c_1 == c && sat' (propAnds $ map propLit $ g vs_1 /# ([0..],xs)) |
    Pattern c_1 vs_1 <- map complete cs] ==> c `elem` cs
    -- \eq remove the list comprehension
any (\(Pattern c_1 vs_1) -> c_1 == c &&
    sat' (propAnds $ map propLit $ g vs_1 /# ([0..],xs))) (map complete cs) ==> c `elem` cs
    -- \eq |any f (map g xs) === any (f . g) xs|
any ((\(Pattern c_1 vs_1) -> c_1 == c &&
    sat' (propAnds $ map propLit $ g vs_1 /# ([0..],xs))) . complete) cs ==> c `elem` cs
    -- \eq |c `elem` cs === any (== c) cs|
any ((\(Pattern c_1 vs_1) -> c_1 == c &&
    sat' (propAnds $ map propLit $ g vs_1 /# ([0..],xs))) . complete) cs ==> any (== c) cs
    -- \im lift implication over |any|
(\(Pattern c_1 vs_1) -> c_1 == c &&
    sat' (propAnds $ map propLit $ g vs_1 /# ([0..],xs))) (complete c') ==> c' == c
    -- \eq inline |complete|
c' == c && sat' (propAnds $ map propLit $ g (map (const Any) (nonRecs c'))
    /# ([0..],xs)) ==> c' == c
    -- \im weaken implication
c' == c ==> c' == c
    -- \eq tautology
True
\end{code}

\define{\lemSatTri\ (MP)}

As |f| is a local function definition of both | <|| | and | ||> |, we use |f_lhd| and |f_rhd| to indicate which |f| we are referring to.

\h{.mp exprlist}\begin{code}
sat $ Sat (Value c xs) ((c,i) |> k) ==> sat $ Sat (xs !! i) k
    -- \eq inline | ||> |
sat $ Sat (Value c xs) (map f k) ==> sat $ Sat (xs !! i) k
    -- \eq inline |sat|
sat' $ (c <| map f_rhd k) /# ([0..],xs) ==> sat $ Sat (xs !! i) k
    -- \eq inline | <|| |
sat' $ propOrs (map f_lhd (map f_rhd k)) /# ([0..],xs) ==> sat $ Sat (xs !! i) k
    -- \eq |map f . map g === map (f . g)|
sat' $ propOrs (map (f_lhd . f_rhd) k) /# ([0..],xs) ==> sat $ Sat (xs !! i) k
\end{code}

We now proceed by induction over |k|. We assume |k| may take the values |[]|, |Any:ks| and \h{.mp}|(ms_1 :* ms_2):ks|.

\case{|k === []|}

\h{.mp exprlist}\begin{code}
sat' $ propOrs (map (f_lhd . f_rhd) k) /# ([0..],xs) ==> sat $ Sat (xs !! i) k
    -- \eq |k === []|
sat' $ propOrs (map (f_lhd . f_rhd) []) /# ([0..],xs) ==> sat $ Sat (xs !! i) []
    -- \eq inline |map|
sat' $ propOrs [] /# ([0..],xs) ==> sat $ Sat (xs !! i) []
    -- \eq inline |propOrs|
sat' $ propFalse /# ([0..],xs) ==> sat $ Sat (xs !! i) []
    -- \eq inline |(/)|
sat' propFalse ==> sat $ Sat (xs !! i) []
    -- \eq inline |sat'|
False ==> sat $ Sat (xs !! i) []
    -- \eq implication
True
\end{code}

\case{|k === Any:ks|}

\h{.mp exprlist}\begin{code}
sat' $ propOrs (map (f_lhd . f_rhd) k) /# ([0..],xs) ==> sat $ Sat (xs !! i) k
    -- \eq |k === Any:ks|
sat' $ propOrs (map (f_lhd . f_rhd) (Any:ks)) /# ([0..],xs) ==> sat $ Sat (xs !! i) (Any:ks)
    -- \im weaken implication
sat $ Sat (xs !! i) (Any:ks)
\end{code}

\case{|k === Any:ks| \csp |xs !! i === Bottom|}

\h{.mp exprlist}\begin{code}
sat $ Sat (xs !! i) (Any:ks)
    -- \eq |xs !! i === Bottom|
sat $ Sat Bottom (Any:ks)
    -- \eq inline |sat|
True
\end{code}

\case{|k === Any:ks| \csp |xs !! i === Value c' ys|}

\h{.mp exprlist}\begin{code}
sat $ Sat (xs !! i) (Any:ks)
    -- \eq |xs !! i === Value c' ys|
sat $ Sat (Value c ys) (Any:ks)
    -- \eq inline |sat|
sat' $ (c' <| (Any:ks)) /# ([0..],ys)
    -- \eq inline | <|| |
sat' $ propOrs (map f (Any:ks)) /# ([0..],ys)
    -- \eq inline |map f|
sat' $ propOrs (propTrue : map f ks) /# ([0..],ys)
    -- \eq inline |propOrs|
sat' $ propTrue /# ([0..],ys)
    -- \eq inline |(/)|
sat' propTrue
    -- \eq inline |sat'|
True
\end{code}

\case{\h{.mp}|k === (ms_1 :* ms_2):ks|}

\h{.mp exprlist}\begin{code}
sat' $ propOrs (map (f_lhd . f_rhd) k) /# ([0..],xs) ==> sat $ Sat (xs !! i) k
    -- \eq \h{.mp}|k === (ms_1 :* ms_2):ks|
sat' $ propOrs (map (f_lhd . f_rhd) ((ms_1 :* ms_2):ks)) /# ([0..],xs) ==>
    sat $ Sat (xs !! i) ((ms_1 :* ms_2):ks)
    -- \eq inline |map|
sat' $ propOrs ((f_lhd $ f_rhd $ ms_1 :* ms_2) : map (f_lhd . f_rhd) ks) /# ([0..],xs) ==> rhs
    -- \eq inline |(/)|
sat' $ propOrs (((f_lhd $ f_rhd $ ms_1 :* ms_2) /# ([0..],xs)) :
    (map (f_lhd . f_rhd) ks /# ([0..],xs))) ==> rhs
    -- \eq inline |propOrs|
sat' $ ((f_lhd $ f_rhd $ ms_1 :* ms_2) /# ([0..],xs)) `propOr`
    propOrs (map (f_lhd . f_rhd) ks /# ([0..],xs)) ==> rhs
    -- \eq inline |sat'|
sat' ((f_lhd $ f_rhd $ ms_1 :* ms_2) /# ([0..],xs)) ||
    sat' (propOrs (map (f_lhd . f_rhd) ks /# ([0..],xs))) ==> rhs
    -- \eq reinstate RHS
sat' ((f_lhd $ f_rhd $ ms_1 :* ms_2) /# ([0..],xs)) ||
    sat' (propOrs (map (f_lhd . f_rhd) ks /# ([0..],xs))) ==>
    sat $ Sat (xs !! i) ((ms_1 :* ms_2):ks)
\end{code}

\case{\h{.mp}|k === (ms_1 :* ms_2):ks| \csp |xs !! i === Bottom|}

\h{.mp exprlist}\begin{code}
sat' ((f_lhd $ f_rhd $ ms_1 :* ms_2) /# ([0..],xs)) ||
    sat' (propOrs (map (f_lhd . f_rhd) ks /# ([0..],xs))) ==>
    sat $ Sat (xs !! i) ((ms_1 :* ms_2):ks)
    -- \im weaken implication
sat $ Sat (xs !! i) ((ms_1 :* ms_2):ks)
    -- \eq |xs !! i === Bottom|
sat $ Sat Bottom ((ms_1 :* ms_2):ks)
    -- \eq inline |sat|
True
\end{code}

\case{\h{.mp}|k === (ms_1 :* ms_2):ks| \csp |xs !! i === Value c' ys|}

\h{.mp exprlist}\begin{code}
sat' ((f_lhd $ f_rhd $ ms_1 :* ms_2) /# ([0..],xs)) ||
    sat' (propOrs (map (f_lhd . f_rhd) ks /# ([0..],xs))) ==>
    sat $ Sat (xs !! i) ((ms_1 :* ms_2):ks)
    -- \eq |xs !! i === Value c' ys|
lhs ==> sat $ Sat (Value c' ys) ((ms_1 :* ms_2):ks)
    -- \eq \lemma{\lemMPAny}
lhs ==> any (\k -> sat $ Sat (Value c' ys) [k]) ((ms_1 :* ms_2):ks)
    -- \eq inline |any|
lhs ==> sat (Sat (Value c' ys) [ms_1 :* ms_2]) ||
    any (\k -> sat $ Sat (Value c' xs) [k]) ks
    -- \eq \lemma{\lemMPAny}
lhs ==> sat (Sat (Value c' ys) [ms_1 :* ms_2]) || sat (Sat (Value c' ys) ks)
    -- \eq reinstate LHS
sat' ((f_lhd $ f_rhd $ ms_1 :* ms_2) /# ([0..],xs)) ||
    sat' (propOrs (map (f_lhd . f_rhd) ks /# ([0..],xs))) ==>
    sat (Sat (Value c ys) [ms_1 :* ms_2]) || sat (Sat (Value c' ys) ks)
    -- \im split the implication
(sat' ((f_lhd $ f_rhd $ ms_1 :* ms_2) /# ([0..],xs)) ==>
    sat (Sat (Value c' ys) [ms_1 :* ms_2])) &&
    (sat' (propOrs (map (f_lhd . f_rhd) ks /# ([0..],xs))) ==> sat (Sat (Value c' ys) ks))
    -- \eq |xs !! i === Value c' ys|
(sat' ((f_lhd $ f_rhd $ ms_1 :* ms_2) /# ([0..],xs)) ==> sat (Sat (xs !! i) [ms_1 :* ms_2])) &&
    (sat' (propOrs (map (f_lhd . f_rhd) ks /# ([0..],xs))) ==> sat (Sat (xs !! i) ks))
    -- \eq inductive hypothesis
sat' $ (f_lhd $ f_rhd $ ms_1 :* ms_2) /# ([0..],xs) ==>
    sat $ Sat (xs !! i) [ms_1 :* ms_2]
\end{code}

\case{\h{.mp}|k === (ms_1 :* ms_2):ks| \csp |xs !! i === Value c' ys| \csp |isRec (c,i) === False|}

\h{.mp exprlist}\begin{code}
sat' $ (f_lhd $ f_rhd $ ms_1 :* ms_2) /# ([0..],xs) ==> sat $ Sat (xs !! i) [ms_1 :* ms_2]
    -- \eq inline |f_rhd|, assuming |isRec (c,i) === False|
sat' $ (f_lhd $ [Pattern c [if i == j then ms_1 :* ms_2 else Any | j <- nonRecs c]] :*
    map complete (ctors c)) /# ([0..],xs) ==> lhs
    -- \eq inline |f_lhd|
sat' $ propOrs [propAnds $ map propLit $ g vs_1 | Pattern c_1 vs_1 <-
    [Pattern c [if i == j then ms_1 :* ms_2 else Any | j <- nonRecs c]],
     c_1 == c] /# ([0..],xs) ==> lhs
    -- \eq simplify list comprehension
sat' $ propOrs [propAnds $ map propLit $ g
    [if i == j then ms_1 :* ms_2 else Any | j <- nonRecs c]]
    /# ([0..],xs) ==> lhs
    -- \eq inline |propOrs|
sat' $ (propAnds $ map propLit $ g
    [if i == j then ms_1 :* ms_2 else Any | j <- nonRecs c])
    /# ([0..],xs) ==> lhs
    -- \eq inline |(/)|
sat' $ propAnds $ map propLit $ g
    [if i == j then ms_1 :* ms_2 else Any | j <- nonRecs c]
    /# ([0..],xs) ==> lhs
    -- \eq inline |sat'|
all sat $ g [if i == j then ms_1 :* ms_2 else Any | j <- nonRecs c]
    /# ([0..],xs) ==> lhs
    -- \eq inline |g|
all sat $ (zipWith Sat non (map (:[])
    [if i == j then ms_1 :* ms_2 else Any | j <- nonRecs c]) ++
    map (`Sat` [map complete (ctors c) :* map complete (ctors c)]) rec)
    /# ([0..],xs) ==> lhs
    -- \eq inline |(/)|
all sat $ zipWith Sat (non /# ([0..],xs))
    (map (:[]) [if i == j then ms_1 :* ms_2 else Any | j <- nonRecs c]) ++
    map (`Sat` [map complete (ctors c) :* map complete (ctors c)])
    (rec /# ([0..],xs)) ==> lhs
    -- \eq inline |all|
all sat (zipWith Sat (non /# ([0..],xs))
    (map (:[]) [if i == j then ms_1 :* ms_2 else Any | j <- nonRecs c])) &&
    all sat (map (`Sat` [map complete (ctors c) :* map complete (ctors c)])
    (rec /# ([0..],xs))) ==> lhs
    -- \im weaken implication
all sat $ zipWith Sat (non /# ([0..],xs))
    (map (:[]) [if i == j then ms_1 :* ms_2 else Any | j <- nonRecs c]) ==> lhs
    -- \eq inline |map|
all sat $ zipWith Sat (non /# ([0..],xs))
    [if i == j then [ms_1 :* ms_2] else [Any] | j <- nonRecs c] ==> lhs
    -- \eq \h{.mp}|non === nonRecs c|, by definition of |nonRecs|
all sat $ zipWith Sat (non /# ([0..],xs))
    [if i == j then [ms_1 :* ms_2] else [Any] | j <- non] ==> lhs
    -- \eq rewrite list comprehension
all sat $ zipWith Sat (non /# ([0..],xs))
    (map (\j -> if i == j then [ms_1 :* ms_2] else [Any]) non) ==> lhs
    -- \eq inline |(/)|
all sat $ zipWith Sat (map (/# ([0..],xs)) non)
    (map (\j -> if i == j then [ms_1 :* ms_2] else [Any]) non) ==> lhs
    -- \eq |zipWith f (map g xs) (map h xs) === map (\x -> f (g x) (h x)) xs|
all sat $ map (\j -> Sat (j /# ([0..],xs))
    (if i == j then [ms_1 :* ms_2] else [Any])) non ==> lhs
    -- \im weaken implication, using \h{.mp}|i `elem` non| because of false |isRec| test
all sat $ map (\j -> Sat (j /# ([0..],xs))
    (if i == j then [ms_1 :* ms_2] else [Any])) [i] ==> lhs
    -- \eq inline |map|
all sat $ [Sat (i /# ([0..],xs)) (if i == i then [ms_1 :* ms_2] else [Any])] ==> lhs
    -- \eq inline |all|
sat $ Sat (i /# ([0..],xs)) (if i == i then [ms_1 :* ms_2] else [Any]) ==> lhs
    -- \eq inline |(==)|
sat $ Sat (i /# ([0..],xs)) (if True then [ms_1 :* ms_2] else [Any]) ==> lhs
    -- \eq simplify |if|
sat $ Sat (i /# ([0..],xs)) [ms_1 :* ms_2] ==> lhs
    -- \eq inline |(/)|
sat $ Sat (xs !! i) [ms_1 :* ms_2] ==> lhs
    -- \eq reinstate LHS
sat $ Sat (xs !! i) [ms_1 :* ms_2] ==> sat $ Sat (xs !! i) [ms_1 :* ms_2]
    -- \eq tautology
True
\end{code}

\case{\h{.mp}|k === (ms_1 :* ms_2):ks| \csp |xs !! i === Value c' ys| \csp |isRec (c,i) === True|}

\h{.mp exprlist}\begin{code}
sat' $ (f_lhd $ f_rhd $ ms_1 :* ms_2) /# ([0..],xs) ==> sat $ Sat (xs !! i) [ms_1 :* ms_2]
    -- \eq inline |f_rhd|, assuming |isRec (c,i)|
sat' $ (f_lhd $ [complete c] :* merge ms_1 ms_2) /# ([0..],xs) ==> lhs
    -- \eq inline |f_lhd|
sat' $ propOrs [propAnds $ map propLit $ g vs_1 |
    Pattern c_1 vs_1 <- [complete c], c_1 == c] /# ([0..],xs) ==> lhs
    -- \eq inline \h{.mp}|complete c|
sat' $ propOrs [propAnds $ map propLit $ g vs_1 | Pattern c_1 vs_1 <-
    [Pattern c (map (const Any) (nonRecs c))], c_1 == c] /# ([0..],xs) ==> lhs
    -- \eq simplify list comprehension
sat' $ propOrs [propAnds $ map propLit $ g $ map (const Any) (nonRecs c)]
    /# ([0..],xs) ==> lhs
    -- \eq inline |propOrs|
sat' $ propAnds (map propLit $ g $ map (const Any) (nonRecs c))
    /# ([0..],xs) ==> lhs
    -- \eq inline |(/)|
sat' $ propAnds $ map propLit $ (g $ map (const Any) (nonRecs c))
    /# ([0..],xs) ==> lhs
    -- \eq inline |sat'|
all sat $ (g $ map (const Any) (nonRecs c)) /# ([0..],xs) ==> lhs
    -- \eq inline |g|
all sat $ (zipWith Sat non (map (:[]) vs) ++
    map (`Sat` [merge ms_1 ms_2 :* merge ms_1 ms_2]) rec) /# ([0..],xs) ==> lhs
    -- \eq inline |(/)|
all sat $ zipWith Sat non (map (:[]) vs) /# ([0..],xs) ++
    map (`Sat` [merge ms_1 ms_2 :* merge ms_1 ms_2]) rec /# ([0..],xs) ==> lhs
    -- \eq inline |all|
all sat (zipWith Sat non (map (:[]) vs) /# ([0..],xs)) &&
    all sat (map (`Sat` [merge ms_1 ms_2 :* merge ms_1 ms_2]) rec
    /# ([0..],xs)) ==> lhs
    -- \eq weaken implication
all sat $ map (`Sat` [merge ms_1 ms_2 :* merge ms_1 ms_2]) rec
    /# ([0..],xs) ==> lhs
    -- \eq eta expand
all sat $ map (\j -> Sat j [merge ms_1 ms_2 :* merge ms_1 ms_2]) rec
    /# ([0..],xs) ==> lhs
    -- \eq inline |(/)|
all sat $ map (\j -> Sat (j /# ([0..],xs))
    [merge ms_1 ms_2 :* merge ms_1 ms_2]) rec ==> lhs
    -- \eq combine |all| and |map|
all (\j -> sat $ Sat (j /# ([0..],xs))
    [merge ms_1 ms_2 :* merge ms_1 ms_2]) rec ==> lhs
    -- \im weaken implication, as \h{.mp}|i `elem` rec|, because of |isRec| test
all (\j -> sat $ Sat (j /# ([0..],xs))
    [merge ms_1 ms_2 :* merge ms_1 ms_2]) [i] ==> lhs
    -- \eq inline |all|
sat $ Sat (i /# ([0..],xs)) [merge ms_1 ms_2 :* merge ms_1 ms_2] ==> lhs
    -- \eq inline |(/)|
sat $ Sat (xs !! i) [merge ms_1 ms_2 :* merge ms_1 ms_2] ==> rhs
    -- \eq reinstate RHS
sat $ Sat (xs !! i) [merge ms_1 ms_2 :* merge ms_1 ms_2] ==>
    sat $ Sat (xs !! i) [ms_1 :* ms_2]
    -- \eq |xs !! i === Value c' ys|
sat $ Sat (Value c' ys) [merge ms_1 ms_2 :* merge ms_1 ms_2] ==>
    sat $ Sat (Value c' ys) [ms_1 :* ms_2]
    -- \im \lemma{\lemMPMerge}
sat $ Sat (Value c' ys) [ms_1 :* ms_2] ==> sat $ Sat (Value c' ys) [ms_1 :* ms_2]
    -- \eq tautology
True
\end{code}


\section{Auxiliary Lemmas}
\label{secP:general_lemmas}

To prove the main result we shall need the following lemmas.

\define{\lemElem}

\h{expr}\begin{code}
(x `elem` (ys \\ [x])) == False
\end{code}

The |elem| application is only true if |ys \\ [x]| contains |x|. The expression cannot contain |x|, as if it existed in |ys| it was removed, therefore this application is always |False|.


\define{\lemSatE}

\h{exprlist}\begin{code}
sat' (eval x -< cs) == satE' (x -< cs)
\end{code}

We argue as follows:

\h{exprlist}\begin{code}
sat' (eval x -< cs) == satE' (x -< cs)
    -- \eq inline |sat'| and |satE'|
propTaut sat (eval x -< cs) == propTaut satE (x -< cs)
    -- \eq inline |propTaut| and reduce common bits
propMap (propBool . sat) (eval x -< cs) == propMap (propBool . satE) (x -< cs)
\end{code}

Now we can use the type signature of |-<|:

\begin{code}
(-<) :: alpha -> [CtorName] -> Prop (Sat alpha)
\end{code}

The theorems for free work \cite{wadler:theorems} shows that the first argument will end up as the first argument of the |Sat| constructor, unmodified and unexamined. The |satE| function applies |eval| to the first argument of |Sat|, therefore the equivalence holds.


\define{\lemPrecondError}

\h{expr}\begin{code}
precond "error" == propFalse
\end{code}

The initial computation of |precond| will return |propFalse|. All successive computations will be at least as restrictive, therefore the result must be |propFalse|.


\define{\lemPrecond}

\h{expr}\begin{code}
precond f ==> reduce $ pre $ body f
\end{code}

The definition of |precond f| is a conjunction where the second conjunct is |reduce $ pre $ body f|, therefore |precond f| is at least as restrictive as the alternative.


\define{\lemPrePost}

\h{expr}\begin{code}
prePost f k ==> reduce (propLit $ body f `Sat` k)
\end{code}

The definition of |prePost f k| is a conjunction where the second conjunct is |reduce (propLit $ body f `Sat` k)|, therefore |prePost f k| is at least as restrictive as the alternative.


\define{\lemPre}

\h{exprlist}\begin{code}
satE' (pre e / (vs, ys)) && all (satE' . pre) ys ==> satE' $ pre $ e / (vs, ys)
\end{code}

We assume that all free variables in |e| are bound in |vs|. To shorten the proofs we do not explicitly write the |all (satE' . pre) ys| term, as it is never manipulated. We proceed by induction on |e|.

\case{|e === Var v|}

\h{exprlist}\begin{code}
satE' $ pre e / (vs, ys) ==> satE' $ pre $ e / (vs, ys)
    -- \eq |e === Var v|
satE' $ pre (Var v) / (vs, ys) ==> satE' $ pre $ Var v / (vs, ys)
    -- \eq inline |pre| on LHS
satE' $ propTrue / (vs, ys) ==> satE' $ pre $ Var v / (vs, ys)
    -- \eq inline |(/)| on LHS
satE' propTrue ==> satE' $ pre $ Var v / (vs, ys)
    -- \eq inline |satE'|
True ==> satE' $ pre $ Var v / (vs, ys)
    -- \eq reintroduce hidden term
all (satE' . pre) ys ==> satE' $ pre $ Var v / (vs, ys)
\end{code}

We know that |v| will be a member of |vs|, and that the result will be |pre y|, where |y| is drawn from |ys|. Since all |ys| satisfy the precondition, then so will the particular |y| we substitute.

\case{|e === Sel x s|}

\h{exprlist}\begin{code}
satE' $ pre e / (vs, ys) ==> satE' $ pre $ e / (vs, ys)
    -- \eq |e === Sel x s|
satE' $ pre (Sel x s) / (vs, ys) ==> satE' $ pre $ Sel x s / (vs, ys)
    -- \eq inline |(/)| on RHS
satE' $ pre (Sel x s) / (vs, ys) ==> satE' $ pre $ Sel (x / (vs,ys)) s
    -- \eq inline |pre| on RHS
satE' $ pre (Sel x s) / (vs, ys) ==> satE' $ propTrue
    -- \eq inline |satE'| on RHS
satE' $ pre (Sel x s) / (vs, ys) ==> True
    -- \eq implication
True
\end{code}

\case{|e === Make c xs|}

\h{exprlist}\begin{code}
satE' $ pre x / (vs, ys) ==> satE' $ pre $ x / (vs, ys)
    -- \eq |x === Make c xs|
satE' $ pre (Make c xs) / (vs, ys) ==> satE' $ pre $ Make c xs / (vs, ys)
    -- \eq inline |(/)| on RHS
satE' $ pre (Make c xs) / (vs, ys) ==>
    satE' $ pre $ Make c $ map (/ (vs, ys)) xs
    -- \eq inline |pre| on both sides
satE' $ propAnds (map pre xs) / (vs, ys) ==>
    satE' $ propAnds $ map (pre . (/ (vs, ys))) xs
    -- \eq inline |(/)| on LHS
satE' $ propAnds $ map ((/ (vs,ys)) . pre) xs ==>
    satE' $ propAnds $ map (pre . (/ (vs, ys))) xs
    -- \eq inline |satE'| on both sides
all (satE' . (/ (vs,ys)) . pre) xs ==> all (satE' . pre . (/ (vs, ys))) xs
    -- \im by induction
True
\end{code}

\case{|e === Call f xs|}

\h{exprlist}\begin{code}
satE' $ pre e / (vs, ys) ==> satE' $ pre $ e / (vs, ys)
    -- \eq |e === Call f xs|
satE' $ pre (Call f xs) / (vs, ys) ==> satE' $ pre $ Call f xs / (vs, ys)
    -- \eq inline |(/)| on RHS
satE' $ pre (Call f xs) / (vs, ys) ==> satE' $ pre $ Call f $ map (/ (vs, ys)) xs
    -- \eq inline |pre|
satE' $ (pre' f xs `propAnd` propAnds (map pre xs)) / (vs,ys) ==> rhs
    -- \eq inline |(/)|
satE' $ (pre' f xs / (vs,ys)) `propAnd` propAnds (map (pre . (/ (vs,ys))) xs) ==> rhs
    -- \eq inline |satE'|
satE' (pre' f xs / (vs,ys)) && all (satE' . pre . (/ (vs,ys))) xs ==> rhs
    -- \eq switch to RHS
lhs ==> satE' $ pre $ Call f $ map (/ (vs, ys)) xs
    -- \eq inline |pre|
lhs ==> satE' $ (pre' f (map (/ (vs, ys)) xs)) `propAnd`
    propAnds (map (pre . (/ (vs, ys))) xs)
    -- \eq inline |satE'|
lhs ==> satE' (pre' f (map (/ (vs, ys)) xs)) && all (satE' . pre . (/ (vs, ys))) xs
    -- \eq reinstate LHS
satE' (pre' f xs / (vs,ys)) && all (satE' . pre . (/ (vs,ys))) xs ==>
    satE' (pre' f (map (/ (vs, ys)) xs)) && all (satE' . pre . (/ (vs, ys))) xs
    -- \im eliminate common term
satE' $ pre' f xs / (vs,ys) ==> satE' $ pre' f (map (/ (vs, ys)) xs)
    -- \eq inline |pre'|
satE' $ (precond f /# (args f, xs)) / (vs,ys) ==>
    satE' $ precond f /# (args f, map (/ (vs, ys)) xs)
    -- \eq inline |(/)| on LHS
satE' $ precond f /# (args f, map (/ (vs,ys)) xs) ==>
    satE' $ precond f /# (args f, map (/ (vs, ys)) xs)
    -- \eq tautology
True
\end{code}

\case{|e === Case x as|}

\h{exprlist}\begin{code}
satE' $ pre e / (vs, ys) ==> satE' $ pre $ e / (vs, ys)
    -- \eq |e === Case x as|
satE' $ pre (Case x as) / (vs, ys) ==> satE' $ pre $ Case x as / (vs, ys)
    -- \eq inline |(/)| on RHS
satE' $ pre (Case x as) / (vs, ys) ==>
    satE' $ pre $ Case (x / (vs, ys)) (map (/ (vs, ys)) as)
    -- \eq inline |pre| on both sides
satE' $ (pre x `propAnd` propAnds (map alt as)) / (vs, ys) ==>
    satE' $ pre (x / (vs, ys)) `propAnd` propAnds (map (alt . (/ (vs, ys))) as)
    -- \eq inline |(/)| on LHS
satE' $ (pre x / (vs, ys)) `propAnd` propAnds (map ((/ (vs, ys)) . alt) as)  ==>
    satE' $ pre (x / (vs, ys)) `propAnd` propAnds (map (alt . (/ (vs, ys))) as)
    -- \eq inline |satE'|
satE' (pre x / (vs, ys)) && all (satE' . (/ (vs, ys)) . alt) as ==>
    satE' (pre (x / (vs, ys))) && all (satE' . alt . (/ (vs, ys))) as
    -- \im by induction
all (satE' . (/ (vs, ys)) . alt) as  ==> all (satE' . alt . (/ (vs, ys))) as
    -- \im implication over |all|
satE' $ alt a / (vs, ys) ==> satE' $ alt $ a / (vs, ys)
    -- \eq instantiate |a| as a general |Alt|
satE' $ alt (Alt c ws y) / (vs, ys) ==> satE' $ alt $ Alt c ws y / (vs, ys)
    -- \eq inline |(/)| on RHS
satE' $ alt (Alt c ws y) / (vs, ys) ==> satE' $ alt $ Alt c ws (y / (vs, ys))
    -- \eq inline |alt|
satE' $ (x -< (ctors c \\ [c]) `propOr` pre y) / (vs, ys) ==>
    satE' $ (x / (vs,ys) -< (ctors c \\ [c])) `propOr` pre (y / (vs, ys))
    -- \eq let |cs === ctors c \\ [c]|
satE' $ (x -< cs `propOr` pre y) / (vs, ys) ==>
    satE' $ (x / (vs,ys) -< cs) `propOr` pre (y / (vs, ys))
    -- \eq inline |(/)| on LHS
satE' $ (x / (vs,ys) -< cs) `propOr` (pre y / (vs, ys)) ==>
    satE' $ (x / (vs,ys) -< cs) `propOr` pre (y / (vs, ys))
    -- \eq inline |satE'| on both sides
satE' (x / (vs,ys) -< cs) || satE' (pre y / (vs, ys)) ==>
    satE' (x / (vs,ys) -< cs) || satE' (pre (y / (vs, ys)))
    -- \im remove duplicate bits on each side
satE' $ pre y / (vs, ys) ==> satE' $ pre $ y / (vs, ys)
    -- \im by induction
True
\end{code}


\define{\lemRed}

\h{expr}\begin{code}
satE' $ red e k /# sub ==> sat $ Sat (eval $ e / sub) k
\end{code}

We proceed by induction on |e|.

\case{|e === Var v|}

\h{exprlist}\begin{code}
satE' $ red e k /# sub ==> sat $ Sat (eval $ e / sub) k
    -- \eq |e === Var v|
satE' $ red (Var v) k /# sub ==> sat $ Sat (eval $ Var v / sub) k
    -- \eq inline |red|
satE' $ propLit (Sat v k) /# sub ==> sat $ Sat (eval $ Var v / sub) k
    -- \eq inline |(/)| on LHS
satE' $ propLit (Sat (v /# sub) k) ==> sat $ Sat (eval $ Var v / sub) k
    -- \eq promote |v| on LHS to |Var v| because |(/)| operates identically on both
satE' $ propLit (Sat (Var v / sub) k) ==> sat $ Sat (eval $ Var v / sub) k
    -- \eq inline |satE'|
satE (Sat (Var v / sub) k) ==> sat $ Sat (eval $ Var v / sub) k
    -- \eq inline |satE|
sat $ Sat (eval $ Var v / sub) k ==> sat $ Sat (eval $ Var v / sub) k
    -- \eq tautology
True
\end{code}

\case{|e === Sel x (c,i)|}

Here we may assume |eval (x / sub) === Value c xs|.

\h{exprlist}\begin{code}
satE' $ red e k /# sub ==> sat $ Sat (eval $ e / sub) k
    -- \eq |e === Sel x (c,i)|
satE' $ red (Sel x (c,i)) k /# sub ==> sat $ Sat (eval $ Sel x (c,i) / sub) k
    -- \eq inline |red|
satE' $ red x ((c,i) |> k) /# sub ==> sat $ Sat (eval $ Sel x (c,i) / sub) k
    -- \eq inline |(/)| on RHS
satE' $ red x ((c,i) |> k) /# sub ==> sat $ Sat (eval $ Sel (x / sub) (c,i)) k
    -- \eq inline |eval| on RHS
satE' $ red x ((c,i) |> k) /# sub ==> sat $ Sat (xs !! i) k
    -- \im \lemma{\lemSatTri}
satE' $ red x ((c,i) |> k) /# sub ==> sat $ Sat (Value c xs) ((c,i) |> k)
    -- \eq replace using the assumption
satE' $ red x ((c,i) |> k) /# sub ==> sat $ Sat (eval (x / sub)) ((c,i) |> k)
    -- \im by induction
True
\end{code}

\case{|e === Make c xs|}

\h{exprlist}\begin{code}
satE' $ red e k /# sub ==> sat $ Sat (eval $ e / sub) k
    -- \eq |e === Make c xs|
satE' $ red (Make c xs) k /# sub ==> sat $ Sat (eval $ Make c xs / sub) k
    -- \eq inline |red|
satE' $ reduce ((c <| k) /# ([0..], xs)) /# sub ==> sat $ Sat (eval $ Make c xs / sub) k
    -- \im \lemma{\lemReduce}
satE' $ ((c <| k) /# ([0..], xs)) / sub ==> sat $ Sat (eval $ Make c xs / sub) k
    -- \eq inline |(/)| on LHS
satE' $ (c <| k) /# ([0..], map (/ sub) xs) ==> sat $ Sat (eval $ Make c xs / sub) k
    -- \eq inline |satE'| on LHS
sat' $ (c <| k) /# ([0..], map (eval . (/ sub)) xs) ==>
    sat $ Sat (eval $ Make c xs / sub) k
    -- \eq inline |(/)| on RHS
sat' $ (c <| k) /# ([0..], map (eval . (/ sub)) xs) ==>
    sat $ Sat (eval $ Make c (map (/ sub) xs)) k
    -- \eq inline |eval| on RHS
sat' $ (c <| k) /# ([0..], map (eval . (/ sub)) xs) ==>
    sat $ Sat (Value c (map (eval . (/ sub)) xs)) k
    -- \eq fold back |sat|
sat $ Sat (Value c (map (eval . (/ sub)) xs)) k ==>
    sat $ Sat (Value c (map (eval . (/ sub)) xs)) k
    -- \eq tautology
True
\end{code}

\case{|e === Call f xs|}

\h{exprlist}\begin{code}
satE' $ red e k /# sub ==> sat $ Sat (eval $ e / sub) k
    -- \eq |e === Call f xs|
satE' $ red (Call f xs) k /# sub ==> sat $ Sat (eval $ Call f xs / sub) k
    -- \eq inline |red|
satE' $ reduce (prePost f k /# (args f, xs)) /# sub ==> rhs
    -- \im \lemma{\lemReduce}
satE' $ (prePost f k /# (args f, xs)) / sub ==> rhs
    -- \eq inline |(/)| on LHS
satE' $ prePost f k /# (args f, map (/sub) xs) ==> rhs
    -- \im \lemma{\lemPrePost}
satE' $ reduce (propLit $ Sat (body f) k) /# (args f, map (/sub) xs) ==> rhs
    -- \im \lemma{\lemReduce}
satE' $ (propLit $ Sat (body f) k) / (args f, map (/sub) xs) ==> rhs
    -- \eq inline |(/)| on LHS
satE' $ (propLit $ Sat (body f / (args f, map (/sub) xs)) k) ==> rhs
    -- \eq inline |satE'|
satE $ Sat (body f / (args f, map (/sub) xs)) k ==> rhs
    -- \eq inline |satE|
sat $ Sat (eval $ body f / (args f, map (/sub) xs)) k ==>
    sat $ Sat (eval $ Call f xs / sub) k
    -- \eq inline |(/)| on RHS
sat $ Sat (eval $ body f / (args f, map (/sub) xs)) k ==>
    sat $ Sat (eval $ Call f (map (/ sub) xs)) k
\end{code}

\case{|e === Call f xs| \csp |f === "error"|}

\h{exprlist}\begin{code}
sat $ Sat (eval $ body f / (args f, map (/ sub) xs)) k ==>
    sat $ Sat (eval $ Call f (map (/ sub) xs)) k
    -- \eq assume |f === "error"|
sat $ Sat (eval $ body "error" / (args f, map (/ sub) xs)) k ==>
    sat $ Sat (eval $ Call "error" (map (/ sub) xs)) k
    -- \eq inline |eval| on RHS
sat $ Sat (eval $ body "error" / (args f, map (/ sub) xs)) k ==>
    sat $ Sat Bottom k
    -- \eq inline |sat|
sat $ Sat (eval $ Call "error" [Var "x"] / (["x"], map (/sub) xs)) k ==> False
    -- \eq implies
True
\end{code}

\case{|e === Call f xs| \csp |f /= "error"|}

\h{exprlist}\begin{code}
sat $ Sat (eval $ body f / (args f, map (/ sub) xs)) k ==>
    sat $ Sat (eval $ Call f (map (/ sub) xs)) k
    -- \eq inline |eval| on RHS, assuming |f /= "error"|
sat $ Sat (eval $ body f / (args f, map (/ sub) xs)) k ==>
    sat $ Sat (eval $ body f / (args f, map (/ sub) xs)) k
    -- \eq tautology
True
\end{code}

\case{|e === Case x as|}

\h{exprlist}\begin{code}
satE' $ red e k /# sub ==> sat $ Sat (eval $ e / sub) k
    -- \eq |e === Case x as|
satE' $ red (Case x as) k /# sub ==> sat $ Sat (eval $ Case x as / sub) k
    -- \eq inline |red|
satE' $ propAnds (map alt as) /# sub ==> sat $ Sat (eval $ Case x as / sub) k
    -- \eq inline |(/)| on LHS
satE' $ propAnds $ map ((/# sub) . alt) as ==> sat $ Sat (eval $ Case x as / sub) k
    -- \eq inline |satE'|
all (satE' . (/# sub) . alt) as ==> sat $ Sat (eval $ Case x as / sub) k
    -- \eq inline |(/)| on RHS
all (satE' . (/# sub) . alt) as ==> sat $ Sat (eval $ Case (x / sub) (as / sub)) k
\end{code}

\case{|e === Case x as| \csp |eval (x / sub) === Bottom|}

\h{exprlist}\begin{code}
all (satE' . (/# sub) . alt) as ==> sat $ Sat (eval $ Case (x / sub) (as / sub)) k
    -- \eq inline |eval|, assuming |eval (x / sub) === Bottom|
all (satE' . (/# sub) . alt) as ==> sat $ Sat Bottom k
    -- \eq inline |sat|
all (satE' . (/# sub) . alt) as ==> True
    -- \eq implies
True
\end{code}

\case{|e === Case x as| \csp |eval (x / sub) === Value c xs|}

\h{exprlist}\begin{code}
all (satE' . (/# sub) . alt) as ==> sat $ Sat (eval $ Case (x / sub) (as / sub)) k
    -- \eq inline |eval|, assuming |eval (x / sub) === Value c xs|
lhs ==> sat $ Sat (head [eval y | Alt c' vs y <- as / sub, c == c']) k
    -- \eq expand RHS, removing list comprehension
all (satE' . (/# sub) . alt) as ==>
    all (\(Alt c' vs y) -> c == c' ==> sat $ Sat (eval y) k) (as / sub)
    -- \im lift implication over |all|
satE' $ alt a /# sub ==>
    (\(Alt c' vs y) -> c == c' ==> sat $ Sat (eval y) k) (a / sub)
    -- \eq instantiate |a === Alt c' vs y|
satE' $ alt a /# sub ==>
    (\(Alt c' vs y) -> c == c' ==> sat $ Sat (eval y) k) (Alt c' vs y / sub)
    -- \eq inline |(/)| on RHS
satE' $ alt a /# sub ==>
    (\(Alt c' vs y) -> c == c' ==> sat $ Sat (eval y) k) (Alt c' vs $ y / sub)
    -- \eq inline lambda on RHS
satE' $ alt (Alt c' vs y) /# sub ==>
    (c == c' ==> sat $ Sat (eval $ y / sub) k)
    -- \eq use knowledge from RHS in LHS
satE' $ alt (Alt c vs y) /# sub ==> sat $ Sat (eval $ y / sub) k
    -- \eq inline |alt| on LHS
satE' $ (reduce (x -< (ctors c \\ [c])) `propOr` red y k) /# sub ==> rhs
    -- \eq inline |(/)| on LHS
satE' $ (reduce (x -< (ctors c \\ [c])) /# sub) `propOr` (red y k /# sub) ==> rhs
    -- \eq inline |satE'| on LHS
satE' (reduce (x -< (ctors c \\ [c])) /# sub) || satE' (red y k /# sub) ==> rhs
    -- \im \lemma{\lemReduce}
satE' ((x -< (ctors c \\ [c])) / sub) || satE' (red y k /# sub) ==> rhs
    -- \eq inline |(/)| on LHS
satE' ((x / sub) -< (ctors c \\ [c])) || satE' (red y k /# sub) ==> rhs
    -- \eq \lemma{\lemSatE}
sat' (eval (x / sub) -< (ctors c \\ [c])) || satE' (red y k /# sub) ==> rhs
    -- \eq substitute |eval (x / sub) === Value c xs|
sat' (Value c xs -< (ctors c \\ [c])) || satE' (red y k /# sub) ==> rhs
    -- \im \lemma{\lemSat}
c `elem` (ctors c \\ [c]) || satE' (red y k /# sub) ==> rhs
    -- \eq \lemma{\lemElem}
False || satE' (red y k /# sub) ==> rhs
    -- \eq inline |(||||)|
satE' $ red y k /# sub ==> sat $ Sat (eval $ y / sub) k
    -- \im by induction
True
\end{code}


\define{\lemReduce}

\h{exprlist}\begin{code}
satE' $ reduce x /# sub ==> satE' $ x / sub
    -- \eq inline |reduce|
satE' $ propMap (\(Sat x k) -> red x k) x /# sub ==> satE' $ x / sub
    -- \eq inline |(/)| on LHS
satE' $ propMap (\(Sat x k) -> red x k /# sub) x ==> satE' $ x / sub
    -- \eq inline |(/)| on RHS
satE' $ propMap (\(Sat x k) -> red x k /# sub) x ==>
    satE' $ propMap (\(Sat x k) -> propLit $ Sat x k / sub) x
    -- \eq inline |(/)| on RHS
satE' $ propMap (\(Sat x k) -> red x k /# sub) x ==>
    satE' $ propMap (\(Sat x k) -> propLit $ Sat (x / sub) k) x
    -- \eq inline |satE'|
propIsTrue $ propMap (\(Sat x k) -> propBool $ satE' $ red x k /# sub) x ==>
    propIsTrue $ propMap (\(Sat x k) -> propBool $ satE' $ propLit $ Sat (x / sub) k) x
    -- \im lift |propMap| over |(==>)|
satE' $ red x k /# sub ==> satE' $ propLit $ Sat (x / sub) k
    -- \eq inline |satE'| on RHS
satE' $ red x k /# sub ==> satE $ Sat (x / sub) k
    -- \eq inline |satE| on RHS
satE' $ red x k /# sub ==> sat $ Sat (eval $ x / sub) k
    -- \im \lemma{\lemRed}
True
\end{code}



\section{The Soundness Theorem}
\label{secP:proof}

\subsection{Theorem}

\h{expr}\begin{code}
satE' $ pre e ==> not $ isBottom $ eval e
\end{code}

That is, the analysis defined in Figures \ref{figC:property_fixp}, \ref{figC:precondition}, \ref{figC:precond_fixp} and \ref{figC:prop} is sound.

\subsection{Proof}

We proceed by case analysis on the structure of the expression |e|. We inductively assume that the theorem is true for all subexpressions of |e|.

\case{|e === Var v|}

We do not need to consider |Var| as |eval| cannot be called on expressions with free variables, see \S\ref{secP:theorem}.

\case{|e === Sel x (c,i)|}

By definition:

\begin{code}
eval (Sel x (c,i)) | c == c' = xs !! i
    where Value c' xs = eval x
\end{code}

We know that any \ignore|Sel x _| value must be contained within an alternative of a \ignore|Case x _| expression. We may assume that the original |Case| expression satisfied its precondition.

\h{exprlist}\begin{code}
satE' $ pre e ==> not $ isBottom $ eval e
    -- \eq |e === Sel x (c,i)|
satE' $ pre $ Sel x (c,i) ==> not $ isBottom $ eval $ Sel x (c,i)
    -- \eq inline |eval|
satE' $ pre $ Sel x (c,i) ==> not $ isBottom $ xs !! i
    -- \im strengthen implication
satE' $ pre $ Sel x (c,i) ==> all (not . isBottom) xs
    -- \eq by definition of |isBottom|
satE' $ pre $ Sel x (c,i) ==> not $ isBottom $ Value c' xs
    -- \eq |Value c' xs === eval x|
satE' $ pre $ Sel x (c,i) ==> not $ isBottom $ eval x
    -- \im inductive hypothesis
satE' $ pre $ Sel x (c,i) ==> satE' $ pre x
    -- \eq assuming original |Case| satisfied its constraint
satE' $ pre $ Case x as ==> satE' $ pre x
    -- \eq inline |pre|
satE' $ pre x `propAnd` propAnds (map alt as) ==> satE' $ pre x
    -- \eq inline |satE'|
satE' (pre x) && satE' (propAnds $ map alt as) ==> satE' $ pre x
    -- \im weaken implication
satE' $ pre x ==> satE' $ pre x
    -- \eq tautology
True
\end{code}

\case{|e === Make c xs|}

\h{exprlist}\begin{code}
satE' $ pre e ==> not $ isBottom $ eval e
    -- \eq |e === Make c xs|
satE' $ pre $ Make c xs ==> not $ isBottom $ eval $ Make c xs
    -- \eq inline |eval|
satE' $ pre $ Make c xs ==> not $ isBottom $ Value c $ map eval xs
    -- \eq inline |isBottom|
satE' $ pre $ Make c xs ==> all (not . isBottom . eval) xs
    -- \im inductive hypothesis
satE' $ pre $ Make c xs ==> all (satE' . pre) xs
    -- \eq inline |pre|
satE' $ propAnds $ map pre xs ==> all (satE' . pre) xs
    -- \eq inline |satE'|
and $ map satE' $ map pre xs  ==> all (satE' . pre) xs
    -- \eq |map f . map g === map (f . g)|
and $ map (satE' . pre) xs ==> all (satE' . pre) xs
    -- \eq |and . map f === all f|
all (satE' . pre) xs ==> all (satE' . pre) xs
    -- \eq tautology
True
\end{code}

\case{|e === Call f xs|}

\h{exprlist}\begin{code}
satE' $ pre e ==> not $ isBottom $ eval e
    -- \eq |e === Call f xs|
satE' $ pre $ Call f xs ==> not $ isBottom $ eval $ Call f xs
\end{code}

\case{|e === Call f xs| \csp |f === "error"|}

\h{exprlist}\begin{code}
satE' $ pre $ Call f xs ==> not $ isBottom $ eval $ Call f xs
    -- \eq |f === "error"|
satE' $ pre $ Call "error" xs ==> not $ isBottom $ eval $ Call "error" xs
    -- \eq inline |eval|
satE' $ pre $ Call "error" xs ==> not $ isBottom Bottom
    -- \eq inline |isBottom|
satE' $ pre $ Call "error" xs ==> not True
    -- \eq inline |not|
satE' $ pre $ Call "error" xs ==> False
    -- \eq implication
not $ satE' $ pre $ Call "error" xs
    -- \eq inline |pre|
not $ satE' $ (precond "error" /# (args "error", xs)) `propAnd` propAnds (map pre xs)
    -- \eq inline |satE'|
not $ satE' (precond "error" /# (args "error", xs)) && all (satE' . pre) xs
    -- \eq inline |not|
not (satE' (precond "error" /# (args "error", xs))) || not (all (satE' . pre) xs)
    -- \im weaken proposition
not $ satE' (precond "error" /# (args "error", xs))
    -- \eq \lemma{\lemPrecondError}
not $ satE' $ (propFalse /# (args "error", xs))
    -- \eq inline |(/)|
not $ satE' propFalse
    -- \eq inline |satE'|
not $ False
    -- \eq inline |not|
True
\end{code}

\case{|e === Call f xs| \csp |f /= "error"|}

\h{exprlist}\begin{code}
satE' $ pre $ Call f xs ==> not $ isBottom $ eval $ Call f xs
    -- \eq inline |eval|, assuming |f /= "error"|
satE' $ pre $ Call f xs ==> not $ isBottom $ eval $ body f / (args f, xs)
    -- \im inductive hypothesis
satE' $ pre $ Call f xs ==> satE' $ pre $ body f / (args f, xs)
    -- \eq inline pre on LHS
satE' $ (precond f /# (args f, xs)) `propAnd` propAnds (map pre xs) ==> rhs
    -- \eq inline |satE'|
satE' (precond f /# (args f, xs)) && all (satE' . pre) xs ==> rhs
    -- \im \lemma{\lemPrecond}
satE' ((reduce $ pre $ body f) /# (args f, xs)) && all (satE' . pre) xs ==> rhs
    -- \im \lemma{\lemReduce}
satE' (pre (body f) / (args f, xs)) && all (satE' . pre) xs ==> rhs
    -- \im \lemma{\lemPre}
satE' $ pre $ body f / (args f, xs) ==> satE' $ pre $ body f / (args f, xs)
    -- \eq tautology
True
\end{code}

\case{|e === Case x as|}

\h{exprlist}\begin{code}
satE' $ pre e ==> not $ isBottom $ eval e
    -- \eq |e === Case x as|
satE' $ pre $ Case x as ==> not $ isBottom $ eval $ Case x as
\end{code}

\case{|e === Case x as| \csp |eval x === Bottom|}

\h{exprlist}\begin{code}
satE' $ pre $ Case x as ==> not $ isBottom $ eval $ Case x as
    -- \eq inline |eval|, assuming |eval x === Bottom|
satE' $ pre $ Case x as ==> not $ isBottom Bottom
    -- \eq inline |isBottom|
satE' $ pre $ Case x as ==> not True
    -- \eq inline |not|
satE' $ pre $ Case x as ==> False
    -- \eq implication
not $ satE' $ pre $ Case x as
    -- \eq inline |pre|
not $ satE' $ pre x `propAnd` propAnds (map alt as)
    -- \eq inline |satE'|
not $ satE' (pre x) && satE' (propAnds $ map alt as)
    -- \eq inline |not|
not (satE' $ pre x) || not  (satE' $ propAnds $ map alt as)
    -- \im weaken condition
not $ satE' $ pre x
    -- \im inductive hypothesis
not $ not $ isBottom $ eval e
    -- \eq |not (not x) === x|
isBottom $ eval e
    -- \eq |eval x === Bottom|
isBottom Bottom
    -- \eq inline |isBottom|
True
\end{code}

\case{|e === Case x as| \csp |eval x === Value c xs|}

\h{exprlist}\begin{code}
satE' $ pre $ Case x as ==> not $ isBottom $ eval $ Case x as
    -- \eq inline |eval|, assuming |eval x === Value c xs|
lhs ==> not $ isBottom $ head [eval y | Alt c' vs y <- as, c == c']
    -- \im strengthen implication
lhs ==> all (not .  isBottom) [eval y | Alt c' vs y <- as, c == c']
    -- \eq inline |all| over list comprehension
lhs ==> and [not $ isBottom $ eval y | Alt c' vs y <- as, c == c']
    -- \eq rearrange guard as an implication
lhs ==> and [c == c' ==> not $ isBottom $ eval y | Alt c' vs y <- as]
    -- \eq rewrite list comprehension as an |all|
lhs ==> all (\(Alt c' vs y) -> c == c' ==> not $ isBottom $ eval y) as
    -- \im inductive hypothesis
lhs ==> all (\(Alt c' vs y) -> c == c' ==> satE' $ pre y) as
    -- \eq switch to LHS
satE' $ pre $ Case x as ==> rhs
    -- \eq inline |pre|
satE' $ pre x `propAnd` propAnds (map alt as) ==> rhs
    -- \eq inline |satE'|
satE' (pre x) && all (satE' . alt) as ==> rhs
    -- \im weaken implication
all (satE' . alt) as ==>
    all (\(Alt c' vs y) -> c == c' ==> satE' $ pre y) as
    -- \im lift implies over all
satE' $ alt a ==> (\(Alt c' vs y) -> c == c' ==> satE' $ pre y) a
    -- \eq instantiate |a === Alt c' v ys|
satE' $ alt $ Alt c' v ys ==> (c == c' ==> satE' $ pre y)
    -- \eq rearrange implication
satE' (alt $ Alt c' v ys) && (c == c') ==> satE' $ pre y
    -- \eq substitute |c == c'|
satE' $ alt $ Alt c v ys ==> rhs
    -- \eq inline |alt|
satE' (x -< (ctors c \\ [c]) `propOr` pre y) ==> rhs
    -- \eq inline |satE'|
satE' (x -< (ctors c \\ [c])) || satE' (pre y) ==> rhs
    -- \eq \lemma{\lemSatE}
sat' (eval x -< (ctors c \\ [c])) || satE' (pre y) ==> rhs
    -- \eq |eval x === Value c xs|
sat' (Value c ys -< (ctors c \\ [c])) || satE' (pre y) ==> rhs
    -- \im \lemma{\lemSat}
c `elem` (ctors c \\ [c]) || satE' (pre y) ==> rhs
    -- \eq \lemma{\lemElem}
False || satE' (pre y) ==> rhs
    -- \eq inline |(||||)|
satE' $ pre y ==> satE' $ pre y
    -- \eq tautology
True
\end{code}

\section{Summary}
\label{secP:summary}

We have outlined an argument that the Catch analysis method presented in Chapter \ref{chp:catch} is sound. In doing so, we have characterised the properties that a constraint system must obey, and have shown these properties for BP-constraints and MP-constraints. The majority of the proof uses equational reasoning, apart from Lemma \lemMPMerge\ which has been tested for all small values. The proof has undergone limited checking for simple type-correctness, but has not been fully machine-checked.