[Agda] Bezonas helpon !
Serge Leblanc
33dbqnxpy7if at gmail.com
Sun Aug 27 22:15:48 CEST 2017
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170827/646b79b6/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₆ : ∀ x xs → max″ (x ∷⁺ xs) ≥ x
lemma₆ x (h ∷ t) = 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₆ x (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/20170827/646b79b6/attachment-0001.sig>
More information about the Agda
mailing list