<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:DengXian;
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:"\@DengXian";
panose-1:2 1 6 0 3 1 1 1 1 1;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-US" link="blue" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<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"><o:p> </o:p></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"><o:p> </o:p></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"><o:p> </o:p></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"><o:p> </o:p></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"><o:p> </o:p></p>
<p class="MsoNormal">Thanks,<o:p></o:p></p>
<p class="MsoNormal">Jason<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div style="mso-element:para-border-div;border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0in 0in 0in">
<p class="MsoNormal" style="border:none;padding:0in"><b>From: </b><a href="mailto:kindaro@gmail.com">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">agda@lists.chalmers.se</a><br>
<b>Subject: </b>[Agda] Path to success with Agda?</p>
</div>
<p class="MsoNormal"><o:p> </o:p></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>
Agda@lists.chalmers.se<br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>