## Operator-based Equational Reasoning

The support for equational reasoning in Isabelle, Lean and Dafny is built into their syntax, while in Liquid Haskell, the operators for equational reasoning can be provided by a library. This is highly inspired by Agda.

Agda is a general theorem prover based on dependent type theory. Its type system and syntax is flexible enough to allow the library-defined operator

  _≡⟨_⟩_ :∀ (x {y z} : A) -> x ≡ y -> y ≡ z -> x ≡ z


which expresses an equality together with its proof. Observe the similarity between Liquid Haskell's (==.) operator.

  a ≡⟨explanation⟩ b     -- Agda
a ==. b ? explanation  -- Liquid Haskell


One disadvantages of the operator-based equational reasoning in Liquid Haskell over built-in support like in, say, Dafny is that there each equation is checked independently, whereas Liquid Haskell checks all equalities in one function at once, which can be slower.

While the above tools allow equational reasoning, Liquid Haskell is unique in extending an existing, general-purpose programming language to support theorem proving. This makes Liquid Haskell a more natural choice for verifying Haskell code, both because it is familiar to Haskell programmers, and because it does not require porting code to a separate verification language.