<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>Bedaŭrinde, tio maltrafas. Agda ne vidas la malkreskanton de la
listo malgraŭ la ampleksa ordono eĉ ĝis 15 !<br>
</p>
<span id="result_box" class="" lang="en"><span class="">Unfortunately
this fails, Agda doesn't see the descent of the list despite the
command even up to 15 !</span></span><span id="result_box"
class="" lang="en"><span class=""><br>
<br>
Sincere,<br>
<br>
</span></span>
<div class="moz-cite-prefix">On 2017-08-16 22:53, Sergei Meshveliani
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:1502916835.4258.5.camel@one.mechvel.pereslavl.ru">
<pre wrap="">I would try to call
agda --termination-depth=2 Foo.agda
Maybe, this will help Agda to see that (x ∷ xs) is less than
(n ∷ (x ∷ xs)).
------
Sergei
On Wed, 2017-08-16 at 22:23 +0200, Serge Leblanc wrote:
</pre>
<blockquote type="cite">
<pre wrap="">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:
</pre>
<blockquote type="cite">
<pre wrap="">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 <a class="moz-txt-link-rfc2396E" href="mailto:Jesper@sikanda.be"><Jesper@sikanda.be></a>
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
<a class="moz-txt-link-rfc2396E" href="mailto:33dbqnxpy7if@gmail.com"><33dbqnxpy7if@gmail.com></a>:
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
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<pre wrap="">
--
Serge Leblanc
______________________________________________________________________
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<pre wrap="">
</pre>
</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>