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