There are a few ways we can answer this, starting in with the most pedantic let's construct the proof tree and then see if we can come up with a counter example, we consider the following hoare triple:
\[
\{i = 1\}\ a[i] := 3; a[1] := 2\ \{a[i] = 3\}
\]
By the sequence and precondition strengthening rule we have that
Of note here we are deriving \(i = 1\) through the following implications:
\[
Q[a[i] \mapsto 3] \equiv (a[i] = 3)[a[i] \mapsto 3] \equiv (3 = 3) \equiv \top
\]
Where we know that \(i = 1 \to \top \) so we can use precondition strengthening to use \(i = 1\) as our precondition since it implies something we've already syntactically demonstrated to be provable.
Clearly we have that the first assignment in the sequence holds by the naive assignment, same for the second assignment \(a[1] = 2\) since it precondition reduces to the tautology \(\top \), so the final rule is then derivable. But we can obviously see that it erroneously assumes that \(i\) represents some kind of distinct index but, we can see that in the second assignment its aliased by the constant index \(1\) which means that while we can derive the rule it is not semantically valid hence unsound.
To compare this with the correct rule we have that:
Now again let's try to derive the hoare triple we want to prove correct:
To derive we want to find some assertion \(R\), applying the correct assignment rule to the second assignment we define \(R\) as.
\[
R \equiv (a[i] := 3)[a \mapsto a \langle 1 \lhd 2 \rangle ]
\]
we can think of this as defining the function:
\[
a'(j) = \begin {cases}
2 & \texttt {if}\ j = 1 \\
a(j) & \text {otherwise}
\end {cases}
\]
we can then do a case split on the equality \(i = 1\) using our defined function
-
If \(i = 1\) then we have
\[
a'[i] = a[1] = 2 \to a'[i] = 3 \equiv 2 = 3 \equiv \bot
\]
-
If \(i \ \mathrlap {\,/}{=}\ 1\) we have
\[
a'[i] = a[i] \to a'[i] = 3 \equiv a[i] = 3
\]
Since it clearly must be the case that \(i \ \mathrlap {\,/}{=}\ 1\) it implies that our assertion \(R\) is equivalent to:
\[
R \equiv (i \ \mathrlap {\,/}{=}\ 1\land a[i] = 3)
\]
Now testing this rule on the first hoare triple:
\[
\{i = 1\}\ a[i] := 3\ \{i \ \mathrlap {\,/}{=}\ 1\land a[i] = 3\}
\]
By the assignment rule we must somehow be able to derive \(i = 1\) from the following:
\[
R[a \mapsto a \langle i \lhd 3 \rangle ]
\]
substituting in our \(R\) we get
\[
(i \ \mathrlap {\,/}{=}\ 1\land a[i] = 3)[a \mapsto a \langle i \lhd 3 \rangle ]
\]
after a reduction we have
\[
(i \ \mathrlap {\,/}{=}\ 1 \land \underbrace {(a \langle i \lhd 3 \rangle [i] = 3)}_{\top })
\]
simplifying this we get
\[
(i \ \mathrlap {\,/}{=}\ 1)
\]
Which is where the crux of our issue lies, the precondition of our Hoare triple was \(i = 1\), but clearly here to derive our sequence of assignments we must have that i is not 1, hence this hoare triple is not derivable as its also clearly not valid.
A simpler approach at establishing the same idea is by just directly working backwards
\[
\begin {align}
a \langle 1 \lhd 2 \rangle [i] & = 3 \\
a \langle i \lhd 3 \rangle \langle 1 \lhd 2 \rangle [i] & = 3
\end {align}
\]
so first we substitute \(a\) for the assignment \(a[1] := 2\), then we update it for the assignment \(a[i] := 3\), then our precondition would imply that:
\[
i = 1 \to a \langle i \lhd 3 \rangle \langle 1 \lhd 2 \rangle [i] = 3
\]
We indeed cannot derive the triple with the precondition, as it should be trivially apparent that if \(i = 1\) after overwriting with \(a[1] = 2\) we clearly cannot have \(a[1] = 3\).