[Agda] Bezonas helpon !

[Serge Leblanc]

Bedaŭrinde, tio maltrafas.  Agda ne vidas la malkreskanton de la listo
malgraŭ la ampleksa ordono eĉ ĝis 15 !

Unfortunately this fails, Agda doesn't see the descent of the list
despite the command even up to 15 !

Sincere,

On 2017-08-16 22:53, Sergei Meshveliani wrote:
> I would try to call  
>                agda --termination-depth=2 Foo.agda  
>
> Maybe, this will help Agda to see that  (x ∷ xs)  is less than 
> (n ∷ (x ∷ xs)).
>
> ------
> Sergei
>
>
> On Wed, 2017-08-16 at 22:23 +0200, 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>
>>> 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>:
>>>         
>>>                 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
>>>                 https://lists.chalmers.se/mailman/listinfo/agda
>>>                 
>>>         
>>>         
>>>         
>>>         _______________________________________________
>>>         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
>> _______________________________________________
>> 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/7b728c5f/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/7b728c5f/attachment.sig>