use drop, tail and take from Data.Vec in examples
[~helmut/bidiragda.git] / Examples.agda
1 module Examples where
2
3 open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; ⌈_/2⌉)
4 open import Data.Nat.Properties using (cancel-+-left)
5 import Algebra.Structures
6 open Algebra.Structures.IsCommutativeSemiring Data.Nat.Properties.isCommutativeSemiring using (+-isCommutativeMonoid)
7 open Algebra.Structures.IsCommutativeMonoid +-isCommutativeMonoid using () renaming (comm to +-comm)
8 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_ ; tail ; take ; drop)
9 open import Function using (id)
10 open import Function.Injection using () renaming (Injection to _↪_ ; id to id↪)
11 open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) renaming (setoid to EqSetoid)
12
13 open import Generic using (≡-to-Π)
14 import GetTypes
15 import FreeTheorems
16
17 open GetTypes.PartialVecVec using (Get)
18 open FreeTheorems.PartialVecVec using (assume-get)
19
20 reverse' : Get
21 reverse' = assume-get id↪ (≡-to-Π id) reverse
22
23 double' : Get
24 double' = assume-get id↪ (≡-to-Π g) f
25   where g : ℕ → ℕ
26         g zero = zero
27         g (suc n) = suc (suc (g n))
28         f : {A : Set} {n : ℕ} → Vec A n → Vec A (g n)
29         f []      = []
30         f (x ∷ v) = x ∷ x ∷ f v
31
32 double'' : Get
33 double'' = assume-get id↪ (≡-to-Π _) (λ v → v ++ v)
34
35 drop-suc : {n m : ℕ} → suc n ≡ suc m → n ≡ m
36 drop-suc refl = refl
37
38 suc-injection : EqSetoid ℕ ↪ EqSetoid ℕ
39 suc-injection = record { to = ≡-to-Π suc; injective = drop-suc }
40
41 tail' : Get
42 tail' = assume-get suc-injection (≡-to-Π id) tail
43
44 n+-injection : ℕ → EqSetoid ℕ ↪ EqSetoid ℕ
45 n+-injection n = record { to = ≡-to-Π (_+_ n); injective = cancel-+-left n }
46
47 take' : ℕ → Get
48 take' n = assume-get (n+-injection n) (≡-to-Π _) (take n)
49
50 drop' : ℕ → Get
51 drop' n = assume-get (n+-injection n) (≡-to-Π _) (drop n)
52
53 sieve' : Get
54 sieve' = assume-get id↪ (≡-to-Π _) f
55   where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉
56         f []           = []
57         f (x ∷ [])     = x ∷ []
58         f (x ∷ _ ∷ xs) = x ∷ f xs