[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