diff --git a/Everything/Safe.agda b/Everything/Safe.agda index 37dce6b..cb002a0 100644 --- a/Everything/Safe.agda +++ b/Everything/Safe.agda @@ -2,14 +2,14 @@ -- This file contains everything that can be compiled in --safe mode. -open import Numbers.Naturals +open import Numbers.Naturals.Naturals open import Numbers.BinaryNaturals.Definition open import Lists.Lists open import Groups.Groups open import Groups.FinitePermutations -open import Groups.GroupsLemmas +open import Groups.Lemmas open import Fields.Fields open import Fields.FieldOfFractions @@ -34,4 +34,8 @@ open import WellFoundedInduction open import ClassicalLogic.ClassicalFive +open import Monoids.Definition + +open import Semirings.Definition + module Everything.Safe where diff --git a/Everything/WithK.agda b/Everything/WithK.agda index b084cc2..fef8285 100644 --- a/Everything/WithK.agda +++ b/Everything/WithK.agda @@ -27,5 +27,7 @@ open import Rings.Examples.Proofs open import Groups.FreeGroups open import Groups.Groups2 +open import Groups.Examples.ExampleSheet1 +open import Groups.LectureNotes.Lecture1 module Everything.WithK where diff --git a/Fields/FieldOfFractions.agda b/Fields/FieldOfFractions.agda index 520348e..f265177 100644 --- a/Fields/FieldOfFractions.agda +++ b/Fields/FieldOfFractions.agda @@ -2,8 +2,8 @@ open import LogicalFormulae open import Groups.Groups -open import Groups.GroupDefinition -open import Groups.GroupsLemmas +open import Groups.Definition +open import Groups.Lemmas open import Rings.Definition open import Rings.Lemmas open import Rings.IntegralDomains diff --git a/Fields/FieldOfFractionsOrder.agda b/Fields/FieldOfFractionsOrder.agda index 58fb801..bc99570 100644 --- a/Fields/FieldOfFractionsOrder.agda +++ b/Fields/FieldOfFractionsOrder.agda @@ -2,8 +2,8 @@ open import LogicalFormulae open import Groups.Groups -open import Groups.GroupDefinition -open import Groups.GroupsLemmas +open import Groups.Definition +open import Groups.Lemmas open import Rings.Definition open import Rings.Lemmas open import Rings.IntegralDomains diff --git a/Fields/Fields.agda b/Fields/Fields.agda index bc950f5..4eadb99 100644 --- a/Fields/Fields.agda +++ b/Fields/Fields.agda @@ -2,7 +2,7 @@ open import LogicalFormulae open import Groups.Groups -open import Groups.GroupDefinition +open import Groups.Definition open import Rings.Definition open import Rings.Lemmas open import Setoids.Setoids diff --git a/Groups/GroupActions.agda b/Groups/Actions.agda similarity index 100% rename from Groups/GroupActions.agda rename to Groups/Actions.agda diff --git a/Groups/GroupCosets.agda b/Groups/Cosets.agda similarity index 100% rename from Groups/GroupCosets.agda rename to Groups/Cosets.agda diff --git a/Groups/CyclicGroups.agda b/Groups/CyclicGroups.agda index 065a6bf..b06fad1 100644 --- a/Groups/CyclicGroups.agda +++ b/Groups/CyclicGroups.agda @@ -8,7 +8,7 @@ open import Numbers.Naturals open import Numbers.Integers open import Sets.FinSet open import Groups.Groups -open import Groups.GroupDefinition +open import Groups.Definition module Groups.CyclicGroups where diff --git a/Groups/GroupDefinition.agda b/Groups/Definition.agda similarity index 92% rename from Groups/GroupDefinition.agda rename to Groups/Definition.agda index 51d4a3b..90ff332 100644 --- a/Groups/GroupDefinition.agda +++ b/Groups/Definition.agda @@ -4,10 +4,10 @@ open import LogicalFormulae open import Setoids.Setoids open import Functions open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) -open import Numbers.Naturals +open import Numbers.Naturals.Naturals open import Sets.FinSet -module Groups.GroupDefinition where +module Groups.Definition where record Group {lvl1 lvl2} {A : Set lvl1} (S : Setoid {lvl1} {lvl2} A) (_·_ : A → A → A) : Set (lsuc lvl1 ⊔ lvl2) where open Setoid S diff --git a/Groups/GroupsExampleSheet1.agda b/Groups/Examples/ExampleSheet1.agda similarity index 98% rename from Groups/GroupsExampleSheet1.agda rename to Groups/Examples/ExampleSheet1.agda index 5ff53ed..f9a83ed 100644 --- a/Groups/GroupsExampleSheet1.agda +++ b/Groups/Examples/ExampleSheet1.agda @@ -1,17 +1,19 @@ {-# OPTIONS --safe --warning=error #-} open import LogicalFormulae -open import Setoids +open import Setoids.Setoids open import Functions open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) -open import Naturals -open import Integers -open import FinSet -open import Groups -open import Rings -open import Fields +open import Numbers.Naturals.Naturals +open import Numbers.Integers +open import Sets.FinSet +open import Groups.Definition +open import Groups.Groups +open import Rings.Definition +open import Rings.Lemmas +open import Fields.Fields -module GroupsExampleSheet1 where +module Groups.Examples.ExampleSheet1 where {- Question 1: e is the unique solution of x^2 = x diff --git a/Groups/GroupsExamples.agda b/Groups/Examples/Examples.agda similarity index 97% rename from Groups/GroupsExamples.agda rename to Groups/Examples/Examples.agda index b52c8c6..8c9634a 100644 --- a/Groups/GroupsExamples.agda +++ b/Groups/Examples/Examples.agda @@ -1,19 +1,20 @@ {-# OPTIONS --safe --warning=error #-} -open import Groups +open import Groups.Definition open import Orders -open import Integers -open import Setoids +open import Numbers.Integers +open import Setoids.Setoids open import LogicalFormulae -open import FinSet +open import Sets.FinSet open import Functions -open import Naturals +open import Numbers.Naturals open import IntegersModN -open import RingExamples +open import Rings.Examples.Examples open import PrimeNumbers -open import Groups2 +open import Groups.Groups2 +open import Groups.CyclicGroups -module GroupsExamples where +module Groups.Examples.Examples where elementPowZ : (n : ℕ) → (elementPower ℤGroup (nonneg 1) n) ≡ nonneg n elementPowZ zero = refl elementPowZ (succ n) rewrite elementPowZ n = refl diff --git a/Groups/FinitePermutations.agda b/Groups/FinitePermutations.agda index bee2bc2..f6adbe8 100644 --- a/Groups/FinitePermutations.agda +++ b/Groups/FinitePermutations.agda @@ -1,7 +1,7 @@ {-# OPTIONS --safe --warning=error --without-K #-} open import LogicalFormulae -open import Numbers.Naturals -- for length +open import Numbers.Naturals.Naturals -- for length open import Lists.Lists open import Functions open import Groups.SymmetryGroups diff --git a/Groups/FreeGroups.agda b/Groups/FreeGroups.agda index 8c36bc3..ade249e 100644 --- a/Groups/FreeGroups.agda +++ b/Groups/FreeGroups.agda @@ -5,10 +5,10 @@ open import WithK open import Setoids.Setoids open import Functions open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) -open import Numbers.Naturals -open import Numbers.NaturalsWithK +open import Numbers.Naturals.Naturals +open import Numbers.Naturals.WithK open import Sets.FinSet -open import Groups.GroupDefinition +open import Groups.Definition open import Groups.SymmetryGroups open import DecidableSet diff --git a/Groups/Groups.agda b/Groups/Groups.agda index b555272..5fe5b13 100644 --- a/Groups/Groups.agda +++ b/Groups/Groups.agda @@ -4,9 +4,9 @@ open import LogicalFormulae open import Setoids.Setoids open import Functions open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) -open import Numbers.Naturals +open import Numbers.Naturals.Naturals open import Sets.FinSet -open import Groups.GroupDefinition +open import Groups.Definition module Groups.Groups where diff --git a/Groups/Groups2.agda b/Groups/Groups2.agda index f5a1fcb..9045559 100644 --- a/Groups/Groups2.agda +++ b/Groups/Groups2.agda @@ -1,14 +1,14 @@ {-# OPTIONS --safe --warning=error #-} open import Groups.Groups -open import Groups.GroupDefinition +open import Groups.Definition open import Orders open import Numbers.Integers open import Setoids.Setoids open import LogicalFormulae open import Sets.FinSet open import Functions -open import Numbers.Naturals +open import Numbers.Naturals.Naturals open import IntegersModN open import Rings.Examples.Examples open import PrimeNumbers diff --git a/Groups/LectureNotes/Lecture1.agda b/Groups/LectureNotes/Lecture1.agda index 9dcda01..8f4d7eb 100644 --- a/Groups/LectureNotes/Lecture1.agda +++ b/Groups/LectureNotes/Lecture1.agda @@ -4,13 +4,13 @@ open import LogicalFormulae open import Setoids.Setoids open import Functions open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) -open import Numbers.Naturals +open import Numbers.Naturals.Naturals open import Numbers.Integers open import Numbers.Rationals open import Sets.FinSet -open import Groups.GroupDefinition +open import Groups.Definition open import Groups.Groups -open import Rings.RingDefinition +open import Rings.Definition open import IntegersModN module Groups.LectureNotes.Lecture1 where diff --git a/Groups/GroupsLemmas.agda b/Groups/Lemmas.agda similarity index 95% rename from Groups/GroupsLemmas.agda rename to Groups/Lemmas.agda index e0638b5..a14fdfd 100644 --- a/Groups/GroupsLemmas.agda +++ b/Groups/Lemmas.agda @@ -4,11 +4,11 @@ open import LogicalFormulae open import Setoids.Setoids open import Functions open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) -open import Numbers.Naturals +open import Numbers.Naturals.Naturals open import Groups.Groups -open import Groups.GroupDefinition +open import Groups.Definition -module Groups.GroupsLemmas where +module Groups.Lemmas where invInv : {a b : _} → {A : Set a} → {_·_ : A → A → A} → {S : Setoid {a} {b} A} → (G : Group S _·_) → {x : A} → Setoid._∼_ S (Group.inverse G (Group.inverse G x)) x invInv {S = S} G {x} = symmetric (transferToRight' G invRight) where diff --git a/Groups/SymmetryGroups.agda b/Groups/SymmetryGroups.agda index d80b712..cdbcf78 100644 --- a/Groups/SymmetryGroups.agda +++ b/Groups/SymmetryGroups.agda @@ -4,10 +4,10 @@ open import LogicalFormulae open import Setoids.Setoids open import Functions open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) -open import Numbers.Naturals +open import Numbers.Naturals.Naturals open import Sets.FinSet open import Groups.Groups -open import Groups.GroupDefinition +open import Groups.Definition module Groups.SymmetryGroups where data SymmetryGroupElements {a b : _} {A : Set a} (S : Setoid {a} {b} A) : Set (a ⊔ b) where diff --git a/IntegersModN.agda b/IntegersModN.agda index 38245dc..fc60dab 100644 --- a/IntegersModN.agda +++ b/IntegersModN.agda @@ -1,15 +1,18 @@ {-# OPTIONS --safe --warning=error #-} open import LogicalFormulae -open import Groups.GroupDefinition +open import Groups.Definition open import Groups.Groups -open import Numbers.Naturals +open import Numbers.Naturals.Naturals +open import Numbers.Naturals.Addition -- TODO remove this dependency open import PrimeNumbers open import Setoids.Setoids open import Sets.FinSet open import Sets.FinSetWithK open import Functions -open import Numbers.NaturalsWithK +open import Numbers.Naturals.WithK +open import Semirings.Definition +open import Orders module IntegersModN where record ℤn (n : ℕ) (pr : 0 n +N c) pr +addingPreservesEqualityLeft : {a b : ℕ} (c : ℕ) → (a ≡ b) → (c +N a ≡ c +N b) +addingPreservesEqualityLeft {a} {b} c pr = applyEquality (λ n -> c +N n) pr + +additionNIsAssociative : (a b c : ℕ) → ((a +N b) +N c) ≡ (a +N (b +N c)) +additionNIsAssociative zero b c = refl +additionNIsAssociative (succ a) zero c = transitivity (transitivity (applyEquality (λ n → n +N c) (applyEquality succ (addZeroRight a))) refl) (transitivity refl refl) +additionNIsAssociative (succ a) (succ b) c = transitivity refl (transitivity refl (transitivity (applyEquality succ (additionNIsAssociative a (succ b) c)) refl)) + +succIsAddOne : (a : ℕ) → succ a ≡ a +N succ zero +succIsAddOne a = equalityCommutative (transitivity (additionNIsCommutative a (succ zero)) refl) diff --git a/Numbers/Naturals/Definition.agda b/Numbers/Naturals/Definition.agda new file mode 100644 index 0000000..d12fd99 --- /dev/null +++ b/Numbers/Naturals/Definition.agda @@ -0,0 +1,16 @@ +{-# OPTIONS --warning=error --safe --without-K #-} + +open import LogicalFormulae + +module Numbers.Naturals.Definition where + +data ℕ : Set where + zero : ℕ + succ : ℕ → ℕ + +infix 100 succ + +{-# BUILTIN NATURAL ℕ #-} + +succInjective : {a b : ℕ} → (succ a ≡ succ b) → a ≡ b +succInjective {a} {.a} refl = refl diff --git a/Numbers/Naturals/Multiplication.agda b/Numbers/Naturals/Multiplication.agda new file mode 100644 index 0000000..fa877e8 --- /dev/null +++ b/Numbers/Naturals/Multiplication.agda @@ -0,0 +1,82 @@ +{-# OPTIONS --warning=error --safe --without-K #-} + +open import LogicalFormulae +open import Numbers.Naturals.Definition +open import Numbers.Naturals.Addition + +module Numbers.Naturals.Multiplication where + +infix 25 _*N_ +_*N_ : ℕ → ℕ → ℕ +zero *N y = zero +(succ x) *N y = y +N (x *N y) + +productZeroIsZeroLeft : (a : ℕ) → (zero *N a ≡ zero) +productZeroIsZeroLeft a = refl + +productZeroIsZeroRight : (a : ℕ) → (a *N zero ≡ zero) +productZeroIsZeroRight zero = refl +productZeroIsZeroRight (succ a) = productZeroIsZeroRight a + +productWithOneLeft : (a : ℕ) → ((succ zero) *N a) ≡ a +productWithOneLeft a = transitivity refl (transitivity (applyEquality (λ { m -> a +N m }) refl) (additionNIsCommutative a zero)) + +productWithOneRight : (a : ℕ) → a *N succ zero ≡ a +productWithOneRight zero = refl +productWithOneRight (succ a) = transitivity refl (addingPreservesEqualityLeft (succ zero) (productWithOneRight a)) + +productDistributes : (a b c : ℕ) → (a *N (b +N c)) ≡ a *N b +N a *N c +productDistributes zero b c = refl +productDistributes (succ a) b c = transitivity refl + (transitivity (addingPreservesEqualityLeft (b +N c) (productDistributes a b c)) + (transitivity (equalityCommutative (additionNIsAssociative (b +N c) (a *N b) (a *N c))) + (transitivity (addingPreservesEqualityRight (a *N c) (additionNIsCommutative (b +N c) (a *N b))) + (transitivity (addingPreservesEqualityRight (a *N c) (equalityCommutative (additionNIsAssociative (a *N b) b c))) + (transitivity (addingPreservesEqualityRight (a *N c) (addingPreservesEqualityRight c (additionNIsCommutative (a *N b) b))) + (transitivity (addingPreservesEqualityRight (a *N c) (addingPreservesEqualityRight {b +N a *N b} {(succ a) *N b} c (refl))) + (transitivity (additionNIsAssociative ((succ a) *N b) c (a *N c)) + (transitivity (addingPreservesEqualityLeft (succ a *N b) refl) + refl) + ) + )))))) + +productPreservesEqualityLeft : (a : ℕ) → {b c : ℕ} → b ≡ c → a *N b ≡ a *N c +productPreservesEqualityLeft a {b} {.b} refl = refl + +aSucB : (a b : ℕ) → a *N succ b ≡ a *N b +N a +aSucB a b = transitivity {_} {ℕ} {a *N succ b} {a *N (b +N succ zero)} (productPreservesEqualityLeft a (succIsAddOne b)) (transitivity {_} {ℕ} {a *N (b +N succ zero)} {a *N b +N a *N succ zero} (productDistributes a b (succ zero)) (addingPreservesEqualityLeft (a *N b) (productWithOneRight a))) + +aSucBRight : (a b : ℕ) → (succ a) *N b ≡ a *N b +N b +aSucBRight a b = additionNIsCommutative b (a *N b) + +multiplicationNIsCommutative : (a b : ℕ) → (a *N b) ≡ (b *N a) +multiplicationNIsCommutative zero b = transitivity (productZeroIsZeroLeft b) (equalityCommutative (productZeroIsZeroRight b)) +multiplicationNIsCommutative (succ a) zero = multiplicationNIsCommutative a zero +multiplicationNIsCommutative (succ a) (succ b) = transitivity refl + (transitivity (addingPreservesEqualityLeft (succ b) (aSucB a b)) + (transitivity (additionNIsCommutative (succ b) (a *N b +N a)) + (transitivity (additionNIsAssociative (a *N b) a (succ b)) + (transitivity (addingPreservesEqualityLeft (a *N b) (succCanMove a b)) + (transitivity (addingPreservesEqualityLeft (a *N b) (additionNIsCommutative (succ a) b)) + (transitivity (equalityCommutative (additionNIsAssociative (a *N b) b (succ a))) + (transitivity (addingPreservesEqualityRight (succ a) (equalityCommutative (aSucBRight a b))) + (transitivity (addingPreservesEqualityRight (succ a) (multiplicationNIsCommutative (succ a) b)) + (transitivity (additionNIsCommutative (b *N (succ a)) (succ a)) + refl + ))))))))) + +productDistributes' : (a b c : ℕ) → (a +N b) *N c ≡ a *N c +N b *N c +productDistributes' a b c rewrite multiplicationNIsCommutative (a +N b) c | productDistributes c a b | multiplicationNIsCommutative c a | multiplicationNIsCommutative c b = refl + +flipProductsWithinSum : (a b c : ℕ) → (c *N a +N c *N b ≡ a *N c +N b *N c) +flipProductsWithinSum a b c = transitivity (addingPreservesEqualityRight (c *N b) (multiplicationNIsCommutative c a)) ((addingPreservesEqualityLeft (a *N c) (multiplicationNIsCommutative c b))) + +productDistributesRight : (a b c : ℕ) → (a +N b) *N c ≡ a *N c +N b *N c +productDistributesRight a b c = transitivity (multiplicationNIsCommutative (a +N b) c) (transitivity (productDistributes c a b) (flipProductsWithinSum a b c)) + +multiplicationNIsAssociative : (a b c : ℕ) → (a *N (b *N c)) ≡ ((a *N b) *N c) +multiplicationNIsAssociative zero b c = refl +multiplicationNIsAssociative (succ a) b c = + transitivity refl + (transitivity refl + (transitivity (applyEquality ((λ x → b *N c +N x)) (multiplicationNIsAssociative a b c)) (transitivity (equalityCommutative (productDistributesRight b (a *N b) c)) refl))) diff --git a/Numbers/Naturals.agda b/Numbers/Naturals/Naturals.agda similarity index 80% rename from Numbers/Naturals.agda rename to Numbers/Naturals/Naturals.agda index c115b4c..34ad67d 100644 --- a/Numbers/Naturals.agda +++ b/Numbers/Naturals/Naturals.agda @@ -5,196 +5,31 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) open import WellFoundedInduction open import Functions open import Orders +open import Numbers.Naturals.Definition +open import Numbers.Naturals.Addition +open import Numbers.Naturals.Order +open import Numbers.Naturals.Multiplication +open import Semirings.Definition +open import Monoids.Definition -module Numbers.Naturals where - data ℕ : Set where - zero : ℕ - succ : ℕ → ℕ +module Numbers.Naturals.Naturals where - {-# BUILTIN NATURAL ℕ #-} + open Numbers.Naturals.Definition using (ℕ ; zero ; succ; succInjective) public + open Numbers.Naturals.Addition using (_+N_) public + open Numbers.Naturals.Multiplication using (_*N_ ; multiplicationNIsCommutative) public + open Numbers.Naturals.Order using (_ n +N c) pr - addingPreservesEqualityLeft : {a b : ℕ} (c : ℕ) → (a ≡ b) → (c +N a ≡ c +N b) - addingPreservesEqualityLeft {a} {b} c pr = applyEquality (λ n -> c +N n) pr - - additionNIsAssociative : (a b c : ℕ) → ((a +N b) +N c) ≡ (a +N (b +N c)) - additionNIsAssociative zero b c = refl - additionNIsAssociative (succ a) zero c = transitivity (transitivity (applyEquality (λ n → n +N c) (applyEquality succ (addZeroRight a))) refl) (transitivity refl refl) - additionNIsAssociative (succ a) (succ b) c = transitivity refl (transitivity refl (transitivity (applyEquality succ (additionNIsAssociative a (succ b) c)) refl)) - - productZeroIsZeroLeft : (a : ℕ) → (zero *N a ≡ zero) - productZeroIsZeroLeft a = refl - - productZeroIsZeroRight : (a : ℕ) → (a *N zero ≡ zero) - productZeroIsZeroRight zero = refl - productZeroIsZeroRight (succ a) = productZeroIsZeroRight a - - productWithOneLeft : (a : ℕ) → ((succ zero) *N a) ≡ a - productWithOneLeft a = transitivity refl (transitivity (applyEquality (λ { m -> a +N m }) refl) (additionNIsCommutative a zero)) - - productWithOneRight : (a : ℕ) → a *N succ zero ≡ a - productWithOneRight zero = refl - productWithOneRight (succ a) = transitivity refl (addingPreservesEqualityLeft (succ zero) (productWithOneRight a)) - - productDistributes : (a b c : ℕ) → (a *N (b +N c)) ≡ a *N b +N a *N c - productDistributes zero b c = refl - productDistributes (succ a) b c = transitivity refl - (transitivity (addingPreservesEqualityLeft (b +N c) (productDistributes a b c)) - (transitivity (equalityCommutative (additionNIsAssociative (b +N c) (a *N b) (a *N c))) - (transitivity (addingPreservesEqualityRight (a *N c) (additionNIsCommutative (b +N c) (a *N b))) - (transitivity (addingPreservesEqualityRight (a *N c) (equalityCommutative (additionNIsAssociative (a *N b) b c))) - (transitivity (addingPreservesEqualityRight (a *N c) (addingPreservesEqualityRight c (additionNIsCommutative (a *N b) b))) - (transitivity (addingPreservesEqualityRight (a *N c) (addingPreservesEqualityRight {b +N a *N b} {(succ a) *N b} c (refl))) - (transitivity (additionNIsAssociative ((succ a) *N b) c (a *N c)) - (transitivity (addingPreservesEqualityLeft (succ a *N b) refl) - refl) - ) - )))))) - - succIsAddOne : (a : ℕ) → succ a ≡ a +N succ zero - succIsAddOne a = equalityCommutative (transitivity (additionNIsCommutative a (succ zero)) refl) - - productPreservesEqualityLeft : (a : ℕ) → {b c : ℕ} → b ≡ c → a *N b ≡ a *N c - productPreservesEqualityLeft a {b} {.b} refl = refl - - aSucB : (a b : ℕ) → a *N succ b ≡ a *N b +N a - aSucB a b = transitivity {_} {ℕ} {a *N succ b} {a *N (b +N succ zero)} (productPreservesEqualityLeft a (succIsAddOne b)) (transitivity {_} {ℕ} {a *N (b +N succ zero)} {a *N b +N a *N succ zero} (productDistributes a b (succ zero)) (addingPreservesEqualityLeft (a *N b) (productWithOneRight a))) - - aSucBRight : (a b : ℕ) → (succ a) *N b ≡ a *N b +N b - aSucBRight a b = additionNIsCommutative b (a *N b) - - multiplicationNIsCommutative : (a b : ℕ) → (a *N b) ≡ (b *N a) - multiplicationNIsCommutative zero b = transitivity (productZeroIsZeroLeft b) (equalityCommutative (productZeroIsZeroRight b)) - multiplicationNIsCommutative (succ a) zero = multiplicationNIsCommutative a zero - multiplicationNIsCommutative (succ a) (succ b) = transitivity refl - (transitivity (addingPreservesEqualityLeft (succ b) (aSucB a b)) - (transitivity (additionNIsCommutative (succ b) (a *N b +N a)) - (transitivity (additionNIsAssociative (a *N b) a (succ b)) - (transitivity (addingPreservesEqualityLeft (a *N b) (succCanMove a b)) - (transitivity (addingPreservesEqualityLeft (a *N b) (additionNIsCommutative (succ a) b)) - (transitivity (equalityCommutative (additionNIsAssociative (a *N b) b (succ a))) - (transitivity (addingPreservesEqualityRight (succ a) (equalityCommutative (aSucBRight a b))) - (transitivity (addingPreservesEqualityRight (succ a) (multiplicationNIsCommutative (succ a) b)) - (transitivity (additionNIsCommutative (b *N (succ a)) (succ a)) - refl - ))))))))) - - productDistributes' : (a b c : ℕ) → (a +N b) *N c ≡ a *N c +N b *N c - productDistributes' a b c rewrite multiplicationNIsCommutative (a +N b) c | productDistributes c a b | multiplicationNIsCommutative c a | multiplicationNIsCommutative c b = refl - - flipProductsWithinSum : (a b c : ℕ) → (c *N a +N c *N b ≡ a *N c +N b *N c) - flipProductsWithinSum a b c = transitivity (addingPreservesEqualityRight (c *N b) (multiplicationNIsCommutative c a)) ((addingPreservesEqualityLeft (a *N c) (multiplicationNIsCommutative c b))) - - productDistributesRight : (a b c : ℕ) → (a +N b) *N c ≡ a *N c +N b *N c - productDistributesRight a b c = transitivity (multiplicationNIsCommutative (a +N b) c) (transitivity (productDistributes c a b) (flipProductsWithinSum a b c)) - - multiplicationNIsAssociative : (a b c : ℕ) → (a *N (b *N c)) ≡ ((a *N b) *N c) - multiplicationNIsAssociative zero b c = refl - multiplicationNIsAssociative (succ a) b c = - transitivity refl - (transitivity refl - (transitivity (applyEquality ((λ x → b *N c +N x)) (multiplicationNIsAssociative a b c)) (transitivity (equalityCommutative (productDistributesRight b (a *N b) c)) refl))) + ℕSemiring : Semiring 0 1 _+N_ _*N_ + Monoid.associative (Semiring.monoid ℕSemiring) a b c = equalityCommutative (additionNIsAssociative a b c) + Monoid.idLeft (Semiring.monoid ℕSemiring) _ = refl + Monoid.idRight (Semiring.monoid ℕSemiring) a = additionNIsCommutative a 0 + Semiring.commutative ℕSemiring = additionNIsCommutative + Monoid.associative (Semiring.multMonoid ℕSemiring) = multiplicationNIsAssociative + Monoid.idLeft (Semiring.multMonoid ℕSemiring) a = additionNIsCommutative a 0 + Monoid.idRight (Semiring.multMonoid ℕSemiring) a = transitivity (multiplicationNIsCommutative a 1) (additionNIsCommutative a 0) + Semiring.productZeroLeft ℕSemiring _ = refl + Semiring.productZeroRight ℕSemiring a = multiplicationNIsCommutative a 0 + Semiring.+DistributesOver* ℕSemiring = productDistributes canAddZeroOnLeft : {a b : ℕ} → (a x Set a where [] : Vec X zero @@ -67,7 +69,7 @@ vecSolelyContains {m} n record { index = zero ; index