<div dir="ltr"><div><div>Dear Agda list,<br><br></div>Yes, this is homework for my class, so thanks for your nonresponse.<br><br></div>Aaron<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Sep 22, 2015 at 6:32 AM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Sounds like you want us to solve your homework. ;) --Andreas<div><div class="h5"><br>
<br>
On 20.09.2015 23:36, Ismail Alyassiri wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
{--<br>
Hello guys, I am trying to gather many proofs using Agda now that I<br>
am studying it on own.<br>
Bellow, I have a few problems I would love your help of solving. Thank<br>
you in advances guys.<br>
<br>
<br>
<br>
<br>
--}<br>
module list-todo where<br>
<br>
open import lib<br>
<br>
{- define this function so that it removes the last element from a list.<br>
If the list is empty, you can just return the empty list. -}<br>
removelast : ∀{ℓ}{A : Set ℓ} → 𝕃 A → 𝕃 A<br>
removelast = {!!}<br>
<br>
{- once you have a correct definition of removelast, the yellow<br>
highlighting<br>
for the following two tests will disappear. -}<br>
test1-removelast : removelast (1 :: 2 :: 3 :: 4 :: []) ≡ 1 :: 2 :: 3 :: []<br>
test1-removelast = refl<br>
<br>
test2-removelast : removelast ('a' :: 'b' :: 'z' :: 'y' :: 'z' :: [])<br>
≡ 'a' :: 'b' :: 'z' :: 'y' :: []<br>
test2-removelast = refl<br>
<br>
concat[] : ∀ {ℓ}{A : Set ℓ}(n : ℕ) → concat{A = A} (repeat n []) ≡ []<br>
concat[] = {!!}<br>
<br>
-- you have to implement removelast above in order to do this problem<br>
removelast++ : ∀{ℓ}{A : Set ℓ}(l1 l2 : 𝕃 A) → is-empty l2 ≡ ff →<br>
removelast (l1 ++ l2) ≡ l1 ++ removelast l2<br>
removelast++ = {!!}<br>
<br>
shorter-trans : ∀{ℓ}{A : Set ℓ}(l1 l2 l3 : 𝕃 A) →<br>
l1 shorter l2 ≡ tt →<br>
l2 shorter l3 ≡ tt →<br>
l1 shorter l3 ≡ tt<br>
shorter-trans = {!!}<br>
<br>
list-all-any : ∀{ℓ}{A : Set ℓ}(pred : A → 𝔹)(l : 𝕃 A) →<br>
list-all pred l ≡ ~ (list-any (λ a → ~ (pred a)) l)<br>
list-all-any = {!!}<br>
<br>
filter-list-all : ∀{ℓ}{A : Set ℓ}(pred : A → 𝔹)(l : 𝕃 A) →<br>
list-all pred l ≡ tt →<br>
filter pred l ≡ l<br>
filter-list-all = {!!}<br>
<br>
filter-member : ∀{ℓ}{A : Set ℓ}(eq : A → A → 𝔹)(a : A)(pred : A →<br>
𝔹)(l : 𝕃 A) →<br>
list-member eq a (filter pred l) ≡ tt →<br>
list-member eq a l ≡ tt ∧ pred a ≡ tt<br>
filter-member = {!!}<br>
<br>
<br>
zip-unzip : ∀{ℓ₁ ℓ₂}{A : Set ℓ₁}{B : Set ℓ₂}(x : 𝕃 A)(y : 𝕃 B) →<br>
length x ≡ length y → unzip (zip x y) ≡ x , y<br>
zip-unzip = {!!}<br>
</blockquote>
<br>
<br>
<br></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br><span class="HOEnZb"><font color="#888888">
</font></span></blockquote><span class="HOEnZb"><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" rel="noreferrer" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</font></span></blockquote></div><br></div>