[Agda] Bezonas helpon !

[Serge Leblanc]

Thank you for your help.

Why Agda refuses the following  structurally decreasing function?

foldl″ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldl″ c (n ∷ []) = n
foldl″ c (n ∷ (x ∷ xs)) = foldl″ c (c n x ∷ xs)

/home/serge/agda/Maximal.agda:47,1-49,50 Termination checking failed for
the following functions: foldl″ Problematic calls: foldl″ c (c n x ∷ xs)
(at /home/serge/agda/Maximal.agda:49,27-33)

On 2017-08-14 20:55, Ulf Norell wrote:
> The fact that foldr₁ is using a private recursive helper function will
> likely make it impossible to prove your theorem.
>
> / Ulf
>
> On Mon, Aug 14, 2017 at 6:47 PM, Jesper Cockx <Jesper at sikanda.be
> <mailto:Jesper at sikanda.be>> wrote:
>
>     Maybe you can explain what approaches you have already tried and
>     why you got stuck? I think people would be more inclined to help
>     that way.
>
>     To get you started on proof1, here's a hint: since you are proving
>     something about the functions foldr₁ and _⊔_, you can take a look
>     at their definitions and follow the same structure for your proof.
>     For example, since foldr₁ is defined in terms of the helper
>     function foldr, you probably also need to define a helper lemma
>     that proves a similar statement about foldr.
>
>     Best regards,
>     Jesper
>
>     2017-08-14 18:33 GMT+02:00 Serge Leblanc <33dbqnxpy7if at gmail.com
>     <mailto:33dbqnxpy7if at gmail.com>>:
>
>         Saluton, neniu bonvolas helpi min?
>
>         Hi, nobody wants to help me?
>
>
>         On 2017-08-06 18:23, Serge Leblanc wrote:
>>         Dear All,
>>         I need help to finish these lemmas.
>>         They have the same meaning, I am right?
>>         All helpers are welcome!
>>
>>         Estimata ĉiuj,
>>         Mi bezonas helpon por daŭrigi ci-tiuj pruvojn!
>>         Ĉu ili havas je la saman signifon! Ĉu mi pravas?
>>         Ĉiuj helpantoj estas bonvenaj!
>>
>>         Sincere.
>>         -- 
>>         Serge Leblanc
>>         ------------------------------------------------------------------------
>>         gpg --search-keys 0x67B17A3F
>>         Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>
>         -- 
>         Serge Leblanc
>         ------------------------------------------------------------------------
>         gpg --search-keys 0x67B17A3F
>         Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>         https://lists.chalmers.se/mailman/listinfo/agda
>         <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>
>

-- 
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170816/7fa80c78/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170816/7fa80c78/attachment.sig>