[Import] Algebra.Solver.* (#2614)

* Cleaning importation solver * Cleaning importation solver * fix * fix * fix * fix
agda · Mar 1, 2025 · 771de0c · 771de0c
1 parent 8867628
commit 771de0c
Show file tree

Hide file tree

Showing 9 changed files with 29 additions and 24 deletions.
diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda
@@ -13,14 +13,17 @@ open import Algebra.Bundles using (CommutativeMonoid)
 module Algebra.Solver.CommutativeMonoid.Normal {c ℓ} (M : CommutativeMonoid c ℓ) where
 
 import Algebra.Properties.CommutativeSemigroup as CSProperties
+  using (interchange)
 import Algebra.Properties.Monoid.Mult as MultProperties
+  using (_×_; ×-homo-1; ×-homo-+)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Nat as ℕ using (ℕ; zero; suc; _+_)
 open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate; zipWith)
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
+  using (Pointwise; _∷_; []; Pointwise-≡↔≡; decidable)
 open import Relation.Binary.Definitions using (DecidableEquality)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-import Relation.Nullary.Decidable as Dec
+import Relation.Nullary.Decidable as Dec using (map)
 
 open CommutativeMonoid M
 open MultProperties monoid using (_×_; ×-homo-1; ×-homo-+)

diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Example.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Example.agda
@@ -13,10 +13,8 @@ import Algebra.Solver.IdempotentCommutativeMonoid as ICM-Solver
 
 open import Data.Bool.Base using (_∨_)
 open import Data.Bool.Properties using (∨-idempotentCommutativeMonoid)
-
 open import Data.Fin.Base using (zero; suc)
 open import Data.Vec.Base using ([]; _∷_)
-
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 open ICM-Solver ∨-idempotentCommutativeMonoid

diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda
@@ -20,9 +20,10 @@ open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Nat.Base using (ℕ)
 open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate; zipWith)
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
+  using (Pointwise; _∷_; []; Pointwise-≡↔≡; decidable)
 open import Relation.Binary.Definitions using (DecidableEquality)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-import Relation.Nullary.Decidable       as Dec
+import Relation.Nullary.Decidable as Dec using (map)
 
 open IdempotentCommutativeMonoid M
 open CSProperties commutativeSemigroup using (x∙yz≈xy∙z; x∙yz≈y∙xz)

diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda
@@ -19,7 +19,7 @@ open import Data.Vec.Base using (lookup)
 open import Function.Base using (_∘_; _$_)
 open import Relation.Binary.Definitions using (DecidableEquality)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-import Relation.Nullary.Decidable as Dec
+import Relation.Nullary.Decidable as Dec using (map; map′)
 
 open Monoid M
 open ≈-Reasoning setoid

diff --git a/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda b/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda
@@ -9,13 +9,14 @@
 
 module Algebra.Solver.Ring.AlmostCommutativeRing where
 
-open import Algebra
-open import Algebra.Structures
-open import Algebra.Definitions
-import Algebra.Morphism as Morphism
-import Algebra.Morphism.Definitions as MorphismDefinitions
+open import Algebra  using
+  (Op₁; Op₂; CommutativeSemiring; RawRing; CommutativeRing)
+open import Algebra.Structures using (IsCommutativeSemiring)
+open import Algebra.Definitions using (Congruent₁; Congruent₂)
+import Algebra.Morphism.Definitions as MorphismDefinitions using
+  (Homomorphic₀; Homomorphic₁; Homomorphic₂; Morphism)
 open import Function.Base using (id)
-open import Level
+open import Level using (suc; _⊔_)
 open import Relation.Binary.Core using (Rel)
 
 

diff --git a/src/Algebra/Solver/Ring/Lemmas.agda b/src/Algebra/Solver/Ring/Lemmas.agda
@@ -8,8 +8,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
-open import Algebra.Solver.Ring.AlmostCommutativeRing
+open import Algebra using (RawRing)
+open import Algebra.Solver.Ring.AlmostCommutativeRing using (AlmostCommutativeRing; _-Raw-AlmostCommutative⟶_)
 
 module Algebra.Solver.Ring.Lemmas
   {r₁ r₂ r₃ r₄}

diff --git a/src/Algebra/Solver/Ring/NaturalCoefficients.agda b/src/Algebra/Solver/Ring/NaturalCoefficients.agda
@@ -7,23 +7,23 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
+open import Algebra using (RawRing; CommutativeSemiring )
 import Algebra.Properties.Semiring.Mult as SemiringMultiplication
 open import Data.Maybe.Base using (Maybe; just; nothing; map)
-open import Algebra.Solver.Ring.AlmostCommutativeRing
-open import Data.Nat.Base as ℕ
-open import Data.Product.Base using (module Σ)
-open import Function.Base using (id)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 module Algebra.Solver.Ring.NaturalCoefficients
   {r₁ r₂} (R : CommutativeSemiring r₁ r₂)
   (open CommutativeSemiring R)
   (open SemiringMultiplication semiring using () renaming (_×_ to _×ᵤ_))
   (dec : ∀ m n → Maybe (m ×ᵤ 1# ≈ n ×ᵤ 1#)) where
 
-open import Algebra.Properties.Semiring.Mult.TCOptimised semiring
+open import Algebra.Solver.Ring.AlmostCommutativeRing
+open import Data.Nat.Base as ℕ using (ℕ; _+_; _*_)
+open import Data.Product.Base using (module Σ)
+open import Function.Base using (id)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
+open import Algebra.Properties.Semiring.Mult.TCOptimised semiring
 open import Relation.Binary.Reasoning.Setoid setoid
 
 private

diff --git a/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda b/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda
@@ -16,11 +16,11 @@ open import Algebra
 module Algebra.Solver.Ring.NaturalCoefficients.Default
   {r₁ r₂} (R : CommutativeSemiring r₁ r₂) where
 
-import Algebra.Properties.Semiring.Mult as SemiringMultiplication
+import Algebra.Properties.Semiring.Mult as SemiringMultiplication using (_×_)
 open import Data.Maybe.Base using (Maybe; map)
 open import Data.Nat using (_≟_)
 open import Relation.Binary.Consequences using (dec⇒weaklyDec)
-import Relation.Binary.PropositionalEquality.Core as ≡
+import Relation.Binary.PropositionalEquality.Core as ≡ using (refl; cong)
 
 open CommutativeSemiring R
 open SemiringMultiplication semiring

diff --git a/src/Algebra/Solver/Ring/Simple.agda b/src/Algebra/Solver/Ring/Simple.agda
@@ -7,15 +7,17 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Solver.Ring.AlmostCommutativeRing
+open import Algebra.Solver.Ring.AlmostCommutativeRing using
+  (AlmostCommutativeRing; -raw-almostCommutative⟶)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Binary.Consequences using (dec⇒weaklyDec)
 
 module Algebra.Solver.Ring.Simple
   {r₁ r₂} (R : AlmostCommutativeRing r₁ r₂)
   (_≟_ : Decidable (AlmostCommutativeRing._≈_ R))
   where
 
+open import Relation.Binary.Consequences using (dec⇒weaklyDec)
+
 open AlmostCommutativeRing R
 import Algebra.Solver.Ring as RS
 open RS rawRing R (-raw-almostCommutative⟶ R) (dec⇒weaklyDec _≟_) public