diff options
Diffstat (limited to 'src/Cfe/Fin/Base.agda')
| -rw-r--r-- | src/Cfe/Fin/Base.agda | 162 |
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) |