[Agda] Path to success with Agda?

[William DeMeo]

I feel your pain.  I started learning Agda on a number of occasions, only
to put it aside having made no discernible progress.  It wasn't until the
third time I tried that I actually succeeded.

What finally clicked for me was Martin Escardo's course Introduction to
Univalent Foundations in Agda
<https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/>.  Imho, it
achieves the perfect balance between Agda basics/background and interesting
mathematics that I wanted to learn about for its own sake.  After working
through the course, the main Agda idioms (and Martin's style) were firmly
implanted in my brain and I could prove pretty much whatever I wanted after
that.

Martin structures proofs in a uniform and elementary way that makes them
easy to learn.  Moreover, he is skilled at avoiding parts of the language
that might cause difficulties or confusion. Martin's course---as well as
our own agda-algebras library, ualib.org (shameless plug 😊)---support the
claim that you don't really need `with`, or the K axiom for that matter, to
prove many deep theorems with Agda.

Good luck and don't give up!

Sincerely,
William



[image: NJIT logo] <https://www.njit.edu/> *William DeMeo, PhD*
Senior University Lecturer in Computer Science
Ying Wu College of Computing
wjd at njit.edu <william.demeo at njit.edu> • williamdemeo.org • (516)912-3162
<5169123162>


On Mon, Aug 29, 2022 at 5:50 PM Jason Hu <fdhzs2010 at hotmail.com> wrote:

> Indeed, pattern matching in Agda is very powerful, often more powerful
> than expected if you come from Coq, but usually the complete opposite if
> you just follow your nose. I think you fall into the latter case.
>
>
>
> If you ignore some bugs in the pattern matcher (which you might well bump
> into), from my learning experience, I think it is the best to learn why
> Agda refuses your pattern by writing out a helper function supposedly
> generated by the pattern matcher and with-patterns; recall that this is
> also how Agda handles it after all (at least this is how the doc phrases
> it). By writing a helper out, you might obtain some information about why
> Agda rejects you, or you might just succeed. The latter case could mean
> that you just phrased a smarter helper than Agda could, or you worked
> around an Agda bug.
>
>
>
> To answer your questions directly, if a case split fails, it is likely
> that the variable you are splitting is depended on by some other type,
> which triggers some further mechanisms that eventually fails the case
> split. Another common possibility is that you turned on without-K, but your
> case split effectively is doing that. This case can be checked by observing
> whether a case split will cause unification of the same variable.
>
>
>
> If your with-pattern fails, it could mean that you are not generalizing
> enough. For example, if you are with-patterning a term of type (foo bar)
> and it fails, it might be fixed by generalizing bar before (foo bar), which
> causes both bar and (foo bar) being abstracted and thus making the
> Typechecker happy.
>
>
>
> In general, I don’t think you need to read anybody’s thesis to have a
> high-level impression on how to please Agda. However, having experience in
> another proof assistant or type theory in general definitely helps. If you
> have more questions I think many can answer you if you ask here.
>
>
>
> Thanks,
>
> Jason
>
>
>
> *From: *Ignat Insarov <kindaro at gmail.com>
> *Sent: *Monday, August 29, 2022 5:12 PM
> *To: *agda at lists.chalmers.se
> *Subject: *[Agda] Path to success with Agda?
>
>
>
> Hello!
>
> I have been trying to learn Agda time and again and I have not made much
> headway
> yet. Once I stray a little aside from the happy path of _Programming
> Language
> Foundations with Agda_, things start to get sour. Even the exercises in
> the book
> give me a hard time whenever they let me a little freedom to get myself
> lost.
>
> * You cannot always make cases for a given parameter. If you want to
> understand
>   when you can and cannot make cases for a parameter, you have to read a
> thesis
>   of the person that has written the pattern matching code.
>
> * You cannot always have a with-abstraction — sometimes the auxiliary
> functions
>   it compiles to do not type check. If you want to understand when you can
> and
>   cannot make a with-abstraction, you only have the language reference to
> help
>   you out, and it does not explain the problem in enough detail.
>
> But there is nothing in the language to help me write proofs but pattern
> matching and with-abstractions!
>
> My first language is Haskell and it was a bit hard to learn, but there was
> the
> amazing community to support my efforts. With Agda, the main venue seems
> to be
> the Zulip chat, but it is more dead than alive. No one is rushing to
> explain
> anything to me.
>
> I have no problem learning Type Theory by itself, since there are great
> books
> out there. Σ types, eliminators, you name it — no problem. My problem
> seems to
> be rooted in the technical difficulties that are specific to Agda — the
> pattern
> matching algorithm and the ill-typed with-abstractions.
>
> Are there any success stories from people that did not learn Agda as a
> student
> with the people that have written Agda itself or do research in Type
> Theory with
> Agda or something to that end? I can see how someone might get good with
> Agda if
> one is near to an expert, but doing it on my own seems to be a hard task.
> Ars
> longa, vita brevis! What is the path I should take so that I get to write
> realistic proofs and still have time left to enjoy the success?
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220829/8b2d4649/attachment.html>