[Agda] Bezonas helpon !

[Serge Leblanc]

Sinceran dankon Andreas.

I don't understand that the following function (foldr″) is well accepted
while foldl″ is not?
Mi ne komprenas kial la sekva funkcio (foldr″) trafas kvankam la
funkciofoldl″ maltrafas?

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

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)

Termination checking failed for the following functions: foldl″

I also remarked that Agda rejects that:
Mi ankaŭ remarkis ke agda malakceptas tion:

foldr‴  : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldr‴ c (n ∷ []) = n
foldr‴ c (n ∷ (x ∷ xs)) = c x (foldr‴ c (*id* n ∷ xs))
   where
    open import Function using (id)

Termination checking failed for the following functions:foldr‴

Andreas,unfortunately I really don't understand your explanation of the
/length/ of the list!
Andreas, bedaûrinde mi vere ne komprenis vian klarigon pri la grandeco
de la listo!


On 2017-08-16 22:54, Andreas Abel wrote:
> The function is structurally recursive on the /length/ of the list,
> not on the list itself.  You can expose the length by
>
>   1. using vectors instead of lists, or
>   2. using sized lists (sized types).
>
> Alternatively, you can just define an auxiliary function first which
> takes the first element of List+ as separate argument.  Then the
> recursion on the list goes through.
>
> Best,
> Andreas
>
> On 16.08.2017 22:23, Serge Leblanc wrote:
>> 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
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> 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/20170817/035fd136/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/20170817/035fd136/attachment.sig>