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