[rational] lassos

agda/Data/Fin/MoreProps.agda

@@ -4,11 +4,22 @@ module Data.Fin.MoreProps where
 open import Data.Nat hiding (_>_) renaming (_<_ to _<ℕ_)
 open import Data.Fin
 open import Data.Fin.Properties
+open import Data.Unit
+open import Data.Empty
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.PropositionalEquality.WithK
 open import Algebra.Structures.Propositional
 open import Function
 
+IsMax : ∀ {n} → Fin n → Set
+IsMax {(suc zero)} zero = ⊤
+IsMax {(suc (suc _))} zero = ⊥
+IsMax (suc x) = IsMax x
+
+fromℕ-ismax : ∀ n → IsMax (fromℕ n)
+fromℕ-ismax zero = tt
+fromℕ-ismax (suc n) = fromℕ-ismax n
+
 <-isPropStrictTotalOrder : ∀ n → IsPropStrictTotalOrder (_≡_ {A = Fin n}) _<_
 IsPropStrictTotalOrder.isSTO (<-isPropStrictTotalOrder n) = <-isStrictTotalOrder
 IsPropStrictTotalOrder.≈-prop (<-isPropStrictTotalOrder n) = ≡-irrelevant

agda/Data/List/Snoc.agda

@@ -0,0 +1,44 @@
+{-# OPTIONS --safe --cubical-compatible #-}
+
+-- Working with snoc lists.
+module Data.List.Snoc where
+open import Data.Product
+open import Relation.Nullary
+
+private variable
+  X : Set
+
+data List (X : Set) : Set where
+  [] : List X
+  _,-_ : X → List X → List X
+
+data Empty {X : Set} : List X → Set where
+  instance [] : Empty []
+
+data NonEmpty {X : Set} : List X → Set where
+  instance cons : ∀ {x xs} → NonEmpty (x ,- xs)
+
+¬Empty&NonEmpty : ∀ {X} {xs : List X} → ¬ (Empty xs × NonEmpty xs)
+¬Empty&NonEmpty ([] , ())
+
+data Tsil (X : Set) : Set where
+  [] : Tsil X
+  _-,_ : Tsil X → X → Tsil X
+
+head : (xs : List X) → {{_ : NonEmpty xs}} → X
+head (x ,- xs) = x
+
+_><<_ : Tsil X → List X → List X
+[] ><< ys = ys
+(sx -, x) ><< ys = sx ><< (x ,- ys)
+
+_><>_ : Tsil X → List X → Tsil X
+sx ><> [] = sx
+sx ><> (x ,- xs) = (sx -, x) ><> xs
+
+record Zipper (X : Set) : Set where
+  constructor _,_
+  field
+    front : Tsil X
+    back : List X
+open Zipper

agda/Data/Nat/MoreProps.agda

@@ -3,7 +3,15 @@ module Data.Nat.MoreProps where
 open import Algebra.Structures.Propositional
 open import Data.Nat
 open import Data.Nat.Properties
+open import Data.Product
 open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+
+data Zero : ℕ → Set where
+  instance zero : Zero zero
+
+¬Z&NZ : {n : ℕ} → ¬ (Zero n × NonZero n)
+¬Z&NZ (zero , ())
 
 ≤-stepL : ∀ {x y} → suc x ≤ y → x ≤ y
 ≤-stepL (s≤s z≤n) = z≤n

agda/Data/Vec/Snoc.agda

@@ -0,0 +1,48 @@
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+-- Working with snoc lists.
+module Data.Vec.Snoc where
+open import Data.Product
+open import Data.Nat
+open import Data.Nat.Properties
+open import Data.List.Snoc using (List; Tsil; []; _,-_; _-,_)
+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
+
+_><<_ : ∀ {n m} → Cev X n → Vec X m → Vec X (n + m)
+[] ><< ys = ys
+_><<_ {n = suc n} {m} (sx -, x) ys rewrite sym (+-suc n m) = sx ><< (x ,- ys)
+
+_><>_ : ∀ {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)
+
+repeat : ∀ {n} → (k : ℕ) → Vec X n → Vec X (k * n)
+repeat zero xs = []
+repeat (suc k) xs = xs <<< repeat k xs
+
+-- record Zipper (X : Set) : Set where
+--   constructor _,_
+--   field
+--     front : Tsil X
+--     back : List X
+-- open Zipper