Cleaning up dependencies on Data.Fin and Data.Nat ahead of a first attempt to fix Issue1686

CHANGELOG.md

@@ -1468,6 +1468,8 @@ Other minor changes
   funToFin  : (Fin m → Fin n) → Fin (n ^ m)
   quotient  : Fin (m * n) → Fin m
   remainder : Fin (m * n) → Fin n
+
+  _ℕ-suc_ : (n : ℕ) → Fin n → ℕ
   ```
 
 * Added new proofs in `Data.Fin.Induction`:
@@ -1516,6 +1518,9 @@ Other minor changes
   combine-surjective : ∀ i → ∃₂ λ j k → combine j k ≡ i
   combine-monoˡ-<    : i < j → combine i k < combine j l
 
+  ℕ-ℕ≡toℕ‿ℕ-         : n ℕ-ℕ i ≡ toℕ (n ℕ- i)
+  nℕ-suci<n          : n ℕ-suc i ℕ.< n
+
   lower₁-injective   : lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j
   pinch-injective    : suc i ≢ j → suc i ≢ k → pinch i j ≡ pinch i k → j ≡ k
 

src/Data/Fin/Base.agda

@@ -11,13 +11,15 @@
 
 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₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)
 open import Level using (0ℓ)
 open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Nullary.Decidable.Core using (True; toWitness)
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
@@ -122,7 +124,7 @@ inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n)
 lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n
 lower₁ {zero}  zero    ne = ⊥-elim (ne refl)
 lower₁ {suc n} zero    _  = zero
-lower₁ {suc n} (suc i) ne = suc (lower₁ i λ x → ne (cong suc x))
+lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc))
 
 -- A strengthening injection into the minimal Fin fibre.
 strengthen : ∀ (i : Fin n) → Fin′ (suc i)
@@ -234,6 +236,13 @@ _ℕ-ℕ_ : (n : ℕ) → Fin (suc n) → ℕ
 n     ℕ-ℕ zero   = n
 suc n ℕ-ℕ suc i  = n ℕ-ℕ i
 
+-- n ℕ-suc "i" = n ∸ (suc i)
+
+infixl 6 _ℕ-suc_
+
+_ℕ-suc_ : (n : ℕ) → Fin n → ℕ
+suc n ℕ-suc i = n ℕ-ℕ i
+
 -- pred "i" = "pred i".
 
 pred : Fin n → Fin n

src/Data/Fin/Properties.agda

@@ -790,6 +790,10 @@ toℕ‿ℕ- (suc n) (suc i)  = toℕ‿ℕ- n i
 -- _ℕ-ℕ_
 ------------------------------------------------------------------------
 
+ℕ-ℕ≡toℕ‿ℕ- : ∀ n i → n ℕ-ℕ i ≡ toℕ (n ℕ- i)
+ℕ-ℕ≡toℕ‿ℕ- n       zero    = sym (toℕ-fromℕ n)
+ℕ-ℕ≡toℕ‿ℕ- (suc n) (suc i) = ℕ-ℕ≡toℕ‿ℕ- n i
+
 nℕ-ℕi≤n : ∀ n i → n ℕ-ℕ i ℕ.≤ n
 nℕ-ℕi≤n n       zero     = ℕₚ.≤-refl
 nℕ-ℕi≤n (suc n) (suc i)  = begin
@@ -798,6 +802,9 @@ nℕ-ℕi≤n (suc n) (suc i)  = begin
   suc n    ∎
   where open ℕₚ.≤-Reasoning
 
+nℕ-suci<n : ∀ n i → n ℕ-suc i ℕ.< n
+nℕ-suci<n (suc n) i = s<s (nℕ-ℕi≤n n i)
+
 ------------------------------------------------------------------------
 -- punchIn
 ------------------------------------------------------------------------

src/Data/List/Membership/Setoid.agda

@@ -11,7 +11,6 @@ open import Relation.Binary
 module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
 
 open import Function.Base using (_∘_; id; flip)
-open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List; []; _∷_; length; lookup)
 open import Data.List.Relation.Unary.Any
   using (Any; index; map; here; there)

src/Data/List/Properties.agda

@@ -15,7 +15,7 @@ open import Algebra.Bundles
 open import Algebra.Definitions as AlgebraicDefinitions using (Involutive)
 import Algebra.Structures as AlgebraicStructures
 open import Data.Bool.Base using (Bool; false; true; not; if_then_else_)
-open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ; inject₁)
+open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ)
 open import Data.List.Base as List
 open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)

src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda

@@ -14,7 +14,6 @@ module Data.List.Relation.Binary.Permutation.Setoid.Properties
 
 open import Algebra
 open import Data.Bool.Base using (true; false)
-open import Data.Fin.Base using (Fin)
 open import Data.List.Base as List hiding (head; tail)
 open import Data.List.Relation.Binary.Pointwise as Pointwise
   using (Pointwise; head; tail)

src/Data/List/Relation/Unary/All/Properties.agda

@@ -12,7 +12,7 @@ open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Bool.Base using (Bool; T; true; false)
 open import Data.Bool.Properties using (T-∧)
 open import Data.Empty
-open import Data.Fin.Base using (Fin; zero; suc)
+open import Data.Fin.Base using (zero; suc)
 open import Data.List.Base as List hiding (lookup)
 open import Data.List.Properties as Listₚ using (partition-defn)
 open import Data.List.Membership.Propositional
@@ -551,13 +551,11 @@ applyDownFrom⁺₂ f n Pf = applyDownFrom⁺₁ f n (λ _ → Pf _)
 ------------------------------------------------------------------------
 -- tabulate
 
-tabulate⁺ : ∀ {n} {f : Fin n → A} →
-            (∀ i → P (f i)) → All P (tabulate f)
+tabulate⁺ : ∀ {n} {f} → (∀ i → P (f i)) → All P (tabulate {n = n} f)
 tabulate⁺ {n = zero}  Pf = []
 tabulate⁺ {n = suc _} Pf = Pf zero ∷ tabulate⁺ (Pf ∘ suc)
 
-tabulate⁻ : ∀ {n} {f : Fin n → A} →
-            All P (tabulate f) → (∀ i → P (f i))
+tabulate⁻ : ∀ {n} {f} → All P (tabulate {n = n} f) → (∀ i → P (f i))
 tabulate⁻ (px ∷ _) zero    = px
 tabulate⁻ (_ ∷ pf) (suc i) = tabulate⁻ pf i
 

src/Data/List/Relation/Unary/AllPairs/Properties.agda

@@ -13,7 +13,6 @@ open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 import Data.List.Relation.Unary.All.Properties as All
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
 open import Data.Bool.Base using (true; false)
-open import Data.Fin.Base using (Fin)
 open import Data.Fin.Properties using (suc-injective)
 open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s)
 open import Data.Nat.Properties using (≤-refl; ≤-step)
@@ -114,8 +113,8 @@ module _ {R : Rel A ℓ} where
 
 module _ {R : Rel A ℓ} where
 
-  tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → i ≢ j → R (f i) (f j)) →
-              AllPairs R (tabulate f)
+  tabulate⁺ : ∀ {n} {f} → (∀ {i j} → i ≢ j → R (f i) (f j)) →
+              AllPairs R (tabulate {n = n} f)
   tabulate⁺ {zero}  fᵢ~fⱼ = []
   tabulate⁺ {suc n} fᵢ~fⱼ =
     All.tabulate⁺ (λ j → fᵢ~fⱼ λ()) ∷

src/Data/List/Relation/Unary/Any.agda

@@ -9,7 +9,7 @@
 module Data.List.Relation.Unary.Any where
 
 open import Data.Empty
-open import Data.Fin.Base
+open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List; []; [_]; _∷_)
 open import Data.Product as Prod using (∃; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)

src/Data/List/Relation/Unary/Any/Properties.agda

@@ -11,7 +11,7 @@ module Data.List.Relation.Unary.Any.Properties where
 open import Data.Bool.Base using (Bool; false; true; T)
 open import Data.Bool.Properties using (T-∨; T-≡)
 open import Data.Empty using (⊥)
-open import Data.Fin.Base using (Fin; zero; suc)
+open import Data.Fin.Base using (zero; suc)
 open import Data.List.Base as List
 open import Data.List.Properties using (ʳ++-defn)
 open import Data.List.Effectful using (monad)
@@ -511,11 +511,11 @@ module _ {P : A → Set p} where
 ------------------------------------------------------------------------
 -- tabulate
 
-tabulate⁺ : ∀ {n} {f : Fin n → A} i → P (f i) → Any P (tabulate f)
+tabulate⁺ : ∀ {n} {f} i → P (f i) → Any P (tabulate {n = n} f)
 tabulate⁺ zero    p = here p
 tabulate⁺ (suc i) p = there (tabulate⁺ i p)
 
-tabulate⁻ : ∀ {n} {f : Fin n → A} → Any P (tabulate f) → ∃ λ i → P (f i)
+tabulate⁻ : ∀ {n} {f} → Any P (tabulate {n = n} f) → ∃ λ i → P (f i)
 tabulate⁻ {n = suc _} (here p)  = zero , p
 tabulate⁻ {n = suc _} (there p) = Prod.map suc id (tabulate⁻ p)
 

src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda

@@ -6,7 +6,6 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-open import Data.Fin hiding (_≟_)
 open import Data.List.Base
 open import Data.List.Membership.Setoid.Properties as Membership
 open import Data.List.Relation.Unary.Any using (index)
@@ -85,5 +84,5 @@ module _ (S? : DecSetoid a ℓ₁) where
 module _ (S : Setoid a ℓ₁) where
 
   lookup-surjective : ∀ {xs} → IsEnumeration S xs →
-                      Surjective {A = Fin (length xs)} _≡_ (_≈_ S) (lookup xs)
+                      Surjective _≡_ (_≈_ S) (lookup xs)
   lookup-surjective _∈xs y = index (y ∈xs) , sym S (lookup-index (y ∈xs))

src/Data/List/Relation/Unary/Linked/Properties.agda

@@ -16,8 +16,6 @@ import Data.List.Relation.Unary.AllPairs.Properties as AllPairs
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Linked as Linked
   using (Linked; []; [-]; _∷_)
-open import Data.Fin.Base using (Fin)
-open import Data.Fin.Properties using (suc-injective)
 open import Data.Nat.Base using (zero; suc; _<_; z<s; s<s)
 open import Data.Nat.Properties using (≤-refl; ≤-pred; ≤-step)
 open import Data.Maybe.Relation.Binary.Connected

src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda

@@ -8,14 +8,13 @@
 
 module Data.List.Relation.Unary.Unique.Propositional.Properties where
 
-open import Data.Fin.Base using (Fin)
 open import Data.List.Base
 open import Data.List.Relation.Binary.Disjoint.Propositional
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
 open import Data.List.Relation.Unary.Unique.Propositional
 import Data.List.Relation.Unary.Unique.Setoid.Properties as Setoid
-open import Data.Nat.Base
+open import Data.Nat.Base using (_<_)
 open import Data.Nat.Properties using (<⇒≢)
 open import Data.Product using (_×_; _,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (≡⇒≡×≡)
@@ -132,8 +131,8 @@ downFrom⁺ n = applyDownFrom⁺₁ id n (λ j<i _ → <⇒≢ j<i ∘ sym)
 
 module _ {A : Set a} where
 
-  tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → f i ≡ f j → i ≡ j) →
-              Unique (tabulate f)
+  tabulate⁺ : ∀ {n} {f} → (∀ {i j} → f i ≡ f j → i ≡ j) →
+              Unique (tabulate {n = n} f)
   tabulate⁺ = Setoid.tabulate⁺ (setoid A)
 
 ------------------------------------------------------------------------

src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda

@@ -8,7 +8,6 @@
 
 module Data.List.Relation.Unary.Unique.Setoid.Properties where
 
-open import Data.Fin.Base using (Fin)
 open import Data.List.Base
 open import Data.List.Membership.Setoid.Properties
 open import Data.List.Relation.Binary.Disjoint.Setoid
@@ -20,7 +19,7 @@ open import Data.List.Relation.Unary.Unique.Setoid
 open import Data.Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 import Data.List.Relation.Unary.AllPairs.Properties as AllPairs
-open import Data.Nat.Base
+open import Data.Nat.Base using (_<_)
 open import Function.Base using (_∘_; id)
 open import Level using (Level)
 open import Relation.Binary using (Rel; Setoid)
@@ -144,8 +143,8 @@ module _ (S : Setoid a ℓ) where
 
   open Setoid S renaming (Carrier to A)
 
-  tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → f i ≈ f j → i ≡ j) →
-              Unique S (tabulate f)
+  tabulate⁺ : ∀ {n} {f} → (∀ {i j} → f i ≈ f j → i ≡ j) →
+              Unique S (tabulate {n = n} f)
   tabulate⁺ f-inj = AllPairs.tabulate⁺ (_∘ f-inj)
 
 ------------------------------------------------------------------------

src/Data/Nat/DivMod/WithK.agda

@@ -8,7 +8,7 @@
 
 module Data.Nat.DivMod.WithK where
 
-open import Data.Nat using (ℕ; NonZero; _+_; _*_; _≟_; zero; suc)
+open import Data.Nat using (ℕ; NonZero; _+_; _*_; _≟_)
 open import Data.Nat.DivMod hiding (_mod_; _divMod_)
 open import Data.Nat.Properties using (≤⇒≤″)
 open import Data.Nat.WithK

src/Data/Vec/Functional.agda

@@ -17,7 +17,7 @@ module Data.Vec.Functional where
 
 open import Data.Fin.Base
 open import Data.List.Base as L using (List)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; pred)
 open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Vec.Base as V using (Vec)

src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda

@@ -6,8 +6,7 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-open import Data.Fin.Base
-open import Data.Nat.Base
+open import Data.Nat.Base using (ℕ)
 open import Data.Vec.Functional as VF hiding (map)
 open import Data.Vec.Functional.Relation.Binary.Pointwise
   using (Pointwise)

src/Data/Vec/Functional/Relation/Binary/Pointwise.agda

@@ -8,8 +8,6 @@
 
 module Data.Vec.Functional.Relation.Binary.Pointwise where
 
-open import Data.Fin.Base
-open import Data.Nat.Base
 open import Data.Vec.Functional as VF hiding (map)
 open import Level using (Level)
 open import Relation.Binary

src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda

@@ -8,9 +8,9 @@
 
 module Data.Vec.Functional.Relation.Binary.Pointwise.Properties where
 
-open import Data.Fin.Base
-open import Data.Fin.Properties
-open import Data.Nat.Base
+open import Data.Fin.Base using (zero; suc; _↑ˡ_; _↑ʳ_; splitAt)
+open import Data.Fin.Properties using (all?; splitAt-↑ˡ; splitAt-↑ʳ)
+open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
   using () renaming (Pointwise to ×-Pointwise)

src/Data/Vec/Functional/Relation/Unary/All.agda

@@ -8,9 +8,7 @@
 
 module Data.Vec.Functional.Relation.Unary.All where
 
-open import Data.Fin.Base
-open import Data.Fin.Properties
-open import Data.Nat.Base
+open import Data.Fin.Properties using (all?)
 open import Data.Product using (_,_)
 open import Data.Vec.Functional as VF hiding (map)
 open import Level using (Level)

src/Data/Vec/Functional/Relation/Unary/All/Properties.agda

@@ -8,9 +8,8 @@
 
 module Data.Vec.Functional.Relation.Unary.All.Properties where
 
-open import Data.Fin.Base
-open import Data.Fin.Properties
-open import Data.Nat.Base
+open import Data.Fin.Base using (zero; suc; _↑ˡ_; _↑ʳ_; splitAt)
+open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ)
 open import Data.Product as Σ using (_×_; _,_; proj₁; proj₂; uncurry)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Vec.Functional as VF hiding (map)
@@ -38,7 +37,7 @@ module _ {P : Pred A p} {Q : Pred B q} {f : A → B} where
 ------------------------------------------------------------------------
 -- replicate
 
-module _ {P : Pred A p} {x : A} {n : ℕ} where
+module _ {P : Pred A p} {x : A} {n} where
 
   replicate⁺ : P x → All P (replicate {n = n} x)
   replicate⁺ = const
@@ -87,14 +86,14 @@ tail⁺ P ps = ps ∘ suc
 ------------------------------------------------------------------------
 -- ++
 
-module _ (P : Pred A p) {m n : ℕ} {xs : Vector A m} {ys : Vector A n} where
+module _ (P : Pred A p) {m n} {xs : Vector A m} {ys : Vector A n} where
 
   ++⁺ : All P xs → All P ys → All P (xs ++ ys)
   ++⁺ pxs pys i with splitAt m i
   ... | inj₁ i′ = pxs i′
   ... | inj₂ j′ = pys j′
 
-module _ (P : Pred A p) {m n : ℕ} (xs : Vector A m) {ys : Vector A n} where
+module _ (P : Pred A p) {m n} (xs : Vector A m) {ys : Vector A n} where
 
   ++⁻ˡ : All P (xs ++ ys) → All P xs
   ++⁻ˡ ps i with ps (i ↑ˡ n)

src/Data/Vec/Functional/Relation/Unary/Any.agda

@@ -8,8 +8,8 @@
 
 module Data.Vec.Functional.Relation.Unary.Any where
 
-open import Data.Fin.Base
-open import Data.Fin.Properties
+open import Data.Fin.Base using (zero; suc)
+open import Data.Fin.Properties using (any?)
 open import Data.Nat.Base
 open import Data.Product as Σ using (Σ; ∃; _×_; _,_; proj₁; proj₂)
 open import Data.Vec.Functional as VF hiding (map)

src/Data/Vec/Recursive.agda

@@ -19,7 +19,7 @@ module Data.Vec.Recursive where
 open import Level using (Level; lift)
 open import Function.Bundles using (mk↔′)
 open import Function.Properties.Inverse using (↔-isEquivalence; ↔-refl; ↔-sym; ↔-trans)
-open import Data.Nat.Base as Nat using (ℕ; zero; suc)
+open import Data.Nat.Base as Nat using (ℕ; zero; suc; NonZero; pred)
 open import Data.Nat.Properties using (+-comm; *-comm)
 open import Data.Empty.Polymorphic
 open import Data.Fin.Base as Fin using (Fin; zero; suc)

src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda

@@ -9,7 +9,6 @@
 module Data.Vec.Relation.Binary.Pointwise.Extensional where
 
 open import Data.Fin.Base using (zero; suc)
-open import Data.Nat.Base using (zero; suc)
 open import Data.Vec.Base as Vec hiding ([_]; head; tail; map)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive as Inductive
   using ([]; _∷_)
@@ -73,8 +72,8 @@ module _ {_∼_ : REL A B ℓ} where
 
   extensional⇒inductive : ∀ {n} {xs : Vec A n} {ys : Vec B n} →
                            Pointwise _∼_ xs ys → IPointwise _∼_ xs ys
-  extensional⇒inductive {zero} {[]}       {[]}      xs∼ys = []
-  extensional⇒inductive {suc n} {x ∷ xs} {y ∷ ys} xs∼ys =
+  extensional⇒inductive {xs = []}       {[]}   xs∼ys = []
+  extensional⇒inductive {xs = x ∷ xs} {y ∷ ys} xs∼ys =
     (head xs∼ys) ∷ extensional⇒inductive (tail xs∼ys)
 
   inductive⇒extensional : ∀ {n} {xs : Vec A n} {ys : Vec B n} →