[Agda] Agda Questions.

[Ismail Alyassiri]

{--
   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 = {!!}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150920/eff0d6df/attachment.html