899   \newcommand{\posix}{\succcurlyeq_{PX}}

   899   \newcommand{\posix}{>}

   909   correctness proof of the POSIX algorithm. Frisch and Cardelli introduced

   945   correctness proof of the POSIX value algorithm. Frisch and Cardelli

   910   an ordering, written $\greedy$, for values and they show that their greedy

   946   introduced an ordering, written $\greedy$, for values and they show that

   911   matching algorithm always produces a maximal element according to this

   947   their greedy matching algorithm always produces a maximal element

   912   ordering (from all possible solutions). The ordering $\greedy$ is defined

   948   according to this ordering (from all possible solutions). The only

   913   by the following rules:

   949   difference between their greedy ordering and the ``ordering'' by Sulzmann

   950   and Lu is that GREEDY always prefers a $Left$-value over a $Right-value$.

   951   What is interesting for our purposes is that the properties reflexivity,

   952   totality and transitivity for this GREEDY ordering can be proved

   953   relatively easily by induction.

   954 

   955   These properties of GREEDY, however, do not transfer to POSIX by 

   956   Sulzmann and Lu. To start with, transitivity does not hold anymore in the

   957 ``normal'' formulation, that is:

   958 

   959 \begin{property}

   960 Suppose $v_1 : r$, $v_2 : r$ and $v_3 : r$.

   961 If $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$

   962 then $v_1 \posix_r v_3$.

   963 \end{property}

   964 

   965 \noindent If formulated like this, then there are various counter examples:

   966 Suppose $r$ is $a + ((a + a)(a + \textbf{0}))$ then the $v_1$, $v_2$ and $v_3$

   967 below are values of $r$:

   916 \begin{tabular}{cc}

   970 \begin{tabular}{lcl}

   917 \infer{v_{1} \greedy v'_{1}} {(v_{1},v_{2}) \greedy (v'_{1},v'_{2})}

   971  $v_1$ & $=$ & $Left(Char\;a)$\\

   918 &

   972  $v_2$ & $=$ & $Right((Left(Char\;a), Right(Void)))$\\

   919 \infer{v_{2} \greedy v'_{2}} {(v_{1},v_{2}) \greedy (v_{1},v'_{2})}

   973  $v_3$ & $=$ & $Right((Right(Char\;a), Left(Char\;a)))$

   920 \smallskip\\

   921 \infer{v_{1} \greedy v_{2}} {Left \; v_{1} \greedy Left \; v_{2}}

   922 &

   923 \infer{v_{1} \greedy v_{2}} {Right \; v_{1} \greedy Right \; v_{2}}

   924 \\

   925 

   926 \infer{\mbox{}}{Left \; v_{2}\greedy Right \; v_{1} }

   927 \medskip\\

   928 

   929 $\infer{ v_{1} \greedy v_{2}} {v_{1} :: vs_{1} \greedy v_{2} :: vs_{2}} $ & 

   930 $\infer{ vs_{1} \greedy vs_{2}} {v :: vs_{1} \greedy v :: vs_{2}}$

   931 \\

   932 

   933 & 

   934 $\infer{\mbox{}} { v::vs \greedy []}$

   935 \\

   936 

   937 \infer{\mbox{}}{Char \; c \greedy Char \; c}

   938 &

   939 \infer{\mbox{}}{Void \greedy Void}\\

   940 

   944 \noindent That these rules realise a greedy ordering can be

   977 \noindent Moreover $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$,

   945 seen in the first rule in the third line where a $Left$-value

   978 but \emph{not} $v_1 \posix_r v_3$! The reason is that although

   946 is always bigger than (or preferred over) a $Right$-value.

   979 $v_3$ is a $Right$-value, it can match a longer string, namely

   947 What is interesting for our purposes is that the properties

   980 $|v_3| = aa$, while $|v_1|$ (and $|v_2|$) matches only $a$. So

   948 reflexivity, totality and transitivity for this greedy

   981 transitivity in this formulation does not hold---in this

   949 ordering can be proved relatively easily by

   982 example actually $v_3 \posix_r v_1$!

   950 induction.

   983 

   984 Sulzmann and Lu ``fix'' this problem by weakening the

   985 transitivity property. They require in addition that the

   986 underlying strings are of the same length. This excludes the

   987 counter example above and any counter-example we could find

   988 with our implementation. Thus the transitivity lemma in

   989 \cite{Sulzmann2014} is:

   990 

   991 \begin{property}

   992 Suppose $v_1 : r$, $v_2 : r$ and 

   993 $v_3 : r$, and also $|v_1|=|v_2|=|v_3|$.\\

   994 If $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$

   995 then $v_1 \posix_r v_3$.

   996 \end{property}

   997 

   998 \noindent While we agree with Sulzmann and Lu that this

   999 property probably holds, proving it seems not so

  1000 straightforward. Sulzmann and Lu do not give an explicit proof

  1001 of the transitivity property, but give a closely related

  1002 property about the existence of maximal elements. They state

  1003 that this can be verified by an induction on $r$. We disagree

  1004 with this as we shall show next in case of transitivity.

  1005 

  1006 The case where the reasoning breaks down is the sequence case,

  1007 say $r_1\,r_2$. The induction hypotheses in this case

  1008 are

  1009 

  1010 \begin{center}

  1011 \begin{tabular}{@ {}cc@ {}}

  1012 \begin{tabular}{@ {}ll@ {}}

  1013 IH $r_1$:\\

  1014 $\forall v_1, v_2, v_3.$ 

  1015   & $\vdash v_1 : r_1\;\wedge$\\

  1016   & $\vdash v_2 : r_1\;\wedge$\\

  1017   & $\vdash v_3 : r_1\;\wedge$\\

  1018   & $|v_1|=|v_2|=|v_3|\;\wedge$\\

  1019   & $v_1 \posix^{r_1} v_2\;\wedge\; v_2 \posix^{r_1} v_3$\medskip\\

  1020   & $\;\;\Rightarrow v_1 \posix^{r_1} v_3$

  1021 \end{tabular} &

  1022 \begin{tabular}{@ {}ll@ {}}

  1023 IH $r_2$:\\

  1024 $\forall v_1, v_2, v_3.$ 

  1025   & $\vdash v_1 : r_2\;\wedge$\\

  1026   & $\vdash v_2 : r_2\;\wedge$\\

  1027   & $\vdash v_3 : r_2\;\wedge$\\

  1028   & $|v_1|=|v_2|=|v_3|\;\wedge$\\

  1029   & $v_1 \posix^{r_2} v_2\;\wedge\; v_2 \posix^{r_2} v_3$\medskip\\

  1030   & $\;\;\Rightarrow v_1 \posix^{r_2} v_3$

  1031 \end{tabular}

  1032 \end{tabular}

  1033 \end{center} 

  1034 

  1035 \noindent

  1036 We can assume that 

  1037 

  1038 \begin{equation}

  1039 (v_{1l}, v_{1r}) \posix^{r_1\,r_2} (v_{2l}, v_{2r})

  1040 \qquad\textrm{and}\qquad

  1041 (v_{2l}, v_{2r}) \posix^{r_1\,r_2} (v_{3l}, v_{3r})

  1042 \label{assms}

  1043 \end{equation}

  1044 

  1045 \noindent

  1046 hold, and furthermore that the values have equal length, 

  1047 namely:

  1048 

  1049 \begin{equation}

  1050 |(v_{1l}, v_{1r})| = |(v_{2l}, v_{2r})|

  1051 \qquad\textrm{and}\qquad

  1052 |(v_{2l}, v_{2r})| = |(v_{3l}, v_{3r})|

  1053 \label{lens}

  1054 \end{equation}

  1055 

  1056 \noindent

  1057 We need to show that

  1058 

  1059 \[

  1060 (v_{1l}, v_{1r}) \posix^{r_1\,r_2} (v_{3l}, v_{3r})

  1061 \]

  1062 

  1063 \noindent holds. We can proceed by analysing how the

  1064 assumptions in \eqref{assms} have arisen. There are four

  1065 cases. Let us assume we are in the case where

  1066 we know 

  1067 

  1068 \[

  1069 v_{1l} \posix^{r_1} v_{2l}

  1070 \qquad\textrm{and}\qquad

  1071 v_{2l} \posix^{r_1} v_{3l}

  1072 \]

  1073 

  1074 \noindent and also know the corresponding typing judgements.

  1075 This is exactly a case where we would like to apply the

  1076 induction hypothesis IH~$r_1$. But we cannot! We still need to

  1077 show that $|v_{1l}| = |v_{2l}|$ and $|v_{2l}| = |v_{3l}|$. We

  1078 know from \eqref{lens} that the lengths of the sequence values

  1079 are equal, but from this we cannot infer anything about the

  1080 lengths of the component values. Indeed in general they will

  1081 be unequal, that is 

  1082 

  1083 \[

  1084 |v_{1l}| \not= |v_{2l}|  

  1085 \qquad\textrm{and}\qquad

  1086 |v_{1r}| \not= |v_{2r}|

  1087 \]

  1088 

  1089 \noindent but still \eqref{lens} will hold. Now we are stuck,

  1090 since the IH does not apply. Sulzmann and Lu overlook this

  1091 fact and just apply the IHs. Obviously nothing which a 

  1092 theorem prover allows us to do.

  1093