Fast.Int Update

Cubical/Algebra/AbGroup/Instances/Fast/Int.agda

@@ -0,0 +1,9 @@
+module Cubical.Algebra.AbGroup.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Fast.Int
+open import Cubical.Algebra.AbGroup.Base
+open import Cubical.Algebra.Group.Instances.Fast.Int
+
+ℤAbGroup : AbGroup ℓ-zero
+ℤAbGroup = Group→AbGroup ℤGroup +Comm

Cubical/Algebra/CommRing/Instances/Fast/Int.agda

@@ -0,0 +1,23 @@
+module Cubical.Algebra.CommRing.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Algebra.CommRing
+open import Cubical.Data.Fast.Int as Int renaming (_+_ to _+ℤ_; _·_ to _·ℤ_ ; -_ to -ℤ_)
+
+open CommRingStr using (0r ; 1r ; _+_ ; _·_ ; -_ ; isCommRing)
+
+ℤCommRing : CommRing ℓ-zero
+fst ℤCommRing = ℤ
+0r (snd ℤCommRing) = pos 0
+1r (snd ℤCommRing) = pos 1
+_+_ (snd ℤCommRing) = _+ℤ_
+_·_ (snd ℤCommRing) = _·ℤ_
+- snd ℤCommRing = -ℤ_
+isCommRing (snd ℤCommRing) = isCommRingℤ
+  where
+  abstract
+    isCommRingℤ : IsCommRing (pos 0) (pos 1) _+ℤ_ _·ℤ_ -ℤ_
+    isCommRingℤ = makeIsCommRing isSetℤ Int.+Assoc +IdR
+                                 -Cancel Int.+Comm Int.·Assoc
+                                 Int.·IdR ·DistR+ Int.·Comm

Cubical/Algebra/Group/Instances/Fast/Int.agda

@@ -0,0 +1,56 @@
+module Cubical.Algebra.Group.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+
+open import Cubical.Data.Fast.Int renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_ ; _·_ to _·ℤ_ ; -_ to -ℤ_)
+
+open import Cubical.Data.Nat using (ℕ ; zero ; suc)
+open import Cubical.Data.Fin.Base
+
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.Properties
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+
+
+open GroupStr
+
+ℤGroup : Group₀
+fst ℤGroup = ℤ
+1g (snd ℤGroup) = 0
+_·_ (snd ℤGroup) = _+ℤ_
+inv (snd ℤGroup) = -ℤ_
+isGroup (snd ℤGroup) = isGroupℤ
+  where
+  abstract
+    isGroupℤ : IsGroup (pos 0) (_+ℤ_) (-ℤ_)
+    isGroupℤ = makeIsGroup isSetℤ
+                           +Assoc +IdR +IdL
+                           -Cancel -Cancel'
+
+ℤHom : (n : ℤ) → GroupHom ℤGroup ℤGroup
+fst (ℤHom n) x = n ·ℤ x
+snd (ℤHom n) =
+  makeIsGroupHom λ x y → ·DistR+ n x y
+
+negEquivℤ : GroupEquiv ℤGroup ℤGroup
+fst negEquivℤ =
+  isoToEquiv
+    (iso (GroupStr.inv (snd ℤGroup))
+         (GroupStr.inv (snd ℤGroup))
+         (GroupTheory.invInv ℤGroup)
+         (GroupTheory.invInv ℤGroup))
+snd negEquivℤ =
+  makeIsGroupHom -Dist+
+
+sumFinGroupℤComm : (G : Group₀) (h : GroupIso G ℤGroup) {n : ℕ}
+  (f : Fin n → fst G) → sumFinℤ {n = n} (λ a → Iso.fun (fst h) (f a))
+  ≡ Iso.fun (fst h) (sumFinGroup G {n = n} f)
+sumFinGroupℤComm G h {n = zero} f = sym (IsGroupHom.pres1 (snd h))
+sumFinGroupℤComm G h {n = suc n} f =
+    cong₂ _+ℤ_ (λ _ → Iso.fun (fst h) (f flast))
+      (sumFinGroupℤComm G h {n = n} (f ∘ injectSuc {n = n}))
+  ∙ sym (IsGroupHom.pres· (snd h) (f flast)
+    (sumFinGroup G {n = n} (λ x → f (injectSuc {n = n} x))))

Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda

@@ -0,0 +1,66 @@
+module Cubical.Algebra.OrderedCommRing.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+
+open import Cubical.Data.Empty as ⊥
+
+open import Cubical.HITs.PropositionalTruncation
+
+open import Cubical.Data.Fast.Int as ℤ
+  renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_)
+open import Cubical.Data.Fast.Int.Order
+  renaming (_<_ to _<ℤ_ ; _≤_ to _≤ℤ_)
+
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommRing.Instances.Fast.Int
+
+open import Cubical.Algebra.OrderedCommRing
+
+open import Cubical.Relation.Nullary
+
+open import Cubical.Relation.Binary.Order.StrictOrder
+open import Cubical.Relation.Binary.Order.StrictOrder.Instances.Fast.Int
+
+open import Cubical.Relation.Binary.Order.Pseudolattice
+open import Cubical.Relation.Binary.Order.Pseudolattice.Instances.Fast.Int
+
+open import Cubical.Relation.Binary
+open BinaryRelation
+
+open CommRingStr
+open OrderedCommRingStr
+open PseudolatticeStr
+open StrictOrderStr
+
+ℤOrderedCommRing : OrderedCommRing ℓ-zero ℓ-zero
+fst ℤOrderedCommRing = ℤ
+0r  (snd ℤOrderedCommRing) = 0
+1r  (snd ℤOrderedCommRing) = 1
+_+_ (snd ℤOrderedCommRing) = _+ℤ_
+_·_ (snd ℤOrderedCommRing) = _·ℤ_
+-_  (snd ℤOrderedCommRing) = -ℤ_
+_<_ (snd ℤOrderedCommRing) = _<ℤ_
+_≤_ (snd ℤOrderedCommRing) = _≤ℤ_
+isOrderedCommRing (snd ℤOrderedCommRing) = isOrderedCommRingℤ
+  where
+    open IsOrderedCommRing
+
+    isOrderedCommRingℤ : IsOrderedCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_ _<ℤ_ _≤ℤ_
+    isOrderedCommRingℤ .isCommRing      = ℤCommRing .snd .isCommRing
+    isOrderedCommRingℤ .isPseudolattice = ℤ≤Pseudolattice .snd .is-pseudolattice
+    isOrderedCommRingℤ .isStrictOrder   = ℤ<StrictOrder .snd .isStrictOrder
+    isOrderedCommRingℤ .<-≤-weaken      = λ _ _ → <-weaken
+    isOrderedCommRingℤ .≤≃¬>            = λ x y →
+      propBiimpl→Equiv isProp≤ (isProp¬ (y <ℤ x))
+        (λ x≤y y<x → isIrrefl< (≤<-trans x≤y y<x))
+        isAsym'<
+    isOrderedCommRingℤ .+MonoR≤         = λ _ _ _ → ≤-+o
+    isOrderedCommRingℤ .+MonoR<         = λ _ _ _ → <-+o
+    isOrderedCommRingℤ .posSum→pos∨pos  = λ _ _ → ∣_∣₁ ∘ 0<+ _ _
+    isOrderedCommRingℤ .<-≤-trans       = λ _ _ _ → <≤-trans
+    isOrderedCommRingℤ .≤-<-trans       = λ _ _ _ → ≤<-trans
+    isOrderedCommRingℤ .·MonoR≤         = λ _ _ _ → 0≤o→≤-·o
+    isOrderedCommRingℤ .·MonoR<         = λ _ _ _ → 0<o→<-·o
+    isOrderedCommRingℤ .0<1             = zero-<possuc

Cubical/Data/Fast/Int.agda

@@ -0,0 +1,6 @@
+-- This is the fast version of the integers.
+-- It uses the preferred version of the integers, but with more efficient operations.
+module Cubical.Data.Fast.Int where
+
+open import Cubical.Data.Fast.Int.Base public
+open import Cubical.Data.Fast.Int.Properties public

Cubical/Data/Fast/Int/Base.agda

@@ -0,0 +1,40 @@
+module Cubical.Data.Fast.Int.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat as ℕ hiding (_+_ ; _·_)
+open import Cubical.Data.Int.Base hiding (_ℕ-_ ; _+_ ; _-_ ; _·_ ; sumFinℤ ; sumFinℤId) public
+open import Cubical.Data.Fin.Base
+
+infixl 7 _·_
+infixl 6 _+_ _-_
+
+ℕ-hlp : ℕ → ℕ → ℤ
+ℕ-hlp m-n@zero n-m = - (pos n-m)
+ℕ-hlp m-n@(suc _) n-m = pos m-n
+
+_ℕ-_ : ℕ → ℕ → ℤ
+m ℕ- n = ℕ-hlp (m ℕ.∸ n) (n ℕ.∸ m)
+
+_+_ : ℤ → ℤ → ℤ
+pos m    + pos n    = pos (m ℕ.+ n)
+negsuc m + negsuc n = negsuc (suc (m ℕ.+ n))
+pos m    + negsuc n = m ℕ- (suc n)
+negsuc m + pos n    = n ℕ- (suc m)
+
+_-_ : ℤ → ℤ → ℤ
+m - n = m + (- n)
+
+_·_ : ℤ → ℤ → ℤ
+pos m       · pos n       = pos (m ℕ.· n)
+pos zero    · negsuc n    = pos zero
+pos (suc m) · negsuc n    = negsuc (predℕ (suc m ℕ.· suc n))
+negsuc m    · pos zero    = pos zero
+negsuc m    · pos (suc n) = negsuc (predℕ (suc m ℕ.· suc n))
+negsuc m    · negsuc n    = pos (suc m ℕ.· suc n)
+
+sumFinℤ : {n : ℕ} (f : Fin n → ℤ) → ℤ
+sumFinℤ {n = n} f = sumFinGen {n = n} _+_ 0 f
+
+sumFinℤId : (n : ℕ) {f g : Fin n → ℤ}
+  → ((x : _) → f x ≡ g x) → sumFinℤ {n = n} f ≡ sumFinℤ {n = n} g
+sumFinℤId n t i = sumFinℤ {n = n} λ x → t x i