Rework Context one last time.

2 files changed, 125 insertions, 0 deletions

diff --git a/src/Cfe/Fin/Base.agda b/src/Cfe/Fin/Base.agda
new file mode 100644
index 0000000..9a0a4aa
--- /dev/null
+++ b/src/Cfe/Fin/Base.agda
@@ -0,0 +1,92 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Cfe.Fin.Base where
+
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Fin using (Fin; Fin′; zero; suc; inject₁)
+
+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} → Fin n → Set where
+  zero : ∀ {n} → Fin> {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)
+
+toℕ< : ∀ {n i} → Fin< {n} i → ℕ
+toℕ< zero    = 0
+toℕ< (suc j) = suc (toℕ< j)
+
+toℕ> : ∀ {n i} → Fin> {n} i → ℕ
+toℕ> zero    = 0
+toℕ> (suc j) = suc (toℕ> j)
+toℕ> (inj j) = suc (toℕ> j)
+
+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)
+
+cast<-inject₁ : ∀ {n i} → Fin< {n} i → Fin< (inject₁ i)
+cast<-inject₁ zero    = zero
+cast<-inject₁ (suc j) = suc (cast<-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<!′-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)
+
+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)
+
+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)
+
+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)
+
+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 (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)
diff --git a/src/Cfe/Fin/Properties.agda b/src/Cfe/Fin/Properties.agda
new file mode 100644
index 0000000..56a2c77
--- /dev/null
+++ b/src/Cfe/Fin/Properties.agda
@@ -0,0 +1,33 @@
+{-# OPTIONS --without-K --safe #-}
+
+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 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)