[Agda] Bezonas helpon !

[Sergei Meshveliani]

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).
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