Example: show that PairVec is Shaped

Example inspired in VoigtlaenderHMW13. Note that Vec (α × β) (length s)
is not Shaped in this way since its real index is only a number.

1 files changed, 32 insertions, 1 deletions

diff --git a/Examples.agda b/Examples.agda
index c82bcf4..eca3c90 100644
--- a/Examples.agda
+++ b/Examples.agda
@@ -5,12 +5,14 @@ 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 (Injection to _↪_ ; id to id↪)
-open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) renaming (setoid to EqSetoid)
+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
 
@@ -71,3 +73,32 @@ 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)