<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>Sinceran dankon Andreas.</p>
<span id="result_box" class="" lang="en"><span class="">I don't
understand that the following function (</span></span><span
id="result_box" class="" lang="en"><span class="">foldr″) is well
accepted while </span></span><span id="result_box" class=""
lang="en"><span class="">foldl″ is not?</span></span><br>
<span id="result_box" class="" lang="en"><span class="">Mi ne
komprenas kial la sekva funkcio (</span></span><span
id="result_box" class="" lang="en"><span class="">foldr″) trafas
kvankam la funkcio</span></span><span id="result_box" class=""
lang="en"><span class=""><span id="result_box" class="" lang="en"><span
class=""> </span></span><span id="result_box" class=""
lang="en"><span class="">foldl″</span></span> maltrafas?</span></span>
<p><span id="result_box" class="" lang="en"><span class=""></span></span>foldr″
: ∀ {a} {A : Set a} → (A → A → A) → List⺠A → A<br>
foldr″ c (n ∷ []) = n<br>
foldr″ c (n ∷ (x ∷ xs)) = c x (foldr″ c (n ∷ xs))<br>
</p>
<p><span id="result_box" class="" lang="en"><span class=""> </span></span><span
id="result_box" class="" lang="en"><span class=""> </span></span><span
id="result_box" class="" lang="en"><span class="">foldl″ : ∀ {a}
{A : Set a} → (A → A → A) → List⺠A → A<br>
foldl″ c (n ∷ []) = n<br>
foldl″ c (n ∷ (x ∷ xs)) = foldl″ c (c n x ∷ xs)<br>
</span></span></p>
<p><font color="#3333ff">Termination checking failed for the
following functions: foldl″</font></p>
<span id="result_box" class="short_text" lang="en"><span class="">I
also remarked that Agda rejects that:</span></span><br>
Mi ankaÅ remarkis ke agda malakceptas tion:<br>
<br>
foldr‴ : ∀ {a} {A : Set a} → (A → A → A) → List⺠A → A<br>
foldr‴ c (n ∷ []) = n<br>
foldr‴ c (n ∷ (x ∷ xs)) = c x (foldr‴ c (<b><font color="#990000">id</font></b>
n ∷ xs))<br>
  where<br>
   open import Function using (id)<br>
<font color="#3333ff"><br>
Termination checking failed for the following functions:</font><font
color="#3333ff"> foldr‴ </font><br>
<br>
Andreas,<span id="result_box" class="" lang="en"><span class="">
unfortunately </span></span> I really don't understand your
explanation of the /length/ of the list!<br>
Andreas, bedaûrinde mi vere ne komprenis vian klarigon pri la
grandeco de la listo!<br>
<br>
<br>
<div class="moz-cite-prefix">On 2017-08-16 22:54, Andreas Abel
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:6e6a4b66-40fe-0806-53ad-98cce40bc480@chalmers.se">The
function is structurally recursive on the /length/ of the list,
not on the list itself. You can expose the length by
<br>
<br>
 1. using vectors instead of lists, or
<br>
 2. using sized lists (sized types).
<br>
<br>
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.
<br>
<br>
Best,
<br>
Andreas
<br>
<br>
On 16.08.2017 22:23, Serge Leblanc wrote:
<br>
<blockquote type="cite">Thank you for your help.
<br>
<br>
Why Agda refuses the following structurally decreasing
function?
<br>
<br>
foldl″ : ∀ {a} {A : Set a} → (A → A → A) → List⺠A → A
<br>
foldl″ c (n ∷ []) = n
<br>
foldl″ c (n ∷ (x ∷ xs)) = foldl″ c (c n x ∷ xs)
<br>
<br>
/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)
<br>
<br>
On 2017-08-14 20:55, Ulf Norell wrote:
<br>
<blockquote type="cite">The fact that foldrâ‚ is using a private
recursive helper function will likely make it impossible to
prove your theorem.
<br>
<br>
/ Ulf
<br>
<br>
On Mon, Aug 14, 2017 at 6:47 PM, Jesper Cockx
<<a class="moz-txt-link-abbreviated" href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a> <a class="moz-txt-link-rfc2396E" href="mailto:Jesper@sikanda.be"><mailto:Jesper@sikanda.be></a>>
wrote:
<br>
<br>
   Maybe you can explain what approaches you have already
tried and
<br>
   why you got stuck? I think people would be more inclined
to help
<br>
   that way.
<br>
<br>
   To get you started on proof1, here's a hint: since you are
proving
<br>
   something about the functions foldr₠and _⊔_, you can take
a look
<br>
   at their definitions and follow the same structure for
your proof.
<br>
   For example, since foldr₠is defined in terms of the
helper
<br>
   function foldr, you probably also need to define a helper
lemma
<br>
   that proves a similar statement about foldr.
<br>
<br>
   Best regards,
<br>
   Jesper
<br>
<br>
   2017-08-14 18:33 GMT+02:00 Serge Leblanc
<<a class="moz-txt-link-abbreviated" href="mailto:33dbqnxpy7if@gmail.com">33dbqnxpy7if@gmail.com</a>
<br>
   <a class="moz-txt-link-rfc2396E" href="mailto:33dbqnxpy7if@gmail.com"><mailto:33dbqnxpy7if@gmail.com></a>>:
<br>
<br>
       Saluton, neniu bonvolas helpi min?
<br>
<br>
       Hi, nobody wants to help me?
<br>
<br>
<br>
       On 2017-08-06 18:23, Serge Leblanc wrote:
<br>
<blockquote type="cite">Â Â Â Â Â Â Â Dear All,
<br>
       I need help to finish these lemmas.
<br>
       They have the same meaning, I am right?
<br>
       All helpers are welcome!
<br>
<br>
       Estimata ĉiuj,
<br>
       Mi bezonas helpon por daÅrigi ci-tiuj pruvojn!
<br>
       Ĉu ili havas je la saman signifon! Ĉu mi pravas?
<br>
       Ĉiuj helpantoj estas bonvenaj!
<br>
<br>
       Sincere.
<br>
       --        Serge Leblanc
<br>
      Â
------------------------------------------------------------------------
<br>
       gpg --search-keys 0x67B17A3F
<br>
       Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C
F631 67B1 7A3F
<br>
</blockquote>
<br>
       --        Serge Leblanc
<br>
      Â
------------------------------------------------------------------------
<br>
       gpg --search-keys 0x67B17A3F
<br>
       Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631
67B1 7A3F
<br>
<br>
       _______________________________________________
<br>
       Agda mailing list
<br>
       <a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-rfc2396E" href="mailto:Agda@lists.chalmers.se"><mailto:Agda@lists.chalmers.se></a>
<br>
       <a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
<br>
      Â
<a class="moz-txt-link-rfc2396E" href="https://lists.chalmers.se/mailman/listinfo/agda"><https://lists.chalmers.se/mailman/listinfo/agda></a>
<br>
<br>
<br>
<br>
   _______________________________________________
<br>
   Agda mailing list
<br>
   <a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-rfc2396E" href="mailto:Agda@lists.chalmers.se"><mailto:Agda@lists.chalmers.se></a>
<br>
   <a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
<br>
   <a class="moz-txt-link-rfc2396E" href="https://lists.chalmers.se/mailman/listinfo/agda"><https://lists.chalmers.se/mailman/listinfo/agda></a>
<br>
<br>
<br>
</blockquote>
<br>
--Â <br>
Serge Leblanc
<br>
------------------------------------------------------------------------
<br>
gpg --search-keys 0x67B17A3F
<br>
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
<br>
<br>
<br>
_______________________________________________
<br>
Agda mailing list
<br>
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<br>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
<br>
<br>
</blockquote>
<br>
<br>
</blockquote>
<br>
<div class="moz-signature">-- <br>
Serge Leblanc
<hr>
gpg --search-keys 0x67B17A3F
<br>
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F</div>
</body>
</html>