How are the equational reasoning operators used in practice?

Question

The Agda Standard Library exports some operators that allow you to write proofs in a manner similar to what you would do on paper, or how it is taught in the Haskell community. While you can write "conventional" Agda proofs in a somewhat systematic manner by refining a Goal using with abstractions, rewrites or helper lemmas as needed, it isn't really clear to me how a proof using the equality reasoning primitives "comes to be".

That is, while you can find examples about what these proofs look like when they are finished and type-check here and there, these already worked examples don't show you how they are developed in a systematic step-by-step (maybe hole-driven) manner.

How is it done in practice? Do people "refactor" an already existing proof? Do you try to "burn the candle from both sides" by starting with the left-hand and right-hand sides of the initial Goal and a hole in the middle?

Furthermore, the Agda documentation states that if the equality reasoning primitives are in scope, "then Auto will do equality reasoning using these constructs". What does that mean?

I would appreciate it if someone could point me in the right direction, or even post an example of how they develop these kinds of proofs step-by-step, what questions they ask themselves as they go through it, where they put the holes and so on. Thanks!

Answer 1

I think it would be more helpful for you to look at the definitions for equational reasoning for Identity here Equational Reasoning. The main point is that it is just a nicer way to apply transitivity chains and allowing the user to see the actual expression in code, rather than the proof evidence which is not that easy to read.

The way I go about building a proof using equational reasoning for any setoid is this. With the example of natural numbers

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
m + zero   = m
m + succ n = succ (m + n)

Let's take commutativity as an example. This is how I start with the goals.

comm+ : ∀ m n → m + n ≡ n + m
comm+ m zero     = {!!}
comm+ m (succ n) =
  begin
    succ (m + n)
  ≡⟨ {!!} ⟩
    succ n + m
  ∎

Now I see the original expression and goal and my goal proof is between the brackets. I work only on the expression leaving the proof objects untouched and add what I think should work.

comm+ : ∀ m n → m + n ≡ n + m
comm+ m zero     = {!!}
comm+ m (succ n) =
  begin
    succ (m + n)
  ≡⟨ {!!} ⟩
    succ (n + m)
  ≡⟨ {!!}⟩
    succ n + m
  ∎

Once I think I have a proof, I work on the proof objects that justify my steps.

Regarding the auto-tactic, you should not bother with that in my opinion. It's not being worked on for a while.