[Agda] Path to success with Agda?

[Jason Hu]

A helper function I was referring to includes only the minimal information to finish your proof. Maybe you can try to do this exercise: end all proofs with a function application of some lemmas and these lemmas must not live in the where block of your main lemma. This I can ensure you is achievable.  Then you are forced to think about what are the least required assumptions.

Regarding your second question, without-K is an option that overcomes a historical limitation of dependent pattern matching. I am not capable of explaining what is the effect of K in short sentences, but one such example is when you try to eliminate a term of type x ≡ x. This will fail because it requires to unify x and x. In general, the guiding principle is, when two variables are meant to be equal, use equality, instead of writing the same variable twice.

Generalization just means to include more assumptions. Generalization of arguments is a common proof technique which is frequently seen in, say, induction. You generalize when your induction hypothesis or any assumption in general is not strong enough. Here, it means that the helper function generated by Agda is not general enough to pass typechecking, so your with-pattern fails. Like I suggested, if you can just try to distill the only necessary assumptions of your problem, you will learn much about your problem and Agda.

I first started with Coq and worked with all the minor details of proof term constructions (e.g. through convoy patterns, etc.). Like I said, that gave me a positive shock because the good overwhelmed the bad. If learning Agda is not a must for you, I think it might be better to look at other systems like Lean or Coq, which you might find easier to pick up and could give you another view of type theory, but it’s really up to your background and what you already know. If you try Coq, there is a plugin called Equations which actually implements Agda style with-patterns.

Thanks,
Jason

From: Ignat Insarov<mailto:kindaro at gmail.com>
Sent: Monday, August 29, 2022 7:01 PM
To: Jason Hu<mailto:fdhzs2010 at hotmail.com>
Cc: agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>
Subject: Re: [Agda] Path to success with Agda?

Cool, let us dig in!

> 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.

I am all for it, but how do I write such a helper? I tried to follow the
language reference, but it does not make sense. It reads more like a remainder
for someone who is already familiar with the principles, than as an
introduction.

> 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.

What do you mean when you say _«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.

What does it mean to _«generalize»_ here? Following your example, how would a
generalized _bar_ look? What does it mean for _bar_ and _foo bar_ to be
abstracted? How does this help with type checking?

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220829/8110b8c4/attachment-0001.html>