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