[Agda] Bezonas helpon !

[Sergei Meshveliani]

On Thu, 2017-08-17 at 21:02 +0300, Sergei Meshveliani wrote:
> On Thu, 2017-08-17 at 12:18 +0200, Serge Leblanc wrote:
> 
> > [..]
> > Andreas, unfortunately I really don't understand your explanation of
> > the /length/ of the list!
> 
> 
> Concerning using  (length xs)  in addition to  xs : List C:
> 
> as to me, I sometimes I use  (length xs)  as a counter that helps to
> prove termination for some functions on  List C.
> For example, Agda did not see termination in my merge sorting. So I use
> the counter (cnt): 
> 
> --------------------------------------------------------------------
> sort : (xs : List C) → SortRes xs
> sort xs =
>         aux xs (length xs) (≤n-refl PE.refl)
>   where
>   aux : (xs : List C) → (cnt : ℕ) → length xs ≤n cnt → SortRes xs
> 
>   -- The counter  cnt  is used for termination proof.
> 
>   aux []       _ _ = sortRes [] nil (=ms-refl {∅})
>   aux (x ∷ []) _ _ = sortRes (x ∷ []) (single x)
>                                         (=ms-refl {singleMS (x , 1)})
> 
>   aux (_ ∷ _ ∷ zs) 0 2+|zs|≤0 =  ⊥-elim $ ≤→≯ 2+|zs|≤0 2+|zs|>0
>                                  where
>                                  2+|zs|>0 : 2 + (length zs) >n 0
>                                  2+|zs|>0 = suc>0
> 
>   aux (x ∷ y ∷ zs) (suc cnt) |x:y:zs|≤scnt =
>     let
>       (sortRes lList ord-lList toMS-ls=ms=toMS-lList) =
>                                                    aux ls cnt |ls|≤cnt
>       ...
>       ...
>     in
>     sortRes ys ord-ys <x:y:zs>=ms=<ys>
> --------------------------------------------------------------------
> 
> The counter steps from  (suc cnt)  to  cnt,  and it always holds

> (length currentList) ≤ (length currentList).


Improvement:  (length currentList) ≤ current-cnt. 



> This helps Agda to see termination.
> 
> For some reason (unknown to me) Agda easier sees termination when the
> argument is built by the  suc  constructor rather than _∷_. 
> 
> ------
> Sergei
> 
>  
> > > 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
> > _______________________________________________
> > 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