[Agda] Bezonas helpon !

Discussion:

Serge Leblanc

2017-08-06 16:23:25 UTC

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

2017-08-14 16:33:59 UTC

Permalink

Saluton, neniu bonvolas helpi min?

Hi, nobody wants to help me?

Post by Serge Leblanc
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

Jesper Cockx

2017-08-14 16:47:36 UTC

Permalink

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

Post by Serge Leblanc
Saluton, neniu bonvolas helpi min?
Hi, nobody wants to help me?
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
https://lists.chalmers.se/mailman/listinfo/agda

Ulf Norell

2017-08-14 18:55:06 UTC

Permalink

The fact that foldrâ is using a private recursive helper function will
likely make it impossible to prove your theorem.

/ Ulf

Post by Jesper Cockx
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

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Serge Leblanc

2017-08-16 20:23:09 UTC

Permalink

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)

Post by Ulf Norell
The fact that foldrâ is using a private recursive helper function will
likely make it impossible to prove your theorem.
/ Ulf
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
Saluton, neniu bonvolas helpi min?
Hi, nobody wants to help me?

--
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
<https://lists.chalmers.se/mailman/listinfo/agda>
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
<https://lists.chalmers.se/mailman/listinfo/agda>

--
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F

Sergei Meshveliani

2017-08-16 20:53:55 UTC

Permalink

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

Post by Serge Leblanc
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)

The fact that foldr₁ is using a private recursive helper function
will likely make it impossible to prove your theorem.
/ Ulf
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
Saluton, neniu bonvolas helpi min?
Hi, nobody wants to help me?

Post by Serge Leblanc
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
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

--
Serge Leblanc
______________________________________________________________________
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Serge Leblanc

2017-08-17 09:08:34 UTC

Permalink

BedaÅrinde, tio maltrafas. Agda ne vidas la malkreskanton de la listo
malgraÅ la ampleksa ordono eÄ Äis 15 !

Unfortunately this fails, Agda doesn't see the descent of the list
despite the command even up to 15 !

Sincere,

Post by Sergei Meshveliani
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

Post by Serge Leblanc
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)

Post by Ulf Norell
The fact that foldrâ is using a private recursive helper function
will likely make it impossible to prove your theorem.
/ Ulf
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
Saluton, neniu bonvolas helpi min?
Hi, nobody wants to help me?

Post by Serge Leblanc
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

Andreas Abel

2017-08-16 20:54:45 UTC

Permalink

The function is structurally recursive on the /length/ of the list, not
on the list itself. You can expose the length by

1. using vectors instead of lists, or
2. using sized lists (sized types).

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.

Best,
Andreas

Post by Serge Leblanc
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)

The fact that foldr₁ is using a private recursive helper function will
likely make it impossible to prove your theorem.
/ Ulf
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
Saluton, neniu bonvolas helpi min?
Hi, nobody wants to help me?

Post by Serge Leblanc
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

--
Andreas Abel <>< Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

***@gu.se
http://www.cse.chalmers.se/~abela/

Serge Leblanc

2017-08-17 10:18:32 UTC

Permalink

Sinceran dankon Andreas.

I don't understand that the following function (foldrâ³) is well accepted
while foldlâ³ is not?
Mi ne komprenas kial la sekva funkcio (foldrâ³) trafas kvankam la
funkciofoldlâ³ maltrafas?

foldrâ³ : â {a} {A : Set a} â (A â A â A) â Listâº A â A
foldrâ³ c (n â· []) = n
foldrâ³ c (n â· (x â· xs)) = c x (foldrâ³ c (n â· xs))

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)

Termination checking failed for the following functions: foldlâ³

I also remarked that Agda rejects that:
Mi ankaÅ remarkis ke agda malakceptas tion:

foldrâŽ : â {a} {A : Set a} â (A â A â A) â Listâº A â A
foldrâŽ c (n â· []) = n
foldrâŽ c (n â· (x â· xs)) = c x (foldrâŽ c (*id* n â· xs))
where
open import Function using (id)

Termination checking failed for the following functions:foldrâŽ

Andreas,unfortunately I really don't understand your explanation of the
/length/ of the list!
Andreas, bedaÃ»rinde mi vere ne komprenis vian klarigon pri la grandeco
de la listo!

Post by Andreas Abel
The function is structurally recursive on the /length/ of the list,
not on the list itself. You can expose the length by
1. using vectors instead of lists, or
2. using sized lists (sized types).
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.
Best,
Andreas

Post by Serge Leblanc
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)

Post by Ulf Norell
The fact that foldrâ is using a private recursive helper function
will likely make it impossible to prove your theorem.
/ Ulf
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
Saluton, neniu bonvolas helpi min?
Hi, nobody wants to help me?

Post by Serge Leblanc
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
https://lists.chalmers.se/mailman/listinfo/agda
<https://lists.chalmers.se/mailman/listinfo/agda>
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
<https://lists.chalmers.se/mailman/listinfo/agda>

--
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F

Sergei Meshveliani

2017-08-17 18:02:44 UTC

Permalink

[..]
Andreas, unfortunately I really don't understand your explanation of
the /length/ of the list!

Concerning using (length xs) in addition to xs : List C:

as to me, I sometimes I use (length xs) as a counter that helps to
prove termination for some functions on List C.
For example, Agda did not see termination in my merge sorting. So I use
the counter (cnt):

--------------------------------------------------------------------
sort : (xs : List C) → SortRes xs
sort xs =
aux xs (length xs) (≤n-refl PE.refl)
where
aux : (xs : List C) → (cnt : ℕ) → length xs ≤n cnt → SortRes xs

-- The counter cnt is used for termination proof.

aux [] _ _ = sortRes [] nil (=ms-refl {∅})
aux (x ∷ []) _ _ = sortRes (x ∷ []) (single x)
(=ms-refl {singleMS (x , 1)})

aux (_ ∷ _ ∷ zs) 0 2+|zs|≤0 = ⊥-elim $ ≤→≯ 2+|zs|≤0 2+|zs|>0
where
2+|zs|>0 : 2 + (length zs) >n 0
2+|zs|>0 = suc>0

aux (x ∷ y ∷ zs) (suc cnt) |x:y:zs|≤scnt =
let
(sortRes lList ord-lList toMS-ls=ms=toMS-lList) =
aux ls cnt |ls|≤cnt
...
...
in
sortRes ys ord-ys <x:y:zs>=ms=<ys>
--------------------------------------------------------------------

The counter steps from (suc cnt) to cnt, and it always holds
(length currentList) ≤ (length currentList).
This helps Agda to see termination.

For some reason (unknown to me) Agda easier sees termination when the
argument is built by the suc constructor rather than _∷_.

------
Sergei

Post by Serge Leblanc
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
foldl″ c (c n x ∷ xs) (at /home/serge/agda/Maximal.agda:49,27-33)

The fact that foldr₁ is using a private recursive helper
function will likely make it impossible to prove your theorem.
/ Ulf
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
Saluton, neniu bonvolas helpi min?
Hi, nobody wants to help me?

Post by Serge Leblanc
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
https://lists.chalmers.se/mailman/listinfo/agda
<https://lists.chalmers.se/mailman/listinfo/agda>
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
<https://lists.chalmers.se/mailman/listinfo/agda>

Sergei Meshveliani

2017-08-17 18:05:07 UTC

Permalink

Post by Sergei Meshveliani

[..]
Andreas, unfortunately I really don't understand your explanation of
the /length/ of the list!

as to me, I sometimes I use (length xs) as a counter that helps to
prove termination for some functions on List C.
For example, Agda did not see termination in my merge sorting. So I use
--------------------------------------------------------------------
sort : (xs : List C) → SortRes xs
sort xs =
aux xs (length xs) (≤n-refl PE.refl)
where
aux : (xs : List C) → (cnt : ℕ) → length xs ≤n cnt → SortRes xs
-- The counter cnt is used for termination proof.
aux [] _ _ = sortRes [] nil (=ms-refl {∅})
aux (x ∷ []) _ _ = sortRes (x ∷ []) (single x)
(=ms-refl {singleMS (x , 1)})
aux (_ ∷ _ ∷ zs) 0 2+|zs|≤0 = ⊥-elim $ ≤→≯ 2+|zs|≤0 2+|zs|>0
where
2+|zs|>0 : 2 + (length zs) >n 0
2+|zs|>0 = suc>0
aux (x ∷ y ∷ zs) (suc cnt) |x:y:zs|≤scnt =
let
(sortRes lList ord-lList toMS-ls=ms=toMS-lList) =
aux ls cnt |ls|≤cnt
...
...
in
sortRes ys ord-ys <x:y:zs>=ms=<ys>
--------------------------------------------------------------------
The counter steps from (suc cnt) to cnt, and it always holds
(length currentList) ≤ (length currentList).

Improvement: (length currentList) ≤ current-cnt.

Post by Sergei Meshveliani
This helps Agda to see termination.
For some reason (unknown to me) Agda easier sees termination when the
argument is built by the suc constructor rather than _∷_.
------
Sergei

Post by Serge Leblanc
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
foldl″ c (c n x ∷ xs) (at /home/serge/agda/Maximal.agda:49,27-33)

The fact that foldr₁ is using a private recursive helper
function will likely make it impossible to prove your theorem.
/ Ulf
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
Saluton, neniu bonvolas helpi min?
Hi, nobody wants to help me?

Post by Serge Leblanc
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
https://lists.chalmers.se/mailman/listinfo/agda
<https://lists.chalmers.se/mailman/listinfo/agda>
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
<https://lists.chalmers.se/mailman/listinfo/agda>

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Andreas Abel

2017-08-18 11:15:57 UTC

Permalink

Dear Serge,

foldr″ c (n ∷ (x ∷ xs)) = c x (foldr″ c (n ∷ xs))

For the structural ordering (<), Agda sees that

(n :: xs) < (n :: (x :: xs)) iff xs < (x :: xs)

The latter holds since xs is a subterm of x :: xs.

foldl″ c (n ∷ (x ∷ xs)) = foldl″ c (c n x ∷ xs)

This does not work since c n x is not a subterm of n or x.

foldr‴ c (n ∷ (x ∷ xs)) = c x (foldr‴ c (*id* n ∷ xs))

Since Agda does not reduce call arguments during structural comparison,
this fails, as

id n is not the same as n

(syntactically).

Andreas,unfortunately I really don't understand your explanation of the
/length/ of the list!

My explanation was probably wrong.

Sinceran dankon Andreas.
I don't understand that the following function (foldr″) is well accepted
while foldl″ is not?
Mi ne komprenas kial la sekva funkcio (foldr″) trafas kvankam la
funkciofoldl″ maltrafas?
foldr″ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldr″ c (n ∷ []) = n
foldr″ c (n ∷ (x ∷ xs)) = c x (foldr″ c (n ∷ xs))
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)
Termination checking failed for the following functions: foldl″
foldr‴ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldr‴ c (n ∷ []) = n
foldr‴ c (n ∷ (x ∷ xs)) = c x (foldr‴ c (*id* n ∷ xs))
where
open import Function using (id)
Termination checking failed for the following functions:foldr‴
Andreas,unfortunately I really don't understand your explanation of the
/length/ of the list!
Andreas, bedaûrinde mi vere ne komprenis vian klarigon pri la grandeco
de la listo!

Post by Serge Leblanc
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)

The fact that foldr₁ is using a private recursive helper function
will likely make it impossible to prove your theorem.
/ Ulf
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
Saluton, neniu bonvolas helpi min?
Hi, nobody wants to help me?

--
Andreas Abel <>< Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

***@gu.se
http://www.cse.chalmers.se/~abela/

Serge Leblanc

2017-08-21 06:07:34 UTC

Permalink

Thank you very much, Andreas, I understand more.

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

proofâ : (xs : Listâº â) â All (_â¥_ (maxâ³ xs)) (toList xs)
proofâ (h â· []) = {! []!}
proofâ (h â· (x â· xs)) = {! (proofâ (x â· xs))!}

Thank you for your help!

Koran dankon, Andreas, mi plibone komprenas.

Nun, mi provis plenumi la pruvon proofâ. VerÅajne, mi malsukcesas pro la
propozicio P enhavas 'xs'.
Äu iu havas sugeston ? Intuicie, mi bezonos indukton kun 'mâ€mân'.

proofâ : (xs : Listâº â) â All (_â¥_ (maxâ³ xs)) (toList xs)
proofâ (h â· []) = {! []!}
proofâ (h â· (x â· xs)) = {! (proofâ (x â· xs))!}

AntaÅan dankon pro via venonta helpo !

Sincere,

Post by Andreas Abel
Dear Serge,

Post by Serge Leblanc
foldrâ³ c (n â· (x â· xs)) = c x (foldrâ³ c (n â· xs))

For the structural ord\ering (<), Agda sees that
(n :: xs) < (n :: (x :: xs)) iff xs < (x :: xs)
The latter holds since xs is a subterm of x :: xs.

Post by Serge Leblanc
foldlâ³ c (n â· (x â· xs)) = foldlâ³ c (c n x â· xs)

This does not work since c n x is not a subterm of n or x.

Post by Serge Leblanc
foldrâŽ c (n â· (x â· xs)) = c x (foldrâŽ c (*id* n â· xs))

Since Agda does not reduce call arguments during structural
comparison, this fails, as
id n is not the same as n
(syntactically).

Post by Serge Leblanc
Andreas,unfortunately I really don't understand your explanation of the
/length/ of the list!

My explanation was probably wrong.

Post by Serge Leblanc
Sinceran dankon Andreas.
I don't understand that the following function (foldrâ³) is well
accepted while foldlâ³ is not?
Mi ne komprenas kial la sekva funkcio (foldrâ³) trafas kvankam la
funkciofoldlâ³ maltrafas?
foldrâ³ : â {a} {A : Set a} â (A â A â A) â Listâº A â A
foldrâ³ c (n â· []) = n
foldrâ³ c (n â· (x â· xs)) = c x (foldrâ³ c (n â· xs))
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)
Termination checking failed for the following functions: foldlâ³
foldrâŽ : â {a} {A : Set a} â (A â A â A) â Listâº A â A
foldrâŽ c (n â· []) = n
foldrâŽ c (n â· (x â· xs)) = c x (foldrâŽ c (*id* n â· xs))
where
open import Function using (id)
Termination checking failed for the following functions:foldrâŽ
Andreas,unfortunately I really don't understand your explanation of
the /length/ of the list!
Andreas, bedaÃ»rinde mi vere ne komprenis vian klarigon pri la
grandeco de la listo!

Post by Serge Leblanc
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
foldlâ³ c (c n x â· xs) (at /home/serge/agda/Maximal.agda:49,27-33)

Post by Ulf Norell
The fact that foldrâ is using a private recursive helper function
will likely make it impossible to prove your theorem.
/ Ulf
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
Saluton, neniu bonvolas helpi min?
Hi, nobody wants to help me?

--
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F

Andreas Abel

2017-08-22 15:53:25 UTC

Permalink

It might be sufficient to prove

max (x :: xs) >= max xs

and use this in your induction hypothesis (with transitivity of >=).

Cheers,
Andreas

Post by Serge Leblanc
Thank you very much, Andreas, I understand more.
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'.
proof₁ : (xs : List⁺ ℕ) → All (_≥_ (max″ xs)) (toList xs)
proof₁ (h ∷ []) = {! []!}
proof₁ (h ∷ (x ∷ xs)) = {! (proof₁ (x ∷ xs))!}
Thank you for your help!
Koran dankon, Andreas, mi plibone komprenas.
Nun, mi provis plenumi la pruvon proof₁. Verŝajne, mi malsukcesas pro la
propozicio P enhavas 'xs'.
Ĉu iu havas sugeston ? Intuicie, mi bezonos indukton kun 'm≤m⊔n'.
proof₁ : (xs : List⁺ ℕ) → All (_≥_ (max″ xs)) (toList xs)
proof₁ (h ∷ []) = {! []!}
proof₁ (h ∷ (x ∷ xs)) = {! (proof₁ (x ∷ xs))!}
Antaŭan dankon pro via venonta helpo !
Sincere,

Post by Andreas Abel
Dear Serge,

foldr″ c (n ∷ (x ∷ xs)) = c x (foldr″ c (n ∷ xs))

For the structural ord\ering (<), Agda sees that
(n :: xs) < (n :: (x :: xs)) iff xs < (x :: xs)
The latter holds since xs is a subterm of x :: xs.

foldl″ c (n ∷ (x ∷ xs)) = foldl″ c (c n x ∷ xs)

This does not work since c n x is not a subterm of n or x.

foldr‴ c (n ∷ (x ∷ xs)) = c x (foldr‴ c (*id* n ∷ xs))

Since Agda does not reduce call arguments during structural
comparison, this fails, as
id n is not the same as n
(syntactically).

Andreas,unfortunately I really don't understand your explanation of the
/length/ of the list!

My explanation was probably wrong.

Sinceran dankon Andreas.
I don't understand that the following function (foldr″) is well
accepted while foldl″ is not?
Mi ne komprenas kial la sekva funkcio (foldr″) trafas kvankam la
funkciofoldl″ maltrafas?
foldr″ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldr″ c (n ∷ []) = n
foldr″ c (n ∷ (x ∷ xs)) = c x (foldr″ c (n ∷ xs))
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)
Termination checking failed for the following functions: foldl″
foldr‴ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldr‴ c (n ∷ []) = n
foldr‴ c (n ∷ (x ∷ xs)) = c x (foldr‴ c (*id* n ∷ xs))
where
open import Function using (id)
Termination checking failed for the following functions:foldr‴
Andreas,unfortunately I really don't understand your explanation of
the /length/ of the list!
Andreas, bedaûrinde mi vere ne komprenis vian klarigon pri la
grandeco de la listo!

Post by Serge Leblanc
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
foldl″ c (c n x ∷ xs) (at /home/serge/agda/Maximal.agda:49,27-33)

The fact that foldr₁ is using a private recursive helper function
will likely make it impossible to prove your theorem.
/ Ulf
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
Saluton, neniu bonvolas helpi min?
Hi, nobody wants to help me?

--
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F

--
Andreas Abel <>< Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

***@gu.se
http://www.cse.chalmers.se/~abela/

Serge Leblanc

2017-08-27 20:15:48 UTC

Permalink

I fail to make the proof. I don't understand how built the All
structure. Can someone show me?

Mi malsukcesas fari la pruvon. Mi tute ne komprenas kiel oni konstruas
la structuron All. Äu iu povas montri al mi?

Sinceran dankon !

Post by Andreas Abel
It might be sufficient to prove
max (x :: xs) >= max xs
and use this in your induction hypothesis (with transitivity of >=).
Cheers,
Andreas

Post by Serge Leblanc
Thank you very much, Andreas, I understand more.
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'.
proofâ : (xs : Listâº â) â All (_â¥_ (maxâ³ xs)) (toList xs)
proofâ (h â· []) = {! []!}
proofâ (h â· (x â· xs)) = {! (proofâ (x â· xs))!}
Thank you for your help!
Koran dankon, Andreas, mi plibone komprenas.
Nun, mi provis plenumi la pruvon proofâ. VerÅajne, mi malsukcesas pro
la propozicio P enhavas 'xs'.
Äu iu havas sugeston ? Intuicie, mi bezonos indukton kun 'mâ€mân'.
proofâ : (xs : Listâº â) â All (_â¥_ (maxâ³ xs)) (toList xs)
proofâ (h â· []) = {! []!}
proofâ (h â· (x â· xs)) = {! (proofâ (x â· xs))!}
AntaÅan dankon pro via venonta helpo !
Sincere,

Post by Andreas Abel
Dear Serge,

Post by Serge Leblanc
foldrâ³ c (n â· (x â· xs)) = c x (foldrâ³ c (n â· xs))

For the structural ord\ering (<), Agda sees that
(n :: xs) < (n :: (x :: xs)) iff xs < (x :: xs)
The latter holds since xs is a subterm of x :: xs.

Post by Serge Leblanc
foldlâ³ c (n â· (x â· xs)) = foldlâ³ c (c n x â· xs)

This does not work since c n x is not a subterm of n or x.

Post by Serge Leblanc
foldrâŽ c (n â· (x â· xs)) = c x (foldrâŽ c (*id* n â· xs))

Since Agda does not reduce call arguments during structural
comparison, this fails, as
id n is not the same as n
(syntactically).

Post by Serge Leblanc
Andreas,unfortunately I really don't understand your explanation

of the

Post by Serge Leblanc
/length/ of the list!

My explanation was probably wrong.

Post by Andreas Abel
The function is structurally recursive on the /length/ of the
list, not on the list itself. You can expose the length by
1. using vectors instead of lists, or
2. using sized lists (sized types).
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.
Best,
Andreas

Post by Serge Leblanc
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
foldlâ³ c (c n x â· xs) (at /home/serge/agda/Maximal.agda:49,27-33)

Post by Ulf Norell
The fact that foldrâ is using a private recursive helper
function will likely make it impossible to prove your theorem.
/ Ulf
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
Saluton, neniu bonvolas helpi min?
Hi, nobody wants to help me?

--
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F

Mario Castelán Castro

2017-08-27 20:20:33 UTC

Permalink

Post by Serge Leblanc
Mi malsukcesas fari la pruvon. Mi tute ne komprenas kiel oni konstruas
la structuron All. Äu iu povas montri al mi?

What language is this? It looks a bit like Esperanto.

--
Do not eat animals, respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan

Serge Leblanc

2017-08-30 23:29:38 UTC

Permalink

Does somone have an example of uses All?
Äu iu havas ekzemplon de 'All' uzado?

Thank you very much!
Sinceran dankon!

Post by Serge Leblanc
I fail to make the proof. I don't understand how built the All
structure. Can someone show me?
Mi malsukcesas fari la pruvon. Mi tute ne komprenas kiel oni konstruas
la structuron All. Äu iu povas montri al mi?
Sinceran dankon !

Post by Andreas Abel
It might be sufficient to prove
max (x :: xs) >= max xs
and use this in your induction hypothesis (with transitivity of >=).
Cheers,
Andreas

Post by Serge Leblanc
Thank you very much, Andreas, I understand more.
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'.
proofâ : (xs : Listâº â) â All (_â¥_ (maxâ³ xs)) (toList xs)
proofâ (h â· []) = {! []!}
proofâ (h â· (x â· xs)) = {! (proofâ (x â· xs))!}
Thank you for your help!
Koran dankon, Andreas, mi plibone komprenas.
Nun, mi provis plenumi la pruvon proofâ. VerÅajne, mi malsukcesas
pro la propozicio P enhavas 'xs'.
Äu iu havas sugeston ? Intuicie, mi bezonos indukton kun 'mâ€mân'.
proofâ : (xs : Listâº â) â All (_â¥_ (maxâ³ xs)) (toList xs)
proofâ (h â· []) = {! []!}
proofâ (h â· (x â· xs)) = {! (proofâ (x â· xs))!}
AntaÅan dankon pro via venonta helpo !
Sincere,

Post by Andreas Abel
Dear Serge,

Post by Serge Leblanc
foldrâ³ c (n â· (x â· xs)) = c x (foldrâ³ c (n â· xs))

For the structural ord\ering (<), Agda sees that
(n :: xs) < (n :: (x :: xs)) iff xs < (x :: xs)
The latter holds since xs is a subterm of x :: xs.

Post by Serge Leblanc
foldlâ³ c (n â· (x â· xs)) = foldlâ³ c (c n x â· xs)

This does not work since c n x is not a subterm of n or x.

Post by Serge Leblanc
foldrâŽ c (n â· (x â· xs)) = c x (foldrâŽ c (*id* n â· xs))

Since Agda does not reduce call arguments during structural
comparison, this fails, as
id n is not the same as n
(syntactically).

Post by Serge Leblanc
Andreas,unfortunately I really don't understand your explanation

of the

Post by Serge Leblanc
/length/ of the list!

My explanation was probably wrong.

Post by Serge Leblanc
Sinceran dankon Andreas.
I don't understand that the following function (foldrâ³) is well
accepted while foldlâ³ is not?
Mi ne komprenas kial la sekva funkcio (foldrâ³) trafas kvankam la
funkciofoldlâ³ maltrafas?
foldrâ³ : â {a} {A : Set a} â (A â A â A) â Listâº A â A
foldrâ³ c (n â· []) = n
foldrâ³ c (n â· (x â· xs)) = c x (foldrâ³ c (n â· xs))
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)
Termination checking failed for the following functions: foldlâ³
foldrâŽ : â {a} {A : Set a} â (A â A â A) â Listâº A â A
foldrâŽ c (n â· []) = n
foldrâŽ c (n â· (x â· xs)) = c x (foldrâŽ c (*id* n â· xs))
where
open import Function using (id)
Termination checking failed for the following functions:foldrâŽ
Andreas,unfortunately I really don't understand your explanation
of the /length/ of the list!
Andreas, bedaÃ»rinde mi vere ne komprenis vian klarigon pri la
grandeco de la listo!

Post by Andreas Abel
The function is structurally recursive on the /length/ of the
list, not on the list itself. You can expose the length by
1. using vectors instead of lists, or
2. using sized lists (sized types).
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.
Best,
Andreas

Post by Serge Leblanc
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
foldlâ³ c (c n x â· xs) (at /home/serge/agda/Maximal.agda:49,27-33)

Post by Ulf Norell
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
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
Saluton, neniu bonvolas helpi min?
Hi, nobody wants to help me?

--
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F

Andreas Abel

2017-09-02 17:25:37 UTC

Permalink

Serge,

something of type

All P (x1 :: x2 :: x3 :: [])

should be a list of proofs

p1 :: p2 :: p3 :: []

where

p1 : P x1
p2 : P x2
p3 : P x3

Best,
Andreas

Post by Serge Leblanc
Does somone have an example of uses All?
Ĉu iu havas ekzemplon de 'All' uzado?
Thank you very much!
Sinceran dankon!

Post by Andreas Abel
It might be sufficient to prove
max (x :: xs) >= max xs
and use this in your induction hypothesis (with transitivity of >=).
Cheers,
Andreas

Post by Serge Leblanc
Thank you very much, Andreas, I understand more.
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'.
proof₁ : (xs : List⁺ ℕ) → All (_≥_ (max″ xs)) (toList xs)
proof₁ (h ∷ []) = {! []!}
proof₁ (h ∷ (x ∷ xs)) = {! (proof₁ (x ∷ xs))!}
Thank you for your help!
Koran dankon, Andreas, mi plibone komprenas.
Nun, mi provis plenumi la pruvon proof₁. Verŝajne, mi malsukcesas
pro la propozicio P enhavas 'xs'.
Ĉu iu havas sugeston ? Intuicie, mi bezonos indukton kun 'm≤m⊔n'.
proof₁ : (xs : List⁺ ℕ) → All (_≥_ (max″ xs)) (toList xs)
proof₁ (h ∷ []) = {! []!}
proof₁ (h ∷ (x ∷ xs)) = {! (proof₁ (x ∷ xs))!}
Antaŭan dankon pro via venonta helpo !
Sincere,

Post by Andreas Abel
Dear Serge,

foldr″ c (n ∷ (x ∷ xs)) = c x (foldr″ c (n ∷ xs))

For the structural ord\ering (<), Agda sees that
(n :: xs) < (n :: (x :: xs)) iff xs < (x :: xs)
The latter holds since xs is a subterm of x :: xs.

foldl″ c (n ∷ (x ∷ xs)) = foldl″ c (c n x ∷ xs)

This does not work since c n x is not a subterm of n or x.

foldr‴ c (n ∷ (x ∷ xs)) = c x (foldr‴ c (*id* n ∷ xs))

Since Agda does not reduce call arguments during structural
comparison, this fails, as
id n is not the same as n
(syntactically).

Andreas,unfortunately I really don't understand your explanation

of the

/length/ of the list!

My explanation was probably wrong.

Sinceran dankon Andreas.
I don't understand that the following function (foldr″) is well
accepted while foldl″ is not?
Mi ne komprenas kial la sekva funkcio (foldr″) trafas kvankam la
funkciofoldl″ maltrafas?
foldr″ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldr″ c (n ∷ []) = n
foldr″ c (n ∷ (x ∷ xs)) = c x (foldr″ c (n ∷ xs))
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)
Termination checking failed for the following functions: foldl″
foldr‴ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldr‴ c (n ∷ []) = n
foldr‴ c (n ∷ (x ∷ xs)) = c x (foldr‴ c (*id* n ∷ xs))
where
open import Function using (id)
Termination checking failed for the following functions:foldr‴
Andreas,unfortunately I really don't understand your explanation
of the /length/ of the list!
Andreas, bedaûrinde mi vere ne komprenis vian klarigon pri la
grandeco de la listo!

Post by Andreas Abel
The function is structurally recursive on the /length/ of the
list, not on the list itself. You can expose the length by
1. using vectors instead of lists, or
2. using sized lists (sized types).
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.
Best,
Andreas

Post by Serge Leblanc
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
foldl″ c (c n x ∷ xs) (at /home/serge/agda/Maximal.agda:49,27-33)

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
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
Saluton, neniu bonvolas helpi min?
Hi, nobody wants to help me?

--
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F

--
Andreas Abel <>< Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

***@gu.se
http://www.cse.chalmers.se/~abela/

Serge Leblanc

2017-09-14 14:34:50 UTC

Permalink

Dear, I succeeded completing the proof1: â xs â All (_â¥_ (max "xs))
(toList xs)" using "tabulate". Can anyone show me a simple method?

Sincerely thank you,

Estimata, mi sukcesis plenumi pruvon "proofââ² : â xs â All (_â¥_ (maxâ³
xs)) (toList xs)" per uzado de 'tabulate'. Äu ekzistas pli simpla metodo ?

Sinceran dankon,

proofââ² : â xs â All (_â¥_ (maxâ³ xs)) (toList xs)
proofââ² (h â· t) = tabulate helper
where
helperâ² : â {x xs} â x â xs â (â xâ â maxâ³ (xâ â· xs) â¥ x)
helperâ² {x} (here {xâ²} {xsâ²} px) xâ = begin
x â€âš lemmaâ (xâ â· xsâ²) x â©
Data.List.foldl _â_ (x â xâ) xsâ² â¡âš cong (Î» s â Data.List.foldl
_â_ s xsâ²) (â-comm x xâ) â©
Data.List.foldl _â_ (xâ â x) xsâ² â¡âš cong (Î» s â Data.List.foldl
_â_ (xâ â s) xsâ²) px â©
Data.List.foldl _â_ (xâ â xâ²) xsâ²
â
where open Data.Nat.â€-Reasoning
helperâ² {x} (there {xâ²} {xsâ²} pxs) xâ = helperâ² pxs (xâ â xâ²)

helper : {x : â} â x â (h â· t) â maxâ³ (h â· t) â¥ x
helper {x} (here px) = begin
x â¡âš px â©
h â€âš lemmaâ t h â©
maxâ³ (h â· t)
â
where open Data.Nat.â€-Reasoning
helper {x} (there pxs) = (helperâ² pxs h)

--
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F