[Agda] Bezonas helpon !
Andreas Abel
abela at chalmers.se
Tue Aug 22 17:53:25 CEST 2017
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
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/
More information about the Agda
mailing list