From 2ef7348d30fda98a0c2729d379f1ef2faa320cce Mon Sep 17 00:00:00 2001 From: Patrick Stevens Date: Wed, 13 Nov 2019 18:35:41 +0000 Subject: [PATCH] A bit of cleanup (#69) --- Everything/Safe.agda | 3 +++ Groups/ActionIsSymmetry.agda | 37 ++++++++++++-------------- Groups/SymmetricGroups/Definition.agda | 30 ++++++--------------- Lists/SortList.agda | 12 ++++----- LogicalFormulaeProofs.agda | 8 ------ Setoids/Functions/Definition.agda | 10 +++++++ Setoids/Functions/Extension.agda | 20 ++++++++++++++ 7 files changed, 64 insertions(+), 56 deletions(-) delete mode 100644 LogicalFormulaeProofs.agda create mode 100644 Setoids/Functions/Definition.agda create mode 100644 Setoids/Functions/Extension.agda diff --git a/Everything/Safe.agda b/Everything/Safe.agda index bdd02a3..aa80811 100644 --- a/Everything/Safe.agda +++ b/Everything/Safe.agda @@ -26,6 +26,7 @@ open import Groups.SymmetricGroups.Definition open import Groups.Actions.Stabiliser open import Groups.Actions.Orbit open import Groups.SymmetricGroups.Lemmas +open import Groups.ActionIsSymmetry open import Groups.Cyclic.Definition open import Fields.Fields @@ -46,6 +47,8 @@ open import Rings.IntegralDomains open import Setoids.Setoids open import Setoids.Lists open import Setoids.Orders +open import Setoids.Functions.Definition +open import Setoids.Functions.Extension open import Sets.Cardinality open import Sets.FinSet diff --git a/Groups/ActionIsSymmetry.agda b/Groups/ActionIsSymmetry.agda index 5bef3bb..7536230 100644 --- a/Groups/ActionIsSymmetry.agda +++ b/Groups/ActionIsSymmetry.agda @@ -8,31 +8,28 @@ open import Numbers.Naturals.Naturals open import Sets.FinSet open import Groups.Definition open import Groups.Lemmas +open import Groups.Homomorphisms.Definition open import Groups.Groups open import Groups.SymmetricGroups.Definition open import Groups.Groups2 -open import Groups.Actions +open import Groups.Actions.Definition +open import Sets.EquivalenceRelations -module Groups.ActionIsSymmetry where +module Groups.ActionIsSymmetry {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (gAction : GroupAction G T) where -actionPermutation : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} → (action : GroupAction G T) → (g : A) → SymmetryGroupElements T -actionPermutation {B = B} {T = T} {_+_ = _+_} {G = G} action g = sym {f = λ x → (GroupAction.action action g x)} (record { inj = record { injective = inj ; wellDefined = GroupAction.actionWellDefined2 action } ; surj = record { surjective = surj ; wellDefined = GroupAction.actionWellDefined2 action } }) +open Group G +open GroupAction gAction + +actionPermutation : (g : A) → SymmetryGroupElements T +actionPermutation g = sym {f = λ x → action g x} (record { inj = record { injective = inj ; wellDefined = actionWellDefined2 } ; surj = record { surjective = surj ; wellDefined = actionWellDefined2 } }) where open Setoid T - open Reflexive (Equivalence.reflexiveEq (Setoid.eq T)) - open Symmetric (Equivalence.symmetricEq (Setoid.eq T)) - open Transitive (Equivalence.transitiveEq (Setoid.eq T)) - open Group G - inj : {x y : B} → (Setoid._∼_ T (GroupAction.action action g x) (GroupAction.action action g y)) → Setoid._∼_ T x y - inj {x} {y} gx=gy = transitive (symmetric (GroupAction.identityAction action)) (transitive (transitive (symmetric (GroupAction.actionWellDefined1 action (invLeft {g}))) (transitive (transitive (GroupAction.associativeAction action) (transitive (GroupAction.actionWellDefined2 action gx=gy) (symmetric (GroupAction.associativeAction action)))) (GroupAction.actionWellDefined1 action (invLeft {g})))) (GroupAction.identityAction action)) - surj : {x : B} → Sg B (λ a → GroupAction.action action g a ∼ x) - surj {x} = GroupAction.action action (inverse g) x , transitive (symmetric (GroupAction.associativeAction action)) (transitive (GroupAction.actionWellDefined1 action invRight) (GroupAction.identityAction action)) + open Equivalence eq + inj : {x y : B} → (Setoid._∼_ T (action g x) (action g y)) → Setoid._∼_ T x y + inj {x} {y} gx=gy = transitive (symmetric identityAction) (transitive (transitive (symmetric (actionWellDefined1 (invLeft {g}))) (transitive (transitive associativeAction (transitive (actionWellDefined2 gx=gy) (symmetric associativeAction))) (actionWellDefined1 (invLeft {g})))) identityAction) + surj : {x : B} → Sg B (λ a → action g a ∼ x) + surj {x} = action (inverse g) x , transitive (symmetric associativeAction) (transitive (actionWellDefined1 invRight) identityAction) -actionPermutationMapIsHom : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) → GroupHom G (symmetricGroup T) (actionPermutation action) -GroupHom.groupHom (actionPermutationMapIsHom {T = T} action) = ExtensionallyEqual.eq λ {z} → GroupAction.associativeAction action - where - open Setoid T - open Reflexive (Equivalence.reflexiveEq (Setoid.eq T)) - open Symmetric (Equivalence.symmetricEq (Setoid.eq T)) - open Transitive (Equivalence.transitiveEq (Setoid.eq T)) -GroupHom.wellDefined (actionPermutationMapIsHom action) x=y = ExtensionallyEqual.eq λ {z} → GroupAction.actionWellDefined1 action x=y +actionPermutationMapIsHom : GroupHom G (symmetricGroup T) actionPermutation +GroupHom.groupHom actionPermutationMapIsHom = associativeAction +GroupHom.wellDefined actionPermutationMapIsHom x=y = actionWellDefined1 x=y diff --git a/Groups/SymmetricGroups/Definition.agda b/Groups/SymmetricGroups/Definition.agda index 2d784d1..18eef09 100644 --- a/Groups/SymmetricGroups/Definition.agda +++ b/Groups/SymmetricGroups/Definition.agda @@ -9,28 +9,14 @@ open import Sets.FinSet open import Groups.Groups open import Groups.Definition open import Sets.EquivalenceRelations +open import Setoids.Functions.Extension module Groups.SymmetricGroups.Definition where data SymmetryGroupElements {a b : _} {A : Set a} (S : Setoid {a} {b} A) : Set (a ⊔ b) where sym : {f : A → A} → SetoidBijection S S f → SymmetryGroupElements S - WellDefined : {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f : A → B) → Set (a ⊔ c ⊔ d) - WellDefined {A = A} S T f = {x y : A} → Setoid._∼_ S x y → Setoid._∼_ T (f x) (f y) - - data ExtensionallyEqual {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f g : A → B) (fWd : WellDefined S T f) (gWd : WellDefined S T g) : Set (a ⊔ b ⊔ c ⊔ d) where - eq : ({x : A} → Setoid._∼_ T (f x) (g x)) → ExtensionallyEqual S T f g fWd gWd - - extensionallyEqualReflexive : {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f : A → B) (fWD1 fWD2 : WellDefined S T f) → ExtensionallyEqual S T f f fWD1 fWD2 - extensionallyEqualReflexive S T f fWD1 _ = eq (Equivalence.reflexive (Setoid.eq T)) - - extensionallyEqualSymmetric : {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f g : A → B) (fWD : WellDefined S T f) (gWD : WellDefined S T g) → ExtensionallyEqual S T f g fWD gWD → ExtensionallyEqual S T g f gWD fWD - extensionallyEqualSymmetric S T f g fWD gWD (eq pr) = eq (Equivalence.symmetric (Setoid.eq T) pr) - - extensionallyEqualTransitive : {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f g h : A → B) (fWD : WellDefined S T f) (gWD : WellDefined S T g) (hWD : WellDefined S T h) → ExtensionallyEqual S T f g fWD gWD → ExtensionallyEqual S T g h gWD hWD → ExtensionallyEqual S T f h fWD hWD - extensionallyEqualTransitive S T f g h fWD gWD hWD (eq pr1) (eq pr2) = eq (Equivalence.transitive (Setoid.eq T) pr1 pr2) - symmetricSetoid : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Setoid (SymmetryGroupElements S) - Setoid._∼_ (symmetricSetoid S) (sym {f} bijF) (sym {g} bijG) = ExtensionallyEqual S S f g (SetoidBijection.wellDefined bijF) (SetoidBijection.wellDefined bijG) + Setoid._∼_ (symmetricSetoid S) (sym {f} bijF) (sym {g} bijG) = ExtensionallyEqual {S = S} {S} (SetoidBijection.wellDefined bijF) (SetoidBijection.wellDefined bijG) Equivalence.reflexive (Setoid.eq (symmetricSetoid S)) {sym {f} bijF} = extensionallyEqualReflexive S S f (SetoidBijection.wellDefined bijF) (SetoidBijection.wellDefined bijF) Equivalence.symmetric (Setoid.eq (symmetricSetoid S)) {sym {f} bijF} {sym {g} bijG} f~g = extensionallyEqualSymmetric S S f g (SetoidBijection.wellDefined bijF) (SetoidBijection.wellDefined bijG) f~g Equivalence.transitive (Setoid.eq (symmetricSetoid S)) {sym {f} bijF} {sym {g} bijG} {sym {h} bijH} f~g g~h = extensionallyEqualTransitive S S f g h (SetoidBijection.wellDefined bijF) (SetoidBijection.wellDefined bijG) (SetoidBijection.wellDefined bijH) f~g g~h @@ -43,27 +29,27 @@ module Groups.SymmetricGroups.Definition where ... | record { inverse = inverse ; inverseWellDefined = iwd ; isLeft = isLeft ; isRight = isRight } = sym (setoidInvertibleImpliesBijective (record { fWellDefined = iwd ; inverse = f ; inverseWellDefined = SetoidInjection.wellDefined (SetoidBijection.inj bijF) ; isLeft = λ b → isRight b ; isRight = λ b → isLeft b })) symmetricGroupInvIsLeft : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → {x : SymmetryGroupElements S} → Setoid._∼_ (symmetricSetoid S) (symmetricGroupOp (symmetricGroupInv S x) x) (sym setoidIdIsBijective) - symmetricGroupInvIsLeft {A = A} S {sym {f = f} fBij} = ExtensionallyEqual.eq ans + symmetricGroupInvIsLeft {A = A} S {sym {f = f} fBij} = ans where ans : {x : A} → Setoid._∼_ S (SetoidInvertible.inverse (setoidBijectiveImpliesInvertible fBij) (f x)) x ans {x} with SetoidSurjection.surjective (SetoidBijection.surj fBij) {f x} ans {x} | a , b = SetoidInjection.injective (SetoidBijection.inj fBij) b symmetricGroupInvIsRight : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → {x : SymmetryGroupElements S} → Setoid._∼_ (symmetricSetoid S) (symmetricGroupOp x (symmetricGroupInv S x)) (sym setoidIdIsBijective) - symmetricGroupInvIsRight {A = A} S {sym {f = f} fBij} = ExtensionallyEqual.eq ans + symmetricGroupInvIsRight {A = A} S {sym {f = f} fBij} = ans where ans : {x : A} → Setoid._∼_ S (f (SetoidInvertible.inverse (setoidBijectiveImpliesInvertible fBij) x)) x ans {x} with SetoidSurjection.surjective (SetoidBijection.surj fBij) {x} ans {x} | a , b = b symmetricGroup : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Group (symmetricSetoid S) (symmetricGroupOp {A = A}) - Group.+WellDefined (symmetricGroup A) {sym {m} bijM} {sym {n} bijN} {sym {x} bijX} {sym {y} bijY} (ExtensionallyEqual.eq m~x) (ExtensionallyEqual.eq n~y) = ExtensionallyEqual.eq (transitive m~x (SetoidBijection.wellDefined bijX n~y)) + Group.+WellDefined (symmetricGroup A) {sym {m} bijM} {sym {n} bijN} {sym {x} bijX} {sym {y} bijY} m~x n~y = transitive m~x (SetoidBijection.wellDefined bijX n~y) where open Equivalence (Setoid.eq A) Group.0G (symmetricGroup A) = sym setoidIdIsBijective Group.inverse (symmetricGroup S) = symmetricGroupInv S - Group.+Associative (symmetricGroup A) {sym {f} bijF} {sym {g} bijG} {sym {h} bijH} = ExtensionallyEqual.eq λ {x} → Equivalence.reflexive (Setoid.eq A) - Group.identRight (symmetricGroup A) {sym {f} bijF} = ExtensionallyEqual.eq λ {x} → Equivalence.reflexive (Setoid.eq A) - Group.identLeft (symmetricGroup A) {sym {f} bijF} = ExtensionallyEqual.eq λ {x} → Equivalence.reflexive (Setoid.eq A) + Group.+Associative (symmetricGroup A) {sym {f} bijF} {sym {g} bijG} {sym {h} bijH} = Equivalence.reflexive (Setoid.eq A) + Group.identRight (symmetricGroup A) {sym {f} bijF} = Equivalence.reflexive (Setoid.eq A) + Group.identLeft (symmetricGroup A) {sym {f} bijF} = Equivalence.reflexive (Setoid.eq A) Group.invLeft (symmetricGroup S) {x} = symmetricGroupInvIsLeft S {x} Group.invRight (symmetricGroup S) {x} = symmetricGroupInvIsRight S {x} diff --git a/Lists/SortList.agda b/Lists/SortList.agda index 2e90fa9..750cf30 100644 --- a/Lists/SortList.agda +++ b/Lists/SortList.agda @@ -1,7 +1,7 @@ -{-# OPTIONS --safe --warning=error #-} +{-# 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 Orders open import Functions @@ -98,7 +98,7 @@ module Lists.SortList where lexIrrefl : {a b : _} {A : Set a} (o : TotalOrder {a} {b} A) → {x : List A} → lexicographicOrderRel o x x → False lexIrrefl o {[]} () lexIrrefl o {x :: l} (inl x