Modify Fin definitions.

1 files changed, 113 insertions, 49 deletions

diff --git a/src/Cfe/Fin/Base.agda b/src/Cfe/Fin/Base.agda
index 9a0a4aa..f357048 100644
--- a/src/Cfe/Fin/Base.agda
+++ b/src/Cfe/Fin/Base.agda
@@ -2,29 +2,33 @@
 
 module Cfe.Fin.Base where
 
-open import Data.Nat using (ℕ; zero; suc)
-open import Data.Fin using (Fin; Fin′; zero; suc; inject₁)
+open import Data.Empty using (⊥-elim)
+open import Data.Nat using (ℕ; zero; suc; pred; z≤n)
+open import Data.Nat.Properties using (pred-mono)
+open import Data.Fin using (Fin; zero; suc; toℕ; inject₁; _≤_)
+open import Function using (_∘_)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong)
 
 data Fin< : ∀ {n} → Fin n → Set where
   zero : ∀ {n i} → Fin< {suc n} (suc i)
   suc  : ∀ {n i} → Fin< {n} i → Fin< (suc i)
 
-data Fin<′ : ∀ {n i} → Fin< {n} i → Set where
-  zero : ∀ {n i j} → Fin<′ {suc n} {suc i} (suc j)
-  suc  : ∀ {n i j} → Fin<′ {n} {i} j → Fin<′ (suc j)
-
--- Fin> {n} zero    ≡ Fin n
--- Fin>     (suc i) ≡ Fin> i
+data Fin<< : ∀ {n i} → Fin< {n} i → Set where
+  zero : ∀ {n i j} → Fin<< {suc n} {suc i} (suc j)
+  suc  : ∀ {n i j} → Fin<< {n} {i} j → Fin<< (suc j)
 
 data Fin> : ∀ {n} → Fin n → Set where
-  zero : ∀ {n} → Fin> {suc n} zero
+  zero : ∀ {n} → Fin> {suc (suc n)} zero
   suc  : ∀ {n} → Fin> {suc n} zero → Fin> {suc (suc n)} zero
   inj  : ∀ {n i} → Fin> {n} i → Fin> (suc i)
 
-data Fin>′ : ∀ {n i} → Fin> {n} i → Set where
-  zero : ∀ {n j} → Fin>′ {suc (suc n)} {zero} (suc j)
-  suc  : ∀ {n j} → Fin>′ {suc n} {zero} j → Fin>′ (suc j)
-  inj  : ∀ {n i j} → Fin>′ {n} {i} j → Fin>′ (inj j)
+data Fin>< : ∀ {n i} → Fin> {n} i → Set where
+  zero : ∀ {n j} → Fin>< {suc (suc n)} {zero} (suc j)
+  suc  : ∀ {n j} → Fin>< {suc n} {zero} j → Fin>< (suc j)
+  inj  : ∀ {n i j} → Fin>< {n} {i} j → Fin>< (inj j)
+
+------------------------------------------------------------------------
+-- Coversions to ℕ
 
 toℕ< : ∀ {n i} → Fin< {n} i → ℕ
 toℕ< zero    = 0
@@ -35,58 +39,118 @@ toℕ> zero    = 0
 toℕ> (suc j) = suc (toℕ> j)
 toℕ> (inj j) = suc (toℕ> j)
 
+------------------------------------------------------------------------
+-- Upwards injections
+
+inject!< : ∀ {n i} → Fin< {suc n} i → Fin n
+inject!< {suc _} zero    = zero
+inject!< {suc _} (suc j) = suc (inject!< j)
+
+inject< : ∀ {n i} → Fin< {n} i → Fin n
+inject< zero    = zero
+inject< (suc j) = suc (inject< j)
+
+inject₁< : ∀ {n i} → Fin< {n} i → Fin< (suc i)
+inject₁< zero    = zero
+inject₁< (suc j) = suc (inject₁< j)
+
+inject!<< : ∀ {n i j} → Fin<< {suc n} {suc i} j → Fin< i
+inject!<< {suc _} {suc _} zero    = zero
+inject!<< {suc _} {suc _} (suc k) = suc (inject!<< k)
+
+inject<< : ∀ {n i j} → Fin<< {n} {i} j → Fin< i
+inject<< zero    = zero
+inject<< (suc k) = suc (inject<< k)
+
+inject!>< : ∀ {n i j} → Fin>< {suc n} {inject₁ i} j → Fin> i
+inject!>< {suc (suc _)} {zero}  {suc j}  zero    = zero
+inject!>< {suc (suc _)} {zero}  {suc j}  (suc k) = suc (inject!>< k)
+inject!>< {suc (suc _)} {suc _} {inj j}  (inj k) = inj (inject!>< k)
+
+inject>< : ∀ {n i j} → Fin>< {n} {i} j → Fin> {n} i
+inject>< zero    = zero
+inject>< (suc k) = suc (inject>< k)
+inject>< (inj k) = inj (inject>< k)
+
+------------------------------------------------------------------------
+-- Downwards injections
+
 strengthen< : ∀ {n} → (i : Fin n) → Fin< (suc i)
 strengthen< zero    = zero
 strengthen< (suc i) = suc (strengthen< i)
 
-inject<! : ∀ {n i} → Fin< {suc n} i → Fin n
-inject<! {suc _} zero    = zero
-inject<! {suc _} (suc j) = suc (inject<! j)
+------------------------------------------------------------------------
+-- Casts
 
-cast<-inject₁ : ∀ {n i} → Fin< {n} i → Fin< (inject₁ i)
-cast<-inject₁ zero    = zero
-cast<-inject₁ (suc j) = suc (cast<-inject₁ j)
+cast< : ∀ {m n i j} → .(toℕ i ≡ toℕ j) → Fin< {m} i → Fin< {n} j
+cast< {i = suc _} {suc _} _   zero    = zero
+cast< {i = suc _} {suc _} i≡j (suc k) = suc (cast< (cong pred i≡j) k)
 
-inject<!′ : ∀ {n i j} → Fin<′ {suc n} {suc i} j → Fin< i
-inject<!′ {suc _} {suc _} zero    = zero
-inject<!′ {suc _} {suc _} (suc k) = suc (inject<!′ k)
+cast<< : ∀ {m n i j k l} → .(toℕ< k ≡ toℕ< l) → Fin<< {m} {i} k → Fin<< {n} {j} l
+cast<< {k = suc _} {suc _} _   zero    = zero
+cast<< {k = suc _} {suc _} k≡l (suc x) = suc (cast<< (cong pred k≡l) x)
 
-inject<′ : ∀ {n i j} → Fin<′ {n} {i} j → Fin< i
-inject<′ zero    = zero
-inject<′ (suc k) = suc (inject<′ k)
+cast> : ∀ {n i j} → .(j ≤ i) → Fin> {n} i → Fin> j
+cast> {_}           {zero}  {zero}  j≤i zero    = zero
+cast> {_}           {zero}  {zero}  j≤i (suc k) = suc (cast> j≤i k)
+cast> {suc (suc _)} {suc i} {zero}  j≤i (inj k) = suc (cast> z≤n k)
+cast> {suc (suc _)} {suc i} {suc j} j≤i (inj k) = inj (cast> (pred-mono j≤i) k)
 
-inject<!′-inject! : ∀ {n i j} → Fin<′ {suc n} {i} j → Fin< (inject<! j)
-inject<!′-inject! {suc n} {_} {suc j} zero    = zero
-inject<!′-inject! {suc n} {_} {suc j} (suc k) = suc (inject<!′-inject! k)
+------------------------------------------------------------------------
+-- Additions
 
-raise> : ∀ {n i} → Fin> {n} i → Fin n
-raise> {suc _} zero    = zero
-raise> {suc _} (suc j) = suc (raise> j)
-raise> {suc _} (inj j) = suc (raise> j)
+raise!> : ∀ {n i} → Fin> {suc n} i → Fin n
+raise!> {suc _} zero    = zero
+raise!> {suc _} (suc j) = suc (raise!> j)
+raise!> {suc _} (inj j) = suc (raise!> j)
 
 suc> : ∀ {n i} → Fin> {n} i → Fin> (inject₁ i)
 suc> zero    = suc zero
 suc> (suc j) = suc (suc> j)
 suc> (inj j) = inj (suc> j)
 
-inject>!′ : ∀ {n i j} → Fin>′ {suc n} {inject₁ i} j → Fin> {n} i
-inject>!′ {suc _}       {zero}          zero    = zero
-inject>!′ {suc (suc _)} {zero}  {suc _} (suc k) = suc (inject>!′ k)
-inject>!′ {suc _}       {suc i}         (inj k) = inj (inject>!′ k)
+------------------------------------------------------------------------
+-- Operations on the index
+
+-- predⁱ< {i = "i"} _ = "pred i"
+
+predⁱ< : ∀ {n i} → Fin< {suc n} i → Fin n
+predⁱ< {i = suc i} _ = i
+
+-- inject₁ⁱ> {i = "i"} _ = "i"
+
+inject₁ⁱ> : ∀ {n i} → Fin> {suc n} i → Fin n
+inject₁ⁱ>         zero    = zero
+inject₁ⁱ>         (suc _) = zero
+inject₁ⁱ> {suc _} (inj j) = suc (inject₁ⁱ> j)
+
+------------------------------------------------------------------------
+-- Operations
+
+punchIn> : ∀ {n i} → Fin> {suc n} (inject₁ i) → Fin> i → Fin> (inject₁ i)
+punchIn> {i = zero}  zero    k       = suc k
+punchIn> {i = zero}  (suc j) zero    = zero
+punchIn> {i = zero}  (suc j) (suc k) = suc (punchIn> j k)
+punchIn> {i = suc _} (inj j) (inj k) = inj (punchIn> j k)
+
+punchOut> : ∀ {n i j k} → raise!> {n} {i} j ≢ raise!> {n} {i} k → Fin> (inject₁ⁱ> j)
+punchOut>               {j = zero}        {zero}  j≢k = ⊥-elim (j≢k refl)
+punchOut>               {j = zero}        {suc k} j≢k = k
+punchOut> {suc (suc _)} {j = suc j}       {zero}  j≢k = zero
+punchOut> {suc (suc _)} {j = suc zero}    {suc k} j≢k = suc (punchOut> (j≢k ∘ cong suc))
+punchOut> {suc (suc _)} {j = suc (suc j)} {suc k} j≢k = suc (punchOut> {j = suc j} (j≢k ∘ cong suc))
+punchOut> {suc _}       {j = inj j}       {inj k} j≢k = inj (punchOut> (j≢k ∘ cong suc))
 
-inject>′ : ∀ {n i j} → Fin>′ {n} {i} j → Fin> {n} i
-inject>′ zero    = zero
-inject>′ (suc k) = suc (inject>′ k)
-inject>′ (inj k) = inj (inject>′ k)
+-- reflect "j" _ ≡ "j"
 
-cast>-inject<! : ∀ {n i} (j : Fin< (suc i)) → Fin> {suc n} i → Fin> (inject<! j)
-cast>-inject<!         zero    zero    = zero
-cast>-inject<!         zero    (suc k) = suc (cast>-inject<! zero k)
-cast>-inject<! {suc n} zero    (inj k) = suc (cast>-inject<! zero k)
-cast>-inject<! {suc n} (suc j) (inj k) = inj (cast>-inject<! j k)
+reflect! :
+  ∀ {n i} → (j : Fin< (suc {n} i)) → (k : Fin<< (suc j)) → Fin> (inject₁ (inject!< (inject!<< k)))
+reflect! {suc _}               zero    zero    = zero
+reflect! {suc (suc _)} {suc _} (suc j) zero    = suc (reflect! j zero)
+reflect! {suc (suc _)} {suc _} (suc j) (suc k) = inj (reflect! j k)
 
 reflect :
-  ∀ {n i} → (j : Fin< {suc (suc n)} (suc i)) → (k : Fin<′ (suc j)) → Fin> (inject<! (inject<!′ k))
-reflect                 zero    zero    = zero
-reflect {suc n} {suc i} (suc j) zero    = suc (reflect j zero)
-reflect {suc n} {suc i} (suc j) (suc k) = inj (reflect j k)
+  ∀ {n i} → (j : Fin< {n} i) → (k : Fin<< (suc j)) → Fin> (inject< (inject!<< k))
+reflect {suc (suc n)}               zero    zero    = zero
+reflect {_}           {suc (suc _)} (suc j) zero    = suc (reflect j zero)
+reflect {_}           {suc (suc _)} (suc j) (suc k) = inj (reflect j k)