diff options
Diffstat (limited to 'src/Cfe/Fin')
| -rw-r--r-- | src/Cfe/Fin/Base.agda | 162 | ||||
| -rw-r--r-- | src/Cfe/Fin/Properties.agda | 252 |
2 files changed, 339 insertions, 75 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) diff --git a/src/Cfe/Fin/Properties.agda b/src/Cfe/Fin/Properties.agda index 56a2c77..c07aa56 100644 --- a/src/Cfe/Fin/Properties.agda +++ b/src/Cfe/Fin/Properties.agda @@ -3,31 +3,231 @@ module Cfe.Fin.Properties where open import Cfe.Fin.Base -open import Data.Fin using (zero; suc; toℕ) -open import Data.Nat using (suc; pred) +open import Data.Empty using (⊥-elim) +open import Data.Fin using (zero; suc; toℕ; punchIn; punchOut; inject₁) +open import Data.Nat using (suc; pred; _≤_; _<_; _≥_; z≤n; s≤s) +open import Data.Nat.Properties using (suc-injective; pred-mono; module ≤-Reasoning) +open import Function using (_∘_) open import Relation.Binary.PropositionalEquality -inject<!-cong : ∀ {n i j k l} → toℕ< {i = i} k ≡ toℕ< {i = j} l → inject<! {n} k ≡ inject<! l -inject<!-cong {suc _} {k = zero} {zero} _ = refl -inject<!-cong {suc _} {k = suc k} {suc l} k≡l = cong suc (inject<!-cong (cong pred k≡l)) - -raise>-cong : ∀ {n i j k l} → toℕ> {i = i} k ≡ toℕ> {i = j} l → raise> {n} k ≡ raise> l -raise>-cong {suc _} {k = zero} {zero} _ = refl -raise>-cong {suc _} {k = suc k} {suc l} k≡l = cong suc (raise>-cong (cong pred k≡l)) -raise>-cong {suc _} {k = suc k} {inj l} k≡l = cong suc (raise>-cong (cong pred k≡l)) -raise>-cong {suc _} {k = inj k} {suc l} k≡l = cong suc (raise>-cong (cong pred k≡l)) -raise>-cong {suc _} {k = inj k} {inj l} k≡l = cong suc (raise>-cong (cong pred k≡l)) - -toℕ>-suc> : ∀ {n} j → toℕ> (suc> {suc n} j) ≡ toℕ> (suc j) -toℕ>-suc> zero = refl -toℕ>-suc> (suc j) = cong suc (toℕ>-suc> j) - -toℕ<-inject<! : ∀ {n i} j → toℕ (inject<! {n} {i} j) ≡ toℕ< j -toℕ<-inject<! {suc n} zero = refl -toℕ<-inject<! {suc n} (suc j) = cong suc (toℕ<-inject<! j) - -toℕ>-cast>-inject<! : ∀ {n i} j k → toℕ> k ≡ toℕ> (cast>-inject<! {n} {i} j k) -toℕ>-cast>-inject<! zero zero = refl -toℕ>-cast>-inject<! zero (suc k) = cong suc (toℕ>-cast>-inject<! zero k) -toℕ>-cast>-inject<! {suc n} zero (inj k) = cong suc (toℕ>-cast>-inject<! zero k) -toℕ>-cast>-inject<! {suc n} (suc j) (inj k) = cong suc (toℕ>-cast>-inject<! j k) +------------------------------------------------------------------------ +-- Properties missing from Data.Fin.Properties +------------------------------------------------------------------------ + +inject₁-mono : ∀ {n i j} → toℕ {n} i ≤ toℕ {n} j → toℕ (inject₁ i) ≤ toℕ (inject₁ j) +inject₁-mono {i = zero} i≤j = z≤n +inject₁-mono {i = suc i} {suc j} (s≤s i≤j) = s≤s (inject₁-mono i≤j) + +------------------------------------------------------------------------ +-- Properties of toℕ< +------------------------------------------------------------------------ + +toℕ<<i : ∀ {n i} j → toℕ< {n} {i} j < toℕ i +toℕ<<i zero = s≤s z≤n +toℕ<<i (suc j) = s≤s (toℕ<<i j) + +------------------------------------------------------------------------ +-- Properties of toℕ> + +toℕ>≥i : ∀ {n i} j → toℕ> {n} {i} j ≥ toℕ i +toℕ>≥i zero = z≤n +toℕ>≥i (suc j) = z≤n +toℕ>≥i (inj j) = s≤s (toℕ>≥i j) + +------------------------------------------------------------------------ +-- Properties of inject!< +------------------------------------------------------------------------ + +toℕ-inject!< : ∀ {n i} j → toℕ (inject!< {n} {i} j) ≡ toℕ< j +toℕ-inject!< {suc _} zero = refl +toℕ-inject!< {suc _} (suc j) = cong suc (toℕ-inject!< j) + +inject!<-mono : + ∀ {m n i j k l} → toℕ< k ≤ toℕ< l → toℕ (inject!< {m} {i} k) ≤ toℕ (inject!< {n} {j} l) +inject!<-mono {k = k} {l} k≤l = begin + toℕ (inject!< k) ≡⟨ toℕ-inject!< k ⟩ + toℕ< k ≤⟨ k≤l ⟩ + toℕ< l ≡˘⟨ toℕ-inject!< l ⟩ + toℕ (inject!< l) ∎ + where open ≤-Reasoning + +inject!<-cong : + ∀ {m n i j k l} → toℕ< k ≡ toℕ< l → toℕ (inject!< {m} {i} k) ≡ toℕ (inject!< {n} {j} l) +inject!<-cong {k = k} {l} k≡l = begin + toℕ (inject!< k) ≡⟨ toℕ-inject!< k ⟩ + toℕ< k ≡⟨ k≡l ⟩ + toℕ< l ≡˘⟨ toℕ-inject!< l ⟩ + toℕ (inject!< l) ∎ + where open ≡-Reasoning + +------------------------------------------------------------------------ +-- Properties of inject*<* +------------------------------------------------------------------------ + +inject-square : ∀ {n i j} k → inject< (inject!<< {n} {i} {j} k) ≡ inject!< (inject<< k) +inject-square {suc n} {suc i} zero = refl +inject-square {suc n} {suc i} (suc k) = cong suc (inject-square k) + +------------------------------------------------------------------------ +-- Properties of strengthen< +------------------------------------------------------------------------ + +toℕ-strengthen< : ∀ {n} i → toℕ< (strengthen< {n} i) ≡ toℕ i +toℕ-strengthen< zero = refl +toℕ-strengthen< (suc i) = cong suc (toℕ-strengthen< i) + +strengthen<-inject!< : ∀ {n i} j → toℕ< (strengthen< (inject!< {n} {i} j)) ≡ toℕ< j +strengthen<-inject!< {suc _} zero = refl +strengthen<-inject!< {suc _} (suc j) = cong suc (strengthen<-inject!< j) + +------------------------------------------------------------------------ +-- Properties of cast< +------------------------------------------------------------------------ + +toℕ-cast< : ∀ {m n i j} i≡j k → toℕ< (cast< {m} {n} {i} {j} i≡j k) ≡ toℕ< k +toℕ-cast< {i = suc _} {suc _} i≡j zero = refl +toℕ-cast< {i = suc _} {suc _} i≡j (suc k) = cong suc (toℕ-cast< (cong pred i≡j) k) + +------------------------------------------------------------------------ +-- Properties of cast> +------------------------------------------------------------------------ + +toℕ-cast> : ∀ {n i j} j≤i k → toℕ> (cast> {n} {i} {j} j≤i k) ≡ toℕ> k +toℕ-cast> {_} {zero} {zero} j≤i zero = refl +toℕ-cast> {_} {zero} {zero} j≤i (suc k) = cong suc (toℕ-cast> j≤i k) +toℕ-cast> {suc (suc n)} {suc i} {zero} j≤i (inj k) = cong suc (toℕ-cast> z≤n k) +toℕ-cast> {suc (suc n)} {suc i} {suc j} j≤i (inj k) = cong suc (toℕ-cast> (pred-mono j≤i) k) + +------------------------------------------------------------------------ +-- Properties of raise!> +------------------------------------------------------------------------ + +toℕ-raise!> : ∀ {n i} j → toℕ (raise!> {n} {i} j) ≡ toℕ> j +toℕ-raise!> zero = refl +toℕ-raise!> (suc j) = cong suc (toℕ-raise!> j) +toℕ-raise!> {suc n} (inj j) = cong suc (toℕ-raise!> j) + +raise!>-cong : ∀ {m n i j k l} → toℕ> k ≡ toℕ> l → toℕ (raise!> {m} {i} k) ≡ toℕ (raise!> {n} {j} l) +raise!>-cong {k = k} {l} k≡l = begin + toℕ (raise!> k) ≡⟨ toℕ-raise!> k ⟩ + toℕ> k ≡⟨ k≡l ⟩ + toℕ> l ≡˘⟨ toℕ-raise!> l ⟩ + toℕ (raise!> l) ∎ + where open ≡-Reasoning + +------------------------------------------------------------------------ +-- Properties of suc> +------------------------------------------------------------------------ + +toℕ-suc> : ∀ {n i} j → toℕ> (suc> {n} {i} j) ≡ suc (toℕ> j) +toℕ-suc> zero = refl +toℕ-suc> (suc j) = cong suc (toℕ-suc> j) +toℕ-suc> (inj j) = cong suc (toℕ-suc> j) + +------------------------------------------------------------------------ +-- Properties of predⁱ< +------------------------------------------------------------------------ + +toℕ-predⁱ< : ∀ {n i} j → suc (toℕ (predⁱ< {n} {i} j)) ≡ toℕ i +toℕ-predⁱ< {i = suc _} _ = refl + +predⁱ<-mono : + ∀ {n i j} k l → toℕ i ≤ toℕ j → toℕ (predⁱ< {n} {i} k) ≤ toℕ (predⁱ< {n} {j} l) +predⁱ<-mono {i = i} {j} k l i≤j = pred-mono (begin + suc (toℕ (predⁱ< k)) ≡⟨ toℕ-predⁱ< k ⟩ + toℕ i ≤⟨ i≤j ⟩ + toℕ j ≡˘⟨ toℕ-predⁱ< l ⟩ + suc (toℕ (predⁱ< l)) ∎) + where open ≤-Reasoning + +predⁱ<-cong : + ∀ {n i j} k l → toℕ i ≡ toℕ j → toℕ (predⁱ< {n} {i} k) ≡ toℕ (predⁱ< {n} {j} l) +predⁱ<-cong {i = i} {j} k l i≡j = suc-injective (begin + suc (toℕ (predⁱ< k)) ≡⟨ toℕ-predⁱ< k ⟩ + toℕ i ≡⟨ i≡j ⟩ + toℕ j ≡˘⟨ toℕ-predⁱ< l ⟩ + suc (toℕ (predⁱ< l)) ∎) + where open ≡-Reasoning + +------------------------------------------------------------------------ +-- Properties of inject₁ⁱ> +------------------------------------------------------------------------ + +toℕ-inject₁ⁱ> : ∀ {n i} j → toℕ (inject₁ⁱ> {n} {i} j) ≡ toℕ i +toℕ-inject₁ⁱ> {suc _} zero = refl +toℕ-inject₁ⁱ> {suc _} (suc k) = refl +toℕ-inject₁ⁱ> {suc _} (inj k) = cong suc (toℕ-inject₁ⁱ> k) + +inject₁ⁱ>-mono : + ∀ {n i j} k l → toℕ i ≤ toℕ j → toℕ (inject₁ⁱ> {n} {i} k) ≤ toℕ (inject₁ⁱ> {n} {j} l) +inject₁ⁱ>-mono {i = i} {j} k l i≤j = begin + toℕ (inject₁ⁱ> k) ≡⟨ toℕ-inject₁ⁱ> k ⟩ + toℕ i ≤⟨ i≤j ⟩ + toℕ j ≡˘⟨ toℕ-inject₁ⁱ> l ⟩ + toℕ (inject₁ⁱ> l) ∎ + where open ≤-Reasoning + +inject₁ⁱ>-cong : + ∀ {n i j} k l → toℕ i ≡ toℕ j → toℕ (inject₁ⁱ> {n} {i} k) ≡ toℕ (inject₁ⁱ> {n} {j} l) +inject₁ⁱ>-cong {i = i} {j} k l i≡j = begin + toℕ (inject₁ⁱ> k) ≡⟨ toℕ-inject₁ⁱ> k ⟩ + toℕ i ≡⟨ i≡j ⟩ + toℕ j ≡˘⟨ toℕ-inject₁ⁱ> l ⟩ + toℕ (inject₁ⁱ> l) ∎ + where open ≡-Reasoning + +------------------------------------------------------------------------ +-- Properties of punchIn> +------------------------------------------------------------------------ + +toℕ-punchIn> : ∀ {n i} j k → toℕ> (punchIn> {suc n} {i} j k) ≡ toℕ (punchIn (raise!> j) (raise!> k)) +toℕ-punchIn> {_} {zero} zero k = sym (cong suc (toℕ-raise!> k)) +toℕ-punchIn> {_} {zero} (suc j) zero = refl +toℕ-punchIn> {_} {zero} (suc j) (suc k) = cong suc (toℕ-punchIn> j k) +toℕ-punchIn> {suc _} {suc i} (inj j) (inj k) = cong suc (toℕ-punchIn> j k) + +------------------------------------------------------------------------ +-- Properties of punchOut> +------------------------------------------------------------------------ + +toℕ-punchOut> : ∀ {n i j k} j≢k → toℕ> (punchOut> {suc n} {i} {j} {k} j≢k) ≡ toℕ (punchOut j≢k) +toℕ-punchOut> {_} {_} {zero} {zero} j≢k = ⊥-elim (j≢k refl) +toℕ-punchOut> {_} {_} {zero} {suc k} j≢k = sym (toℕ-raise!> k) +toℕ-punchOut> {suc _} {_} {suc j} {zero} j≢k = refl +toℕ-punchOut> {suc _} {_} {suc zero} {suc k} j≢k = + cong suc (toℕ-punchOut> (j≢k ∘ cong suc)) +toℕ-punchOut> {suc _} {_} {suc (suc j)} {suc k} j≢k = + cong suc (toℕ-punchOut> {j = suc j} (j≢k ∘ cong suc)) +toℕ-punchOut> {suc _} {suc zero} {inj j} {inj k} j≢k = + cong suc (toℕ-punchOut> (j≢k ∘ cong suc)) +toℕ-punchOut> {suc _} {suc (suc _)} {inj j} {inj k} j≢k = + cong suc (toℕ-punchOut> (j≢k ∘ cong suc)) + +------------------------------------------------------------------------ +-- Properties of reflect! +------------------------------------------------------------------------ + +toℕ-reflect! : ∀ {n i} j k → toℕ> (reflect! {n} {i} j k) ≡ toℕ< j +toℕ-reflect! {suc _} zero zero = refl +toℕ-reflect! {suc (suc _)} {suc _} (suc j) zero = cong suc (toℕ-reflect! j zero) +toℕ-reflect! {suc (suc _)} {suc _} (suc j) (suc k) = cong suc (toℕ-reflect! j k) + +------------------------------------------------------------------------ +-- Properties of reflect +------------------------------------------------------------------------ + +toℕ-reflect : ∀ {n i} j k → toℕ> (reflect {n} {i} j k) ≡ toℕ< j +toℕ-reflect {suc (suc _)} zero zero = refl +toℕ-reflect {_} {suc (suc _)} (suc j) zero = cong suc (toℕ-reflect j zero) +toℕ-reflect {_} {suc (suc _)} (suc j) (suc k) = cong suc (toℕ-reflect j k) + +------------------------------------------------------------------------ +-- Other properties +------------------------------------------------------------------------ + +inj-punchOut : + ∀ {n i j k} → (j≢k : inject!< {suc n} {suc i} j ≢ raise!> (inj {suc n} {i} k)) → + toℕ (punchOut j≢k) ≡ toℕ> k +inj-punchOut {j = zero} {k} j≢k = toℕ-raise!> k +inj-punchOut {suc n} {j = suc j} {inj k} j≢k = cong suc (inj-punchOut (j≢k ∘ cong suc)) + |