[Agda] Bezonas helpon !

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


On 201i7-08-18 13:15, Andreas Abel wrote:
> 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.
>
> On 17.08.2017 12:18, Serge Leblanc wrote:
>> 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!
>>
>>
>> On 2017-08-16 22:54, Andreas Abel wrote:
>>> 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
>>>
>>> On 16.08.2017 22:23, Serge Leblanc wrote:
>>>> 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:
>>>>> 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 <Jesper at sikanda.be
>>>>> <mailto:Jesper at sikanda.be>> 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 <33dbqnxpy7if at gmail.com
>>>>> <mailto:33dbqnxpy7if at gmail.com>>:
>>>>>
>>>>>         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
>

-- 
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170821/dbd75f1c/attachment-0001.html>
-------------- next part --------------
module Maximal where

open import Data.Nat public using (ℕ; zero; suc; _⊔_; _≤_; _≥_; z≤n; s≤s)
open import Data.Nat.Properties public using (m≤m⊔n)
open import Data.List.NonEmpty using (List⁺; foldr₁; _∷_;  _∷⁺_; [_]; toList)
open import Data.List.Any as Any using (Any; here; there)
open import Data.List.All as All -- using (All)

open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; cong; sym )


open import Relation.Binary
open DecTotalOrder Data.Nat.decTotalOrder using () renaming (refl to ≤-refl)

open import Data.List using (List; []; _∷_; _++_)
--open import Function using (id)


foldr : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldr {A = A} c (n ∷ l) = foldr′ n l
  where
    foldr′ : A → List A → A
    foldr′ n [] = n
    foldr′ n (x ∷ xs) = c n (foldr′ x xs)

foldl : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldl {A = A} c (n ∷ l) = foldl′ n l
  where
    foldl′ : A → List A → A
    foldl′ n [] = n
    foldl′ n (x ∷ xs) = foldl′ (c n x) xs

foldl″ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldl″ f (h ∷ t) = Data.List.foldl f h t


max : List⁺ ℕ → ℕ
max l = foldl _⊔_ l

max′ : List⁺ ℕ → ℕ
max′ l = foldr _⊔_ l

max″ : List⁺ ℕ → ℕ
max″ (h ∷ t) = Data.List.foldl _⊔_ h t

private

  max² : max [ 2 ] ≡ 2
  max² = refl

  max²″ : max″ [ 2 ] ≡ 2
  max²″ = refl

  max⁵ : max (4 ∷⁺ 5 ∷⁺ [ 6 ]) ≡ 6
  max⁵ = refl

  max₅″ : max″ (4 ∷⁺ 5 ∷⁺ [ 6 ]) ≡ 6
  max₅″ = refl

  module Examples (_⊙_ : ℕ → ℕ → ℕ)
                  (a b c : ℕ)
                  where

      left₁ : foldl _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ ((a ⊙ b) ⊙ c)
      left₁ = refl

      left₂ : foldl″ _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ ((a ⊙ b) ⊙ c)
      left₂ = refl

      right₁ : foldr _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ (a ⊙ (b ⊙ c))
      right₁ = refl


⊔-right-identity : ∀ n → n ⊔ 0 ≡ n
⊔-right-identity zero = refl
⊔-right-identity (suc n) = refl

⊔-comm : ∀ x y → x ⊔ y ≡ y ⊔ x
⊔-comm zero y = sym (⊔-right-identity y)
⊔-comm (suc x) zero = refl
⊔-comm (suc x) (suc y) = cong suc (⊔-comm x y)

⊔-asso : ∀ x y z → x ⊔ (y ⊔ z) ≡ (x ⊔ y) ⊔ z
⊔-asso zero _ _ = refl
⊔-asso (suc x) zero _ = refl
⊔-asso (suc x) (suc y) zero = refl
⊔-asso (suc x) (suc y) (suc z) = cong suc (⊔-asso x y z)

open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; cong₂)
open PropEq.≡-Reasoning -- renaming (_≡⟨_⟩_ to _≡[_]_)

private

  abstract
    lemma₂ : ∀ x₀ x₁ xs → Data.List.foldl _⊔_ x₀ (x₁ ∷ xs) ≡ Data.List.foldl _⊔_ (x₀ ⊔ x₁) xs
    lemma₂ x₀ x₁ xs = refl


lemma₃ : ∀ x₀ x₁ xs → x₀ ⊔ Data.List.foldl _⊔_ x₁ xs ≡ Data.List.foldl _⊔_ (x₀ ⊔ x₁) xs
lemma₃ x₀ x₁ [] = refl
lemma₃ x₀ x₁ (h ∷ t) = begin
  x₀ ⊔ Data.List.foldl _⊔_ (x₁ ⊔ h) t ≡⟨ lemma₃ x₀ (x₁ ⊔ h) t ⟩
  Data.List.foldl _⊔_ (x₀ ⊔ (x₁ ⊔ h)) t ≡⟨ cong (λ s → Data.List.foldl _⊔_ s t) (⊔-asso x₀ x₁ h) ⟩
  Data.List.foldl _⊔_ (x₀ ⊔ x₁ ⊔ h) t 
  ∎

lemma₄ : ∀ x xs → x ⊔ max″ xs ≡ max″ (x ∷⁺ xs)
lemma₄ x (h ∷ t) = lemma₃ x h t

++⁺ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys : List A} →
        All P xs → All P ys → All P (xs ++ ys)
++⁺ []         pys = pys 
++⁺ (px ∷ pxs) pys = px ∷ ++⁺ pxs pys


proof₁ : (xs : List⁺ ℕ) → All (_≥_ (max″ xs)) (toList xs)
proof₁ (h ∷ []) = {! []!}
proof₁ (h ∷ (x ∷ xs)) = {! (proof₁ (x ∷ xs))!}
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170821/dbd75f1c/attachment-0001.sig>