"Equational logic" has a fairly specific meaning, while you seem to be vaguely referring to the notion of "equational reasoning" which makes your question not meaningful. If we tried to take your question at face value, we immediately run into issues. Before we can talk about whether computation corresponds to proof in the logic, we'd first need to be able represent Haskell programs as terms in the logic! That can't be done, at least, not in a naive way. To handle binding forms and beta reduction, would require something like nominal/higher-order equational logic or utilizing explicit substitutions. This is just the beginning. Another question is: what do you want to constitute a Haskell program? Haskell is a Church-style language, meaning you need the type information to execute the code, i.e. a Haskell program has no meaning without type information. So does "Haskell program" mean some representation with all type information included, or do you intend to model type inference equationally somehow? Once you figure all that out, you then need some equations for your equational logic, at which point you run into another problem: Haskell has no formal semantics.
Let's step way back. For just plain arithmetic, how do we show that $2+2=1+3$? One answer is that we have an equational logic with equations like $2 = 1+1$, $3=1+(1+1)$, $(x+y)+z=x+(y+z)$, $x+y = y+x$, $0+x = x$. We might prove the equality then by using $2=1+1$ twice to get $(1+1)+(1+1) = 1+3$ then use associativity to get $1+(1+(1+1))$, and then $3 = 1+(1+1)$ to get $1+3 = 1+3$ which is then true by reflexivity. There are many other proofs besides this one that could be formulated. Just given a list of equations gives you no guidance on the proof approach, i.e. which equations to apply when and in which direction. Furthermore, if you fail to find a proof, you don't know if that's just because you weren't clever enough, or if there actually is no proof (i.e. the expressions are not equal). Both of these problems are solved by formulating a notion of "normal form" and a rewrite system that takes any term to its normal form. This is what Knuth-Bendix completion and its successors do1. In this case, each rewrite rule is derived from an equational proof, and the sequence of steps can be interpreted as stitching together these proofs with transitivity.
But this is not what people are thinking when they compute by hand, it's not what your calculator/computer is doing, and it's not even what automated theorem provers/proof assistants are typically doing2. Typically this is turned around: we have an algorithm for addition, and two expressions are considered equal when the algorithm produces the same result for both of them (where "the same" here means syntactically identical). In other words, computation comes first and "equality" is a derived concept.
For arithmetic, one might argue about which perspective is more "fundamental", but for a programming language it's clear computation is the fundamental notion. This computational approach frees us to use any representation of "terms" we want and any algorithmic approach we want as long as it's (ultimately) deterministic. Of course, this presumes that normal forms exist and are computable. For a general programming language, neither statement is true. Computing a normal form is then usually semidecidable, and the "equality" gets weakened to a partial equivalence relation. Most proof assistants avoid this issue by restricting to strongly normalizing languages. Computational Type Theory/NuPRL takes a very different approach. It exposes the operational semantics of its built-in notion of computation and gives the user some control over that computation process, e.g. "perform one beta reduction". We can then define "equality" as $x = y$ iff $x \leadsto^* x'$ and $y\leadsto^* y'$ and $x' =_\alpha y'$ where $\leadsto^*$ is the reflexive, transitive closure of the one-step reduction relation. This captures the previous notion when $x$ and $y$ have normal forms, but it allows equating expressions that lack normal forms as well, as long as they reduce to a common expression. This casts us back into the world where there's no obvious strategy, and we can't in general be sure whether two expression are unequal or we have simply failed to find a proof. That's unavoidable, since this notion of equality is not decidable.
Unsurprisingly, the steps of your "equational proofs" don't directly have to do with equality, but are, instead, sketches of proofs that e.g. $1+(2+1)\leadsto^* 4$ with respect to a hypothetical operational semantics for Haskell.
1 For just checking whether two ground terms are equal, a simpler algorithm called congruence closure can be used.
2 It (or congruence closure) is what most automated theorem provers are doing if you do literally present a series of equations and then ask if two expressions are equal, but not if numbers are built-in nor, more for proof assistants, if you define addition algorithmically. More generally, many proof assistants have built-in notion of computation, and many automated theorem provers heavily rely on decision procedures.
