drop-suc is cong pred
[~helmut/bidiragda.git] / Examples.agda
index 25bdbaa..bda3ae1 100644 (file)
@@ -1,11 +1,18 @@
 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⌉ ; pred)
+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.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L_)
+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 ; cong) renaming (setoid to EqSetoid)
 
 open import Generic using (≡-to-Π)
+open import Structures using (Shaped)
 import GetTypes
 import FreeTheorems
 
@@ -27,19 +34,20 @@ double' = assume-get id↪ (≡-to-Π g) f
 double'' : Get
 double'' = assume-get id↪ (≡-to-Π _) (λ v → v ++ v)
 
+suc-injection : EqSetoid ℕ ↪ EqSetoid ℕ
+suc-injection = record { to = ≡-to-Π suc; injective = cong pred }
+
+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
@@ -47,3 +55,47 @@ sieve' = assume-get id↪ (≡-to-Π _) f
         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
+
+data PairVec (α : Set) (β : Set) : List α → Set where
+  []P : PairVec α β []L
+  _,_∷P_ : (x : α) → β → {l : List α} → PairVec α β l → PairVec α β (x ∷L l)
+
+PairVecFirstShaped : (α : Set) → Shaped (List α) (PairVec α)
+PairVecFirstShaped α = record
+  { arity = length
+  ; content = content
+  ; fill = fill
+  ; isShaped = record
+    { content-fill = content-fill
+    ; fill-content = fill-content
+    } }
+  where content : {β : Set} {s : List α} → PairVec α β s → Vec β (length s)
+        content []P          = []
+        content (a , b ∷P p) = b ∷ content p
+
+        fill : {β : Set} → (s : List α) → Vec β (length s) → PairVec α β s
+        fill []L      v       = []P
+        fill (a ∷L s) (b ∷ v) = a , b ∷P fill s v
+
+        content-fill : {β : Set} {s : List α} → (p : PairVec α β s) → fill s (content p) ≡ p
+        content-fill []P          = refl
+        content-fill (a , b ∷P p) = cong (_,_∷P_ a b) (content-fill p)
+
+        fill-content : {β : Set} → (s : List α) → (v : Vec β (length s)) → content (fill s v) ≡ v
+        fill-content []L      []      = refl
+        fill-content (a ∷L s) (b ∷ v) = cong (_∷_ b) (fill-content s v)