[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