No help with homework on this list [Re: [Agda] Agda Questions.]

[Andreas Abel]

I see this happening on the Coq list, "helpful" experts answering 
homework Coq assignments.  I think we should abstain from this here.

--Andreas

On 22.09.2015 14:02, Aaron Stump wrote:
> 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
> <mailto: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 <mailto: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 <mailto:andreas.abel at gu.se>
>     http://www2.tcs.ifi.lmu.de/~abel/
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto: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/