[Agda] Agda beginner.

[Ulf Norell]

A good rule of thumb is that if you want to prove something about a
function (like hermes),
the proof should follow the same recursion pattern as the function.

/ Ulf

On Mon, Apr 6, 2015 at 7:34 PM, Dmytro Starosud <d.starosud at gmail.com>
wrote:

> If you get stuck using pattern matching on first argument try to split
> using another...
>
> Cheers,
> Dmytro
>
> P.S. actually theorem proving is undecidable in general:-D so you
> shouldn't except to get all the knowledge required for this in one go (and
> even in many;)).
> I would suggest you first just try to repeat some existing profs to become
> familiar with this process.
>
>
>
>
>
> 2015-04-06 12:25 GMT+03:00 Serge Leblanc <33dbqnxpy7if at gmail.com>:
>
>>  Thanks Dmytro, is trivial when x = 0, but I have more difficulty when x
>> > 0.
>>
>> hermes≡hermes' : (x y : ℕ) → hermes x y ≡ hermes' x y
>> hermes≡hermes' zero y = refl (suc y)
>> hermes≡hermes' (suc x) y = { }0   {- ?0 : hermes (suc x) y ≡ hermes' (suc
>> x) y -}
>>
>>
>> On 2015-04-05 14:06, Dmytro Starosud wrote:
>>
>>   Hello Serge,
>>
>>  Now try to partially apply corresponding functions to the arguments
>> you've got after pattern matching.
>>  I.e. Think what would you get hermes x y if x were zero.
>>  And the same for fold.
>>
>>  You can use _ for the right hand side and compile your file to see what
>> you need to place there.
>>
>>  Hope this will help.
>>
>>
>>
>> --
>> Serge Leblanc
>> ------------------------------
>> gpg --keyserver hkp://keyserver.ubuntu.com:11371 --recv-keys 0x67B17A3F
>> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150407/8b2b9d85/attachment.html