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

CHANGELOG.md

@@ -1547,6 +1547,8 @@ 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)
+
   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)

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

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/Equality/Setoid.agda

@@ -11,7 +11,7 @@ open import Relation.Binary using (Setoid)
 
 module Data.List.Relation.Binary.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where
 
-open import Data.Fin.Base
+open import Data.Fin.Base using (Fin)
 open import Data.List.Base
 open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise)
 open import Data.List.Relation.Unary.Unique.Setoid S using (Unique)
@@ -129,13 +129,14 @@ concat⁺ = PW.concat⁺
 ------------------------------------------------------------------------
 -- tabulate
 
-tabulate⁺ : ∀ {n} {f : Fin n → A} {g : Fin n → A} →
-            (∀ i → f i ≈ g i) → tabulate f ≋ tabulate g
-tabulate⁺ = PW.tabulate⁺
+module _ {n} {f g : Fin n → A}
+  where
+
+  tabulate⁺ : (∀ i → f i ≈ g i) → tabulate f ≋ tabulate g
+  tabulate⁺ = PW.tabulate⁺
 
-tabulate⁻ : ∀ {n} {f : Fin n → A} {g : Fin n → A} →
-            tabulate f ≋ tabulate g → (∀ i → f i ≈ g i)
-tabulate⁻ = PW.tabulate⁻
+  tabulate⁻ : tabulate f ≋ tabulate g → (∀ i → f i ≈ g i)
+  tabulate⁻ = PW.tabulate⁻
 
 ------------------------------------------------------------------------
 -- filter

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/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/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,14 @@
 
 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.Fin.Base using (Fin)
+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 (≡⇒≡×≡)

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,8 @@ 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.Fin.Base using (Fin)
+open import Data.Nat.Base using (_<_)
 open import Function.Base using (_∘_; id)
 open import Level using (Level)
 open import Relation.Binary using (Rel; Setoid)
@@ -40,8 +40,8 @@ private
 
 module _ (S : Setoid a ℓ₁) (R : Setoid b ℓ₂) where
 
-  open Setoid S renaming (Carrier to A; _≈_ to _≈₁_)
-  open Setoid R renaming (Carrier to B; _≈_ to _≈₂_)
+  open Setoid S renaming (_≈_ to _≈₁_)
+  open Setoid R renaming (_≈_ to _≈₂_)
 
   map⁺ : ∀ {f} → (∀ {x y} → f x ≈₂ f y → x ≈₁ y) →
          ∀ {xs} → Unique S xs → Unique R (map f xs)
@@ -153,7 +153,5 @@ module _ (S : Setoid a ℓ) where
 
 module _ (S : Setoid a ℓ) {P : Pred _ p} (P? : Decidable P) where
 
-  open Setoid S renaming (Carrier to A)
-
   filter⁺ : ∀ {xs} → Unique S xs → Unique S (filter P? xs)
   filter⁺ = AllPairs.filter⁺ P?

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/Properties.agda

@@ -10,11 +10,11 @@ module Data.Vec.Properties where
 
 open import Algebra.Definitions
 open import Data.Bool.Base using (true; false)
-open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ; _↑ˡ_; _↑ʳ_)
+open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_)
 open import Data.List.Base as List using (List)
 open import Data.Nat.Base
-open import Data.Nat.Properties as ℕₚ
-  using (+-assoc; ≤-step; ≤-refl; ≤-trans)
+open import Data.Nat.Properties
+  using (+-assoc; ≤-step; ≤-refl; ≤-trans; suc-injective)
 open import Data.Product as Prod
   using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
 open import Data.Sum.Base using ([_,_]′)
@@ -396,7 +396,7 @@ toList-cast {n = suc _} eq (x ∷ xs) =
 
 cast-is-id : .(eq : m ≡ m) (xs : Vec A m) → cast eq xs ≡ xs
 cast-is-id eq []       = refl
-cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (ℕₚ.suc-injective eq) xs)
+cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs)
 
 subst-is-cast : (eq : m ≡ n) (xs : Vec A m) → subst (Vec A) eq xs ≡ cast eq xs
 subst-is-cast refl xs = sym (cast-is-id refl xs)
@@ -405,7 +405,7 @@ cast-trans : .(eq₁ : m ≡ n) (eq₂ : n ≡ o) (xs : Vec A m) →
              cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
 cast-trans {m = zero}  {n = zero}  {o = zero}  eq₁ eq₂ [] = refl
 cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) =
-  cong (x ∷_) (cast-trans (ℕₚ.suc-injective eq₁) (ℕₚ.suc-injective eq₂) xs)
+  cong (x ∷_) (cast-trans (suc-injective eq₁) (suc-injective eq₂) xs)
 
 ------------------------------------------------------------------------
 -- map
@@ -422,7 +422,7 @@ map-cast : (f : A → B) .(eq : m ≡ n) (xs : Vec A m) →
            map f (cast eq xs) ≡ cast eq (map f xs)
 map-cast {n = zero}  f eq []       = refl
 map-cast {n = suc _} f eq (x ∷ xs)
-  = cong (f x ∷_) (map-cast f (ℕₚ.suc-injective eq) xs)
+  = cong (f x ∷_) (map-cast f (suc-injective eq) xs)
 
 map-++ : ∀ (f : A → B) (xs : Vec A m) (ys : Vec A n) →
          map f (xs ++ ys) ≡ map f xs ++ map f ys
@@ -518,19 +518,19 @@ lookup-cast : .(eq : m ≡ n) (xs : Vec A m) (i : Fin m) →
               lookup (cast eq xs) (Fin.cast eq i) ≡ lookup xs i
 lookup-cast {n = suc _} eq (x ∷ _)  zero    = refl
 lookup-cast {n = suc _} eq (_ ∷ xs) (suc i) =
-  lookup-cast (ℕₚ.suc-injective eq) xs i
+  lookup-cast (suc-injective eq) xs i
 
 lookup-cast₁ : .(eq : m ≡ n) (xs : Vec A m) (i : Fin n) →
                lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
 lookup-cast₁ eq (x ∷ _)  zero    = refl
 lookup-cast₁ eq (_ ∷ xs) (suc i) =
-  lookup-cast₁ (ℕₚ.suc-injective eq) xs i
+  lookup-cast₁ (suc-injective eq) xs i
 
 lookup-cast₂ : .(eq : m ≡ n) (xs : Vec A n) (i : Fin m) →
                lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
-lookup-cast₂ {n = suc _} eq (x ∷ _)  zero    = refl
-lookup-cast₂ {n = suc _} eq (_ ∷ xs) (suc i) =
-  lookup-cast₂ (ℕₚ.suc-injective eq) xs i
+lookup-cast₂ eq (x ∷ _)  zero    = refl
+lookup-cast₂ eq (_ ∷ xs) (suc i) =
+  lookup-cast₂ (suc-injective eq) xs i
 
 lookup-concat : ∀ (xss : Vec (Vec A m) n) i j →
                 lookup (concat xss) (Fin.combine i j) ≡ lookup (lookup xss i) j

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} →