From fb37a9b65813666a3963c240a1bc8f6978a4866f Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sat, 24 Apr 2021 13:55:33 +0100 Subject: Modify Fin definitions. --- src/Cfe/Fin/Base.agda | 162 +++++++++++++++++++++++++++++++++++--------------- 1 file changed, 113 insertions(+), 49 deletions(-) (limited to 'src/Cfe/Fin/Base.agda') 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 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 : ∀ {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 {suc n} i → Fin> (inject-inject-inject-inject-inject-inject-inject-inject (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< (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) -- cgit v1.2.3