[Agda] Agda Questions.

[Aaron Stump]

Dear Agda list,

Yes, this is homework for my class, so thanks for your nonresponse.

Aaron

On Tue, Sep 22, 2015 at 6:32 AM, Andreas Abel <andreas.abel at ifi.lmu.de>
wrote:

> Sounds like you want us to solve your homework. ;) --Andreas
>
>
> On 20.09.2015 23:36, Ismail Alyassiri wrote:
>
>> {--
>>>    Hello guys, I am trying to gather many proofs using Agda now that I
>>> am studying it on own.
>>> Bellow, I have a few problems I would love your help of solving. Thank
>>> you in advances guys.
>>>
>>>
>>>
>>>
>>> --}
>>> module list-todo where
>>>
>>> open import lib
>>>
>>> {- define this function so that it removes the last element from a list.
>>>    If the list is empty, you can just return the empty list. -}
>>> removelast : ∀{ℓ}{A : Set ℓ} → 𝕃 A → 𝕃 A
>>> removelast = {!!}
>>>
>>> {- once you have a correct definition of removelast, the yellow
>>> highlighting
>>>    for the following two tests will disappear. -}
>>> test1-removelast : removelast (1 :: 2 :: 3 :: 4 :: []) ≡ 1 :: 2 :: 3 ::
>>> []
>>> test1-removelast = refl
>>>
>>> test2-removelast : removelast ('a' :: 'b' :: 'z' :: 'y' :: 'z' :: [])
>>> ≡ 'a' :: 'b' :: 'z' :: 'y' :: []
>>> test2-removelast = refl
>>>
>>> concat[] : ∀ {ℓ}{A : Set ℓ}(n : ℕ) → concat{A = A} (repeat n []) ≡ []
>>> concat[] = {!!}
>>>
>>> -- you have to implement removelast above in order to do this problem
>>> removelast++ : ∀{ℓ}{A : Set ℓ}(l1 l2 : 𝕃 A) → is-empty l2 ≡ ff →
>>> removelast (l1 ++ l2) ≡ l1 ++ removelast l2
>>> removelast++ = {!!}
>>>
>>> shorter-trans : ∀{ℓ}{A : Set ℓ}(l1 l2 l3 : 𝕃 A) →
>>>                  l1 shorter l2 ≡ tt →
>>>                  l2 shorter l3 ≡ tt →
>>>                  l1 shorter l3 ≡ tt
>>> shorter-trans = {!!}
>>>
>>> list-all-any : ∀{ℓ}{A : Set ℓ}(pred : A → 𝔹)(l : 𝕃 A) →
>>>                 list-all pred l ≡ ~ (list-any (λ a → ~ (pred a)) l)
>>> list-all-any = {!!}
>>>
>>> filter-list-all : ∀{ℓ}{A : Set ℓ}(pred : A → 𝔹)(l : 𝕃 A) →
>>>                    list-all pred l ≡ tt →
>>>                    filter pred l ≡ l
>>> filter-list-all = {!!}
>>>
>>> filter-member : ∀{ℓ}{A : Set ℓ}(eq : A → A → 𝔹)(a : A)(pred : A →
>>> 𝔹)(l : 𝕃 A) →
>>>                 list-member eq a (filter pred l) ≡ tt →
>>>                 list-member eq a l ≡ tt ∧ pred a ≡ tt
>>> filter-member = {!!}
>>>
>>>
>>> zip-unzip : ∀{ℓ₁ ℓ₂}{A : Set ℓ₁}{B : Set ℓ₂}(x : 𝕃 A)(y : 𝕃 B) →
>>>             length x ≡ length y → unzip (zip x y) ≡ x , y
>>> zip-unzip = {!!}
>>>
>>
>>
>>
>> _______________________________________________
>> 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://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150922/23d27966/attachment.html