Inference rules for deriving invariants in Hoare logic

Question

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string):

X = S1   
Y = S2

E = true   
// (1) S1 = S2 <=> X = Y and E = true
while X != /\ and Y != /\ and E == true          
  if head(X) == head(Y)           
    X = tail(X)
    Y = tail(Y)
  else
    E = false
// (2) S1 = S2 <=> X = /\ and Y = /\ and E = true
if !(X == /\ and Y == /\)    
  E = false 
  // (3) S1 != S2 and E = false
else // an empty else; just for inserting an assertion (i.e., 3' below) here
  // (3') S1 = S2 <=> E = true
// (4) S1 = S2 <=> E = true
return E

There are five invariants:

(1). $S_1 = S_2 \iff X = Y \land E = true$

(2). $S_1 = S_2 \iff X = \Lambda \land Y = \Lambda \land E = true$

(3). $S_1 \neq S_2 \land E = false$

(3'). $S_1 = S_2 \iff E = true$

(4). $S_1 = S_2 \iff E = true$

I can understand these invariants and how they are derived from the previous ones in an intuitive and thus informal way. For example, we can derive (3') from (2) as follows:

At point (2), we know that $S_1$ equals $S_2$ iff $X = \Lambda \land Y = \Lambda \land E = true$. At point (3'), we further know that $X = \Lambda \land Y = \Lambda$. Thus, at this point, we only need to check whether $E = true$ to decide whether $S_1 = S_2$ holds.

However, the reasoning above cannot be justified by the conventional inference rules of propositional logic by which we would have

$$S_1 = S_2 \iff (X = \Lambda \land Y = \Lambda \land E = true) \land (X = \Lambda \land Y = \Lambda),$$ which is $S_1 = S_2 \iff X = \Lambda \land Y = \Lambda \land E = true.$

---

Problem: What are the inference rules for the derivation from (2) to (3')?

Related Post: Developing invariants for comparing two strings

---

Edit: As pointed out by @chi in the comment, it should be $$\big(S_1 = S_2 \iff (X = \Lambda \land Y = \Lambda \land E = true)\big) \land (X = \Lambda \land Y = \Lambda),$$ which implies (3') $S_1 = S_2 \iff E = true$ as the answer given by @kne shows.

Answer 1

There are two ways to answer the question.

The first is on the level of propositional logic. You have three statements, $S_1=S_2$, $(X=\Lambda\wedge Y=\Lambda)$, and $E=true$. Let's call them $A$, $B$, and $C$ for short. (2) is $A\Leftrightarrow(B\wedge C)$ and (3') is $A\Leftrightarrow C$. At point (3') we know $B$. Every assignment of the propositional variables that satisfies $B$ and (2) also satisfies (3'). In other words, at the position (3') we know

$(A\Leftrightarrow(B\wedge C))\wedge B$

from which

$(A\Leftrightarrow C)$

follows semantically. If the propositional proof system of your choice is complete, the above can also be derived using its rules.

The second answer addresses Hoare logic instead of propositional logic. Hoare logic has its own derivations. The neat thing is that most of them can be automated. And they work backwards. In the case at hand, (3') is derived from (4) by copy. After all, at the end of the else clause, the same invariant must hold as after the if-then-else. The then clause does not follow that rule, so let us fix the code

// (2) S1 = S2 <=> X = /\ and Y = /\ and E = true
// (2') (!(X == /\ and Y == /\) and (S1 = S2 <=> false = true)) or
//    ((X == /\ and Y == /\) and (S1 = S2 <=> E = true))
if !(X == /\ and Y == /\)    
  // (3'') S1 = S2 <=> false = true
  E = false 
  // (3) S1 = S2 <=> E = true
else // an empty else
  // (3') S1 = S2 <=> E = true
// (4) S1 = S2 <=> E = true

Now (3) is derived from (4) by copy, (3'') is derived from (3) by substitution (that is the Hoare logic rule for assignment) and (2') is derived from (3''), (3') and the if condition. It remains to see how (2') follows from (2). That is propositional logic plus $false\not=true$.