<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=""></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">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>
-- <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>
</body>
</html>