[Agda] Bezonas helpon !

[Andreas Abel]

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
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/