pigworker / cs410-17 Goto Github PK

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!

My github-fu isn't strong, so hopefully opening an issue as means of communication isn't in bad taste.

In lecture six (actually, at the end of lecture five, if you take the bite and try to implement it yourself), the last equation of findSplit makes you experience first-hand why the order of equations matters.

While following along with the lecture(s) I noticed that the last defining equation of _>[_]<_ gets highlighted in white for me. Since I had no idea what this meant (and after restarting the editor twice), I followed the instructions on the Agda Wiki on how to configure agda-mode highlighting, I saw that this particular color seems to be chosen for catchall-clauses, which - although I'm no expert - seems suspiciously related to me.

I use spacemacs in console-mode by the way, which because of the dark background makes this warning really stick out for me.

So it appears that Agda might be able to warn about these kind of issues, it might have actually been doing so in your case as well, but you didn't see it because of the peculiar choice of default colou for highlighting. I wonder if there is a -Wall kind of configuration to make these things more explicit with a textual message?

Anyway, thanks for making this course available online. Written tutorials don't capture what it means to "think like an Agdaist" in the same way.

Doing exercise 1 I found this warning:

/Volumes/Dev/Programming/Proof/Agda/exercises/CS410-2017/course/exercises/CS410-Prelude.agda:173,1-26
Builtin CONS no longer exists. It is now bound by BUILTIN LIST
when checking the pragma BUILTIN CONS _,-_

/Volumes/Dev/Programming/Proof/Agda/exercises/CS410-2017/course/exercises/CS410-Prelude.agda:172,1-23
Builtin NIL no longer exists. It is now bound by BUILTIN LIST
when checking the pragma BUILTIN NIL []

I'll continue as it is just a warning and try to fix later when I get better.