[imports] Data.Fin.Base .. Data.Integer.Tactic.RingSolver (#2623)

* import cleaning data 4 * fixed * fix * Update src/Data/Integer/DivMod.agda whitespace * Update src/Data/Integer/Coprimality.agda layout of `using` directives * Update src/Data/Graph/Acyclic.agda whitespace --------- Co-authored-by: jamesmckinna <[email protected]>
agda · Feb 28, 2025 · 8867628 · 8867628
1 parent aae4058
commit 8867628
Show file tree

Hide file tree

Showing 21 changed files with 52 additions and 50 deletions.
diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
@@ -17,7 +17,7 @@ open import Data.Product.Base 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.Binary.Core
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
 open import Relation.Nullary.Negation.Core using (contradiction)

diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda
@@ -16,8 +16,8 @@ open import Data.Fin.Properties using (toℕ-inject₁; ≤-refl; <-cmp;
   pigeonhole; ≺⇒<′)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _∸_; s≤s)
 open import Data.Nat.Properties using (n<1+n; ≤⇒≯)
-import Data.Nat.Induction as ℕ
-import Data.Nat.Properties as ℕ
+import Data.Nat.Induction as ℕ using (<′-wellFounded; <-wellFounded)
+import Data.Nat.Properties as ℕ using (<-cmp)
 open import Data.Product.Base using (_,_)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.Vec.Relation.Unary.Linked as Linked using (Linked; [-]; _∷_)
@@ -34,7 +34,7 @@ open import Relation.Binary.Definitions using (Decidable)
 import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
 import Relation.Binary.Construct.Flip.Ord as Ord
 import Relation.Binary.Construct.NonStrictToStrict as ToStrict
-import Relation.Binary.Construct.On as On
+import Relation.Binary.Construct.On as On using (wellFounded)
 open import Relation.Binary.Definitions using (Tri; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym; subst; trans; cong)

diff --git a/src/Data/Fin/Instances.agda b/src/Data/Fin/Instances.agda
@@ -8,8 +8,8 @@
 
 module Data.Fin.Instances where
 
-open import Data.Fin.Base
-open import Data.Fin.Properties
+open import Data.Fin.Base using (Fin)
+open import Data.Fin.Properties using (≡-isDecEquivalence; ≤-isDecTotalOrder)
 
 instance
   Fin-≡-isDecEquivalence = ≡-isDecEquivalence

diff --git a/src/Data/Fin/Literals.agda b/src/Data/Fin/Literals.agda
@@ -8,7 +8,7 @@
 
 module Data.Fin.Literals where
 
-open import Agda.Builtin.FromNat
+open import Agda.Builtin.FromNat using (Number)
 open import Data.Nat using (suc; _≤?_)
 open import Data.Fin using (Fin ; #_)
 open import Relation.Nullary.Decidable using (True)

diff --git a/src/Data/Fin/Patterns.agda b/src/Data/Fin/Patterns.agda
@@ -8,7 +8,7 @@
 
 module Data.Fin.Patterns where
 
-open import Data.Fin.Base
+open import Data.Fin.Base using (Fin; zero; suc)
 
 ------------------------------------------------------------------------
 -- Constants

diff --git a/src/Data/Fin/Reflection.agda b/src/Data/Fin/Reflection.agda
@@ -10,9 +10,9 @@ module Data.Fin.Reflection where
 
 open import Data.Nat.Base as ℕ hiding (module ℕ)
 open import Data.Fin.Base as Fin hiding (module Fin)
-open import Data.List.Base
-open import Reflection.AST.Term
-open import Reflection.AST.Argument
+open import Data.List.Base using (List; _∷_; []; lookup)
+open import Reflection.AST.Term using (Term; con; _⋯⟅∷⟆_)
+open import Reflection.AST.Argument using (Arg; _⟨∷⟩_)
 
 ------------------------------------------------------------------------
 -- Term

diff --git a/src/Data/Fin/Substitution.agda b/src/Data/Fin/Substitution.agda
@@ -17,7 +17,7 @@ module Data.Fin.Substitution where
 
 open import Data.Nat.Base hiding (_⊔_; _/_)
 open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.Vec.Base
+open import Data.Vec.Base using (Vec; []; _∷_; map; lookup)
 open import Function.Base as Fun using (flip)
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
   as Star using (Star; ε; _◅_)

diff --git a/src/Data/Fin/Substitution/Example.agda b/src/Data/Fin/Substitution/Example.agda
@@ -15,11 +15,11 @@ module Data.Fin.Substitution.Example where
 Please see README.Data.Fin.Substitution.UntypedLambda instead."
 #-}
 
-open import Data.Fin.Substitution
-open import Data.Fin.Substitution.Lemmas
+open import Data.Fin.Substitution using (Lift; Sub; Subs; Application; TermSubst)
+open import Data.Fin.Substitution.Lemmas using (TermLemmas)
 open import Data.Nat.Base hiding (_/_)
 open import Data.Fin.Base using (Fin)
-open import Data.Vec.Base
+open import Data.Vec.Base using (Vec; _∷_; []; lookup)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong; cong₂; module ≡-Reasoning)
 open ≡-Reasoning

diff --git a/src/Data/Float/Base.agda b/src/Data/Float/Base.agda
@@ -9,10 +9,10 @@
 module Data.Float.Base where
 
 open import Data.Bool.Base using (T)
-import Data.Word64.Base as Word64
-import Data.Maybe.Base as Maybe
+import Data.Word64.Base as Word64 using (Word64; toℕ)
+import Data.Maybe.Base as Maybe using (Maybe; map)
 open import Function.Base using (_on_; _∘_)
-open import Agda.Builtin.Equality
+open import Agda.Builtin.Equality using (_≡_)
 open import Relation.Binary.Core using (Rel)
 
 ------------------------------------------------------------------------

diff --git a/src/Data/Float/Instances.agda b/src/Data/Float/Instances.agda
@@ -8,7 +8,7 @@
 
 module Data.Float.Instances where
 
-open import Data.Float.Properties
+open import Data.Float.Properties using (_≟_)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
 

diff --git a/src/Data/Float/Properties.agda b/src/Data/Float/Properties.agda
@@ -9,12 +9,12 @@
 module Data.Float.Properties where
 
 open import Data.Bool.Base as Bool using (Bool)
-open import Data.Float.Base
-import Data.Maybe.Base as Maybe
-import Data.Maybe.Properties as Maybe
-import Data.Nat.Properties as ℕ
-import Data.Word64.Base as Word64
-import Data.Word64.Properties as Word64
+open import Data.Float.Base using (Float; _≈_; toWord64)
+import Data.Maybe.Base as Maybe using (Maybe; just; nothing; map)
+import Data.Maybe.Properties as Maybe using (map-injective; ≡-dec)
+import Data.Nat.Properties as ℕ using (_≟_)
+import Data.Word64.Base as Word64 using (Word64; toℕ)
+import Data.Word64.Properties as Word64 using (≈⇒≡)
 open import Function.Base using (_∘_)
 open import Relation.Nullary.Decidable as RN using (map′)
 open import Relation.Binary.Core using (_⇒_)
@@ -23,7 +23,7 @@ open import Relation.Binary.Structures
   using (IsEquivalence; IsDecEquivalence)
 open import Relation.Binary.Definitions
   using (Reflexive; Symmetric; Transitive; Substitutive; Decidable; DecidableEquality)
-import Relation.Binary.Construct.On as On
+import Relation.Binary.Construct.On as On using (decidable)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; cong; sym; trans; subst)
 open import Relation.Binary.PropositionalEquality.Properties

diff --git a/src/Data/Graph/Acyclic.agda b/src/Data/Graph/Acyclic.agda
@@ -15,10 +15,11 @@ module Data.Graph.Acyclic where
 open import Level using (_⊔_)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _<′_)
 open import Data.Nat.Induction using (<′-rec; <′-Rec)
-import Data.Nat.Properties as ℕ
+import Data.Nat.Properties as ℕ using (≤⇒≤′)
 open import Data.Fin as Fin
-  using (Fin; Fin′; zero; suc; #_; toℕ; _≟_; opposite) renaming (_ℕ-ℕ_ to _-_)
-import Data.Fin.Properties as Fin
+  using (Fin; Fin′; zero; suc; #_; toℕ; _≟_; opposite)
+  renaming (_ℕ-ℕ_ to _-_)
+open import Data.Fin.Properties as Fin using (nℕ-ℕi≤n)
 open import Data.Product.Base as Prod using (∃; _×_; _,_)
 open import Data.Maybe.Base as Maybe using (Maybe)
 open import Data.Empty using (⊥)

diff --git a/src/Data/Integer/Coprimality.agda b/src/Data/Integer/Coprimality.agda
@@ -8,11 +8,12 @@
 
 module Data.Integer.Coprimality where
 
-open import Data.Integer.Base
-open import Data.Integer.Divisibility
-open import Data.Integer.Properties
+open import Data.Integer.Base using (ℤ; _*_; ∣_∣)
+open import Data.Integer.Divisibility using (_∣_)
+open import Data.Integer.Properties using (abs-*)
 import Data.Nat.Coprimality as ℕ
-import Data.Nat.Divisibility as ℕ
+  using (Coprime; sym; coprime?; coprime-divisor)
+import Data.Nat.Divisibility as ℕ using (_∣_)
 open import Function.Base using (_on_)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)

diff --git a/src/Data/Integer/DivMod.agda b/src/Data/Integer/DivMod.agda
@@ -13,8 +13,8 @@ open import Data.Integer.Base using (+_; -[1+_]; +[1+_]; NonZero; _%_; ∣_∣;
   +<+)
 open import Data.Integer.Properties
 open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s; z<s; s<s)
-import Data.Nat.Properties as ℕ
-import Data.Nat.DivMod as ℕ
+import Data.Nat.Properties as ℕ using (m∸n≤m)
+import Data.Nat.DivMod as ℕ using (m≡m%n+[m/n]*n; m%n≤n; m%n<n)
 open import Function.Base using (_∘′_)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; cong; sym; subst)

diff --git a/src/Data/Integer/Divisibility.agda b/src/Data/Integer/Divisibility.agda
@@ -11,11 +11,12 @@
 module Data.Integer.Divisibility where
 
 open import Function.Base using (_on_; _$_)
-open import Data.Integer.Base
-open import Data.Integer.Properties
-import Data.Nat.Base as ℕ
+open import Data.Integer.Base using (ℤ; _*_; ∣_∣; NonZero)
+open import Data.Integer.Properties using (abs-*; *-comm)
+import Data.Nat.Base as ℕ using (ℕ; _*_; NonZero)
 import Data.Nat.Divisibility as ℕ
-open import Level
+  using (module ∣-Reasoning; _∣_; divides; *-monoʳ-∣; *-cancelˡ-∣)
+open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
 
 

diff --git a/src/Data/Integer/Divisibility/Signed.agda b/src/Data/Integer/Divisibility/Signed.agda
@@ -13,10 +13,9 @@ open import Data.Integer.Base using (ℤ; _*_; +0; sign; _◃_; ≢-nonZero;
   ∣_∣; 0ℤ; +_; _+_; _-_; -_; NonZero)
 open import Data.Integer.Properties
 import Data.Integer.Divisibility as Unsigned
-import Data.Nat.Base as ℕ
+import Data.Nat.Base as ℕ using (ℕ; suc; _*_)
 import Data.Nat.Divisibility as ℕ
-import Data.Nat.Coprimality as ℕ
-import Data.Nat.Properties as ℕ
+import Data.Nat.Properties as ℕ using (*-zeroʳ ; <-cmp; module ≤-Reasoning)
 import Data.Sign.Base as Sign
 import Data.Sign.Properties as Sign
 open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_)

diff --git a/src/Data/Integer/GCD.agda b/src/Data/Integer/GCD.agda
@@ -8,9 +8,9 @@
 
 module Data.Integer.GCD where
 
-open import Data.Integer.Base
-open import Data.Integer.Divisibility
-open import Data.Integer.Properties
+open import Data.Integer.Base using (ℤ; _+_; +_; 0ℤ; 1ℤ; ∣_∣)
+open import Data.Integer.Divisibility using (_∣_)
+open import Data.Integer.Properties using (+-injective; ∣i∣≡0⇒i≡0)
 import Data.Nat.GCD as ℕ
 open import Data.Product.Base using (_,_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)

diff --git a/src/Data/Integer/Instances.agda b/src/Data/Integer/Instances.agda
@@ -8,7 +8,7 @@
 
 module Data.Integer.Instances where
 
-open import Data.Integer.Properties
+open import Data.Integer.Properties using (_≟_; ≤-isDecTotalOrder)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
 

diff --git a/src/Data/Integer/LCM.agda b/src/Data/Integer/LCM.agda
@@ -9,8 +9,8 @@
 module Data.Integer.LCM where
 
 open import Data.Integer.Base
-open import Data.Integer.Divisibility
-open import Data.Integer.GCD
+open import Data.Integer.Divisibility using (_∣_)
+open import Data.Integer.GCD using (gcd)
 import Data.Nat.LCM as ℕ
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 

diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
@@ -13,7 +13,6 @@ import Algebra.Morphism as Morphism
 open import Algebra.Construct.NaturalChoice.Base
 import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
 import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
-import Algebra.Properties.AbelianGroup
 open import Data.Bool.Base using (T; true; false)
 open import Data.Integer.Base renaming (suc to sucℤ)
 open import Data.Integer.Properties.NatLemmas

diff --git a/src/Data/Integer/Tactic/RingSolver.agda b/src/Data/Integer/Tactic/RingSolver.agda
@@ -18,8 +18,9 @@ open import Data.Integer.Properties using (+-*-commutativeRing)
 open import Level using (0ℓ)
 open import Data.Unit.Base using (⊤)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
-import Tactic.RingSolver as Solver
+import Tactic.RingSolver as Solver using (solve-∀-macro; solve-macro)
 import Tactic.RingSolver.Core.AlmostCommutativeRing as ACR
+  using (AlmostCommutativeRing; fromCommutativeRing)
 
 ------------------------------------------------------------------------
 -- A module for automatically solving propositional equivalences