[Agda] Bezonas helpon !
Andreas Abel
andreas.abel at ifi.lmu.de
Sat Sep 2 19:25:37 CEST 2017
Serge,
something of type
All P (x1 :: x2 :: x3 :: [])
should be a list of proofs
p1 :: p2 :: p3 :: []
where
p1 : P x1
p2 : P x2
p3 : P x3
Best,
Andreas
On 31.08.2017 01:29, Serge Leblanc wrote:
> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
--
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