A followup on the Top view #1923

CHANGELOG.md

@@ -1174,6 +1174,8 @@ Deprecated names
   Likewise under issue #1726: the properties `≺⇒<′` and `<′⇒≺` have been deprecated
   in favour of their proxy counterparts `<⇒<′` and `<′⇒<`.
 
+  Additionally, `lower₁-inject₁′` has been deprecated in favour of `inject₁≡⇒lower₁≡`.
+
 * In `Data.Fin.Permutation.Components`:
   ```
   reverse            ↦ Data.Fin.Base.opposite
@@ -1585,6 +1587,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 +2153,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/Lower.agda

@@ -0,0 +1,140 @@
+------------------------------------------------------------------------
+-- 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`.
+------------------------------------------------------------------------
+
+--- NB this is a provisional commit, ahead of merging PR #1923
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module README.Data.Fin.Relation.Unary.Lower where
+
+open import Data.Nat.Base using (ℕ; zero; suc; pred)
+open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; inject₁)
+open import Data.Fin.Properties
+  using (toℕ-fromℕ; toℕ-inject₁; toℕ-inject₁-≢; inject₁-injective)
+import Data.Fin.Relation.Unary.Top as Top
+open import Level using (Level)
+open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Binary.PropositionalEquality
+open import Relation.Unary using (Pred)
+
+private
+  variable
+    ℓ : Level
+    n : ℕ
+    i j : Fin n
+
+------------------------------------------------------------------------
+-- Derived induction principles from the Top view, via another view!
+
+-- The idea being, that in what follows, a call pattern is repeated over
+-- and over again, so should be reified as induction over a revised view,
+-- obtained from `Top.view` by restricting the domain
+
+data View : {i : Fin (suc n)} → n ≢ toℕ i → Set where
+  ‵inject₁ : (j : Fin n) {n≢j : n ≢ toℕ (inject₁ j)} → View n≢j
+
+view : {i : Fin (suc n)} (n≢i : n ≢ toℕ i) → View n≢i
+view {i = i} n≢i with Top.view i
+... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i
+... | Top.‵inject₁ j = ‵inject₁ j
+
+
+------------------------------------------------------------------------
+-- Reimplementation of `Data.Fin.Base.lower₁` and its properties,
+-- together with the streamlined versions obtained from the view. 
+
+-- definition of lower₁/inject₁⁻¹
+
+lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n
+lower₁ i n≢i with Top.view i
+... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i
+... | Top.‵inject₁ j = j
+
+inject₁⁻¹ : ∀ (i : Fin (suc n)) → (n ≢ toℕ i) → Fin n
+inject₁⁻¹ i n≢i with ‵inject₁ j ← view n≢i = j
+
+------------------------------------------------------------------------
+-- properties of lower₁/inject₁⁻¹
+
+toℕ-lower₁ : ∀ i (n≢i : n ≢ toℕ i) → toℕ (lower₁ i n≢i) ≡ toℕ i
+toℕ-lower₁ i n≢i with Top.view i
+... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i
+... | Top.‵inject₁ j = sym (toℕ-inject₁ j)
+
+toℕ-inject₁⁻¹ : ∀ i (n≢i : n ≢ toℕ i) → toℕ (inject₁⁻¹ i n≢i) ≡ toℕ i
+toℕ-inject₁⁻¹ i n≢i with ‵inject₁ j ← view n≢i = sym (toℕ-inject₁ j)
+
+lower₁-injective : ∀ {n≢i : n ≢ toℕ i} {n≢j : n ≢ toℕ j} →
+                   lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j
+lower₁-injective {i = i} {j = j} {n≢i} {n≢j} eq with Top.view i
+... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i
+... | Top.‵inject₁ _ with Top.view j
+... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢j
+... | Top.‵inject₁ _ = cong inject₁ eq
+
+inject₁⁻¹-injective : ∀ {n≢i : n ≢ toℕ i} {n≢j : n ≢ toℕ j} →
+                   inject₁⁻¹ i n≢i ≡ inject₁⁻¹ j n≢j → i ≡ j
+inject₁⁻¹-injective {i = i} {j = j} {n≢i} {n≢j} eq
+  with ‵inject₁ _ ← view n≢i | ‵inject₁ _ ← view n≢j = cong inject₁ eq
+
+lower₁-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) →
+                    lower₁ i n≢i₁ ≡ lower₁ i n≢i₂
+lower₁-irrelevant i n≢i₁ n≢i₂ with Top.view i
+... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i₁
+... | Top.‵inject₁ _ = refl
+
+-- here we need/use a helper function, in order to avoid having
+-- to appeal to injectivity of inject₁ in the unifier
+inject₁⁻¹-irrelevant′ : ∀ {i j : Fin (suc n)} (i≡j : i ≡ j) →
+                        (n≢i : n ≢ toℕ i) (n≢j : n ≢ toℕ j) →
+                        inject₁⁻¹ i n≢i ≡ inject₁⁻¹ j n≢j
+inject₁⁻¹-irrelevant′ eq n≢i n≢j
+  with ‵inject₁ _ ← view n≢i | ‵inject₁ _ ← view n≢j = inject₁-injective eq
+
+inject₁⁻¹-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) →
+                       inject₁⁻¹ i n≢i₁ ≡ inject₁⁻¹ i n≢i₂
+inject₁⁻¹-irrelevant i = inject₁⁻¹-irrelevant′ refl
+
+------------------------------------------------------------------------
+-- inject₁ and lower₁/inject₁⁻¹
+
+inject₁-lower₁ : ∀ (i : Fin (suc n)) (n≢i : n ≢ toℕ i) →
+                 inject₁ (lower₁ i n≢i) ≡ i
+inject₁-lower₁ i n≢i with Top.view i
+... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i
+... | Top.‵inject₁ _ = refl
+
+inject₁-inject₁⁻¹ : ∀ (i : Fin (suc n)) (n≢i : n ≢ toℕ i) →
+                 inject₁ (inject₁⁻¹ i n≢i) ≡ i
+inject₁-inject₁⁻¹ i n≢i with ‵inject₁ _ ← view n≢i = refl
+
+inject₁≡⇒lower₁≡ : {i : Fin (ℕ.suc n)} (n≢i : n ≢ toℕ i) →
+                   inject₁ j ≡ i → lower₁ i n≢i ≡ j
+inject₁≡⇒lower₁≡ {i = i} n≢i inject₁[j]≡i  with Top.view i
+... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i
+... | Top.‵inject₁ _ = sym (inject₁-injective inject₁[j]≡i)
+
+inject₁≡⇒inject₁⁻¹≡ : {i : Fin (ℕ.suc n)} (n≢i : n ≢ toℕ i) →
+                      inject₁ j ≡ i → inject₁⁻¹ i n≢i ≡ j
+inject₁≡⇒inject₁⁻¹≡ {i = i} n≢i inject₁[j]≡i  with ‵inject₁ _ ← view n≢i
+  = sym (inject₁-injective inject₁[j]≡i)
+
+lower₁-inject₁ : ∀ (i : Fin n) →
+                 lower₁ (inject₁ i) (toℕ-inject₁-≢ i) ≡ i
+lower₁-inject₁ {n} i = inject₁≡⇒lower₁≡ (toℕ-inject₁-≢ i) refl
+
+inject₁⁻¹-inject₁ : ∀ (i : Fin n) →
+                    inject₁⁻¹ (inject₁ i) (toℕ-inject₁-≢ i) ≡ i
+inject₁⁻¹-inject₁ {n} i = inject₁≡⇒inject₁⁻¹≡ (toℕ-inject₁-≢ i) refl
+

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 =
@@ -494,6 +497,13 @@ lower₁-injective {suc n} {zero}  {zero}  {_}   {_}   refl = refl
 lower₁-injective {suc n} {suc i} {suc j} {n≢i} {n≢j} eq   =
   cong suc (lower₁-injective (suc-injective eq))
 
+lower₁-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) →
+                    lower₁ i n≢i₁ ≡ lower₁ i n≢i₂
+lower₁-irrelevant {zero}  zero     0≢0 _ = contradiction refl 0≢0
+lower₁-irrelevant {suc n} zero     _   _ = refl
+lower₁-irrelevant {suc n} (suc i)  _   _ =
+  cong suc (lower₁-irrelevant i _ _)
+
 ------------------------------------------------------------------------
 -- inject₁ and lower₁
 
@@ -504,26 +514,13 @@ inject₁-lower₁ {suc n} zero     _       = refl
 inject₁-lower₁ {suc n} (suc i)  n+1≢i+1 =
   cong suc (inject₁-lower₁ i  (n+1≢i+1 ∘ cong suc))
 
-lower₁-inject₁′ : ∀ (i : Fin n) (n≢i : n ≢ toℕ (inject₁ i)) →
-                  lower₁ (inject₁ i) n≢i ≡ i
-lower₁-inject₁′ zero    _       = refl
-lower₁-inject₁′ (suc i) n+1≢i+1 =
-  cong suc (lower₁-inject₁′ i (n+1≢i+1 ∘ cong suc))
+inject₁≡⇒lower₁≡ : ∀ {j : Fin (ℕ.suc n)} (n≢j : n ≢ toℕ j) →
+                   inject₁ i ≡ j → lower₁ j n≢j ≡ i
+inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-lower₁ _ n≢j) (sym i≡j))
 
 lower₁-inject₁ : ∀ (i : Fin n) →
                  lower₁ (inject₁ i) (toℕ-inject₁-≢ i) ≡ i
-lower₁-inject₁ i = lower₁-inject₁′ i (toℕ-inject₁-≢ i)
-
-lower₁-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) →
-                    lower₁ i n≢i₁ ≡ lower₁ i n≢i₂
-lower₁-irrelevant {zero}  zero     0≢0 _ = contradiction refl 0≢0
-lower₁-irrelevant {suc n} zero     _   _ = refl
-lower₁-irrelevant {suc n} (suc i)  _   _ =
-  cong suc (lower₁-irrelevant i _ _)
-
-inject₁≡⇒lower₁≡ : ∀ {i : Fin n} {j : Fin (ℕ.suc n)} →
-                  (n≢j : n ≢ toℕ j) → inject₁ i ≡ j → lower₁ j n≢j ≡ i
-inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-lower₁ _ n≢j) (sym i≡j))
+lower₁-inject₁ i = inject₁≡⇒lower₁≡ (toℕ-inject₁-≢ i) refl
 
 ------------------------------------------------------------------------
 -- inject≤
@@ -1165,3 +1162,12 @@ Please use <⇒<′ instead."
 "Warning: <′⇒≺ was deprecated in v2.0.
 Please use <′⇒< instead."
 #-}
+
+lower₁-inject₁′ : ∀ (i : Fin n) (n≢i : n ≢ toℕ (inject₁ i)) →
+                  lower₁ (inject₁ i) n≢i ≡ i
+lower₁-inject₁′ i n≢i = inject₁≡⇒lower₁≡ n≢i refl
+{-# WARNING_ON_USAGE lower₁-inject₁′
+"Warning: lower₁-inject₁′ was deprecated in v2.0.
+Please use inject₁≡⇒lower₁≡ instead."
+#-}
+