[ new ] Fin n as a refinement (#2975)

* [ new ] Fin n as a refinement

This version has a better runtime representation
This version lets us have efficient implementations of
things like splitAt and quotRem

* ASCII-fy

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

* Rename `nonZero`

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

* [ fix ] move lemma to Data.Nat.Properties

* [ cosmetic ] use idiom brackets

* Simplify opposite

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

* [ cleanup ] gadget to convert irrelevant-domains

* [ james ] rename unview -> view⁻¹

* [ james ] More descriptive CHANGELOG entry

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

* [ tmp ] merging James' punch* functions

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

* [ cleanup ] avoid recompute, rebuilding (T (i < j))

---------

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

Author: gallais

CHANGELOG.md

@@ -134,6 +134,11 @@ Deprecated names
   truncate-irrelevant  ↦  Relation.Binary.PropositionalEquality.Core.refl
   ```
 
+* In `Function.Base`:
+  ```agda
+  λ∙ : (.(x : A) → B x) → ((x : A) → B x)
+  ```
+
 * In `Relation.Binary.Construct.Intersection`:
   ```agda
   decidable     ↦   _∩?_
@@ -181,6 +186,11 @@ New modules
 
 * `Algebra.Properties.Semiring`.
 
+* A variation on `Fin` seen as a `Nat` refinement, with better runtime representation and performance.
+  ```
+  Data.Nat.Bounded.Base
+  ```
+
 * `Data.List.Fresh.Membership.DecSetoid`.
 
 * Various additions over non-empty lists:
@@ -296,6 +306,12 @@ Additions to existing modules
   ```
   NB. the latter is based on `IsCommutativeRing`, with the former on `IsSemiring`.
 
+
+* In `Data.Bool.Properties`:
+  ```agda
+  ¬T-≡ : (¬ T x) ⇔ x ≡ false
+  ```
+
 * In `Data.Fin.Permutation.Components`:
   ```agda
   transpose[i,i,j]≡j  : (i j : Fin n) → transpose i i j ≡ j
@@ -410,6 +426,7 @@ Additions to existing modules
   m⊔n∸[m∸n]≡n : ∀ m n → m ⊔ n ∸ (m ∸ n) ≡ n
   m⊔n≡m∸n+n : ∀ m n → m ⊔ n ≡ m ∸ n + n
   ∣m-n∣≡m⊔n∸m⊓n : ∀ m n → ∣ m - n ∣ ≡ m ⊔ n ∸ m ⊓ n
+  <″⇒< : _<″_ ⇒ _<_
   ```
 
 * In `Data.Product.Properties`:

src/Data/Bool/Properties.agda

@@ -41,7 +41,7 @@ open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning; setoid; decSetoid; isEquivalence)
 open import Relation.Nullary.Decidable.Core
   using (True; yes; no; fromWitness ; toWitness)
-open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 import Relation.Unary as U
 
 open import Algebra.Definitions {A = Bool} _≡_
@@ -835,6 +835,10 @@ if-cong₂ _ refl refl = refl
 
 open Relation.Nullary.Decidable.Core public using (T?)
 
+¬T-≡ : ∀ {x} → (¬ T x) ⇔ x ≡ false
+¬T-≡ {false} = mk⇔ (const refl) (const id)
+¬T-≡ {true}  = mk⇔ (contradiction _) (λ ())
+
 T-≡ : ∀ {x} → T x ⇔ x ≡ true
 T-≡ {false} = mk⇔ (λ ())       (λ ())
 T-≡ {true}  = mk⇔ (const refl) (const _)

src/Data/Fin/Base.agda

@@ -54,6 +54,17 @@ cast {zero}  {zero}  eq k       = k
 cast {suc m} {suc n} eq zero    = zero
 cast {suc m} {suc n} eq (suc k) = suc (cast (cong ℕ.pred eq) k)
 
+-- Tests showing that cast does compute on constructors
+
+module _ .(eqs : suc m ≡ suc n) where
+
+  _ : cast eqs zero ≡ zero
+  _ = refl
+
+  _ : .(eq : m ≡ n) (k : Fin m) →
+      cast eqs (suc k) ≡ suc (cast eq k)
+  _ = λ eq k → refl
+
 ------------------------------------------------------------------------
 -- Conversions
 
@@ -77,7 +88,7 @@ fromℕ<″ : ∀ m {n} → .(m ℕ.<″ n) → Fin n
 fromℕ<″ zero    {suc _} _    = zero
 fromℕ<″ (suc m) {suc _} m<″n = suc (fromℕ<″ m (ℕ.s<″s⁻¹ m<″n))
 
--- canonical liftings of i:Fin m to larger index
+-- Canonical liftings of i:Fin m to larger index
 
 -- injection on the left: "i" ↑ˡ n = "i" in Fin (m + n)
 infixl 5 _↑ˡ_
@@ -91,6 +102,7 @@ _↑ʳ_ : ∀ {m} n → Fin m → Fin (n ℕ.+ m)
 zero    ↑ʳ i = i
 (suc n) ↑ʳ i = suc (n ↑ʳ i)
 
+
 -- reduce≥ "m + i" _ = "i".
 
 reduce≥ : ∀ (i : Fin (m ℕ.+ n)) → .(m ℕ.≤ toℕ i) → Fin n