[Agda] Path to success with Agda?

[mechvel at scico.botik.ru]

Section 1.2 in

   http://www.botik.ru/pub/local/Mechveliani/docon-A/3.2rc/manual.pdf

has practical advises on how to write proofs in Agda.
I do not know why, but these guidelines help me, and I have managed to 
write
many different proofs.
One of the advises is to use a helper function instead of `with', 
`case', `let'
-- if they fail to type-check.
And if the helper helps, then one could also consider returning back to
`with' or `case' or `let' with improvements.

------
Sergei



On 2022-08-30 02:02, Ignat Insarov wrote:
> 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?
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda