<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    Does somone have an example of uses All?<br>
    Ĉu iu havas ekzemplon de 'All' uzado?<br>
    <span id="result_box" class="" lang="en"><span class=""><br>
        Thank you very much!</span></span><br>
    Sinceran dankon!<br>
    <br>
    <br>
    <div class="moz-cite-prefix">On 2017-08-27 22:15, Serge Leblanc
      wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:8457c90f-5c98-a477-942a-f9916824133f@gmail.com">
      <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
      <p><span id="result_box" class="" lang="en"><span class=""></span><span
            class=""></span></span>I fail to make the proof. I don't
        understand how built the All structure. Can someone show me?<br>
      </p>
      <p>Mi malsukcesas fari la pruvon. Mi tute ne komprenas kiel oni
        konstruas la structuron All. Ĉu iu povas montri al mi?<br>
      </p>
      <p>Sinceran dankon !<br>
      </p>
      <p><br>
      </p>
      <div class="moz-cite-prefix">On 2017-08-22 17:53, Andreas Abel
        wrote:<br>
      </div>
      <blockquote type="cite"
        cite="mid:6441e3b4-c334-0b50-0e7b-988bf15f40c7@chalmers.se">It
        might be sufficient to prove <br>
        <br>
          max (x :: xs) >= max xs <br>
        <br>
        and use this in your induction hypothesis (with transitivity of
        >=). <br>
        <br>
        Cheers, <br>
        Andreas <br>
        <br>
        On 21.08.2017 08:07, Serge Leblanc wrote: <br>
        <blockquote type="cite">Thank you very much, Andreas, I
          understand more. <br>
          <br>
          Now I have tried to proveproof₁. Surely, I miss because the
          proposition P contains 'xs'. Does anyone have a suggestion?
          Intuitively, I need an induction with 'm≤m⊔n'. <br>
          <br>
          proof₁ : (xs : List⁺ ℕ) → All (_≥_ (max″ xs)) (toList xs) <br>
          proof₁ (h ∷ []) = {! []!} <br>
          proof₁ (h ∷ (x ∷ xs)) = {! (proof₁ (x ∷ xs))!} <br>
          <br>
          Thank you for your help! <br>
          <br>
          Koran dankon, Andreas, mi plibone komprenas. <br>
          <br>
          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>
          <br>
          <br>
          proof₁ : (xs : List⁺ ℕ) → All (_≥_ (max″ xs)) (toList xs) <br>
          proof₁ (h ∷ []) = {! []!} <br>
          proof₁ (h ∷ (x ∷ xs)) = {! (proof₁ (x ∷ xs))!} <br>
          <br>
          Antaŭan dankon pro via venonta helpo ! <br>
          <br>
          Sincere, <br>
          <br>
          <br>
          On 201i7-08-18 13:15, Andreas Abel wrote: <br>
          <blockquote type="cite">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"
                      moz-do-not-send="true">Jesper@sikanda.be</a> <a
                      class="moz-txt-link-rfc2396E"
                      href="mailto:Jesper@sikanda.be"
                      moz-do-not-send="true"><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"
                      moz-do-not-send="true">33dbqnxpy7if@gmail.com</a>
                    <br>
                    <a class="moz-txt-link-rfc2396E"
                      href="mailto:33dbqnxpy7if@gmail.com"
                      moz-do-not-send="true"><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>
          -- <br>
          Serge Leblanc <br>
------------------------------------------------------------------------
          <br>
          gpg --search-keys 0x67B17A3F <br>
          Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1
          7A3F <br>
        </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>
    </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>