patrick/agdaproofs
1
0
Fork 0
mirror of https://github.com/Smaug123/agdaproofs synced 2025-10-11 14:48:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

Polynomial ring (#76)

Browse Source
This commit is contained in:
Patrick Stevens
2019-11-17 17:37:10 +00:00
committed by GitHub
parent c55dd5f63e
commit 8377c23613
23 changed files with 984 additions and 341 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
Everything/Safe.agda
View File

@@ -29,6 +29,7 @@ open import Groups.SymmetricGroups.Lemmas
open import Groups.ActionIsSymmetry
open import Groups.Cyclic.Definition
open import Groups.Cyclic.DefinitionLemmas
open import Groups.Polynomials.Examples
open import Fields.Fields
open import Fields.Orders.Partial.Definition
@@ -45,6 +46,9 @@ open import Rings.Orders.Total.Lemmas
open import Rings.Orders.Partial.Lemmas
open import Rings.IntegralDomains
open import Rings.DirectSum
open import Rings.Polynomial.Ring
open import Rings.Ideals.Definition
open import Rings.Isomorphisms.Definition
open import Setoids.Setoids
open import Setoids.DirectSum

1
Fields/FieldOfFractions/Lemmas.agda
View File

@@ -7,6 +7,7 @@ open import Groups.Definition
open import Groups.Lemmas
open import Rings.Definition
open import Rings.Lemmas
open import Rings.Homomorphisms.Definition
open import Rings.IntegralDomains
open import Fields.Fields
open import Functions

61
Groups/Polynomials/Addition.agda Normal file
View File

@@ -0,0 +1,61 @@
{-# OPTIONS --safe --warning=error --without-K #-}
open import LogicalFormulae
open import Groups.Groups
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Numbers.Naturals.Definition
open import Setoids.Orders
open import Setoids.Setoids
open import Functions
open import Sets.EquivalenceRelations
open import Vectors
open import Lists.Lists
open import Maybe
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Groups.Polynomials.Addition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where
open import Groups.Polynomials.Definition G
open Setoid S
open Equivalence eq
open Group G
_+P_ : NaivePoly → NaivePoly → NaivePoly
_+P_ = listZip _+_ id id
PidentRight : {m : NaivePoly} → polysEqual (m +P []) m
PidentRight {[]} = record {}
PidentRight {x :: m} = reflexive ,, identityOfIndiscernablesLeft polysEqual (Equivalence.reflexive (Setoid.eq naivePolySetoid)) (equalityCommutative (mapId m))
+PwellDefined : {m n x y : NaivePoly} → polysEqual m x → polysEqual n y → polysEqual (m +P n) (x +P y)
+PwellDefined {[]} {[]} {[]} {[]} m=x n=y = record {}
+PwellDefined {[]} {[]} {[]} {x :: y} m=x (fst ,, snd) = fst ,, identityOfIndiscernablesRight polysEqual snd (equalityCommutative (mapId y))
+PwellDefined {[]} {[]} {x :: xs} {[]} (fst ,, snd) n=y = fst ,, identityOfIndiscernablesRight polysEqual snd (equalityCommutative (mapId xs))
+PwellDefined {[]} {[]} {x :: xs} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive (+WellDefined fst fst2) identRight ,, +PwellDefined {[]} {[]} {xs} {ys} snd snd2
+PwellDefined {[]} {n :: ns} {[]} {[]} m=x (fst ,, snd) = fst ,, identityOfIndiscernablesLeft polysEqual snd (equalityCommutative (mapId ns))
+PwellDefined {[]} {n :: ns} {[]} {y :: ys} m=x (fst ,, snd) = fst ,, +PwellDefined m=x snd
+PwellDefined {[]} {n :: ns} {x :: xs} {[]} (fst ,, snd) (fst2 ,, snd2) = transitive fst2 (symmetric fst) ,, ans
where
ans : polysEqual (map (λ z → z) ns) (map (λ z → z) xs)
ans rewrite mapId ns | mapId xs = Equivalence.transitive (Setoid.eq naivePolySetoid) snd2 snd
+PwellDefined {[]} {n :: ns} {x :: xs} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive (symmetric identLeft) (+WellDefined (symmetric fst) fst2) ,, (+PwellDefined snd snd2)
+PwellDefined {m :: ms} {[]} {[]} {[]} (fst ,, snd) _ = fst ,, identityOfIndiscernablesLeft polysEqual snd (equalityCommutative (mapId ms))
+PwellDefined {m :: ms} {[]} {[]} {x :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive fst (symmetric fst2) ,, ans
where
ans : polysEqual (map (λ z → z) ms) (map (λ z → z) ys)
ans rewrite mapId ms | mapId ys = Equivalence.transitive (Setoid.eq naivePolySetoid) snd snd2
+PwellDefined {m :: ms} {[]} {x :: xs} {[]} (fst ,, snd) n=y = fst ,, ans
where
ans : polysEqual (map (λ z → z) ms) (map (λ z → z) xs)
ans rewrite mapId ms | mapId xs = snd
+PwellDefined {m :: ms} {[]} {x :: xs} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive (symmetric identRight) (+WellDefined fst (symmetric fst2)) ,, identityOfIndiscernablesLeft polysEqual (Equivalence.transitive (Setoid.eq naivePolySetoid) (Equivalence.symmetric (Setoid.eq naivePolySetoid) PidentRight) (+PwellDefined snd snd2)) (equalityCommutative (mapId ms))
+PwellDefined {m :: ms} {n :: ns} {[]} {[]} (fst ,, snd) (fst2 ,, snd2) = transitive (+WellDefined fst fst2) identLeft ,, +PwellDefined snd snd2
+PwellDefined {m :: ms} {n :: ns} {[]} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive (+WellDefined fst fst2) identLeft ,, +PwellDefined snd snd2
+PwellDefined {m :: ms} {n :: ns} {x :: xs} {[]} (fst ,, snd) (fst2 ,, snd2) = transitive (+WellDefined fst fst2) identRight ,, identityOfIndiscernablesRight polysEqual (Equivalence.transitive (Setoid.eq naivePolySetoid) (+PwellDefined snd snd2) PidentRight) (equalityCommutative (mapId xs))
+PwellDefined {m :: ms} {n :: ns} {x :: xs} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = +WellDefined fst fst2 ,, +PwellDefined snd snd2
PidentLeft : {m : NaivePoly} → polysEqual ([] +P m) m
PidentLeft {[]} = record {}
PidentLeft {x :: m} = reflexive ,, identityOfIndiscernablesLeft polysEqual (Equivalence.reflexive (Setoid.eq naivePolySetoid)) (equalityCommutative (mapId m))

131
Groups/Polynomials/Definition.agda Normal file
View File

@@ -0,0 +1,131 @@
{-# OPTIONS --safe --warning=error --without-K #-}
open import LogicalFormulae
open import Groups.Groups
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Numbers.Naturals.Definition
open import Setoids.Orders
open import Setoids.Setoids
open import Functions
open import Sets.EquivalenceRelations
open import Vectors
open import Lists.Lists
open import Maybe
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Groups.Polynomials.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where
open Setoid S
open Equivalence eq
open Group G
NaivePoly : Set a
NaivePoly = List A
0P : NaivePoly
0P = []
polysEqual : NaivePoly → NaivePoly → Set (a ⊔ b)
polysEqual [] [] = True'
polysEqual [] (x :: b) = (x ∼ 0G) && polysEqual [] b
polysEqual (x :: a) [] = (x ∼ 0G) && polysEqual a []
polysEqual (x :: a) (y :: b) = (x ∼ y) && polysEqual a b
polysReflexive : {x : NaivePoly} → polysEqual x x
polysReflexive {[]} = record {}
polysReflexive {x :: y} = reflexive ,, polysReflexive
polysSymmetricZero : {x : NaivePoly} → polysEqual [] x → polysEqual x []
polysSymmetricZero {[]} 0=x = record {}
polysSymmetricZero {x :: y} (fst ,, snd) = fst ,, polysSymmetricZero snd
polysSymmetricZero' : {x : NaivePoly} → polysEqual x [] → polysEqual [] x
polysSymmetricZero' {[]} 0=x = record {}
polysSymmetricZero' {x :: y} (fst ,, snd) = fst ,, polysSymmetricZero' snd
polysSymmetric : {x y : NaivePoly} → polysEqual x y → polysEqual y x
polysSymmetric {[]} {y} x=y = polysSymmetricZero x=y
polysSymmetric {x :: xs} {[]} x=y = polysSymmetricZero' {x :: xs} x=y
polysSymmetric {x :: xs} {y :: ys} (fst ,, snd) = symmetric fst ,, polysSymmetric {xs} {ys} snd
polysTransitive : {x y z : NaivePoly} → polysEqual x y → polysEqual y z → polysEqual x z
polysTransitive {[]} {[]} {[]} x=y y=z = record {}
polysTransitive {[]} {[]} {x :: z} x=y y=z = y=z
polysTransitive {[]} {x :: y} {[]} (fst ,, snd) y=z = record {}
polysTransitive {[]} {x :: y} {x₁ :: z} (fst ,, snd) (fst2 ,, snd2) = transitive (symmetric fst2) fst ,, polysTransitive snd snd2
polysTransitive {x :: xs} {[]} {[]} x=y y=z = x=y
polysTransitive {x :: xs} {[]} {z :: zs} (fst ,, snd) (fst2 ,, snd2) = transitive fst (symmetric fst2) ,, polysTransitive snd snd2
polysTransitive {x :: xs} {y :: ys} {[]} (fst ,, snd) (fst2 ,, snd2) = transitive fst fst2 ,, polysTransitive snd snd2
polysTransitive {x :: xs} {y :: ys} {z :: zs} (fst ,, snd) (fst2 ,, snd2) = transitive fst fst2 ,, polysTransitive snd snd2
naivePolySetoid : Setoid NaivePoly
Setoid._∼_ naivePolySetoid = polysEqual
Equivalence.reflexive (Setoid.eq naivePolySetoid) = polysReflexive
Equivalence.symmetric (Setoid.eq naivePolySetoid) = polysSymmetric
Equivalence.transitive (Setoid.eq naivePolySetoid) = polysTransitive
polyInjection : A → NaivePoly
polyInjection a = a :: []
polyInjectionIsInj : SetoidInjection S naivePolySetoid polyInjection
SetoidInjection.wellDefined polyInjectionIsInj x=y = x=y ,, record {}
SetoidInjection.injective polyInjectionIsInj {x} {y} (fst ,, snd) = fst
-- the zero polynomial has no degree
-- all other polynomials have a degree
degree : ((x : A) → (x ∼ 0G) || ((x ∼ 0G) → False)) → NaivePoly → Maybe ℕ
degree decide [] = no
degree decide (x :: poly) with decide x
degree decide (x :: poly) | inl x=0 with degree decide poly
degree decide (x :: poly) | inl x=0 | no = no
degree decide (x :: poly) | inl x=0 | yes deg = yes (succ deg)
degree decide (x :: poly) | inr x!=0 with degree decide poly
degree decide (x :: poly) | inr x!=0 | no = yes 0
degree decide (x :: poly) | inr x!=0 | yes n = yes (succ n)
degreeWellDefined : (decide : ((x : A) → (x ∼ 0G) || ((x ∼ 0G) → False))) {x y : NaivePoly} → polysEqual x y → degree decide x ≡ degree decide y
degreeWellDefined decide {[]} {[]} x=y = refl
degreeWellDefined decide {[]} {x :: y} (fst ,, snd) with decide x
degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inl x=0 with inspect (degree decide y)
degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inl x=0 | no with≡ pr rewrite pr = refl
degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inl x=0 | yes bad with≡ pr rewrite pr = exFalso (noNotYes (transitivity (degreeWellDefined decide {[]} {y} snd) pr))
degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inr x!=0 with inspect (degree decide y)
degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inr x!=0 | no with≡ pr rewrite pr = exFalso (x!=0 fst)
degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inr x!=0 | yes deg with≡ pr rewrite pr = exFalso (x!=0 fst)
degreeWellDefined decide {x :: xs} {[]} x=y with decide x
degreeWellDefined decide {x :: xs} {[]} (fst ,, snd) | inl x=0 with inspect (degree decide xs)
degreeWellDefined decide {x :: xs} {[]} (fst ,, snd) | inl x=0 | no with≡ pr rewrite pr = refl
degreeWellDefined decide {x :: xs} {[]} (fst ,, snd) | inl x=0 | yes bad with≡ pr rewrite pr = exFalso (noNotYes (transitivity (equalityCommutative (degreeWellDefined decide snd)) pr))
degreeWellDefined decide {x :: xs} {[]} (fst ,, snd) | inr x!=0 = exFalso (x!=0 fst)
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) with decide x
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 with decide y
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 | inl y=0 with inspect (degree decide ys)
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 | inl y=0 | no with≡ pr rewrite degreeWellDefined decide {xs} {ys} snd | pr = refl
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 | inl y=0 | (yes th) with≡ pr rewrite degreeWellDefined decide {xs} {ys} snd | pr = refl
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 | inr y!=0 = exFalso (y!=0 (transitive (symmetric fst) x=0))
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 with decide y
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 | inl y=0 = exFalso (x!=0 (transitive fst y=0))
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 | inr y!=0 with inspect (degree decide ys)
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 | inr y!=0 | no with≡ pr rewrite degreeWellDefined decide {xs} {ys} snd | pr = refl
degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 | inr y!=0 | yes x₁ with≡ pr rewrite degreeWellDefined decide {xs} {ys} snd | pr = refl
degreeNoImpliesZero : (decide : ((x : A) → (x ∼ 0G) || ((x ∼ 0G) → False))) → (a : NaivePoly) → degree decide a ≡ no → polysEqual a []
degreeNoImpliesZero decide [] not = record {}
degreeNoImpliesZero decide (x :: a) not with decide x
degreeNoImpliesZero decide (x :: a) not | inl x=0 with inspect (degree decide a)
degreeNoImpliesZero decide (x :: a) not | inl x=0 | no with≡ pr rewrite pr = x=0 ,, degreeNoImpliesZero decide a pr
degreeNoImpliesZero decide (x :: a) not | inl x=0 | (yes deg) with≡ pr rewrite pr = exFalso (noNotYes (equalityCommutative not))
degreeNoImpliesZero decide (x :: a) not | inr x!=0 with degree decide a
degreeNoImpliesZero decide (x :: a) () | inr x!=0 | no
degreeNoImpliesZero decide (x :: a) () | inr x!=0 | yes x₁
emptyImpliesDegreeZero : (decide : ((x : A) → (x ∼ 0G) || ((x ∼ 0G) → False))) → (a : NaivePoly) → polysEqual a [] → degree decide a ≡ no
emptyImpliesDegreeZero decide [] a=[] = refl
emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) with decide x
emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) | inl x=0 with inspect (degree decide a)
emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) | inl x=0 | no with≡ pr rewrite pr = refl
emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) | inl x=0 | (yes deg) with≡ pr rewrite pr = exFalso (noNotYes (transitivity (equalityCommutative (emptyImpliesDegreeZero decide a snd)) pr))
emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) | inr x!=0 = exFalso (x!=0 fst)

35
Groups/Polynomials/Examples.agda Normal file
View File

@@ -0,0 +1,35 @@
{-# OPTIONS --safe --warning=error --without-K #-}
open import LogicalFormulae
open import Groups.Groups
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Numbers.Naturals.Definition
open import Numbers.Integers.Integers
open import Numbers.Integers.Definition
open import Setoids.Orders
open import Setoids.Setoids
open import Functions
open import Sets.EquivalenceRelations
open import Vectors
open import Lists.Lists
open import Maybe
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Groups.Polynomials.Examples where
open import Groups.Polynomials.Definition ℤGroup
private
decide : _
decide = (λ a → ℤDecideEquality a (nonneg 0))
p1 : degree decide [] ≡ no
p1 = refl
p2 : degree decide (nonneg 0 :: []) ≡ no
p2 = refl
p3 : degree decide (nonneg 1 :: []) ≡ yes 0
p3 = refl

81
Groups/Polynomials/Group.agda Normal file
View File

@@ -0,0 +1,81 @@
{-# OPTIONS --safe --warning=error --without-K #-}
open import LogicalFormulae
open import Groups.Groups
open import Groups.Abelian.Definition
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Numbers.Naturals.Definition
open import Setoids.Orders
open import Setoids.Setoids
open import Functions
open import Sets.EquivalenceRelations
open import Vectors
open import Lists.Lists
open import Maybe
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Groups.Polynomials.Group {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where
open import Groups.Polynomials.Definition G
open import Groups.Polynomials.Addition G public
open Setoid S
open Equivalence eq
inverse : NaivePoly → NaivePoly
inverse = map (Group.inverse G)
invLeft : {a : NaivePoly} → polysEqual ((inverse a) +P a) []
invLeft {[]} = record {}
invLeft {x :: a} = Group.invLeft G ,, invLeft {a}
invRight : {a : NaivePoly} → polysEqual (a +P (inverse a)) []
invRight {[]} = record {}
invRight {x :: a} = Group.invRight G ,, invRight {a}
assoc : {a b c : NaivePoly} → polysEqual (a +P (b +P c)) ((a +P b) +P c)
assoc {[]} {[]} {[]} = record {}
assoc {[]} {[]} {x :: c} = reflexive ,, ans
where
ans : polysEqual (map (λ z → z) (map (λ z → z) c)) (map (λ z → z) c)
ans rewrite mapId c | mapId c = Equivalence.reflexive (Setoid.eq naivePolySetoid)
assoc {[]} {b :: bs} {[]} = reflexive ,, ans
where
ans : polysEqual (map (λ z → z) (map (λ z → z) bs)) (map (λ z → z) (map (λ z → z) bs))
ans rewrite mapId bs | mapId bs = Equivalence.reflexive (Setoid.eq naivePolySetoid)
assoc {[]} {b :: bs} {c :: cs} = reflexive ,, ans
where
ans : polysEqual (map (λ z → z) (listZip _+_ (λ z → z) (λ z → z) bs cs)) (listZip _+_ (λ z → z) (λ z → z) (map (λ z → z) bs) cs)
ans rewrite mapId bs | mapId (listZip _+_ id id bs cs) = Equivalence.reflexive (Setoid.eq naivePolySetoid)
assoc {a :: as} {[]} {[]} = reflexive ,, ans
where
ans : polysEqual (map (λ z → z) as) (map (λ z → z) (map (λ z → z) as))
ans rewrite mapId as | mapId as = Equivalence.reflexive (Setoid.eq naivePolySetoid)
assoc {a :: as} {[]} {c :: cs} = reflexive ,, ans
where
ans : polysEqual (listZip _+_ (λ z → z) (λ z → z) as (map (λ z → z) cs)) (listZip _+_ (λ z → z) (λ z → z) (map (λ z → z) as) cs)
ans rewrite mapId cs | mapId as = Equivalence.reflexive (Setoid.eq naivePolySetoid)
assoc {a :: as} {b :: bs} {[]} = reflexive ,, ans
where
ans : polysEqual (listZip _+_ (λ z → z) (λ z → z) as (map (λ z → z) bs)) (map (λ z → z) (listZip _+_ (λ z → z) (λ z → z) as bs))
ans rewrite mapId (listZip _+_ id id as bs) | mapId bs = Equivalence.reflexive (Setoid.eq naivePolySetoid)
assoc {a :: as} {b :: bs} {c :: cs} = Group.+Associative G ,, assoc {as} {bs} {cs}
polyGroup : Group naivePolySetoid _+P_
Group.+WellDefined polyGroup = +PwellDefined
Group.0G polyGroup = []
Group.inverse polyGroup = inverse
Group.+Associative polyGroup {a} {b} {c} = assoc {a} {b} {c}
Group.identRight polyGroup = PidentRight
Group.identLeft polyGroup = PidentLeft
Group.invLeft polyGroup {a} = invLeft {a}
Group.invRight polyGroup {a} = invRight {a}
comm : AbelianGroup G → {x y : NaivePoly} → polysEqual (x +P y) (y +P x)
comm com {[]} {y} = Equivalence.transitive (Setoid.eq naivePolySetoid) (Group.identLeft polyGroup) (Equivalence.symmetric (Setoid.eq naivePolySetoid) (Group.identRight polyGroup))
comm com {x :: xs} {[]} = reflexive ,, Equivalence.reflexive (Setoid.eq naivePolySetoid)
comm com {x :: xs} {y :: ys} = AbelianGroup.commutative com ,, comm com {xs} {ys}
abelian : AbelianGroup G → AbelianGroup polyGroup
AbelianGroup.commutative (abelian ab) {x} {y} = comm ab {x} {y}

22
Lists/Lists.agda
View File

@@ -5,8 +5,10 @@ open import Functions
open import Numbers.Naturals.Semiring -- for length
open import Numbers.Naturals.Order
open import Semirings.Definition
open import Maybe
module Lists.Lists where
data List {a} (A : Set a) : Set a where
[] : List A
_::_ : (x : A) (xs : List A) → List A
@@ -157,3 +159,23 @@ module Lists.Lists where
lengthRev : {a : _} {A : Set a} (l : List A) → length (rev l) ≡ length l
lengthRev [] = refl
lengthRev (x :: l) rewrite lengthConcat (rev l) (x :: []) | lengthRev l | Semiring.commutative ℕSemiring (length l) 1 = refl
filter : {a : _} {A : Set a} (l : List A) (f : A → Bool) → List A
filter [] f = []
filter (x :: l) f with f x
filter (x :: l) f | BoolTrue = x :: filter l f
filter (x :: l) f | BoolFalse = filter l f
listLast : {a : _} {A : Set a} (l : List A) → Maybe A
listLast [] = no
listLast (x :: []) = yes x
listLast (x :: y :: l) = listLast (y :: l)
listZip : {a b c : _} {A : Set a} {B : Set b} {C : Set c} (f : A → B → C) → (f1 : A → C) → (f2 : B → C) →(l1 : List A) (l2 : List B) → List C
listZip f f1 f2 [] l2 = map f2 l2
listZip f f1 f2 (x :: l1) [] = map f1 (x :: l1)
listZip f f1 f2 (x :: l1) (y :: l2) = (f x y) :: listZip f f1 f2 l1 l2
mapId : {a : _} {A : Set a} (l : List A) → map id l ≡ l
mapId [] = refl
mapId (x :: l) rewrite mapId l = refl

16
Numbers/Integers/Definition.agda
View File

@@ -8,3 +8,19 @@ module Numbers.Integers.Definition where
data ℤ : Set where
nonneg : ℕ → ℤ
negSucc : ℕ → ℤ
nonnegInjective : {a b : ℕ} → nonneg a ≡ nonneg b → a ≡ b
nonnegInjective refl = refl
negSuccInjective : {a b : ℕ} → negSucc a ≡ negSucc b → a ≡ b
negSuccInjective refl = refl
ℤDecideEquality : (a b : ℤ) → ((a ≡ b) || ((a ≡ b) → False))
ℤDecideEquality (nonneg x) (nonneg y) with ℕDecideEquality x y
ℤDecideEquality (nonneg x) (nonneg y) | inl eq = inl (applyEquality nonneg eq)
ℤDecideEquality (nonneg x) (nonneg y) | inr non = inr λ i → non (nonnegInjective i)
ℤDecideEquality (nonneg x) (negSucc y) = inr λ ()
ℤDecideEquality (negSucc x) (nonneg x₁) = inr λ ()
ℤDecideEquality (negSucc x) (negSucc y) with ℕDecideEquality x y
ℤDecideEquality (negSucc x) (negSucc y) | inl eq = inl (applyEquality negSucc eq)
ℤDecideEquality (negSucc x) (negSucc y) | inr non = inr λ i → non (negSuccInjective i)

4
Numbers/Integers/Integers.agda
View File

@@ -11,7 +11,9 @@ module Numbers.Integers.Integers where
open Numbers.Integers.Definition using (ℤ ; nonneg ; negSucc) public
open Numbers.Integers.Addition using (_+Z_ ; ℤGroup ; ℤAbGrp) public
open Numbers.Integers.Multiplication using (_*Z_ ; ℤIntDom ; ℤRing) public
open Numbers.Integers.Multiplication using (_*Z_) public
open import Numbers.Integers.RingStructure.IntegralDomain public using (ℤIntDom) public
open import Numbers.Integers.RingStructure.Ring public using (ℤRing) public
open Numbers.Integers.Order using (_<Z_ ; ℤOrderedRing) public
_-Z_ : ℤ → ℤ → ℤ

173
Numbers/Integers/Multiplication.agda
View File

@@ -24,176 +24,3 @@ negSucc x *Z negSucc y = nonneg ((succ x) *N (succ y))
*ZInherits : (a b : ℕ) → nonneg (a *N b) ≡ (nonneg a) *Z (nonneg b)
*ZInherits a b = refl
*ZCommutative : (a b : ℤ) → a *Z b ≡ b *Z a
*ZCommutative (nonneg x) (nonneg y) = applyEquality nonneg (multiplicationNIsCommutative x y)
*ZCommutative (nonneg zero) (negSucc y) = refl
*ZCommutative (nonneg (succ x)) (negSucc y) = refl
*ZCommutative (negSucc x) (nonneg zero) = refl
*ZCommutative (negSucc x) (nonneg (succ y)) = refl
*ZCommutative (negSucc x) (negSucc y) = applyEquality nonneg (multiplicationNIsCommutative (succ x) (succ y))
*ZleftIdent : (a : ℤ) → (nonneg 1) *Z a ≡ a
*ZleftIdent (nonneg x) = applyEquality nonneg (Semiring.commutative ℕSemiring x 0)
*ZleftIdent (negSucc x) = applyEquality negSucc (transitivity (Semiring.commutative ℕSemiring (x +N 0) 0) (Semiring.commutative ℕSemiring x 0))
*ZrightIdent : (a : ℤ) → a *Z (nonneg 1) ≡ a
*ZrightIdent (nonneg x) = applyEquality nonneg (Semiring.productOneRight ℕSemiring x)
*ZrightIdent (negSucc x) = applyEquality negSucc (transitivity (Semiring.commutative ℕSemiring (x +N 0) 0) (Semiring.commutative ℕSemiring x 0))
*ZZeroLeft : (a : ℤ) → nonneg 0 *Z a ≡ nonneg 0
*ZZeroLeft (nonneg x) = refl
*ZZeroLeft (negSucc x) = refl
*ZZeroRight : (a : ℤ) → a *Z nonneg 0 ≡ nonneg 0
*ZZeroRight (nonneg x) = applyEquality nonneg (Semiring.productZeroRight ℕSemiring x)
*ZZeroRight (negSucc x) = refl
*ZAssociative : (a b c : ℤ) → a *Z (b *Z c) ≡ (a *Z b) *Z c
*ZAssociative (nonneg zero) b c = transitivity (*ZZeroLeft (b *Z c)) (transitivity (equalityCommutative (*ZZeroLeft c)) (applyEquality (_*Z c) (equalityCommutative (*ZZeroLeft b))))
*ZAssociative (nonneg (succ a)) (nonneg zero) c rewrite Semiring.productZeroRight ℕSemiring a | *ZZeroLeft c | Semiring.productZeroRight ℕSemiring a = refl
*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring b | Semiring.productZeroRight ℕSemiring (b +N a *N succ b) | Semiring.productZeroRight ℕSemiring a = refl
*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (nonneg (succ c)) = applyEquality nonneg (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c))
*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (negSucc x) rewrite productDistributes' b (a *N succ b) x | Semiring.+Associative ℕSemiring x (b *N x) ((a *N succ b) *N x) | equalityCommutative (Semiring.+Associative ℕSemiring ((x +N b *N x) +N b) (a *N ((x +N b *N x) +N b)) a) | equalityCommutative (Semiring.+Associative ℕSemiring (x +N b *N x) ((a *N succ b) *N x) (b +N a *N succ b)) | equalityCommutative (Semiring.+Associative ℕSemiring (x +N b *N x) b (a *N ((x +N b *N x) +N b) +N a)) = applyEquality (λ i → negSucc ((x +N b *N x) +N i)) ans
where
ans3 : (succ b +N (succ b *N x)) *N a ≡ succ x *N (a *N succ b)
ans3 rewrite multiplicationNIsCommutative (succ b) x = transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (succ x) (succ b) a)) (applyEquality (succ x *N_) (multiplicationNIsCommutative (succ b) a))
ans2 : a *N ((x +N b *N x) +N b) +N a ≡ (a *N succ b) +N (a *N succ b) *N x
ans2 rewrite multiplicationNIsCommutative (a *N succ b) x | Semiring.commutative ℕSemiring (succ b *N x) b | multiplicationNIsCommutative a (b +N (succ b *N x)) | Semiring.commutative ℕSemiring ((b +N (succ b *N x)) *N a) a = ans3
ans : b +N (a *N ((x +N b *N x) +N b) +N a) ≡ (a *N succ b) *N x +N (b +N a *N succ b)
ans rewrite Semiring.commutative ℕSemiring ((a *N succ b) *N x) (b +N a *N succ b) | equalityCommutative (Semiring.+Associative ℕSemiring b (a *N succ b) ((a *N succ b) *N x)) = applyEquality (b +N_) ans2
*ZAssociative (nonneg (succ a)) (negSucc b) (nonneg zero) = applyEquality nonneg (Semiring.productZeroRight ℕSemiring a)
*ZAssociative (nonneg (succ a)) (negSucc b) (nonneg (succ c)) = applyEquality negSucc ans
where
ans4 : (b +N b *N c) +N (a *N b +N (a *N b) *N c) ≡ (b +N a *N b) +N (b *N c +N (a *N b) *N c)
ans4 rewrite Semiring.+Associative ℕSemiring (b +N b *N c) (a *N b) ((a *N b) *N c) | Semiring.+Associative ℕSemiring (b +N a *N b) (b *N c) ((a *N b) *N c) = applyEquality (_+N (a *N b) *N c) (transitivity (transitivity (applyEquality (_+N a *N b) (Semiring.commutative ℕSemiring b (b *N c))) (equalityCommutative (Semiring.+Associative ℕSemiring (b *N c) b (a *N b)))) (Semiring.commutative ℕSemiring (b *N c) (b +N a *N b)))
ans3 : ((b +N b *N c) +N (a *N b +N (a *N b) *N c)) +N ((c +N a *N c) +N a) ≡ ((b +N a *N b) +N (b *N c +N (a *N b) *N c)) +N ((a +N a *N c) +N c)
ans3 rewrite Semiring.commutative ℕSemiring (c +N a *N c) a | Semiring.commutative ℕSemiring c (a *N c) | Semiring.+Associative ℕSemiring a (a *N c) c = applyEquality (λ i → i +N ((a +N a *N c) +N c)) {(b +N b *N c) +N (a *N b +N (a *N b) *N c)} {(b +N a *N b) +N (b *N c +N (a *N b) *N c)} ans4
ans2 : (((b +N c *N b) +N (a *N b +N a *N (c *N b))) +N (c +N a *N c)) +N a ≡ (((b +N a *N b) +N (c *N b +N c *N (a *N b))) +N (a +N c *N a)) +N c
ans2 rewrite multiplicationNIsCommutative c b | multiplicationNIsCommutative c (a *N b) | Semiring.*Associative ℕSemiring a b c | multiplicationNIsCommutative c a = transitivity (equalityCommutative (Semiring.+Associative ℕSemiring ((b +N b *N c) +N (a *N b +N (a *N b) *N c)) (c +N a *N c) a)) (transitivity ans3 (Semiring.+Associative ℕSemiring ((b +N a *N b) +N (b *N c +N (a *N b) *N c)) (a +N a *N c) c))
ans : succ a *N ((succ c *N b) +N c) +N a ≡ succ c *N ((succ a *N b) +N a) +N c
ans = transitivity (applyEquality (_+N a) (productDistributes (succ a) (succ c *N b) c)) (transitivity (transitivity (applyEquality (λ i → ((((b +N c *N b) +N i) +N (c +N a *N c)) +N a)) (productDistributes a b (c *N b))) (transitivity ans2 (applyEquality (λ i → (((b +N a *N b) +N i) +N (a +N c *N a)) +N c) (equalityCommutative (productDistributes c b (a *N b)))))) (applyEquality (_+N c) (equalityCommutative (productDistributes (succ c) (succ a *N b) a))))
*ZAssociative (nonneg (succ a)) (negSucc b) (negSucc x) = applyEquality nonneg ans
where
ans : succ a *N (succ b *N succ x) ≡ succ ((succ a *N b) +N a) *N succ x
ans rewrite Semiring.commutative ℕSemiring (succ a *N b) a | multiplicationNIsCommutative (succ a) b = transitivity (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ x)) (applyEquality (_*N succ x) {succ a *N succ b} {succ b *N succ a} (multiplicationNIsCommutative (succ a) (succ b)))
*ZAssociative (negSucc a) (nonneg zero) c rewrite *ZZeroLeft c = refl
*ZAssociative (negSucc a) (nonneg (succ b)) (nonneg zero) rewrite multiplicationNIsCommutative b 0 = refl
*ZAssociative (negSucc a) (nonneg (succ b)) (nonneg (succ c)) = applyEquality negSucc ans
where
ans2 : (d : ℕ) → ((succ b *N d) *N a) +N b *N d ≡ d *N ((succ b *N a) +N b)
ans2 d = transitivity (transitivity (applyEquality (((d +N b *N d) *N a) +N_) (multiplicationNIsCommutative b d)) (applyEquality (_+N d *N b) (transitivity (applyEquality (_*N a) {d +N b *N d} {d *N succ b} (multiplicationNIsCommutative (succ b) d)) (equalityCommutative (Semiring.*Associative ℕSemiring d (succ b) a))))) (equalityCommutative (Semiring.+DistributesOver* ℕSemiring d (succ b *N a) b))
ans : (succ (c +N b *N succ c) *N a) +N (c +N b *N succ c) ≡ (succ c *N ((succ b *N a) +N b)) +N c
ans rewrite Semiring.commutative ℕSemiring c (b *N succ c) | Semiring.+Associative ℕSemiring (succ (b *N succ c +N c) *N a) (b *N succ c) c | Semiring.commutative ℕSemiring (b *N succ c) c = applyEquality (_+N c) (ans2 (succ c))
*ZAssociative (negSucc a) (nonneg (succ b)) (negSucc c) = applyEquality nonneg ans
where
ans : succ a *N ((succ ((succ b) *N c)) +N b) ≡ (succ (succ b *N a) +N b) *N succ c
ans rewrite Semiring.commutative ℕSemiring (succ b *N a) b | multiplicationNIsCommutative (succ b) a = transitivity (applyEquality (succ a *N_) (applyEquality succ (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring c (b *N c) b)) (applyEquality (c +N_) (transitivity (transitivity (Semiring.commutative ℕSemiring (b *N c) b) (applyEquality (b +N_) (multiplicationNIsCommutative b c))) (multiplicationNIsCommutative (succ c) b)))))) (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c))
*ZAssociative (negSucc a) (negSucc b) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring (b +N a *N succ b) = refl
*ZAssociative (negSucc a) (negSucc b) (nonneg (succ x)) = applyEquality nonneg (transitivity (applyEquality (succ a *N_) ans) (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ x)))
where
ans : succ ((succ x *N b) +N x) ≡ (succ b *N succ x)
ans rewrite Semiring.commutative ℕSemiring (succ x *N b) x | multiplicationNIsCommutative (succ x) b = refl
*ZAssociative (negSucc a) (negSucc b) (negSucc x) = applyEquality negSucc t
where
l1 : (a b c d e f g : ℕ) → (a +N b) +N d ≡ e +N (f +N g) → (a +N b) +N (c +N d) ≡ (c +N e) +N (f +N g)
l1 a b c d e f g pr rewrite Semiring.commutative ℕSemiring c d | Semiring.+Associative ℕSemiring (a +N b) d c | pr | Semiring.commutative ℕSemiring (e +N (f +N g)) c | Semiring.+Associative ℕSemiring c e (f +N g) = refl
v : (((succ b) *N succ x) *N a) ≡ (succ x) *N (a *N succ b)
v = transitivity (applyEquality (_*N a) (multiplicationNIsCommutative (succ b) (succ x))) (transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (succ x) (succ b) a)) (applyEquality (succ x *N_) (multiplicationNIsCommutative (succ b) a)))
u : (a +N (x +N b *N succ x) *N a) +N b *N succ x ≡ (b +N a *N succ b) *N x +N (b +N a *N succ b)
u = transitivity (transitivity (transitivity (Semiring.commutative ℕSemiring (a +N (x +N b *N succ x) *N a) (b *N succ x)) (transitivity (applyEquality (_+N (a +N (x +N b *N succ x) *N a)) (multiplicationNIsCommutative b (succ x))) (transitivity (applyEquality ((b +N x *N b) +N_) v) (equalityCommutative (productDistributes (succ x) b (a *N succ b)))))) (applyEquality ((b +N a *N succ b) +N_) (multiplicationNIsCommutative x (b +N a *N succ b)))) (Semiring.commutative ℕSemiring (b +N a *N succ b) ((b +N a *N succ b) *N x))
t : (a +N (x +N b *N succ x) *N a) +N (x +N b *N succ x) ≡ (x +N (b +N a *N succ b) *N x) +N (b +N a *N succ b)
t = l1 a ((x +N b *N succ x) *N a) x (b *N succ x) ((b +N (a *N succ b)) *N x) b (a *N succ b) u
multLemma : (a b : ℕ) → a *N succ b ≡ a *N b +N a
multLemma a b rewrite multiplicationNIsCommutative a (succ b) | Semiring.commutative ℕSemiring a (b *N a) | multiplicationNIsCommutative a b = refl
negSucc+Nonneg : (a b : ℕ) → negSucc a ≡ negSucc (a +N b) +Z nonneg b
negSucc+Nonneg zero zero = refl
negSucc+Nonneg zero (succ b) = negSucc+Nonneg zero b
negSucc+Nonneg (succ a) zero rewrite Semiring.commutative ℕSemiring a 0 = refl
negSucc+Nonneg (succ a) (succ b) rewrite Semiring.commutative ℕSemiring a (succ b) | Semiring.commutative ℕSemiring b a = negSucc+Nonneg (succ a) b
distLemma : (a b : ℕ) → negSucc a *Z nonneg b ≡ negSucc ((a +N b *N a) +N b) +Z nonneg (succ a)
distLemma a b rewrite Semiring.commutative ℕSemiring (a +N b *N a) b | Semiring.commutative ℕSemiring a (b *N a) | Semiring.+Associative ℕSemiring b (b *N a) a = transitivity u (transitivity (equalityCommutative (+ZAssociative (negSucc ((b +N b *N a) +N a)) (nonneg a) (nonneg 1))) (applyEquality ((negSucc ((b +N b *N a) +N a)) +Z_) {nonneg a +Z nonneg 1} {nonneg (succ a)} (+ZCommutative (nonneg a) (nonneg 1))))
where
v : (a b : ℕ) → negSucc a *Z nonneg b ≡ (negSucc (b +N b *N a)) +Z nonneg 1
v zero zero = refl
v zero (succ b) rewrite Semiring.productZeroRight ℕSemiring b = applyEquality negSucc (equalityCommutative (Semiring.sumZeroRight ℕSemiring b))
v (succ a) zero = refl
v (succ a) (succ b) = applyEquality negSucc (Semiring.commutative ℕSemiring (succ (a +N b *N succ a)) b)
u : negSucc a *Z nonneg b ≡ (negSucc ((b +N b *N a) +N a) +Z nonneg a) +Z nonneg 1
u = transitivity (v a b) (applyEquality (_+Z nonneg 1) (negSucc+Nonneg (b +N b *N a) a))
*ZDistributesOver+Z : (a b c : ℤ) → a *Z (b +Z c) ≡ (a *Z b) +Z (a *Z c)
*ZDistributesOver+Z (nonneg zero) b c rewrite *ZZeroLeft (b +Z c) | *ZZeroLeft b | *ZZeroLeft c = refl
*ZDistributesOver+Z (nonneg (succ a)) (nonneg zero) (nonneg c) rewrite Semiring.productZeroRight ℕSemiring a = refl
*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ b)) (nonneg c) = applyEquality nonneg (productDistributes (succ a) (succ b) c)
*ZDistributesOver+Z (nonneg (succ a)) (nonneg zero) (negSucc c) rewrite Semiring.productZeroRight ℕSemiring a = refl
*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ b)) (negSucc zero) rewrite Semiring.productZeroRight ℕSemiring a = t a
where
t : (a : ℕ) → nonneg (succ a *N b) ≡ nonneg (succ a *N succ b) +Z negSucc a
t zero = refl
t (succ a) = transitivity (+Zinherits b (b +N a *N b)) (transitivity (applyEquality (nonneg b +Z_) (t a)) (transitivity (+ZAssociative (nonneg b) (nonneg (succ (b +N a *N succ b))) (negSucc a)) (applyEquality (_+Z negSucc a) {nonneg b +Z nonneg (succ (b +N a *N succ b))} {nonneg (b +N succ (b +N a *N succ b))} (equalityCommutative (+Zinherits b _)))))
*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ x)) (negSucc (succ b)) = transitivity (applyEquality ((nonneg (succ a)) *Z_) (+ZCommutative (nonneg x) (negSucc b))) (transitivity (transitivity (*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg x)) t) (+ZCommutative (negSucc ((b +N a *N succ b) +N a)) (nonneg (x +N a *N succ x))))
where
t : negSucc ((b +N a *N b) +N a) +Z nonneg (x +N a *N x) ≡ negSucc ((b +N a *N succ b) +N a) +Z nonneg (x +N a *N succ x)
t rewrite multLemma a x | multLemma a b | Semiring.+Associative ℕSemiring x (a *N x) a | Semiring.+Associative ℕSemiring b (a *N b) a | Semiring.commutative ℕSemiring (x +N a *N x) a | +Zinherits a (x +N a *N x) | +ZAssociative (negSucc (((b +N a *N b) +N a) +N a)) (nonneg a) (nonneg (x +N a *N x)) = applyEquality (_+Z nonneg (x +N a *N x)) {negSucc ((b +N a *N b) +N a)} {negSucc (((b +N a *N b) +N a) +N a) +Z nonneg a} (negSucc+Nonneg ((b +N a *N b) +N a) a)
*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring a = refl
*ZDistributesOver+Z (nonneg (succ a)) (negSucc zero) (nonneg (succ x)) rewrite Semiring.productZeroRight ℕSemiring a = t a x
where
t : (a x : ℕ) → nonneg (succ a *N x) ≡ negSucc a +Z nonneg (succ a *N succ x)
t zero x = refl
t (succ a) x with t a x
... | bl rewrite +Zinherits x (a *N x) | +Zinherits x (x +N a *N x) = transitivity (transitivity (applyEquality (nonneg x +Z_) (+Zinherits x (a *N x))) (+ZCommutative (nonneg x) (nonneg x +Z nonneg (a *N x)))) (transitivity (applyEquality (_+Z nonneg x) bl) (transitivity (equalityCommutative (+ZAssociative (negSucc a) (nonneg (succ x +N a *N succ x)) (nonneg x))) (applyEquality (λ i → negSucc a +Z nonneg i) {succ (x +N a *N succ x) +N x} {x +N succ (x +N a *N succ x)} (Semiring.commutative ℕSemiring (succ (x +N a *N succ x)) x))))
*ZDistributesOver+Z (nonneg (succ a)) (negSucc (succ b)) (nonneg (succ x)) = transitivity (*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg x)) t
where
t : negSucc ((b +N a *N b) +N a) +Z nonneg (x +N a *N x) ≡ negSucc ((b +N a *N succ b) +N a) +Z nonneg (x +N a *N succ x)
t rewrite multLemma a x | multLemma a b | Semiring.+Associative ℕSemiring x (a *N x) a | Semiring.+Associative ℕSemiring b (a *N b) a | Semiring.commutative ℕSemiring (x +N a *N x) a | +Zinherits a (x +N a *N x) | +ZAssociative (negSucc (((b +N a *N b) +N a) +N a)) (nonneg a) (nonneg (x +N a *N x)) = applyEquality (_+Z nonneg (x +N a *N x)) {negSucc ((b +N a *N b) +N a)} {negSucc (((b +N a *N b) +N a) +N a) +Z nonneg a} (negSucc+Nonneg ((b +N a *N b) +N a) a)
*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (negSucc x) = applyEquality negSucc (transitivity (applyEquality (_+N a) (transitivity (productDistributes (succ a) (succ b) x) (applyEquality (_+N (x +N a *N x)) {succ b +N a *N succ b} {succ (b +N a *N b) +N a} (applyEquality succ u)))) (equalityCommutative (Semiring.+Associative ℕSemiring (succ ((b +N a *N b) +N a)) (succ a *N x) a)))
where
u : b +N a *N succ b ≡ (succ a *N b) +N a
u rewrite multiplicationNIsCommutative a (succ b) | Semiring.commutative ℕSemiring a (b *N a) | multiplicationNIsCommutative b a = Semiring.+Associative ℕSemiring b (a *N b) a
*ZDistributesOver+Z (negSucc a) (nonneg zero) (nonneg x) = refl
*ZDistributesOver+Z (negSucc a) (nonneg zero) (negSucc x) = refl
*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (nonneg zero) rewrite Semiring.commutative ℕSemiring b 0 = refl
*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (nonneg (succ c)) = applyEquality negSucc t
where
v : a *N b +N a *N succ c ≡ c *N a +N (a +N b *N a)
v rewrite multiplicationNIsCommutative b a | Semiring.+Associative ℕSemiring (c *N a) a (a *N b) | Semiring.commutative ℕSemiring (c *N a +N a) (a *N b) | Semiring.commutative ℕSemiring (c *N a) a = applyEquality (λ i → a *N b +N i) (transitivity (multLemma a c) (transitivity (Semiring.commutative ℕSemiring (a *N c) a) (applyEquality (a +N_) (multiplicationNIsCommutative a c))))
u : (a +N (b +N succ c) *N a) +N b ≡ (a +N c *N a) +N ((a +N b *N a) +N b)
u rewrite Semiring.+Associative ℕSemiring (a +N c *N a) (a +N b *N a) b | (equalityCommutative (Semiring.+Associative ℕSemiring a (c *N a) (a +N b *N a))) = applyEquality (λ i → (a +N i) +N b) (transitivity (multiplicationNIsCommutative (b +N succ c) a) (transitivity (productDistributes a b (succ c)) v))
t : (a +N (b +N succ c) *N a) +N (b +N succ c) ≡ succ (((a +N b *N a) +N b) +N ((a +N c *N a) +N c))
t rewrite Semiring.+Associative ℕSemiring ((a +N (b +N succ c) *N a)) b (succ c) | Semiring.commutative ℕSemiring ((a +N b *N a) +N b) ((a +N c *N a) +N c) | Semiring.commutative ℕSemiring (a +N c *N a) c | equalityCommutative (Semiring.+Associative ℕSemiring (succ c) (a +N c *N a) ((a +N b *N a) +N b)) | Semiring.commutative ℕSemiring (succ c) ((a +N c *N a) +N ((a +N b *N a) +N b)) = applyEquality (_+N succ c) u
*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (negSucc zero) rewrite Semiring.productOneRight ℕSemiring a = distLemma a b
*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (negSucc (succ c)) = transitivity (*ZDistributesOver+Z (negSucc a) (nonneg b) (negSucc c)) (transitivity (applyEquality (_+Z nonneg (succ (c +N a *N succ c))) (distLemma a b)) (transitivity (equalityCommutative (+ZAssociative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a)) (nonneg (succ (c +N a *N succ c))))) (applyEquality (negSucc ((a +N b *N a) +N b) +Z_) {nonneg (succ (a +N succ (c +N a *N succ c)))} {nonneg (succ (succ (c +N a *N succ (succ c))))} (applyEquality nonneg (t (succ a) (succ c))))))
where
t : (x y : ℕ) → x +N x *N y ≡ x *N succ y
t x y = transitivity (Semiring.commutative ℕSemiring x (x *N y)) (equalityCommutative (multLemma x y))
*ZDistributesOver+Z (negSucc a) (negSucc b) (nonneg zero) rewrite Semiring.commutative ℕSemiring (b +N a *N succ b) 0 = refl
*ZDistributesOver+Z (negSucc a) (negSucc zero) (nonneg (succ b)) = transitivity (distLemma a b) (transitivity (+ZCommutative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a))) (applyEquality (λ i → nonneg (succ i) +Z negSucc ((a +N b *N a) +N b)) (equalityCommutative (Semiring.productOneRight ℕSemiring a))))
*ZDistributesOver+Z (negSucc a) (negSucc (succ c)) (nonneg (succ b)) = transitivity (applyEquality (negSucc a *Z_) (+ZCommutative (negSucc c) (nonneg b))) (transitivity (transitivity (*ZDistributesOver+Z (negSucc a) (nonneg b) (negSucc c)) (transitivity (applyEquality (_+Z nonneg (succ (c +N a *N succ c))) (distLemma a b)) (transitivity (equalityCommutative (+ZAssociative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a)) (nonneg (succ (c +N a *N succ c))))) (applyEquality (negSucc ((a +N b *N a) +N b) +Z_) {nonneg (succ (a +N succ (c +N a *N succ c)))} {nonneg (succ (succ (c +N a *N succ (succ c))))} (applyEquality nonneg (t (succ a) (succ c))))))) (+ZCommutative (negSucc ((a +N b *N a) +N b)) (nonneg (succ (succ (c +N a *N succ (succ c)))))))
where
t : (x y : ℕ) → x +N x *N y ≡ x *N succ y
t x y = transitivity (Semiring.commutative ℕSemiring x (x *N y)) (equalityCommutative (multLemma x y))
*ZDistributesOver+Z (negSucc a) (negSucc b) (negSucc c) = applyEquality nonneg (transitivity (applyEquality (λ i → succ a *N (succ i)) (transitivity (applyEquality succ (Semiring.commutative ℕSemiring b c)) (Semiring.commutative ℕSemiring (succ c) b))) (productDistributes (succ a) (succ b) (succ c)))
ℤRing : Ring (reflSetoid ℤ) _+Z_ _*Z_
Ring.additiveGroup ℤRing = ℤGroup
Ring.*WellDefined ℤRing refl refl = refl
Ring.1R ℤRing = nonneg 1
Ring.groupIsAbelian ℤRing {a} {b} = +ZCommutative a b
Ring.*Associative ℤRing {a} {b} {c} = *ZAssociative a b c
Ring.*Commutative ℤRing {a} {b} = *ZCommutative a b
Ring.*DistributesOver+ ℤRing {a} {b} {c} = *ZDistributesOver+Z a b c
Ring.identIsIdent ℤRing {a} = *ZleftIdent a
intDom : (a b : ℤ) → a *Z b ≡ nonneg 0 → (a ≡ nonneg 0) || (b ≡ nonneg 0)
intDom (nonneg zero) (nonneg b) pr = inl refl
intDom (nonneg (succ a)) (nonneg zero) pr = inr refl
intDom (nonneg zero) (negSucc b) pr = inl refl
intDom (negSucc a) (nonneg zero) pr = inr refl
ℤIntDom : IntegralDomain ℤRing
IntegralDomain.intDom ℤIntDom {a} {b} = intDom a b
IntegralDomain.nontrivial ℤIntDom ()

4
Numbers/Integers/Order.agda
View File

@@ -4,6 +4,7 @@ open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Integers.Definition
open import Numbers.Integers.RingStructure.Ring
open import Numbers.Integers.Addition
open import Numbers.Integers.Multiplication
open import Semirings.Definition
@@ -30,9 +31,6 @@ lessLemma (succ a) x pr = lessLemma a x q
q : succ x +N a ≡ a
q rewrite Semiring.commutative ℕSemiring a (succ x) | Semiring.commutative ℕSemiring x a | Semiring.commutative ℕSemiring (succ a) x = succInjective pr
nonnegInjective : {a b : ℕ} → (nonneg a ≡ nonneg b) → (a ≡ b)
nonnegInjective {a} {.a} refl = refl
irreflexive : (x : ℤ) → x <Z x → False
irreflexive (nonneg x) record { x = y ; proof = proof } = lessLemma x y (nonnegInjective proof)
irreflexive (negSucc a) record { x = x ; proof = proof } = naughtE (equalityCommutative q)

23
Numbers/Integers/RingStructure/IntegralDomain.agda Normal file
View File

@@ -0,0 +1,23 @@
{-# OPTIONS --safe --warning=error --without-K #-}
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Multiplication
open import Numbers.Integers.RingStructure.Ring
open import Semirings.Definition
open import Groups.Definition
open import Rings.Definition
open import Setoids.Setoids
open import Rings.IntegralDomains
module Numbers.Integers.RingStructure.IntegralDomain where
intDom : (a b : ℤ) → a *Z b ≡ nonneg 0 → (a ≡ nonneg 0) || (b ≡ nonneg 0)
intDom (nonneg zero) (nonneg b) pr = inl refl
intDom (nonneg (succ a)) (nonneg zero) pr = inr refl
intDom (nonneg zero) (negSucc b) pr = inl refl
intDom (negSucc a) (nonneg zero) pr = inr refl
ℤIntDom : IntegralDomain ℤRing
IntegralDomain.intDom ℤIntDom {a} {b} = intDom a b
IntegralDomain.nontrivial ℤIntDom ()

179
Numbers/Integers/RingStructure/Ring.agda Normal file
View File

@@ -0,0 +1,179 @@
{-# OPTIONS --safe --warning=error --without-K #-}
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Multiplication
open import Semirings.Definition
open import Groups.Definition
open import Rings.Definition
open import Setoids.Setoids
open import Rings.IntegralDomains
module Numbers.Integers.RingStructure.Ring where
open import Numbers.Integers.Definition public
open import Numbers.Integers.Addition public
open import Numbers.Integers.Multiplication public
*ZCommutative : (a b : ℤ) → a *Z b ≡ b *Z a
*ZCommutative (nonneg x) (nonneg y) = applyEquality nonneg (multiplicationNIsCommutative x y)
*ZCommutative (nonneg zero) (negSucc y) = refl
*ZCommutative (nonneg (succ x)) (negSucc y) = refl
*ZCommutative (negSucc x) (nonneg zero) = refl
*ZCommutative (negSucc x) (nonneg (succ y)) = refl
*ZCommutative (negSucc x) (negSucc y) = applyEquality nonneg (multiplicationNIsCommutative (succ x) (succ y))
*ZleftIdent : (a : ℤ) → (nonneg 1) *Z a ≡ a
*ZleftIdent (nonneg x) = applyEquality nonneg (Semiring.commutative ℕSemiring x 0)
*ZleftIdent (negSucc x) = applyEquality negSucc (transitivity (Semiring.commutative ℕSemiring (x +N 0) 0) (Semiring.commutative ℕSemiring x 0))
*ZrightIdent : (a : ℤ) → a *Z (nonneg 1) ≡ a
*ZrightIdent (nonneg x) = applyEquality nonneg (Semiring.productOneRight ℕSemiring x)
*ZrightIdent (negSucc x) = applyEquality negSucc (transitivity (Semiring.commutative ℕSemiring (x +N 0) 0) (Semiring.commutative ℕSemiring x 0))
*ZZeroLeft : (a : ℤ) → nonneg 0 *Z a ≡ nonneg 0
*ZZeroLeft (nonneg x) = refl
*ZZeroLeft (negSucc x) = refl
*ZZeroRight : (a : ℤ) → a *Z nonneg 0 ≡ nonneg 0
*ZZeroRight (nonneg x) = applyEquality nonneg (Semiring.productZeroRight ℕSemiring x)
*ZZeroRight (negSucc x) = refl
*ZAssociative : (a b c : ℤ) → a *Z (b *Z c) ≡ (a *Z b) *Z c
*ZAssociative (nonneg zero) b c = transitivity (*ZZeroLeft (b *Z c)) (transitivity (equalityCommutative (*ZZeroLeft c)) (applyEquality (_*Z c) (equalityCommutative (*ZZeroLeft b))))
*ZAssociative (nonneg (succ a)) (nonneg zero) c rewrite Semiring.productZeroRight ℕSemiring a | *ZZeroLeft c | Semiring.productZeroRight ℕSemiring a = refl
*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring b | Semiring.productZeroRight ℕSemiring (b +N a *N succ b) | Semiring.productZeroRight ℕSemiring a = refl
*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (nonneg (succ c)) = applyEquality nonneg (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c))
*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (negSucc x) rewrite productDistributes' b (a *N succ b) x | Semiring.+Associative ℕSemiring x (b *N x) ((a *N succ b) *N x) | equalityCommutative (Semiring.+Associative ℕSemiring ((x +N b *N x) +N b) (a *N ((x +N b *N x) +N b)) a) | equalityCommutative (Semiring.+Associative ℕSemiring (x +N b *N x) ((a *N succ b) *N x) (b +N a *N succ b)) | equalityCommutative (Semiring.+Associative ℕSemiring (x +N b *N x) b (a *N ((x +N b *N x) +N b) +N a)) = applyEquality (λ i → negSucc ((x +N b *N x) +N i)) ans
where
ans3 : (succ b +N (succ b *N x)) *N a ≡ succ x *N (a *N succ b)
ans3 rewrite multiplicationNIsCommutative (succ b) x = transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (succ x) (succ b) a)) (applyEquality (succ x *N_) (multiplicationNIsCommutative (succ b) a))
ans2 : a *N ((x +N b *N x) +N b) +N a ≡ (a *N succ b) +N (a *N succ b) *N x
ans2 rewrite multiplicationNIsCommutative (a *N succ b) x | Semiring.commutative ℕSemiring (succ b *N x) b | multiplicationNIsCommutative a (b +N (succ b *N x)) | Semiring.commutative ℕSemiring ((b +N (succ b *N x)) *N a) a = ans3
ans : b +N (a *N ((x +N b *N x) +N b) +N a) ≡ (a *N succ b) *N x +N (b +N a *N succ b)
ans rewrite Semiring.commutative ℕSemiring ((a *N succ b) *N x) (b +N a *N succ b) | equalityCommutative (Semiring.+Associative ℕSemiring b (a *N succ b) ((a *N succ b) *N x)) = applyEquality (b +N_) ans2
*ZAssociative (nonneg (succ a)) (negSucc b) (nonneg zero) = applyEquality nonneg (Semiring.productZeroRight ℕSemiring a)
*ZAssociative (nonneg (succ a)) (negSucc b) (nonneg (succ c)) = applyEquality negSucc ans
where
ans4 : (b +N b *N c) +N (a *N b +N (a *N b) *N c) ≡ (b +N a *N b) +N (b *N c +N (a *N b) *N c)
ans4 rewrite Semiring.+Associative ℕSemiring (b +N b *N c) (a *N b) ((a *N b) *N c) | Semiring.+Associative ℕSemiring (b +N a *N b) (b *N c) ((a *N b) *N c) = applyEquality (_+N (a *N b) *N c) (transitivity (transitivity (applyEquality (_+N a *N b) (Semiring.commutative ℕSemiring b (b *N c))) (equalityCommutative (Semiring.+Associative ℕSemiring (b *N c) b (a *N b)))) (Semiring.commutative ℕSemiring (b *N c) (b +N a *N b)))
ans3 : ((b +N b *N c) +N (a *N b +N (a *N b) *N c)) +N ((c +N a *N c) +N a) ≡ ((b +N a *N b) +N (b *N c +N (a *N b) *N c)) +N ((a +N a *N c) +N c)
ans3 rewrite Semiring.commutative ℕSemiring (c +N a *N c) a | Semiring.commutative ℕSemiring c (a *N c) | Semiring.+Associative ℕSemiring a (a *N c) c = applyEquality (λ i → i +N ((a +N a *N c) +N c)) {(b +N b *N c) +N (a *N b +N (a *N b) *N c)} {(b +N a *N b) +N (b *N c +N (a *N b) *N c)} ans4
ans2 : (((b +N c *N b) +N (a *N b +N a *N (c *N b))) +N (c +N a *N c)) +N a ≡ (((b +N a *N b) +N (c *N b +N c *N (a *N b))) +N (a +N c *N a)) +N c
ans2 rewrite multiplicationNIsCommutative c b | multiplicationNIsCommutative c (a *N b) | Semiring.*Associative ℕSemiring a b c | multiplicationNIsCommutative c a = transitivity (equalityCommutative (Semiring.+Associative ℕSemiring ((b +N b *N c) +N (a *N b +N (a *N b) *N c)) (c +N a *N c) a)) (transitivity ans3 (Semiring.+Associative ℕSemiring ((b +N a *N b) +N (b *N c +N (a *N b) *N c)) (a +N a *N c) c))
ans : succ a *N ((succ c *N b) +N c) +N a ≡ succ c *N ((succ a *N b) +N a) +N c
ans = transitivity (applyEquality (_+N a) (productDistributes (succ a) (succ c *N b) c)) (transitivity (transitivity (applyEquality (λ i → ((((b +N c *N b) +N i) +N (c +N a *N c)) +N a)) (productDistributes a b (c *N b))) (transitivity ans2 (applyEquality (λ i → (((b +N a *N b) +N i) +N (a +N c *N a)) +N c) (equalityCommutative (productDistributes c b (a *N b)))))) (applyEquality (_+N c) (equalityCommutative (productDistributes (succ c) (succ a *N b) a))))
*ZAssociative (nonneg (succ a)) (negSucc b) (negSucc x) = applyEquality nonneg ans
where
ans : succ a *N (succ b *N succ x) ≡ succ ((succ a *N b) +N a) *N succ x
ans rewrite Semiring.commutative ℕSemiring (succ a *N b) a | multiplicationNIsCommutative (succ a) b = transitivity (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ x)) (applyEquality (_*N succ x) {succ a *N succ b} {succ b *N succ a} (multiplicationNIsCommutative (succ a) (succ b)))
*ZAssociative (negSucc a) (nonneg zero) c rewrite *ZZeroLeft c = refl
*ZAssociative (negSucc a) (nonneg (succ b)) (nonneg zero) rewrite multiplicationNIsCommutative b 0 = refl
*ZAssociative (negSucc a) (nonneg (succ b)) (nonneg (succ c)) = applyEquality negSucc ans
where
ans2 : (d : ℕ) → ((succ b *N d) *N a) +N b *N d ≡ d *N ((succ b *N a) +N b)
ans2 d = transitivity (transitivity (applyEquality (((d +N b *N d) *N a) +N_) (multiplicationNIsCommutative b d)) (applyEquality (_+N d *N b) (transitivity (applyEquality (_*N a) {d +N b *N d} {d *N succ b} (multiplicationNIsCommutative (succ b) d)) (equalityCommutative (Semiring.*Associative ℕSemiring d (succ b) a))))) (equalityCommutative (Semiring.+DistributesOver* ℕSemiring d (succ b *N a) b))
ans : (succ (c +N b *N succ c) *N a) +N (c +N b *N succ c) ≡ (succ c *N ((succ b *N a) +N b)) +N c
ans rewrite Semiring.commutative ℕSemiring c (b *N succ c) | Semiring.+Associative ℕSemiring (succ (b *N succ c +N c) *N a) (b *N succ c) c | Semiring.commutative ℕSemiring (b *N succ c) c = applyEquality (_+N c) (ans2 (succ c))
*ZAssociative (negSucc a) (nonneg (succ b)) (negSucc c) = applyEquality nonneg ans
where
ans : succ a *N ((succ ((succ b) *N c)) +N b) ≡ (succ (succ b *N a) +N b) *N succ c
ans rewrite Semiring.commutative ℕSemiring (succ b *N a) b | multiplicationNIsCommutative (succ b) a = transitivity (applyEquality (succ a *N_) (applyEquality succ (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring c (b *N c) b)) (applyEquality (c +N_) (transitivity (transitivity (Semiring.commutative ℕSemiring (b *N c) b) (applyEquality (b +N_) (multiplicationNIsCommutative b c))) (multiplicationNIsCommutative (succ c) b)))))) (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c))
*ZAssociative (negSucc a) (negSucc b) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring (b +N a *N succ b) = refl
*ZAssociative (negSucc a) (negSucc b) (nonneg (succ x)) = applyEquality nonneg (transitivity (applyEquality (succ a *N_) ans) (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ x)))
where
ans : succ ((succ x *N b) +N x) ≡ (succ b *N succ x)
ans rewrite Semiring.commutative ℕSemiring (succ x *N b) x | multiplicationNIsCommutative (succ x) b = refl
*ZAssociative (negSucc a) (negSucc b) (negSucc x) = applyEquality negSucc t
where
l1 : (a b c d e f g : ℕ) → (a +N b) +N d ≡ e +N (f +N g) → (a +N b) +N (c +N d) ≡ (c +N e) +N (f +N g)
l1 a b c d e f g pr rewrite Semiring.commutative ℕSemiring c d | Semiring.+Associative ℕSemiring (a +N b) d c | pr | Semiring.commutative ℕSemiring (e +N (f +N g)) c | Semiring.+Associative ℕSemiring c e (f +N g) = refl
v : (((succ b) *N succ x) *N a) ≡ (succ x) *N (a *N succ b)
v = transitivity (applyEquality (_*N a) (multiplicationNIsCommutative (succ b) (succ x))) (transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (succ x) (succ b) a)) (applyEquality (succ x *N_) (multiplicationNIsCommutative (succ b) a)))
u : (a +N (x +N b *N succ x) *N a) +N b *N succ x ≡ (b +N a *N succ b) *N x +N (b +N a *N succ b)
u = transitivity (transitivity (transitivity (Semiring.commutative ℕSemiring (a +N (x +N b *N succ x) *N a) (b *N succ x)) (transitivity (applyEquality (_+N (a +N (x +N b *N succ x) *N a)) (multiplicationNIsCommutative b (succ x))) (transitivity (applyEquality ((b +N x *N b) +N_) v) (equalityCommutative (productDistributes (succ x) b (a *N succ b)))))) (applyEquality ((b +N a *N succ b) +N_) (multiplicationNIsCommutative x (b +N a *N succ b)))) (Semiring.commutative ℕSemiring (b +N a *N succ b) ((b +N a *N succ b) *N x))
t : (a +N (x +N b *N succ x) *N a) +N (x +N b *N succ x) ≡ (x +N (b +N a *N succ b) *N x) +N (b +N a *N succ b)
t = l1 a ((x +N b *N succ x) *N a) x (b *N succ x) ((b +N (a *N succ b)) *N x) b (a *N succ b) u
multLemma : (a b : ℕ) → a *N succ b ≡ a *N b +N a
multLemma a b rewrite multiplicationNIsCommutative a (succ b) | Semiring.commutative ℕSemiring a (b *N a) | multiplicationNIsCommutative a b = refl
negSucc+Nonneg : (a b : ℕ) → negSucc a ≡ negSucc (a +N b) +Z nonneg b
negSucc+Nonneg zero zero = refl
negSucc+Nonneg zero (succ b) = negSucc+Nonneg zero b
negSucc+Nonneg (succ a) zero rewrite Semiring.commutative ℕSemiring a 0 = refl
negSucc+Nonneg (succ a) (succ b) rewrite Semiring.commutative ℕSemiring a (succ b) | Semiring.commutative ℕSemiring b a = negSucc+Nonneg (succ a) b
distLemma : (a b : ℕ) → negSucc a *Z nonneg b ≡ negSucc ((a +N b *N a) +N b) +Z nonneg (succ a)
distLemma a b rewrite Semiring.commutative ℕSemiring (a +N b *N a) b | Semiring.commutative ℕSemiring a (b *N a) | Semiring.+Associative ℕSemiring b (b *N a) a = transitivity u (transitivity (equalityCommutative (+ZAssociative (negSucc ((b +N b *N a) +N a)) (nonneg a) (nonneg 1))) (applyEquality ((negSucc ((b +N b *N a) +N a)) +Z_) {nonneg a +Z nonneg 1} {nonneg (succ a)} (+ZCommutative (nonneg a) (nonneg 1))))
where
v : (a b : ℕ) → negSucc a *Z nonneg b ≡ (negSucc (b +N b *N a)) +Z nonneg 1
v zero zero = refl
v zero (succ b) rewrite Semiring.productZeroRight ℕSemiring b = applyEquality negSucc (equalityCommutative (Semiring.sumZeroRight ℕSemiring b))
v (succ a) zero = refl
v (succ a) (succ b) = applyEquality negSucc (Semiring.commutative ℕSemiring (succ (a +N b *N succ a)) b)
u : negSucc a *Z nonneg b ≡ (negSucc ((b +N b *N a) +N a) +Z nonneg a) +Z nonneg 1
u = transitivity (v a b) (applyEquality (_+Z nonneg 1) (negSucc+Nonneg (b +N b *N a) a))
*ZDistributesOver+Z : (a b c : ℤ) → a *Z (b +Z c) ≡ (a *Z b) +Z (a *Z c)
*ZDistributesOver+Z (nonneg zero) b c rewrite *ZZeroLeft (b +Z c) | *ZZeroLeft b | *ZZeroLeft c = refl
*ZDistributesOver+Z (nonneg (succ a)) (nonneg zero) (nonneg c) rewrite Semiring.productZeroRight ℕSemiring a = refl
*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ b)) (nonneg c) = applyEquality nonneg (productDistributes (succ a) (succ b) c)
*ZDistributesOver+Z (nonneg (succ a)) (nonneg zero) (negSucc c) rewrite Semiring.productZeroRight ℕSemiring a = refl
*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ b)) (negSucc zero) rewrite Semiring.productZeroRight ℕSemiring a = t a
where
t : (a : ℕ) → nonneg (succ a *N b) ≡ nonneg (succ a *N succ b) +Z negSucc a
t zero = refl
t (succ a) = transitivity (+Zinherits b (b +N a *N b)) (transitivity (applyEquality (nonneg b +Z_) (t a)) (transitivity (+ZAssociative (nonneg b) (nonneg (succ (b +N a *N succ b))) (negSucc a)) (applyEquality (_+Z negSucc a) {nonneg b +Z nonneg (succ (b +N a *N succ b))} {nonneg (b +N succ (b +N a *N succ b))} (equalityCommutative (+Zinherits b _)))))
*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ x)) (negSucc (succ b)) = transitivity (applyEquality ((nonneg (succ a)) *Z_) (+ZCommutative (nonneg x) (negSucc b))) (transitivity (transitivity (*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg x)) t) (+ZCommutative (negSucc ((b +N a *N succ b) +N a)) (nonneg (x +N a *N succ x))))
where
t : negSucc ((b +N a *N b) +N a) +Z nonneg (x +N a *N x) ≡ negSucc ((b +N a *N succ b) +N a) +Z nonneg (x +N a *N succ x)
t rewrite multLemma a x | multLemma a b | Semiring.+Associative ℕSemiring x (a *N x) a | Semiring.+Associative ℕSemiring b (a *N b) a | Semiring.commutative ℕSemiring (x +N a *N x) a | +Zinherits a (x +N a *N x) | +ZAssociative (negSucc (((b +N a *N b) +N a) +N a)) (nonneg a) (nonneg (x +N a *N x)) = applyEquality (_+Z nonneg (x +N a *N x)) {negSucc ((b +N a *N b) +N a)} {negSucc (((b +N a *N b) +N a) +N a) +Z nonneg a} (negSucc+Nonneg ((b +N a *N b) +N a) a)
*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring a = refl
*ZDistributesOver+Z (nonneg (succ a)) (negSucc zero) (nonneg (succ x)) rewrite Semiring.productZeroRight ℕSemiring a = t a x
where
t : (a x : ℕ) → nonneg (succ a *N x) ≡ negSucc a +Z nonneg (succ a *N succ x)
t zero x = refl
t (succ a) x with t a x
... | bl rewrite +Zinherits x (a *N x) | +Zinherits x (x +N a *N x) = transitivity (transitivity (applyEquality (nonneg x +Z_) (+Zinherits x (a *N x))) (+ZCommutative (nonneg x) (nonneg x +Z nonneg (a *N x)))) (transitivity (applyEquality (_+Z nonneg x) bl) (transitivity (equalityCommutative (+ZAssociative (negSucc a) (nonneg (succ x +N a *N succ x)) (nonneg x))) (applyEquality (λ i → negSucc a +Z nonneg i) {succ (x +N a *N succ x) +N x} {x +N succ (x +N a *N succ x)} (Semiring.commutative ℕSemiring (succ (x +N a *N succ x)) x))))
*ZDistributesOver+Z (nonneg (succ a)) (negSucc (succ b)) (nonneg (succ x)) = transitivity (*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg x)) t
where
t : negSucc ((b +N a *N b) +N a) +Z nonneg (x +N a *N x) ≡ negSucc ((b +N a *N succ b) +N a) +Z nonneg (x +N a *N succ x)
t rewrite multLemma a x | multLemma a b | Semiring.+Associative ℕSemiring x (a *N x) a | Semiring.+Associative ℕSemiring b (a *N b) a | Semiring.commutative ℕSemiring (x +N a *N x) a | +Zinherits a (x +N a *N x) | +ZAssociative (negSucc (((b +N a *N b) +N a) +N a)) (nonneg a) (nonneg (x +N a *N x)) = applyEquality (_+Z nonneg (x +N a *N x)) {negSucc ((b +N a *N b) +N a)} {negSucc (((b +N a *N b) +N a) +N a) +Z nonneg a} (negSucc+Nonneg ((b +N a *N b) +N a) a)
*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (negSucc x) = applyEquality negSucc (transitivity (applyEquality (_+N a) (transitivity (productDistributes (succ a) (succ b) x) (applyEquality (_+N (x +N a *N x)) {succ b +N a *N succ b} {succ (b +N a *N b) +N a} (applyEquality succ u)))) (equalityCommutative (Semiring.+Associative ℕSemiring (succ ((b +N a *N b) +N a)) (succ a *N x) a)))
where
u : b +N a *N succ b ≡ (succ a *N b) +N a
u rewrite multiplicationNIsCommutative a (succ b) | Semiring.commutative ℕSemiring a (b *N a) | multiplicationNIsCommutative b a = Semiring.+Associative ℕSemiring b (a *N b) a
*ZDistributesOver+Z (negSucc a) (nonneg zero) (nonneg x) = refl
*ZDistributesOver+Z (negSucc a) (nonneg zero) (negSucc x) = refl
*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (nonneg zero) rewrite Semiring.commutative ℕSemiring b 0 = refl
*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (nonneg (succ c)) = applyEquality negSucc t
where
v : a *N b +N a *N succ c ≡ c *N a +N (a +N b *N a)
v rewrite multiplicationNIsCommutative b a | Semiring.+Associative ℕSemiring (c *N a) a (a *N b) | Semiring.commutative ℕSemiring (c *N a +N a) (a *N b) | Semiring.commutative ℕSemiring (c *N a) a = applyEquality (λ i → a *N b +N i) (transitivity (multLemma a c) (transitivity (Semiring.commutative ℕSemiring (a *N c) a) (applyEquality (a +N_) (multiplicationNIsCommutative a c))))
u : (a +N (b +N succ c) *N a) +N b ≡ (a +N c *N a) +N ((a +N b *N a) +N b)
u rewrite Semiring.+Associative ℕSemiring (a +N c *N a) (a +N b *N a) b | (equalityCommutative (Semiring.+Associative ℕSemiring a (c *N a) (a +N b *N a))) = applyEquality (λ i → (a +N i) +N b) (transitivity (multiplicationNIsCommutative (b +N succ c) a) (transitivity (productDistributes a b (succ c)) v))
t : (a +N (b +N succ c) *N a) +N (b +N succ c) ≡ succ (((a +N b *N a) +N b) +N ((a +N c *N a) +N c))
t rewrite Semiring.+Associative ℕSemiring ((a +N (b +N succ c) *N a)) b (succ c) | Semiring.commutative ℕSemiring ((a +N b *N a) +N b) ((a +N c *N a) +N c) | Semiring.commutative ℕSemiring (a +N c *N a) c | equalityCommutative (Semiring.+Associative ℕSemiring (succ c) (a +N c *N a) ((a +N b *N a) +N b)) | Semiring.commutative ℕSemiring (succ c) ((a +N c *N a) +N ((a +N b *N a) +N b)) = applyEquality (_+N succ c) u
*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (negSucc zero) rewrite Semiring.productOneRight ℕSemiring a = distLemma a b
*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (negSucc (succ c)) = transitivity (*ZDistributesOver+Z (negSucc a) (nonneg b) (negSucc c)) (transitivity (applyEquality (_+Z nonneg (succ (c +N a *N succ c))) (distLemma a b)) (transitivity (equalityCommutative (+ZAssociative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a)) (nonneg (succ (c +N a *N succ c))))) (applyEquality (negSucc ((a +N b *N a) +N b) +Z_) {nonneg (succ (a +N succ (c +N a *N succ c)))} {nonneg (succ (succ (c +N a *N succ (succ c))))} (applyEquality nonneg (t (succ a) (succ c))))))
where
t : (x y : ℕ) → x +N x *N y ≡ x *N succ y
t x y = transitivity (Semiring.commutative ℕSemiring x (x *N y)) (equalityCommutative (multLemma x y))
*ZDistributesOver+Z (negSucc a) (negSucc b) (nonneg zero) rewrite Semiring.commutative ℕSemiring (b +N a *N succ b) 0 = refl
*ZDistributesOver+Z (negSucc a) (negSucc zero) (nonneg (succ b)) = transitivity (distLemma a b) (transitivity (+ZCommutative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a))) (applyEquality (λ i → nonneg (succ i) +Z negSucc ((a +N b *N a) +N b)) (equalityCommutative (Semiring.productOneRight ℕSemiring a))))
*ZDistributesOver+Z (negSucc a) (negSucc (succ c)) (nonneg (succ b)) = transitivity (applyEquality (negSucc a *Z_) (+ZCommutative (negSucc c) (nonneg b))) (transitivity (transitivity (*ZDistributesOver+Z (negSucc a) (nonneg b) (negSucc c)) (transitivity (applyEquality (_+Z nonneg (succ (c +N a *N succ c))) (distLemma a b)) (transitivity (equalityCommutative (+ZAssociative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a)) (nonneg (succ (c +N a *N succ c))))) (applyEquality (negSucc ((a +N b *N a) +N b) +Z_) {nonneg (succ (a +N succ (c +N a *N succ c)))} {nonneg (succ (succ (c +N a *N succ (succ c))))} (applyEquality nonneg (t (succ a) (succ c))))))) (+ZCommutative (negSucc ((a +N b *N a) +N b)) (nonneg (succ (succ (c +N a *N succ (succ c)))))))
where
t : (x y : ℕ) → x +N x *N y ≡ x *N succ y
t x y = transitivity (Semiring.commutative ℕSemiring x (x *N y)) (equalityCommutative (multLemma x y))
*ZDistributesOver+Z (negSucc a) (negSucc b) (negSucc c) = applyEquality nonneg (transitivity (applyEquality (λ i → succ a *N (succ i)) (transitivity (applyEquality succ (Semiring.commutative ℕSemiring b c)) (Semiring.commutative ℕSemiring (succ c) b))) (productDistributes (succ a) (succ b) (succ c)))
ℤRing : Ring (reflSetoid ℤ) _+Z_ _*Z_
Ring.additiveGroup ℤRing = ℤGroup
Ring.*WellDefined ℤRing refl refl = refl
Ring.1R ℤRing = nonneg 1
Ring.groupIsAbelian ℤRing {a} {b} = +ZCommutative a b
Ring.*Associative ℤRing {a} {b} {c} = *ZAssociative a b c
Ring.*Commutative ℤRing {a} {b} = *ZCommutative a b
Ring.*DistributesOver+ ℤRing {a} {b} {c} = *ZDistributesOver+Z a b c
Ring.identIsIdent ℤRing {a} = *ZleftIdent a

8
Numbers/Naturals/Definition.agda
View File

@@ -21,3 +21,11 @@ naughtE ()
aIsNotSuccA : (a : ℕ) → (a ≡ succ a) → False
aIsNotSuccA zero pr = naughtE pr
aIsNotSuccA (succ a) pr = aIsNotSuccA a (succInjective pr)
ℕDecideEquality : (a b : ℕ) → ((a ≡ b) || ((a ≡ b) → False))
ℕDecideEquality zero zero = inl refl
ℕDecideEquality zero (succ b) = inr (λ ())
ℕDecideEquality (succ a) zero = inr (λ ())
ℕDecideEquality (succ a) (succ b) with ℕDecideEquality a b
ℕDecideEquality (succ a) (succ b) | inl x = inl (applyEquality succ x)
ℕDecideEquality (succ a) (succ b) | inr x = inr λ pr → x (succInjective pr)

1
Numbers/Rationals/Lemmas.agda
View File

@@ -6,6 +6,7 @@ open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.WellFounded
open import Numbers.Naturals.Order.Lemmas
open import Numbers.Integers.Definition
open import Numbers.Integers.Integers
open import Numbers.Integers.Order
open import Groups.Groups

29
Rings/Definition.agda
View File

@@ -14,6 +14,7 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-- Following Part IB's course Groups, Rings, and Modules, we take rings to be commutative with one.
module Rings.Definition where
record Ring {n m} {A : Set n} (S : Setoid {n} {m} A) (_+_ : A → A → A) (_*_ : A → A → A) : Set (lsuc n ⊔ m) where
field
additiveGroup : Group S _+_
@@ -34,29 +35,5 @@ module Rings.Definition where
identIsIdent : {a : A} → 1R * a ∼ a
timesZero : {a : A} → a * 0R ∼ 0R
timesZero {a} = symmetric (transitive (transitive (symmetric invLeft) (+WellDefined reflexive (transitive (*WellDefined {a} {a} reflexive (symmetric identRight)) *DistributesOver+))) (transitive +Associative (transitive (+WellDefined invLeft reflexive) identLeft)))
--directSumRing : {m n : _} → {A : Set m} {B : Set n} (r : Ring A) (s : Ring B) → Ring (A && B)
--Ring.additiveGroup (directSumRing r s) = directSumGroup (Ring.additiveGroup r) (Ring.additiveGroup s)
--Ring._*_ (directSumRing r s) (a ,, b) (c ,, d) = (Ring._*_ r a c) ,, Ring._*_ s b d
--Ring.multWellDefined (directSumRing r s) (a ,, b) (c ,, d) = Ring.multWellDefined r a c ,, Ring.multWellDefined s b d
--Ring.1R (directSumRing r s) = Ring.1R r ,, Ring.1R s
--Ring.groupIsAbelian (directSumRing r s) = Ring.groupIsAbelian r ,, Ring.groupIsAbelian s
--Ring.assoc (directSumRing r s) = Ring.assoc r ,, Ring.assoc s
--Ring.multCommutative (directSumRing r s) = Ring.multCommutative r ,, Ring.multCommutative s
--Ring.multDistributes (directSumRing r s) = Ring.multDistributes r ,, Ring.multDistributes s
--Ring.identIsIdent (directSumRing r s) = Ring.identIsIdent r ,, Ring.identIsIdent s
record RingHom {m n o p : _} {A : Set m} {B : Set n} {SA : Setoid {m} {o} A} {SB : Setoid {n} {p} B} {_+A_ : A → A → A} {_*A_ : A → A → A} (R : Ring SA _+A_ _*A_) {_+B_ : B → B → B} {_*B_ : B → B → B} (S : Ring SB _+B_ _*B_) (f : A → B) : Set (m ⊔ n ⊔ o ⊔ p) where
open Ring S
open Group additiveGroup
open Setoid SB
field
preserves1 : f (Ring.1R R) ∼ 1R
ringHom : {r s : A} → f (r *A s) ∼ (f r) *B (f s)
groupHom : GroupHom (Ring.additiveGroup R) additiveGroup f
--record RingIso {m n : _} {A : Set m} {B : Set n} (R : Ring A) (S : Ring B) (f : A → B) : Set (m ⊔ n) where
-- field
-- ringHom : RingHom R S f
-- bijective : Bijection f
*DistributesOver+' : {a b c : A} → (a + b) * c ∼ (a * c) + (b * c)
*DistributesOver+' = transitive *Commutative (transitive *DistributesOver+ (+WellDefined *Commutative *Commutative))

26
Rings/Homomorphisms/Definition.agda Normal file
View File

@@ -0,0 +1,26 @@
{-# OPTIONS --safe --warning=error --without-K #-}
open import LogicalFormulae
open import Groups.Groups
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Numbers.Naturals.Naturals
open import Setoids.Orders
open import Setoids.Setoids
open import Functions
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-- Following Part IB's course Groups, Rings, and Modules, we take rings to be commutative with one.
module Rings.Homomorphisms.Definition where
record RingHom {m n o p : _} {A : Set m} {B : Set n} {SA : Setoid {m} {o} A} {SB : Setoid {n} {p} B} {_+A_ : A → A → A} {_*A_ : A → A → A} (R : Ring SA _+A_ _*A_) {_+B_ : B → B → B} {_*B_ : B → B → B} (S : Ring SB _+B_ _*B_) (f : A → B) : Set (m ⊔ n ⊔ o ⊔ p) where
open Ring S
open Group additiveGroup
open Setoid SB
field
preserves1 : f (Ring.1R R) ∼ 1R
ringHom : {r s : A} → f (r *A s) ∼ (f r) *B (f s)
groupHom : GroupHom (Ring.additiveGroup R) additiveGroup f

20
Rings/Ideals/Definition.agda Normal file
View File

@@ -0,0 +1,20 @@
{-# OPTIONS --safe --warning=error --without-K #-}
open import LogicalFormulae
open import Groups.Groups
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Numbers.Naturals.Naturals
open import Setoids.Orders
open import Setoids.Setoids
open import Functions
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.Homomorphisms.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Rings.Ideals.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
ringKernel : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} (R2 : Ring T _+2_ _*2_) {f : A → C} (fHom : RingHom R R2 f) → Set (a ⊔ d)
ringKernel {T = T} R2 {f} fHom = Sg A (λ a → Setoid._∼_ T (f a) (Ring.0R R2))

22
Rings/Isomorphisms/Definition.agda Normal file
View File

@@ -0,0 +1,22 @@
{-# OPTIONS --safe --warning=error --without-K #-}
open import LogicalFormulae
open import Groups.Groups
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Numbers.Naturals.Naturals
open import Setoids.Orders
open import Setoids.Setoids
open import Functions
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.Homomorphisms.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Rings.Isomorphisms.Definition {a b c d : _} {A : Set a} {S : Setoid {a} {b} A} {_+1_ _*1_ : A → A → A} (R1 : Ring S _+1_ _*1_) {B : Set c} {T : Setoid {c} {d} B} {_+2_ _*2_ : B → B → B} (R2 : Ring T _+2_ _*2_) where
record RingIso (f : A → B) : Set (a ⊔ b ⊔ c ⊔ d) where
field
ringHom : RingHom R1 R2 f
bijective : Bijection f

33
Rings/Polynomial/Definition.agda Normal file
View File

@@ -0,0 +1,33 @@
{-# OPTIONS --safe --warning=error --without-K #-}
open import LogicalFormulae
open import Groups.Groups
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Numbers.Naturals.Definition
open import Setoids.Orders
open import Setoids.Setoids
open import Functions
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Vectors
open import Lists.Lists
open import Maybe
open import Rings.Homomorphisms.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Rings.Polynomial.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
open Setoid S
open Equivalence eq
open Ring R
open import Groups.Polynomials.Definition additiveGroup
1P : NaivePoly
1P = 1R :: []
inducedFunction : NaivePoly → A → A
inducedFunction [] a = 0R
inducedFunction (x :: p) a = x + (a * inducedFunction p a)

123
Rings/Polynomial/Multiplication.agda Normal file
View File

@@ -0,0 +1,123 @@
{-# OPTIONS --safe --warning=error --without-K #-}
open import LogicalFormulae
open import Groups.Groups
open import Groups.Abelian.Definition
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Numbers.Naturals.Definition
open import Setoids.Orders
open import Setoids.Setoids
open import Functions
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Vectors
open import Lists.Lists
open import Maybe
open import Rings.Homomorphisms.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Rings.Polynomial.Multiplication {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
open Ring R
open Group additiveGroup
open import Groups.Polynomials.Definition additiveGroup
open import Groups.Polynomials.Group additiveGroup
open Setoid S
open Equivalence eq
_*P_ : NaivePoly → NaivePoly → NaivePoly
[] *P b = []
(x :: a) *P [] = []
(x :: a) *P (y :: b) = (x * y) :: ((map (x *_) b) +P (map (y *_) a))
p*Commutative : {a b : NaivePoly} → polysEqual (a *P b) (b *P a)
p*Commutative {[]} {[]} = record {}
p*Commutative {[]} {x :: b} = record {}
p*Commutative {x :: a} {[]} = record {}
p*Commutative {x :: xs} {y :: ys} = *Commutative ,, AbelianGroup.commutative (abelian (record { commutative = Ring.groupIsAbelian R })) {map (_*_ x) ys} {map (_*_ y) xs}
zeroTimes1 : {a : NaivePoly} (c : A) → (c ∼ 0G) → polysEqual (map (_*_ c) a) []
zeroTimes1 {[]} c c=0 = record {}
zeroTimes1 {x :: a} c c=0 = transitive (transitive *Commutative (*WellDefined reflexive c=0)) (timesZero {x}) ,, zeroTimes1 {a} c c=0
zeroTimes2 : {a : NaivePoly} (c : A) → polysEqual a [] → polysEqual (map (_*_ c) a) []
zeroTimes2 {[]} c a=0 = record {}
zeroTimes2 {x :: a} c (fst ,, snd) = transitive (*WellDefined reflexive fst) (timesZero {c}) ,, zeroTimes2 {a} c snd
mapWellDefined : (a c : A) (bs : NaivePoly) → (a ∼ c) → polysEqual (map (_*_ a) bs) (map (_*_ c) bs)
mapWellDefined a c [] a=c = record {}
mapWellDefined a c (x :: bs) a=c = *WellDefined a=c reflexive ,, mapWellDefined a c bs a=c
mapWellDefined' : (a : A) (bs cs : NaivePoly) → polysEqual bs cs → polysEqual (map (_*_ a) bs) (map (_*_ a) cs)
mapWellDefined' a [] [] bs=cs = record {}
mapWellDefined' a [] (x :: cs) (fst ,, snd) = transitive (*WellDefined reflexive fst) (timesZero {a}) ,, Equivalence.symmetric (Setoid.eq naivePolySetoid) (zeroTimes2 {cs} a (Equivalence.symmetric (Setoid.eq naivePolySetoid) snd))
mapWellDefined' a (x :: bs) [] (fst ,, snd) = transitive (*WellDefined reflexive fst) (timesZero {a}) ,, zeroTimes2 {bs} a snd
mapWellDefined' a (b :: bs) (c :: cs) (fst ,, snd) = *WellDefined reflexive fst ,, mapWellDefined' a bs cs snd
*PwellDefinedL : {a b c : NaivePoly} → polysEqual a c → polysEqual (a *P b) (c *P b)
*PwellDefinedL {[]} {[]} {[]} a=c = record {}
*PwellDefinedL {[]} {[]} {x :: c} a=c = record {}
*PwellDefinedL {[]} {x :: b} {[]} a=c = record {}
*PwellDefinedL {[]} {b :: bs} {c :: cs} (fst ,, snd) = transitive (transitive *Commutative (*WellDefined reflexive fst)) (timesZero {b}) ,, Equivalence.symmetric (Setoid.eq naivePolySetoid) (Equivalence.transitive (Setoid.eq naivePolySetoid) (+PwellDefined (zeroTimes1 {bs} c fst) (zeroTimes2 {cs} b (Equivalence.symmetric (Setoid.eq naivePolySetoid) snd))) (Group.identLeft polyGroup))
*PwellDefinedL {a :: as} {[]} {[]} a=c = record {}
*PwellDefinedL {a :: as} {[]} {x :: c} a=c = record {}
*PwellDefinedL {a :: as} {b :: bs} {[]} (fst ,, snd) = transitive (transitive *Commutative (*WellDefined reflexive fst)) (timesZero {b}) ,, Equivalence.transitive (Setoid.eq naivePolySetoid) (+PwellDefined (zeroTimes1 {bs} a fst) (zeroTimes2 {as} b snd)) (Group.identLeft polyGroup)
*PwellDefinedL {a :: as} {b :: bs} {c :: cs} (fst ,, snd) = *WellDefined fst reflexive ,, +PwellDefined (mapWellDefined a c bs fst) (mapWellDefined' b as cs snd)
*PwellDefinedR : {a b c : NaivePoly} → polysEqual b c → polysEqual (a *P b) (a *P c)
*PwellDefinedR {a} {b} {c} b=c = Equivalence.transitive (Setoid.eq naivePolySetoid) (p*Commutative {a} {b}) (Equivalence.transitive (Setoid.eq naivePolySetoid) (*PwellDefinedL b=c) (p*Commutative {c} {a}))
*PwellDefined : {a b c d : NaivePoly} → polysEqual a c → polysEqual b d → polysEqual (a *P b) (c *P d)
*PwellDefined {a}{b}{c}{d} a=c b=d = Equivalence.transitive (Setoid.eq naivePolySetoid) (*PwellDefinedL a=c) (*PwellDefinedR b=d)
private
*1 : (a : NaivePoly) → polysEqual (map (_*_ 1R) a) a
*1 [] = record {}
*1 (x :: a) = Ring.identIsIdent R ,, *1 a
*Pident : {a : NaivePoly} → polysEqual ((1R :: []) *P a) a
*Pident {[]} = record {}
*Pident {x :: a} = Ring.identIsIdent R ,, (Equivalence.transitive (Setoid.eq naivePolySetoid) (Group.identRight polyGroup {map (_*_ 1R) a}) (*1 a))
private
mapMap' : (f g : A → A) (xs : NaivePoly) → map f (map g xs) ≡ map (λ x → f (g x)) xs
mapMap' f g [] = refl
mapMap' f g (x :: xs) rewrite mapMap' f g xs = refl
mapDist : (f : A → A) (fDist : {x y : A} → f (x + y) ∼ (f x) + (f y)) (xs ys : NaivePoly) → polysEqual (map f (xs +P ys)) ((map f xs) +P (map f ys))
mapDist f fDist [] [] = record {}
mapDist f fDist [] (x :: ys) rewrite mapId ys | mapId (map f ys) = reflexive ,, Equivalence.reflexive (Setoid.eq naivePolySetoid)
mapDist f fDist (x :: xs) [] rewrite mapId xs | mapId (map f xs) = reflexive ,, Equivalence.reflexive (Setoid.eq naivePolySetoid)
mapDist f fDist (x :: xs) (y :: ys) = fDist {x} {y} ,, mapDist f fDist xs ys
mapWd : (f g : A → A) (xs : NaivePoly) → ((x : A) → (f x) ∼ (g x)) → polysEqual (map f xs) (map g xs)
mapWd f g [] ext = record {}
mapWd f g (x :: xs) ext = ext x ,, mapWd f g xs ext
mapDist' : (b c : A) → (as : NaivePoly) → polysEqual (map (_*_ (b + c)) as) (map (_*_ c) as +P map (_*_ b) as)
mapDist' b c [] = record {}
mapDist' b c (x :: as) = transitive (Ring.*DistributesOver+' R {b} {c} {x}) groupIsAbelian ,, mapDist' b c as
*Passoc : {a b c : NaivePoly} → polysEqual (a *P (b *P c)) ((a *P b) *P c)
*Passoc {[]} {b} {c} = record {}
*Passoc {a :: as} {[]} {c} = record {}
*Passoc {a :: as} {b :: bs} {[]} = record {}
*Passoc {a :: as} {b :: bs} {c :: cs} = *Associative ,, Equivalence.transitive (Setoid.eq naivePolySetoid) (+PwellDefined (mapDist (_*_ a) *DistributesOver+ (map (_*_ b) cs) (map (_*_ c) bs)) (Equivalence.reflexive (Setoid.eq naivePolySetoid))) (Equivalence.transitive (Setoid.eq naivePolySetoid) ans (+PwellDefined (Equivalence.reflexive (Setoid.eq naivePolySetoid) {map (_*_ (a * b)) cs}) (Equivalence.symmetric (Setoid.eq naivePolySetoid) (mapDist (_*_ c) *DistributesOver+ (map (_*_ a) bs) (map (_*_ b) as)))))
where
ans : polysEqual (listZip _+_ (λ z → z) (λ z → z) (listZip _+_ (λ z → z) (λ z → z) (map (_*_ a) (map (_*_ b) cs)) (map (_*_ a) (map (_*_ c) bs))) (map (_*_ (b * c)) as)) (listZip _+_ (λ z → z) (λ z → z) (map (_*_ (a * b)) cs) (listZip _+_ (λ z → z) (λ z → z) (map (_*_ c) (map (_*_ a) bs)) (map (_*_ c) (map (_*_ b) as))))
ans rewrite mapMap' (_*_ a) (_*_ c) bs | mapMap' (_*_ a) (_*_ b) cs | mapMap' (_*_ c) (_*_ a) bs | mapMap' (_*_ c) (_*_ b) as = Equivalence.transitive (Setoid.eq naivePolySetoid) (Equivalence.symmetric (Setoid.eq naivePolySetoid) (Group.+Associative polyGroup {map (λ x → a * (b * x)) cs} {map (λ x → a * (c * x)) bs} {map (_*_ (b * c)) as})) (+PwellDefined {map (λ x → a * (b * x)) cs} {(map (λ x → a * (c * x)) bs) +P map (_*_ (b * c)) as} {(map (_*_ (a * b)) cs)} (mapWd (λ x → a * (b * x)) (_*_ (a * b)) cs λ x → *Associative) (+PwellDefined {map (λ x → a * (c * x)) bs} {map (_*_ (b * c)) as} {map (λ x → c * (a * x)) bs} {map (λ x → c * (b * x)) as} (mapWd (λ x → a * (c * x)) (λ x → c * (a * x)) bs λ x → transitive *Commutative (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative))) (mapWd (_*_ (b * c)) (λ x → c * (b * x)) as λ x → transitive (*WellDefined *Commutative reflexive) (symmetric *Associative))))
*Pdistrib : {a b c : NaivePoly} → polysEqual (a *P (b +P c)) ((a *P b) +P (a *P c))
*Pdistrib {[]} {b} {c} = record {}
*Pdistrib {a :: as} {[]} {[]} = record {}
*Pdistrib {a :: as} {[]} {c :: cs} = reflexive ,, ans
where
ans : polysEqual (listZip _+_ (λ z → z) (λ z → z) (map (_*_ a) (map (λ z → z) cs)) (map (_*_ c) as)) (map (λ z → z) (listZip _+_ (λ z → z) (λ z → z) (map (_*_ a) cs) (map (_*_ c) as)))
ans rewrite mapId (listZip _+_ id id (map (_*_ a) cs) (map (_*_ c) as)) | mapId cs = Equivalence.reflexive (Setoid.eq naivePolySetoid)
*Pdistrib {a :: as} {b :: bs} {[]} = reflexive ,, ans
where
ans : polysEqual (listZip _+_ (λ z → z) (λ z → z) (map (_*_ a) (map (λ z → z) bs)) (map (_*_ b) as)) (map (λ z → z) (listZip _+_ (λ z → z) (λ z → z) (map (_*_ a) bs) (map (_*_ b) as)))
ans rewrite mapId (listZip _+_ id id (map (_*_ a) bs) (map (_*_ b) as)) | mapId bs = Equivalence.reflexive (Setoid.eq naivePolySetoid)
*Pdistrib {a :: as} {b :: bs} {c :: cs} = *DistributesOver+ ,, Equivalence.transitive (Setoid.eq naivePolySetoid) (Equivalence.transitive (Setoid.eq naivePolySetoid) (Equivalence.transitive (Setoid.eq naivePolySetoid) (Equivalence.transitive (Setoid.eq naivePolySetoid) (Equivalence.transitive (Setoid.eq naivePolySetoid) (+PwellDefined {map (_*_ a) (bs +P cs)} {map (_*_ (b + c)) as} {(map (_*_ a) bs) +P (map (_*_ a) cs)} (mapDist (_*_ a) *DistributesOver+ bs cs) (mapDist' b c as)) (Group.+Associative polyGroup {(map (_*_ a) bs) +P (map (_*_ a) cs)} {map (_*_ c) as} {map (_*_ b) as})) (+PwellDefined (Equivalence.symmetric (Setoid.eq naivePolySetoid) (Group.+Associative polyGroup {map (_*_ a) bs} {map (_*_ a) cs} {map (_*_ c) as})) (Equivalence.reflexive (Setoid.eq naivePolySetoid) {map (_*_ b) as}))) (Equivalence.symmetric (Setoid.eq naivePolySetoid) (Group.+Associative polyGroup {map (_*_ a) bs} {(map (_*_ a) cs) +P (map (_*_ c) as)} {map (_*_ b) as}))) (+PwellDefined (Equivalence.reflexive (Setoid.eq naivePolySetoid) {map (_*_ a) bs}) (AbelianGroup.commutative (abelian (record { commutative = groupIsAbelian })) {map (_*_ a) cs +P map (_*_ c) as} {map (_*_ b) as}))) (Group.+Associative polyGroup {map (_*_ a) bs} {map (_*_ b) as})

45
Rings/Polynomial/Ring.agda Normal file
View File

@@ -0,0 +1,45 @@
{-# OPTIONS --safe --warning=error --without-K #-}
open import LogicalFormulae
open import Groups.Groups
open import Groups.Abelian.Definition
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Numbers.Naturals.Definition
open import Setoids.Orders
open import Setoids.Setoids
open import Functions
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Vectors
open import Lists.Lists
open import Maybe
open import Rings.Homomorphisms.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Rings.Polynomial.Ring {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
open Ring R
open Setoid S
open Equivalence eq
open import Groups.Polynomials.Group additiveGroup
open import Groups.Polynomials.Definition additiveGroup
open import Rings.Polynomial.Definition R
open import Rings.Polynomial.Multiplication R
polyRing : Ring naivePolySetoid _+P_ _*P_
Ring.additiveGroup polyRing = polyGroup
Ring.*WellDefined polyRing {a} {b} {c} {d} = *PwellDefined {a} {b} {c} {d}
Ring.1R polyRing = 1R :: []
Ring.groupIsAbelian polyRing {x} {y} = AbelianGroup.commutative (abelian (record { commutative = Ring.groupIsAbelian R })) {x} {y}
Ring.*Associative polyRing {a} {b} {c} = *Passoc {a} {b} {c}
Ring.*Commutative polyRing {a} {b} = p*Commutative {a} {b}
Ring.*DistributesOver+ polyRing {a} {b} {c} = *Pdistrib {a} {b} {c}
Ring.identIsIdent polyRing {a} = *Pident {a}
polyInjectionIsHom : RingHom R polyRing polyInjection
RingHom.preserves1 polyInjectionIsHom = reflexive ,, record {}
RingHom.ringHom polyInjectionIsHom = reflexive ,, record {}
GroupHom.groupHom (RingHom.groupHom polyInjectionIsHom) = reflexive ,, record {}
GroupHom.wellDefined (RingHom.groupHom polyInjectionIsHom) = SetoidInjection.wellDefined polyInjectionIsInj

14
Vectors.agda
View File

@@ -6,6 +6,7 @@ open import Numbers.Naturals.Order
open import Functions
open import Semirings.Definition
open import Orders
open import Lists.Lists
data Vec {a : _} (X : Set a) : ℕ -> Set a where
[] : Vec X zero
@@ -38,6 +39,9 @@ vecLast {a} {X} {zero} v ()
vecLast {a} {X} {succ zero} (x ,- []) _ = x
vecLast {a} {X} {succ (succ m)} (x ,- v) _ = vecLast v (succIsPositive m)
vecLast' : {a : _} {X : Set a} {m : ℕ} → Vec X (succ m) → X
vecLast' {m = m} v = vecLast v (le m (applyEquality succ (Semiring.sumZeroRight ℕSemiring m)))
vecAppend : {a : _} {X : Set a} {m : ℕ} → Vec X m → (x : X) → Vec X (succ m)
vecAppend {a} {X} {zero} [] x = x ,- []
vecAppend {a} {X} {succ m} (y ,- v) x = y ,- vecAppend v x
@@ -54,9 +58,9 @@ vecMoveAppend : {a : _} {X : Set a} {m : ℕ} → (x : X) → (v : Vec X m) →
vecMoveAppend {a} {X} {.0} x [] = refl
vecMoveAppend {a} {X} {.(succ _)} x (y ,- v) rewrite vecMoveAppend x v = refl
revRevIsId : {a : _} {X : Set a} {m : ℕ} → (v : Vec X m) → (vecRev (vecRev v)) ≡ v
revRevIsId {a} {X} {zero} [] = refl
revRevIsId {a} {X} {succ m} (x ,- v) rewrite vecMoveAppend x (vecRev v) = applyEquality (λ i → x ,- i) (revRevIsId v)
vecRevRevIsId : {a : _} {X : Set a} {m : ℕ} → (v : Vec X m) → (vecRev (vecRev v)) ≡ v
vecRevRevIsId {a} {X} {zero} [] = refl
vecRevRevIsId {a} {X} {succ m} (x ,- v) rewrite vecMoveAppend x (vecRev v) = applyEquality (λ i → x ,- i) (vecRevRevIsId v)
record vecContains {a : _} {X : Set a} {m : ℕ} (vec : Vec X m) (x : X) : Set a where
field
@@ -153,6 +157,10 @@ vecComposition : {a b c : _} {X : Set a} {Y : Set b} {Z : Set c} {n : ℕ} (fs :
vecComposition [] [] [] = refl
vecComposition (f ,- fs) (g ,- gs) (x ,- xs) rewrite vecComposition fs gs xs = refl
vecToList : {a : _} {A : Set a} {n : ℕ} → (v : Vec A n) → List A
vecToList [] = []
vecToList (x ,- v) = x :: vecToList v
------------
data _<=_ : ℕ → ℕ → Set where