[rational] towards proving useful things

agda/Data/Vec/Snoc.agda

@@ -7,22 +7,19 @@ open import Data.Product
 open import Data.Nat
 open import Data.Nat.Properties
 open import Data.List.Snoc using (List; Tsil; []; _,-_; _-,_)
+open import Data.Vec using (Vec; []) renaming (_∷_ to _,-_; _++_ to _<<<_)
 open import Relation.Nullary
 open import Relation.Binary.PropositionalEquality
 
 private variable
   X : Set
 
-data Vec (X : Set) : ℕ → Set where
-  [] : Vec X 0
-  _,-_ : ∀ {n} → X → Vec X n → Vec X (suc n)
-
 data Cev (X : Set) : ℕ → Set where
   [] : Cev X 0
   _-,_ : ∀ {n} → Cev X n → X → Cev X (suc n)
 
-head : ∀ {n} → (xs : Vec X n) {{_ : NonZero n}} → X
-head (x ,- xs) = x
+head : ∀ {n} → (xs : Cev X n) {{_ : NonZero n}} → X
+head (sx -, x) = x
 
 _><<_ : ∀ {n m} → Cev X n → Vec X m → Vec X (n + m)
 [] ><< ys = ys
@@ -32,17 +29,32 @@ _><>_ : ∀ {n m} → Cev X n → Vec X m → Cev X (n + m)
 _><>_ {n = n} sx [] rewrite +-identityʳ n = sx
 _><>_ {n = n} {suc m} sx (x ,- xs) rewrite (+-suc n m) = (sx -, x) ><> xs
 
-_<<<_ : ∀ {n m} → Vec X n → Vec X m → Vec X (n + m)
-_<<<_ [] ys = ys
-_<<<_ (x ,- xs) ys = x ,- (xs <<< ys)
+-- _<><_ : ∀ {n m} → Vec X n → Cev X m → Vec X (n + m)
+-- _<><_ = {!!}
+
+-- _>>>_ : ∀ {n m} → Cev X n → Cev X m → Cev X (n + m)
+-- _>>>_ = {!!}
+
+-- This is the inefficient way, but meh
+rev : ∀ {n} → Cev X n → Vec X n
+rev [] = []
+rev {n = suc n} (sx -, x) rewrite +-comm 1 n = (rev sx) <<< (x ,- [])
+
+data Any {X : Set} (P : X → Set) : ∀ {n} → Cev X n → Set where
+  here : ∀ {n x} {sx : Cev X n} → P x → Any P (sx -, x)
+  there : ∀ {n x} {sx : Cev X n} → Any P sx → Any P (sx -, x)
+
+_∈_ : {X : Set} → X → {n : ℕ} → Cev X n → Set
+x ∈ sx = Any (x ≡_) sx
 
-repeat : ∀ {n} → (k : ℕ) → Vec X n → Vec X (k * n)
-repeat zero xs = []
-repeat (suc k) xs = xs <<< repeat k xs
+-------------
+-- Zippers --
+-------------
 
 -- record Zipper (X : Set) : Set where
---   constructor _,_
+--   constructor _>[_]<_
 --   field
 --     front : Tsil X
+--     focus : X
 --     back : List X
 -- open Zipper

agda/Data/Vec/Util.agda

@@ -0,0 +1,15 @@
+{-# OPTIONS --safe --cubical-compatible #-}
+module Data.Vec.Util where
+
+open import Data.Vec
+open import Data.Nat
+
+private variable
+  X : Set
+
+repeat : ∀ {n} → (k : ℕ) → Vec X n → Vec X (k * n)
+repeat zero xs = []
+repeat (suc k) xs = xs ++ repeat k xs
+
+head-nz : ∀ {n} {{_ : NonZero n}} → Vec X n → X
+head-nz (x ∷ xs) = x