Skip to content

Commit 47725ea

Browse files
LorenzoMolenaLorenzoMolena
authored
Merge branch 'fast-int-with-pl-and-ocr-instances' into ocr+pl-instances
2 parents 561308e + 2484f5f commit 47725ea

File tree

15 files changed

+2503
-19
lines changed

15 files changed

+2503
-19
lines changed

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
module Cubical.Algebra.AbGroup.Instances.Int.Fast where
2+
3+
open import Cubical.Foundations.Prelude
4+
open import Cubical.Data.Int.Fast
5+
open import Cubical.Algebra.AbGroup.Base
6+
open import Cubical.Algebra.Group.Instances.Int.Fast
7+
8+
ℤAbGroup : AbGroup ℓ-zero
9+
ℤAbGroup = Group→AbGroup ℤGroup +Comm

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

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
module Cubical.Algebra.CommRing.Instances.Int.Fast where
2+
3+
open import Cubical.Foundations.Prelude
4+
5+
open import Cubical.Algebra.CommRing
6+
open import Cubical.Data.Int.Fast as Int renaming (_+_ to _+ℤ_; _·_ to _·ℤ_ ; -_ to -ℤ_)
7+
8+
open CommRingStr using (0r ; 1r ; _+_ ; _·_ ; -_ ; isCommRing)
9+
10+
ℤCommRing : CommRing ℓ-zero
11+
fst ℤCommRing = ℤ
12+
0r (snd ℤCommRing) = pos 0
13+
1r (snd ℤCommRing) = pos 1
14+
_+_ (snd ℤCommRing) = _+ℤ_
15+
_·_ (snd ℤCommRing) = _·ℤ_
16+
- snd ℤCommRing = -ℤ_
17+
isCommRing (snd ℤCommRing) = isCommRingℤ
18+
where
19+
abstract
20+
isCommRingℤ : IsCommRing (pos 0) (pos 1) _+ℤ_ _·ℤ_ -ℤ_
21+
isCommRingℤ = makeIsCommRing isSetℤ Int.+Assoc +IdR
22+
-Cancel Int.+Comm Int.·Assoc
23+
Int.·IdR ·DistR+ Int.·Comm

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

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
module Cubical.Algebra.Group.Instances.Int.Fast where
2+
3+
open import Cubical.Foundations.Prelude
4+
open import Cubical.Foundations.Isomorphism
5+
open import Cubical.Foundations.Function
6+
7+
open import Cubical.Data.Int.Fast renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_ ; _·_ to _·ℤ_ ; -_ to -ℤ_)
8+
9+
open import Cubical.Data.Nat using (ℕ ; zero ; suc)
10+
open import Cubical.Data.Fin.Inductive.Base
11+
12+
open import Cubical.Algebra.Group.Base
13+
open import Cubical.Algebra.Group.Properties
14+
open import Cubical.Algebra.Group.Morphisms
15+
open import Cubical.Algebra.Group.MorphismProperties
16+
17+
18+
open GroupStr
19+
20+
ℤGroup : Group₀
21+
fst ℤGroup = ℤ
22+
1g (snd ℤGroup) = 0
23+
_·_ (snd ℤGroup) = _+ℤ_
24+
inv (snd ℤGroup) = -ℤ_
25+
isGroup (snd ℤGroup) = isGroupℤ
26+
where
27+
abstract
28+
isGroupℤ : IsGroup (pos 0) (_+ℤ_) (-ℤ_)
29+
isGroupℤ = makeIsGroup isSetℤ
30+
+Assoc +IdR +IdL
31+
-Cancel -Cancel'
32+
33+
ℤHom : (n : ℤ) → GroupHom ℤGroup ℤGroup
34+
fst (ℤHom n) x = n ·ℤ x
35+
snd (ℤHom n) =
36+
makeIsGroupHom λ x y → ·DistR+ n x y
37+
38+
negEquivℤ : GroupEquiv ℤGroup ℤGroup
39+
fst negEquivℤ =
40+
isoToEquiv
41+
(iso (GroupStr.inv (snd ℤGroup))
42+
(GroupStr.inv (snd ℤGroup))
43+
(GroupTheory.invInv ℤGroup)
44+
(GroupTheory.invInv ℤGroup))
45+
snd negEquivℤ =
46+
makeIsGroupHom -Dist+
47+
48+
sumFinGroupℤComm : (G : Group₀) (h : GroupIso G ℤGroup) {n : ℕ}
49+
(f : Fin n → fst G) → sumFinℤ {n = n} (λ a → Iso.fun (fst h) (f a))
50+
≡ Iso.fun (fst h) (sumFinGroup G {n = n} f)
51+
sumFinGroupℤComm G h {n = zero} f = sym (IsGroupHom.pres1 (snd h))
52+
sumFinGroupℤComm G h {n = suc n} f =
53+
cong₂ _+ℤ_ (λ _ → Iso.fun (fst h) (f flast))
54+
(sumFinGroupℤComm G h {n = n} (f ∘ injectSuc {n = n}))
55+
∙ sym (IsGroupHom.pres· (snd h) (f flast)
56+
(sumFinGroup G {n = n} (λ x → f (injectSuc {n = n} x))))

‎Cubical/Data/Int/Base.agda‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,11 @@ abs : ℤ → ℕ
4242
abs (pos n) = n
4343
abs (negsuc n) = suc n
4444

45+
sign : ℤ → ℤ
46+
sign (pos zero) = pos zero
47+
sign (pos (suc n)) = pos (suc zero)
48+
sign (negsuc n) = negsuc zero
49+
4550
_ℕ-_ : ℕ → ℕ → ℤ
4651
a ℕ- 0 = pos a
4752
0 ℕ- suc b = negsuc b

‎Cubical/Data/Int/Fast.agda‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
-- This is the fast version of the integers.
2+
-- It uses the preferred version of the integers, but with more efficient operations.
3+
module Cubical.Data.Int.Fast where
4+
5+
open import Cubical.Data.Int.Fast.Base public
6+
open import Cubical.Data.Int.Fast.Properties public

‎Cubical/Data/Int/Fast/Base.agda‎

Lines changed: 19 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,8 @@ module Cubical.Data.Int.Fast.Base where
22

33
open import Cubical.Foundations.Prelude
44
open import Cubical.Data.Nat as ℕ hiding (_+_ ; _·_)
5-
open import Cubical.Data.Int.Base hiding (_ℕ-_ ; _+_ ; _-_ ; _·_) public
5+
open import Cubical.Data.Int.Base hiding (_ℕ-_ ; _+_ ; _-_ ; _·_ ; sumFinℤ ; sumFinℤId) public
6+
open import Cubical.Data.Fin.Inductive.Base
67

78
infixl 7 _·_
89
infixl 6 _+_ _-_
@@ -15,18 +16,25 @@ _ℕ-_ : ℕ → ℕ → ℤ
1516
m ℕ- n = ℕ-hlp (m ℕ.∸ n) (n ℕ.∸ m)
1617

1718
_+_ : ℤ → ℤ → ℤ
18-
pos n + pos n₁ = pos (n ℕ.+ n₁)
19-
negsuc n + negsuc n₁ = negsuc (suc (n ℕ.+ n₁))
20-
pos n + negsuc n₁ = n ℕ- (suc n₁)
21-
negsuc n + pos n₁ = n₁ ℕ- (suc n)
19+
pos m + pos n = pos (m ℕ.+ n)
20+
negsuc m + negsuc n = negsuc (suc (m ℕ.+ n))
21+
pos m + negsuc n = m ℕ- (suc n)
22+
negsuc m + pos n = n ℕ- (suc m)
2223

2324
_-_ : ℤ → ℤ → ℤ
2425
m - n = m + (- n)
2526

2627
_·_ : ℤ → ℤ → ℤ
27-
pos n · pos n₁ = pos (n ℕ.· n₁)
28-
pos zero · negsuc n₁ = pos zero
29-
pos (suc n) · negsuc n₁ = negsuc (predℕ (suc n ℕ.· suc n₁))
30-
negsuc n · pos zero = pos zero
31-
negsuc n · pos (suc n₁) = negsuc (predℕ (suc n ℕ.· suc n₁))
32-
negsuc n · negsuc n₁ = pos (suc n ℕ.· suc n₁)
28+
pos m · pos n = pos (m ℕ.· n)
29+
pos zero · negsuc n = pos zero
30+
pos (suc m) · negsuc n = negsuc (predℕ (suc m ℕ.· suc n))
31+
negsuc m · pos zero = pos zero
32+
negsuc m · pos (suc n) = negsuc (predℕ (suc m ℕ.· suc n))
33+
negsuc m · negsuc n = pos (suc m ℕ.· suc n)
34+
35+
sumFinℤ : {n : ℕ} (f : Fin n → ℤ) → ℤ
36+
sumFinℤ {n = n} f = sumFinGen {n = n} _+_ 0 f
37+
38+
sumFinℤId : (n : ℕ) {f g : Fin n → ℤ}
39+
→ ((x : _) → f x ≡ g x) → sumFinℤ {n = n} f ≡ sumFinℤ {n = n} g
40+
sumFinℤId n t i = sumFinℤ {n = n} λ x → t x i

0 commit comments

Comments
 (0)