Question about using the equational reasoning operators.

[mbwgh]

Starting from Lecture 9 or so, some operators are introduced which allow writing a proof in an equational reasoning style. Specifically, I am talking about _=[_>=_, _=<_]=_ and _[QED], the equivalents of which are also found in the Agda Standard Library, defined for different underlying equality definitions (I have no idea about).

However, at least to my knowledge (that is, until the end of Lecture 12), the issue of how to work with these operators in practice wasn't explained, and my search on the interwebs came up empty (I only found a video in french). So, how do you use them?

So far I can think of:

• refactoring an already existing "conventional" Agda proof. Normalization steps then correspond to refl something and rewrites become/are the application of laws. What becomes of a with abstraction then? Or
• trying to work your way from top to bottom, like you would on paper,
• trying to burn the candle from both ends by starting with the left-hand and right-hand side of the Goal and a hole in the middle.

Furthermore, the documentation states that if the equality reasoning primitives are in scope, "then Auto will do equality reasoning using these constructs". I couldn't really get that to work though. Or maybe I did, but I have no idea what the expected behavior is supposed to be.

There are some finished proofs in the lecture and exercise files, all of which are considered either tedious or hairy. Was your usage of equality reasoning necessary, easier than just using pattern-matching/with-abstractions/rewrites etc., or just for documentation purposes?

Any hints would be greatly appreciated!

[mbwgh]

For what it's worth, I asked this question on StackOverflow as well.

[jiangsy]

I am currently trying to solve Ex2, and have some thoughts on this problem

if the goal is x = y,
x =[ (the proof of x=x') >= x' changes the proof to x' = y
and
y' =< (the proof of y=y') ]= y changes the proof to x = y'
you can use the first one only to transform the proof all the way to y = y
or use both to get x = z and z = y in the middle,
the last proof in either case is y [QED]