From d55ce9865125e7bab8fc34e4f1db8b9dcda90285 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 22 Feb 2022 14:29:18 +0000
Subject: [PATCH] adding NonZero to Fin, as per \#1686

---
 src/Data/Fin/Base.agda       | 46 ++++++++++++++++++++++++++++++++++++
 src/Data/Fin/Properties.agda |  5 ++--
 2 files changed, 48 insertions(+), 3 deletions(-)

diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 3a39a2f992..36aa47a2cf 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -12,6 +12,7 @@
 
 module Data.Fin.Base where
 
+open import Data.Bool.Base using (Bool; true; false; T; not)
 open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
 open import Data.Product as Product using (_×_; _,_; proj₁; proj₂)
@@ -20,6 +21,7 @@ open import Function.Base using (id; _∘_; _on_; flip)
 open import Level using (0ℓ)
 open import Relation.Nullary using (yes; no)
 open import Relation.Nullary.Decidable.Core using (True; toWitness)
+open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 open import Relation.Binary.Indexed.Heterogeneous using (IRel)
@@ -33,6 +35,12 @@ data Fin : ℕ → Set where
   zero : {n : ℕ} → Fin (suc n)
   suc  : {n : ℕ} (i : Fin n) → Fin (suc n)
 
+-- Bool-valued zero test
+
+zero? : ∀ {n} (i : Fin n) → Bool
+zero? zero    = true
+zero? (suc i) = false
+
 -- A conversion: toℕ "i" = i.
 
 toℕ : ∀ {n} → Fin n → ℕ
@@ -288,6 +296,44 @@ i > j = toℕ i ℕ.> toℕ j
 data _≺_ : ℕ → ℕ → Set where
   _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n
 
+------------------------------------------------------------------------
+-- Simple predicates
+
+-- Defining `NonZero` in terms of `T` and therefore ultimately `⊤` and
+-- `⊥` allows Agda to automatically infer nonZero-ness for any Fin n
+-- of the form `suc i`. Consequently in many circumstances this
+-- eliminates the need to explicitly pass a proof when the NonZero
+-- argument is either an implicit or an instance argument.
+--
+-- See `Data.Nat.Base` for comparison.
+
+record NonZero {n : ℕ} (i : Fin n) : Set where
+  field
+    nonZero : T (not (zero? i))
+
+-- Instances
+
+instance
+  nonZero : ∀ {n} {i : Fin n} → NonZero (suc i)
+  nonZero = _
+
+-- Constructors
+
+≢-nonZero : ∀ {n} {i : Fin (suc n)} → i ≢ zero → NonZero i
+≢-nonZero {n} {zero}  0≢0 = contradiction refl 0≢0
+≢-nonZero {n} {suc i} i≢0 = _
+
+>-nonZero : ∀ {n} {i : Fin (suc n)} → i > zero {n} → NonZero i
+>-nonZero {n} {suc i} _ = _
+
+-- Destructors
+
+≢-nonZero⁻¹ : ∀ {n} (i : Fin (suc n)) → .{{NonZero i}} → i ≢ zero
+≢-nonZero⁻¹ (suc i) ()
+
+>-nonZero⁻¹ : ∀ {n} (i : Fin (suc n)) → .{{NonZero i}} → i > zero {n}
+>-nonZero⁻¹ (suc i) = z<s
+
 ------------------------------------------------------------------------
 -- An ordering view.
 
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 4d80c7bcab..57d3eef211 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -526,9 +526,8 @@ inject≤-injective (s≤s p) (s≤s q) (suc x) (suc y) eq =
 -- pred
 ------------------------------------------------------------------------
 
-pred< : ∀ {n} → (i : Fin (suc n)) → i ≢ zero → pred i < i
-pred< zero p = contradiction refl p
-pred< (suc i) p = ≤̄⇒inject₁< ℕₚ.≤-refl
+pred< : ∀ {n} (i : Fin (suc n)) .{{_ : NonZero i}} → pred i < i
+pred< (suc i) = ≤̄⇒inject₁< ℕₚ.≤-refl
 
 ------------------------------------------------------------------------
 -- splitAt