use drop, tail and take from Data.Vec in examples

This is possible using the PartialVecVec implementation.

2 files changed, 32 insertions, 18 deletions

diff --git a/BFFPlug.agda b/BFFPlug.agda
index f463a09..9f45db1 100644
--- a/BFFPlug.agda
+++ b/BFFPlug.agda
@@ -3,8 +3,7 @@ open import Relation.Binary using (DecSetoid)
 
 module BFFPlug (A : DecSetoid ℓ₀ ℓ₀) where
 
-open import Data.Nat using (ℕ ; _≟_ ; _+_ ; _∸_ ; zero ; suc ; ⌈_/2⌉)
-open import Data.Nat.Properties using (m+n∸n≡m)
+open import Data.Nat using (ℕ ; _≟_ ; _+_ ; zero ; suc ; ⌈_/2⌉)
 open import Data.Maybe using (Maybe ; just ; nothing)
 open import Data.Vec using (Vec)
 open import Data.Product using (∃ ; _,_)
@@ -43,13 +42,13 @@ bffinv : (G : Get) → (nelteg : PropEq ℕ ⟶ Get.I G) → nelteg RightInverse
 bffinv G nelteg inv {m = m} s v = bff G (nelteg ⟨$⟩ m) s (subst (Vec Carrier) (sym (inv m)) v)
 
 module InvExamples where
-  open Examples using (reverse' ; drop' ; sieve')
+  open Examples using (reverse' ; drop' ; sieve' ; tail' ; take')
   
   reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m)
   reverse-put = bffinv reverse' (≡-to-Π id) (λ _ → refl)
 
-  drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (m + k))
-  drop-put k = bffinv (drop' k) (≡-to-Π (flip _+_ k)) (flip m+n∸n≡m k)
+  drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec Carrier (k + m))
+  drop-put k = bffinv (drop' k) (≡-to-Π id) (λ _ → refl)
 
   double : ℕ → ℕ
   double zero    = zero
@@ -62,3 +61,9 @@ module InvExamples where
 
   sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (double m))
   sieve-put = bffinv sieve' (≡-to-Π double) sieve-inv-len
+
+  tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec Carrier (suc m))
+  tail-put = bffinv tail' (≡-to-Π id) (λ _ → refl)
+
+  take-put : (k : ℕ) → {n : ℕ}  → Vec Carrier (k + n) → Vec Carrier k → Maybe (Vec Carrier (k + n))
+  take-put k = bffsameshape (take' k)
diff --git a/Examples.agda b/Examples.agda
index 25bdbaa..764ac0f 100644
--- a/Examples.agda
+++ b/Examples.agda
@@ -1,9 +1,14 @@
 module Examples where
 
-open import Data.Nat using (ℕ ; zero ; suc ; _⊓_ ; _∸_ ; ⌈_/2⌉)
-open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_)
+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 (id to 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
@@ -27,19 +32,23 @@ double' = assume-get id↪ (≡-to-Π g) f
 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 id↪ (≡-to-Π _) (f n)
-  where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ⊓ n)
-        f n       []       = []
-        f zero    (x ∷ xs) = []
-        f (suc n) (x ∷ xs) = x ∷ f n xs
+take' n = assume-get (n+-injection n) (≡-to-Π _) (take n)
 
 drop' : ℕ → Get
-drop' n = assume-get id↪ (≡-to-Π _) (f n)
-  where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ∸ n)
-        f zero    xs       = xs
-        f (suc n) []       = []
-        f (suc n) (x ∷ xs) = f n xs
+drop' n = assume-get (n+-injection n) (≡-to-Π _) (drop n)
 
 sieve' : Get
 sieve' = assume-get id↪ (≡-to-Π _) f