<div dir="ltr"><div>Since a lot of this discussion is around pattern matching, you may find this interview with Jesper Cocx helpful: <br><br><a href="https://www.typetheoryforall.com/2022/04/02/16-Agda,-K-Axiom,-HoTT,-Rewrite-Theory-(Jesper-Cockx).html#c359641b">https://www.typetheoryforall.com/2022/04/02/16-Agda,-K-Axiom,-HoTT,-Rewrite-Theory-(Jesper-Cockx).html#c359641b</a><br><br></div><div>Best,<br></div><div>Pedro Abreu.<br></div><div><br>On Tue, Aug 30, 2022 at 7:00 AM <<a href="mailto:agda-request@lists.chalmers.se">agda-request@lists.chalmers.se</a>> wrote:<br>><br>> Send Agda mailing list submissions to<br>>         <a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><br>><br>> To subscribe or unsubscribe via the World Wide Web, visit<br>>         <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>> or, via email, send a message with subject or body 'help' to<br>>         <a href="mailto:agda-request@lists.chalmers.se">agda-request@lists.chalmers.se</a><br>><br>> You can reach the person managing the list at<br>>         <a href="mailto:agda-owner@lists.chalmers.se">agda-owner@lists.chalmers.se</a><br>><br>> When replying, please edit your Subject line so it is more specific<br>> than "Re: Contents of Agda digest..."<br>><br>><br>> Today's Topics:<br>><br>>    1. Re: Path to success with Agda? (Andrew Pitts)<br>>    2. Re: Path to success with Agda? (Mi?tek Bak)<br>>    3. Re: Path to success with Agda? (Andrew Pitts)<br>>    4. Re: Path to success with Agda? (<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>)<br>><br>><br>> ----------------------------------------------------------------------<br>><br>> Message: 1<br>> Date: Tue, 30 Aug 2022 08:58:14 +0100<br>> From: Andrew Pitts <<a href="mailto:Andrew.Pitts@cl.cam.ac.uk">Andrew.Pitts@cl.cam.ac.uk</a>><br>> To: Ignat Insarov <<a href="mailto:kindaro@gmail.com">kindaro@gmail.com</a>>,  "<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>"<br>>         <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br>> Subject: Re: [Agda] Path to success with Agda?<br>> Message-ID: <<a href="mailto:EB4861D3-C3DE-461D-BAAB-59E2770AF075@cl.cam.ac.uk">EB4861D3-C3DE-461D-BAAB-59E2770AF075@cl.cam.ac.uk</a>><br>> Content-Type: text/plain;       charset=utf-8<br>><br>><br>> > On 30 Aug 2022, at 00:02, Ignat Insarov <<a href="mailto:kindaro@gmail.com">kindaro@gmail.com</a>> wrote:<br>> ><br>> > Cool, let us dig in!<br>><br>> Personally, Agda?s implementation of dependent pattern matching was what got me using Adga rather than Coq when I first needed to use one of these systems (Lean was not an option at the time). Stick with it ? it?s great, honestly.<br>><br>> But I sympathise about your problems with ?with? (and was interested to read Peter Hancock?s confession). It can be very annoying in the middle of a big proof to try to work around why a particular use of ?with? won?t type check.<br>><br>> So I wanted to mention the humble ?case? expression, which functional programmers can more easily relate to, maybe. It?s less powerful that ?with?, but sometimes works (wrt the not typechecking thing) when ?with? won?t.<br>><br>> It?s not a built-in, so one is just disguising ?ordinary? Type Theory with some user-defined syntax. For example, defining<br>><br>> open import Agda.Primitive public<br>> case :<br>>   {l m : Level}<br>>   {A : Set l}<br>>   {B : A ? Set m}<br>>   (x : A)<br>>   (f : (x : A) ? B x)<br>>   ? -----------------<br>>   B x<br>> case x f  = f x<br>><br>> then the first example of ?with? at <<a href="https://agda.readthedocs.io/en/latest/language/with-abstraction.html">https://agda.readthedocs.io/en/latest/language/with-abstraction.html</a>> becomes<br>><br>> open import Agda.Builtin.Bool public<br>> open import Agda.Builtin.List public<br>> filter : {A : Set} ? (A ? Bool) ? List A ? List A<br>> filter p [] = []<br>> filter p (x ? xs) = case (p x) \{<br>>   true  ? x ? filter p xs ;<br>>   false ? filter p xs     }<br>><br>> (of course you can write ? rather than \ if you prefer).<br>><br>> Andy<br>><br>><br>><br>><br>><br>><br>><br>><br>> ------------------------------<br>><br>> Message: 2<br>> Date: Tue, 30 Aug 2022 10:29:47 +0200<br>> From: Mi?tek Bak <<a href="mailto:mietek@bak.io">mietek@bak.io</a>><br>> To: Andrew Pitts <<a href="mailto:Andrew.Pitts@cl.cam.ac.uk">Andrew.Pitts@cl.cam.ac.uk</a>><br>> Cc: Ignat Insarov <<a href="mailto:kindaro@gmail.com">kindaro@gmail.com</a>>,  "<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>"<br>>         <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br>> Subject: Re: [Agda] Path to success with Agda?<br>> Message-ID: <<a href="mailto:02A6748C-8542-4FBF-A059-FADF7BD130A0@bak.io">02A6748C-8542-4FBF-A059-FADF7BD130A0@bak.io</a>><br>> Content-Type: text/plain;       charset=utf-8<br>><br>> > On 30 Aug 2022, at 09:58, Andrew Pitts <<a href="mailto:Andrew.Pitts@cl.cam.ac.uk">Andrew.Pitts@cl.cam.ac.uk</a>> wrote:<br>> ><br>> > So I wanted to mention the humble ?case? expression, which functional programmers can more easily relate to, maybe. It?s less powerful that ?with?, but sometimes works (wrt the not typechecking thing) when ?with? won?t.<br>><br>> It would be interesting to see an example in which `case` works and `with` does not.<br>><br>> --<br>> MB<br>><br>><br>><br>><br>> ------------------------------<br>><br>> Message: 3<br>> Date: Tue, 30 Aug 2022 09:42:55 +0100<br>> From: Andrew Pitts <<a href="mailto:Andrew.Pitts@cl.cam.ac.uk">Andrew.Pitts@cl.cam.ac.uk</a>><br>> To: "<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>>, Mi?tek Bak<br>>         <<a href="mailto:mietek@bak.io">mietek@bak.io</a>><br>> Subject: Re: [Agda] Path to success with Agda?<br>> Message-ID: <<a href="mailto:FA909DCB-11AC-487A-B2B0-0F128A147036@cl.cam.ac.uk">FA909DCB-11AC-487A-B2B0-0F128A147036@cl.cam.ac.uk</a>><br>> Content-Type: text/plain;       charset=utf-8<br>><br>><br>><br>> > On 30 Aug 2022, at 09:29, Mi?tek Bak <<a href="mailto:mietek@bak.io">mietek@bak.io</a>> wrote:<br>> ><br>> >> On 30 Aug 2022, at 09:58, Andrew Pitts <<a href="mailto:Andrew.Pitts@cl.cam.ac.uk">Andrew.Pitts@cl.cam.ac.uk</a>> wrote:<br>> >><br>> >> So I wanted to mention the humble ?case? expression, which functional programmers can more easily relate to, maybe. It?s less powerful that ?with?, but sometimes works (wrt the not typechecking thing) when ?with? won?t.<br>> ><br>> > It would be interesting to see an example in which `case` works and `with` does not.<br>><br>> I have some and will try to extract them from their context when I get a mo. However, I should qualify what I said:<br>><br>>   "but sometimes [case] works (wrt the not typechecking thing) when ?with? won?t?<br>><br>> What I really meant was that, at the time, it was easier for me to use a ?case" expression than to figure out how to still use ?with? by moving lemmas to the top level, generalizing arguments a bit more, etc, etc. I expect there?s always a way with ?with?.<br>><br>> And if you are heavily in to using ?rewrite? (?with? disguised), then I guess ?case? is not helpful.<br>><br>> Andy<br>><br>><br>><br>> ------------------------------<br>><br>> Message: 4<br>> Date: Tue, 30 Aug 2022 11:45:20 +0300<br>> From: <a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a><br>> To: Ignat Insarov <<a href="mailto:kindaro@gmail.com">kindaro@gmail.com</a>><br>> Cc: Jason Hu <<a href="mailto:fdhzs2010@hotmail.com">fdhzs2010@hotmail.com</a>>, <a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><br>> Subject: Re: [Agda] Path to success with Agda?<br>> Message-ID: <<a href="mailto:8aaacc2155a1655df702849f5b15cdf9@scico.botik.ru">8aaacc2155a1655df702849f5b15cdf9@scico.botik.ru</a>><br>> Content-Type: text/plain; charset=UTF-8; format=flowed<br>><br>> Section 1.2 in<br>><br>>    <a href="http://www.botik.ru/pub/local/Mechveliani/docon-A/3.2rc/manual.pdf">http://www.botik.ru/pub/local/Mechveliani/docon-A/3.2rc/manual.pdf</a><br>><br>> has practical advises on how to write proofs in Agda.<br>> I do not know why, but these guidelines help me, and I have managed to<br>> write<br>> many different proofs.<br>> One of the advises is to use a helper function instead of `with',<br>> `case', `let'<br>> -- if they fail to type-check.<br>> And if the helper helps, then one could also consider returning back to<br>> `with' or `case' or `let' with improvements.<br>><br>> ------<br>> Sergei<br>><br>><br>><br>> On 2022-08-30 02:02, Ignat Insarov wrote:<br>> > Cool, let us dig in!<br>> ><br>> >> If you ignore some bugs in the pattern matcher (which you might well<br>> >> bump<br>> >> into), from my learning experience, I think it is the best to learn<br>> >> why Agda<br>> >> refuses your pattern by writing out a helper function supposedly<br>> >> generated by<br>> >> the pattern matcher and with-patterns; recall that this is also how<br>> >> Agda<br>> >> handles it after all (at least this is how the doc phrases it). By<br>> >> writing a<br>> >> helper out, you might obtain some information about why Agda rejects<br>> >> you, or<br>> >> you might just succeed. The latter case could mean that you just<br>> >> phrased a<br>> >> smarter helper than Agda could, or you worked around an Agda bug.<br>> ><br>> > I am all for it, but how do I write such a helper??I tried to follow<br>> > the<br>> > language reference, but it does not make sense.?It reads more like a<br>> > remainder<br>> > for someone who is already familiar with the principles, than as an<br>> > introduction.<br>> ><br>> >> To answer your questions directly, if a case split fails, it is likely<br>> >> that<br>> >> the variable you are splitting is depended on by some other type,<br>> >> which<br>> >> triggers some further mechanisms that eventually fails the case split.<br>> >> Another<br>> >> common possibility is that you turned on without-K, but your case<br>> >> split<br>> >> effectively is doing that. This case can be checked by observing<br>> >> whether a<br>> >> case split will cause unification of the same variable.<br>> ><br>> > What do you mean when you say _?a case split will cause unification of<br>> > the same<br>> > variable?_?<br>> ><br>> >> If your with-pattern fails, it could mean that you are not<br>> >> generalizing<br>> >> enough. For example, if you are with-patterning a term of type (foo<br>> >> bar) and<br>> >> it fails, it might be fixed by generalizing bar before (foo bar),<br>> >> which causes<br>> >> both bar and (foo bar) being abstracted and thus making the<br>> >> Typechecker happy.<br>> ><br>> > What does it mean to _?generalize?_ here??Following your example, how<br>> > would a<br>> > generalized _bar_ look??What does it mean for _bar_ and _foo bar_ to be<br>> > abstracted??How does this help with type checking?<br>> > _______________________________________________<br>> > Agda mailing list<br>> > <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>> > <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>><br>><br>> ------------------------------<br>><br>> Subject: Digest Footer<br>><br>> _______________________________________________<br>> Agda mailing list<br>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>> <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>><br>><br>> ------------------------------<br>><br>> End of Agda Digest, Vol 204, Issue 8<br>> ************************************</div></div>