<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p><span id="result_box" class="" lang="en"><span class="">Thank you
          very much, Andreas, I understand more.<br>
        </span></span></p>
    <p><span id="result_box" class="" lang="en"><span class="">Now I
          have tried to prove</span></span><span id="result_box"
        class="" lang="en"><span class=""> proof₁</span></span><span
        id="result_box" class="" lang="en"><span class="">. Surely, I
          miss because the proposition P contains 'xs'. Does anyone have
          a suggestion? </span></span><span id="result_box" class=""
        lang="en"><span class=""><span id="result_box" class=""
            lang="en"><span class="">Intuitively, I need an induction
              with 'm≤m⊔n'.</span></span><br>
          <br>
          proof₁ : (xs : List⁺ ℕ) → All (_≥_ (max″ xs)) (toList xs)<br>
          proof₁ (h ∷ []) = {! []!}<br>
          proof₁ (h ∷ (x ∷ xs)) = {! (proof₁ (x ∷ xs))!}<br>
        </span></span><span id="result_box" class="" lang="en"><span
          class=""><br>
          Thank you for your help!<br>
        </span></span></p>
    <p>Koran dankon, Andreas, mi plibone komprenas.</p>
    Nun, mi provis plenumi la pruvon proof₁. Verŝajne, mi malsukcesas
    pro la propozicio P enhavas 'xs'.<br>
    Ĉu iu havas sugeston ? Intuicie, mi bezonos indukton kun 'm≤m⊔n'.<br>
    <p><br>
      proof₁ : (xs : List⁺ ℕ) → All (_≥_ (max″ xs)) (toList xs)<br>
      proof₁ (h ∷ []) = {! []!}<br>
      proof₁ (h ∷ (x ∷ xs)) = {! (proof₁ (x ∷ xs))!}<br>
      <br>
    </p>
    <p>Antaŭan dankon pro via venonta helpo !</p>
    <p>Sincere,<br>
    </p>
    <br>
    <div class="moz-cite-prefix">On 201i7-08-18 13:15, Andreas Abel
      wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:019d9b69-fa88-390a-2bad-baf9515fac21@chalmers.se">Dear
      Serge,
      <br>
      <br>
      > foldr″ c (n ∷ (x ∷ xs)) = c x (foldr″ c (n ∷ xs))
      <br>
      <br>
      For the structural ord\ering (<), Agda sees that
      <br>
      <br>
        (n :: xs) < (n :: (x :: xs)) iff xs < (x :: xs)
      <br>
      <br>
      The latter holds since xs is a subterm of x :: xs.
      <br>
      <br>
      > foldl″ c (n ∷ (x ∷ xs)) = foldl″ c (c n x ∷ xs)
      <br>
      <br>
      This does not work since c n x is not a subterm of n or x.
      <br>
      <br>
      > foldr‴ c (n ∷ (x ∷ xs)) = c x (foldr‴ c (*id* n ∷ xs))
      <br>
      <br>
      Since Agda does not reduce call arguments during structural
      comparison, this fails, as
      <br>
      <br>
        id n   is not the same as  n
      <br>
      <br>
      (syntactically).
      <br>
      <br>
      > Andreas,unfortunately I really don't understand your
      explanation of the
      <br>
      > /length/ of the list!
      <br>
      <br>
      My explanation was probably wrong.
      <br>
      <br>
      On 17.08.2017 12:18, Serge Leblanc wrote:
      <br>
      <blockquote type="cite">Sinceran dankon Andreas.
        <br>
        <br>
        I don't understand that the following function (foldr″) is well
        accepted while foldl″ is not?
        <br>
        Mi ne komprenas kial la sekva funkcio (foldr″) trafas kvankam la
        funkciofoldl″ maltrafas?
        <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 (n ∷ xs))
        <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>
        Termination checking failed for the following functions: foldl″
        <br>
        <br>
        I also remarked that Agda rejects that:
        <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 (*id* n ∷ xs))
        <br>
            where
        <br>
             open import Function using (id)
        <br>
        <br>
        Termination checking failed for the following functions:foldr‴
        <br>
        <br>
        Andreas,unfortunately 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>
        On 2017-08-16 22:54, Andreas Abel wrote:
        <br>
        <blockquote type="cite">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>
              </blockquote>
            </blockquote>
          </blockquote>
        </blockquote>
      </blockquote>
      <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>