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