[Agda] Bezonas helpon !

Serge Leblanc 33dbqnxpy7if at gmail.com
Thu Aug 31 01:29:38 CEST 2017


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

Thank you very much!
Sinceran dankon!


On 2017-08-27 22:15, Serge Leblanc wrote:
>
> 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 !
>
>
> On 2017-08-22 17:53, Andreas Abel wrote:
>> It might be sufficient to prove
>>
>>   max (x :: xs) >= max xs
>>
>> and use this in your induction hypothesis (with transitivity of >=).
>>
>> Cheers,
>> Andreas
>>
>> On 21.08.2017 08:07, Serge Leblanc wrote:
>>> 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
>>
>
> -- 
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170831/f963d6b7/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 
  ∎
  where open PropEq.≡-Reasoning
{-
lemma₄ : ∀ x xs → x ⊔ max″ xs ≡ max″ (x ∷⁺ xs)
lemma₄ x (h ∷ t) = lemma₃ x h t

lemma₅ : ∀ xs x → max″ (x ∷⁺ xs) ≥ max″ xs
lemma₅ (h ∷ t) x = begin
  Data.List.foldl _⊔_ h t ≤⟨ m≤m⊔n (Data.List.foldl _⊔_ h t) x ⟩
  Data.List.foldl _⊔_ h t ⊔ x ≡⟨ ⊔-comm (Data.List.foldl _⊔_ h t) x ⟩
  x ⊔ Data.List.foldl _⊔_ h t ≡⟨ lemma₃ x h t ⟩
  Data.List.foldl _⊔_ (x ⊔ h) t
  ∎
  where open Data.Nat.≤-Reasoning
-}
lemma₆ : ∀ xs x → max″ (x ∷⁺ xs) ≥ x
lemma₆ (h ∷ t) x = begin
  x ≤⟨ m≤m⊔n x (Data.List.foldl _⊔_ h t) ⟩
  x ⊔ Data.List.foldl _⊔_ h t ≡⟨ lemma₃ x h t ⟩
  Data.List.foldl _⊔_ (x ⊔ h) t
  ∎
  where open Data.Nat.≤-Reasoning

≤-trans : ∀ {i j k} → i ≤ j → j ≤ k → i ≤ k
≤-trans z≤n _ = z≤n
≤-trans (s≤s i≤j) (s≤s j≤k) = s≤s (≤-trans i≤j j≤k)

proof₁ : (xs : List⁺ ℕ) → All (_≥_ (max″ xs)) (toList xs)
proof₁ (h ∷ []) = {! [] !}
proof₁ (h ∷ (x ∷ xs)) = {! lemma₆ (h ∷ xs) ∷ proof₁ (h ∷ 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/20170831/f963d6b7/attachment-0001.sig>


More information about the Agda mailing list