[Import] Algebra.Semiring (#2612)

* Import cleaning Semiring

* Import cleaning Semiring

* fix bug

* fix bug

* fix

* fix

Author: jmougeot

src/Algebra/Properties/Semiring/Binomial.agda

@@ -9,6 +9,13 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles using (Semiring)
+
+module Algebra.Properties.Semiring.Binomial
+  {a ℓ} (S : Semiring a ℓ)
+  (open Semiring S)
+  (x y : Carrier)
+  where
+
 open import Data.Bool.Base using (true)
 open import Data.Nat.Base as ℕ hiding (_+_; _*_; _^_)
 open import Data.Nat.Combinatorics
@@ -26,12 +33,6 @@ open import Function.Base using (_∘_)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; _≢_; cong)
 
-module Algebra.Properties.Semiring.Binomial
-  {a ℓ} (S : Semiring a ℓ)
-  (open Semiring S)
-  (x y : Carrier)
-  where
-
 open import Algebra.Definitions _≈_
 open import Algebra.Properties.Semiring.Sum S
 open import Algebra.Properties.Semiring.Mult S

src/Algebra/Properties/Semiring/Exp.agda

@@ -6,16 +6,19 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
-open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-import Data.Nat.Properties as ℕ
+open import Algebra.Bundles using (Semiring)
 
 module Algebra.Properties.Semiring.Exp
   {a ℓ} (S : Semiring a ℓ) where
 
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
+open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
+import Data.Nat.Properties as ℕ using (*-comm)
+
+-- Need to see almost everything, including setoid
 open Semiring S
+
 open import Relation.Binary.Reasoning.Setoid setoid
 import Algebra.Properties.Monoid.Mult *-monoid as Mult
 

src/Algebra/Properties/Semiring/Exp/TCOptimised.agda

@@ -6,15 +6,15 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
-open import Data.Nat.Base as ℕ using (zero; suc)
-import Data.Nat.Properties as ℕ
-open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Algebra.Bundles using (Semiring)
 
 module Algebra.Properties.Semiring.Exp.TCOptimised
   {a ℓ} (S : Semiring a ℓ) where
 
+open import Data.Nat.Base as ℕ using (zero; suc)
+import Data.Nat.Properties as ℕ using (+-suc; *-comm)
+open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 open Semiring S renaming (zero to *-zero)
 open import Relation.Binary.Reasoning.Setoid setoid
 

src/Algebra/Properties/Semiring/Exp/TailRecursiveOptimised.agda

@@ -6,14 +6,15 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
-open import Data.Nat.Base as ℕ using (zero; suc)
-import Data.Nat.Properties as ℕ
-open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
+open import Algebra.Bundles using (Semiring)
 
 module Algebra.Properties.Semiring.Exp.TailRecursiveOptimised
   {a ℓ} (S : Semiring a ℓ) where
 
+open import Data.Nat.Base as ℕ using (zero; suc)
+open import Data.Nat.Properties as ℕ using (+-suc)
+open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
+
 open Semiring S renaming (zero to *-zero)
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Algebra.Properties.Semiring.Exp S as U

src/Algebra/Properties/Semiring/Mult.agda

@@ -7,12 +7,14 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles using (Semiring)
-open import Data.Nat.Base as ℕ using (zero; suc)
 
 module Algebra.Properties.Semiring.Mult
   {a ℓ} (S : Semiring a ℓ) where
 
+open import Data.Nat.Base as ℕ using (zero; suc)
+
 open Semiring S renaming (zero to *-zero)
+
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Algebra.Definitions _≈_ using (_IdempotentOn_)
 

src/Algebra/Properties/Semiring/Sum.agda

@@ -11,7 +11,8 @@ open import Algebra.Bundles using (Semiring)
 module Algebra.Properties.Semiring.Sum {c} {ℓ} (R : Semiring c ℓ) where
 
 open import Data.Nat.Base using (zero; suc)
-open import Data.Vec.Functional
+open import Data.Vec.Functional using (Vector; head; tail; map)
+
 open Semiring R
 
 ------------------------------------------------------------------------