[Agda] Bezonas helpon !

[Sergei Meshveliani]

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