[Agda] Bezonas helpon !

[Andreas Abel]

Dear Serge,

 > foldr″ c (n ∷ (x ∷ xs)) = c x (foldr″ c (n ∷ xs))

For the structural ordering (<), Agda sees that

   (n :: xs) < (n :: (x :: xs)) iff xs < (x :: xs)

The latter holds since xs is a subterm of x :: xs.

 > foldl″ c (n ∷ (x ∷ xs)) = foldl″ c (c n x ∷ xs)

This does not work since c n x is not a subterm of n or x.

 > foldr‴ c (n ∷ (x ∷ xs)) = c x (foldr‴ c (*id* n ∷ xs))

Since Agda does not reduce call arguments during structural comparison, 
this fails, as

   id n   is not the same as  n

(syntactically).

 > Andreas,unfortunately I really don't understand your explanation of the
 > /length/ of the list!

My explanation was probably wrong.

On 17.08.2017 12:18, Serge Leblanc wrote:
> 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

-- 
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/