<div dir="ltr">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.<div><br></div><div>What finally clicked for me was Martin Escardo's course <a href="https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/">Introduction to Univalent Foundations in Agda</a>. 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.</div><div><br></div><div>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, <a href="http://ualib.org">ualib.org</a> (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.</div><div><br></div><div>Good luck and don't give up!</div><div><br></div><div>Sincerely,</div><div>William</div><div><br></div><div><br></div><div><br></div><div><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><table style="border-collapse:collapse;width:525px;border-spacing:0px;background-color:transparent;color:rgb(35,38,54);font-family:Poppins,sans-serif;font-size:16px"><tbody style="border:0px;padding:0px;font-size:0.9em"><tr><td style="padding:5px;font-size:0.9em;font-stretch:normal;line-height:1.5;color:rgb(255,0,0);border-width:0px 3px 0px 0px;border-bottom-style:initial;border-bottom-color:initial;border-top-style:initial;border-right-style:solid;border-left-style:initial;border-top-color:initial;border-right-color:rgb(204,0,0);border-left-color:initial;width:180px;vertical-align:middle"><a href="https://www.njit.edu/" style="background-color:transparent;color:rgb(204,0,0)" target="_blank"><img src="https://assets.njit.edu/uicomponents/NJIT-email-logo.png" alt="NJIT logo" style="border:0px;display:block;vertical-align:middle;width:150px;height:auto;max-width:150px"></a></td><td style="padding:5px 5px 5px 10px;font-size:12px;font-stretch:normal;line-height:16px;border:0px;font-family:Arial,Helvetica,sans-serif"><strong style="color:rgb(111,111,111);font-size:13px!important">William DeMeo, PhD</strong><br><font color="#6f6f6f">Senior University Lecturer in Computer Science</font><br><font color="#6f6f6f">Ying Wu College of Computing</font><br><a href="mailto:william.demeo@njit.edu" style="color:rgb(204,0,0);background-color:transparent" target="_blank">wjd@njit.edu</a><font color="#6f6f6f"> • </font><a href="http://williamdemeo.org" target="_blank"><font color="#cc0000">williamdemeo.org</font></a><font color="#6f6f6f"> </font>• <a href="tel:5169123162" style="background-color:transparent" target="_blank"><font color="#cc0000">(516)912-3162</font></a><font color="#6f6f6f"><br></font></td></tr></tbody></table></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Aug 29, 2022 at 5:50 PM Jason Hu <<a href="mailto:fdhzs2010@hotmail.com">fdhzs2010@hotmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="gmail-msg-6665827654027889481">
<div lang="EN-US" style="overflow-wrap: break-word;">
<div class="gmail-m_-6665827654027889481WordSection1">
<p class="MsoNormal">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.
</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">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.</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">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.</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">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.</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">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.</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Thanks,<u></u><u></u></p>
<p class="MsoNormal">Jason<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<div style="border-right:none;border-bottom:none;border-left:none;border-top:1pt solid rgb(225,225,225);padding:3pt 0in 0in">
<p class="MsoNormal" style="border:none;padding:0in"><b>From: </b><a href="mailto:kindaro@gmail.com" target="_blank">Ignat Insarov</a><br>
<b>Sent: </b>Monday, August 29, 2022 5:12 PM<br>
<b>To: </b><a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a><br>
<b>Subject: </b>[Agda] Path to success with Agda?</p>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Hello!<br>
<br>
I have been trying to learn Agda time and again and I have not made much headway<br>
yet. Once I stray a little aside from the happy path of _Programming Language<br>
Foundations with Agda_, things start to get sour. Even the exercises in the book<br>
give me a hard time whenever they let me a little freedom to get myself lost.<br>
<br>
* You cannot always make cases for a given parameter. If you want to understand<br>
when you can and cannot make cases for a parameter, you have to read a thesis<br>
of the person that has written the pattern matching code.<br>
<br>
* You cannot always have a with-abstraction — sometimes the auxiliary functions<br>
it compiles to do not type check. If you want to understand when you can and<br>
cannot make a with-abstraction, you only have the language reference to help<br>
you out, and it does not explain the problem in enough detail.<br>
<br>
But there is nothing in the language to help me write proofs but pattern<br>
matching and with-abstractions!<br>
<br>
My first language is Haskell and it was a bit hard to learn, but there was the<br>
amazing community to support my efforts. With Agda, the main venue seems to be<br>
the Zulip chat, but it is more dead than alive. No one is rushing to explain<br>
anything to me.<br>
<br>
I have no problem learning Type Theory by itself, since there are great books<br>
out there. Σ types, eliminators, you name it — no problem. My problem seems to<br>
be rooted in the technical difficulties that are specific to Agda — the pattern<br>
matching algorithm and the ill-typed with-abstractions.<br>
<br>
Are there any success stories from people that did not learn Agda as a student<br>
with the people that have written Agda itself or do research in Type Theory with<br>
Agda or something to that end? I can see how someone might get good with Agda if<br>
one is near to an expert, but doing it on my own seems to be a hard task. Ars<br>
longa, vita brevis! What is the path I should take so that I get to write<br>
realistic proofs and still have time left to enjoy the success?<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></blockquote></div>