Add a recursive view of Fin n (#1923)

Author: jamesmckinna

CHANGELOG.md

@@ -1585,6 +1585,11 @@ New modules
   Data.Default
   ```
 
+* A small library defining a structurally recursive view of `Fin n`:
+  ```
+  Data.Fin.Relation.Unary.Top
+  ```
+
 * A small library for a non-empty fresh list:
   ```
   Data.List.Fresh.NonEmpty
@@ -2146,6 +2151,8 @@ Additions to existing modules
   cast-is-id    : cast eq k ≡ k
   subst-is-cast : subst Fin eq k ≡ cast eq k
   cast-trans    : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k
+
+  fromℕ≢inject₁      : {i : Fin n} → fromℕ n ≢ inject₁ i
   ```
 
 * Added new functions in `Data.Integer.Base`:

README/Data/Fin/Relation/Unary/Top.agda

@@ -0,0 +1,100 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Example use of the 'top' view of Fin
+--
+-- This is an example of a view of (elements of) a datatype,
+-- here i : Fin (suc n), which exhibits every such i as
+-- * either, i = fromℕ n
+-- * or, i = inject₁ j for a unique j : Fin n
+--
+-- Using this view, we can redefine certain operations in `Data.Fin.Base`,
+-- together with their corresponding properties in `Data.Fin.Properties`.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module README.Data.Fin.Relation.Unary.Top where
+
+open import Data.Nat.Base using (ℕ; zero; suc; _∸_; _≤_)
+open import Data.Nat.Properties using (n∸n≡0; +-∸-assoc; ≤-reflexive)
+open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; inject₁; _>_)
+open import Data.Fin.Properties using (toℕ-fromℕ; toℕ<n; toℕ-inject₁)
+open import Data.Fin.Induction hiding (>-weakInduction)
+open import Data.Fin.Relation.Unary.Top
+import Induction.WellFounded as WF
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality
+open import Relation.Unary using (Pred)
+
+private
+  variable
+    ℓ : Level
+    n : ℕ
+
+------------------------------------------------------------------------
+-- Reimplementation of `Data.Fin.Base.opposite`, and its properties
+
+-- Definition
+
+opposite : Fin n → Fin n
+opposite {suc n} i with view i
+... | ‵fromℕ     = zero
+... | ‵inject₁ j = suc (opposite {n} j)
+
+-- Properties
+
+opposite-zero≡fromℕ : ∀ n → opposite {suc n} zero ≡ fromℕ n
+opposite-zero≡fromℕ zero    = refl
+opposite-zero≡fromℕ (suc n) = cong suc (opposite-zero≡fromℕ n)
+
+opposite-fromℕ≡zero : ∀ n → opposite {suc n} (fromℕ n) ≡ zero
+opposite-fromℕ≡zero n rewrite view-fromℕ n = refl
+
+opposite-suc≡inject₁-opposite : (j : Fin n) →
+                                opposite (suc j) ≡ inject₁ (opposite j)
+opposite-suc≡inject₁-opposite {suc n} i with view i
+... | ‵fromℕ     = refl
+... | ‵inject₁ j = cong suc (opposite-suc≡inject₁-opposite {n} j)
+
+opposite-involutive : (j : Fin n) → opposite (opposite j) ≡ j
+opposite-involutive {suc n} zero
+  rewrite opposite-zero≡fromℕ n
+        | view-fromℕ n              = refl
+opposite-involutive {suc n} (suc i)
+  rewrite opposite-suc≡inject₁-opposite i
+        | view-inject₁ (opposite i) = cong suc (opposite-involutive i)
+
+opposite-suc : (j : Fin n) → toℕ (opposite (suc j)) ≡ toℕ (opposite j)
+opposite-suc j = begin
+  toℕ (opposite (suc j))      ≡⟨ cong toℕ (opposite-suc≡inject₁-opposite j) ⟩
+  toℕ (inject₁ (opposite j))  ≡⟨ toℕ-inject₁ (opposite j) ⟩
+  toℕ (opposite j)            ∎ where open ≡-Reasoning
+
+opposite-prop : (j : Fin n) → toℕ (opposite j) ≡ n ∸ suc (toℕ j)
+opposite-prop {suc n} i with view i
+... | ‵fromℕ  rewrite toℕ-fromℕ n | n∸n≡0 n = refl
+... | ‵inject₁ j = begin
+  suc (toℕ (opposite j)) ≡⟨ cong suc (opposite-prop j) ⟩
+  suc (n ∸ suc (toℕ j))  ≡˘⟨ +-∸-assoc 1 (toℕ<n j) ⟩
+  n ∸ toℕ j              ≡˘⟨ cong (n ∸_) (toℕ-inject₁ j) ⟩
+  n ∸ toℕ (inject₁ j)    ∎ where open ≡-Reasoning
+
+------------------------------------------------------------------------
+-- Reimplementation of `Data.Fin.Induction.>-weakInduction`
+
+open WF using (Acc; acc)
+
+>-weakInduction : (P : Pred (Fin (suc n)) ℓ) →
+                  P (fromℕ n) →
+                  (∀ i → P (suc i) → P (inject₁ i)) →
+                  ∀ i → P i
+>-weakInduction P Pₙ Pᵢ₊₁⇒Pᵢ i = induct (>-wellFounded i)
+  where
+  induct : ∀ {i} → Acc _>_ i → P i
+  induct {i} (acc rec) with view i
+  ... | ‵fromℕ = Pₙ
+  ... | ‵inject₁ j = Pᵢ₊₁⇒Pᵢ j (induct (rec _ inject₁[j]+1≤[j+1]))
+    where
+    inject₁[j]+1≤[j+1] : suc (toℕ (inject₁ j)) ≤ toℕ (suc j)
+    inject₁[j]+1≤[j+1] = ≤-reflexive (toℕ-inject₁ (suc j))

src/Data/Fin/Properties.agda

@@ -449,6 +449,9 @@ toℕ-inject {i = suc i} (suc j) = cong suc (toℕ-inject j)
 -- inject₁
 ------------------------------------------------------------------------
 
+fromℕ≢inject₁ : fromℕ n ≢ inject₁ i
+fromℕ≢inject₁ {i = suc i} eq = fromℕ≢inject₁ {i = i} (suc-injective eq)
+
 inject₁-injective : inject₁ i ≡ inject₁ j → i ≡ j
 inject₁-injective {i = zero}  {zero}  i≡j = refl
 inject₁-injective {i = suc i} {suc j} i≡j =

src/Data/Fin/Relation/Unary/Top.agda

@@ -0,0 +1,79 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The 'top' view of Fin.
+--
+-- This is an example of a view of (elements of) a datatype,
+-- here i : Fin (suc n), which exhibits every such i as
+-- * either, i = fromℕ n
+-- * or, i = inject₁ j for a unique j : Fin n
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Fin.Relation.Unary.Top where
+
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Fin.Base using (Fin; zero; suc; fromℕ; inject₁)
+open import Relation.Binary.PropositionalEquality.Core
+
+private
+  variable
+    n : ℕ
+    i : Fin n
+
+------------------------------------------------------------------------
+-- The View, considered as a unary relation on Fin n
+
+-- NB `Data.Fin.Properties.fromℕ≢inject₁` establishes that the following
+-- inductively defined family on `Fin n` has constructors which target
+-- *disjoint* instances of the family (moreover at indices `n = suc _`);
+-- hence the interpretations of the View constructors will also be disjoint.
+
+data View : (i : Fin n) → Set where
+  ‵fromℕ : View (fromℕ n)
+  ‵inj₁ : View i → View (inject₁ i)
+
+pattern ‵inject₁ i = ‵inj₁ {i = i} _
+
+-- The view covering function, witnessing soundness of the view
+
+view : (i : Fin n) → View i
+view zero = view-zero where
+  view-zero : View (zero {n})
+  view-zero {n = zero}  = ‵fromℕ
+  view-zero {n = suc _} = ‵inj₁ view-zero
+view (suc i) with view i
+... | ‵fromℕ     = ‵fromℕ
+... | ‵inject₁ i = ‵inj₁ (view (suc i))
+
+-- Interpretation of the view constructors
+
+⟦_⟧ : {i : Fin n} → View i → Fin n
+⟦ ‵fromℕ ⟧     = fromℕ _
+⟦ ‵inject₁ i ⟧ = inject₁ i
+
+-- Completeness of the view
+
+view-complete : (v : View i) → ⟦ v ⟧ ≡ i
+view-complete ‵fromℕ    = refl
+view-complete (‵inj₁ _) = refl
+
+-- 'Computational' behaviour of the covering function
+
+view-fromℕ : ∀ n → view (fromℕ n) ≡ ‵fromℕ
+view-fromℕ zero                         = refl
+view-fromℕ (suc n) rewrite view-fromℕ n = refl
+
+view-inject₁ : (i : Fin n) → view (inject₁ i) ≡ ‵inj₁ (view i)
+view-inject₁ zero                           = refl
+view-inject₁ (suc i) rewrite view-inject₁ i = refl
+
+-- Uniqueness of the view
+
+view-unique : (v : View i) → view i ≡ v
+view-unique ‵fromℕ            = view-fromℕ _
+view-unique (‵inj₁ {i = i} v) = begin
+  view (inject₁ i) ≡⟨ view-inject₁ i ⟩
+  ‵inj₁ (view i)   ≡⟨ cong ‵inj₁ (view-unique v) ⟩
+  ‵inj₁ v          ∎ where open ≡-Reasoning