patrick/agdaproofs
1
0
Fork 0
mirror of https://github.com/Smaug123/agdaproofs synced 2025-10-18 01:38:45 +00:00
Code Issues Packages Projects Releases Wiki Activity

Free-group lemmas (#106)

Browse Source
This commit is contained in:
Patrick Stevens
2020-04-05 11:09:12 +01:00
committed by GitHub
parent 61b5f8acc5
commit 2f07a8e972
18 changed files with 327 additions and 188 deletions
Download Patch File Download Diff File Expand all files Collapse all files

15
Groups/FreeGroup/Definition.agda
View File

@@ -17,6 +17,10 @@ data FreeCompletion {a : _} (A : Set a) : Set a where
ofLetter : A → FreeCompletion A
ofInv : A → FreeCompletion A
freeCompletionMap : {a b : _} {A : Set a} {B : Set b} (f : A → B) (w : FreeCompletion A) → FreeCompletion B
freeCompletionMap f (ofLetter x) = ofLetter (f x)
freeCompletionMap f (ofInv x) = ofInv (f x)
freeInverse : {a : _} {A : Set a} (l : FreeCompletion A) → FreeCompletion A
freeInverse (ofLetter x) = ofInv x
freeInverse (ofInv x) = ofLetter x
@@ -27,8 +31,11 @@ ofLetterInjective refl = refl
ofInvInjective : {a : _} {A : Set a} {x y : A} → (ofInv x ≡ ofInv y) → x ≡ y
ofInvInjective refl = refl
ofLetterOfInv : {a : _} {A : Set a} {x y : A} → ofLetter x ≡ ofInv y → False
ofLetterOfInv ()
decidableFreeCompletion : {a : _} {A : Set a} → DecidableSet A → DecidableSet (FreeCompletion A)
decidableFreeCompletion {A = A} record { eq = dec } = record { eq = pr }
decidableFreeCompletion {A = A} dec = pr
where
pr : (a b : FreeCompletion A) → (a ≡ b) || (a ≡ b → False)
pr (ofLetter x) (ofLetter y) with dec x y
@@ -41,17 +48,17 @@ decidableFreeCompletion {A = A} record { eq = dec } = record { eq = pr }
... | inr x!=y = inr λ p → x!=y (ofInvInjective p)
freeCompletionEqual : {a : _} {A : Set a} (dec : DecidableSet A) (x y : FreeCompletion A) → Bool
freeCompletionEqual dec x y with DecidableSet.eq (decidableFreeCompletion dec) x y
freeCompletionEqual dec x y with decidableFreeCompletion dec x y
freeCompletionEqual dec x y | inl x₁ = BoolTrue
freeCompletionEqual dec x y | inr x₁ = BoolFalse
freeCompletionEqualFalse : {a : _} {A : Set a} (dec : DecidableSet A) {x y : FreeCompletion A} → ((x ≡ y) → False) → (freeCompletionEqual dec x y) ≡ BoolFalse
freeCompletionEqualFalse dec {x = x} {y} x!=y with DecidableSet.eq (decidableFreeCompletion dec) x y
freeCompletionEqualFalse dec {x = x} {y} x!=y with decidableFreeCompletion dec x y
freeCompletionEqualFalse dec {x} {y} x!=y | inl x=y = exFalso (x!=y x=y)
freeCompletionEqualFalse dec {x} {y} x!=y | inr _ = refl
freeCompletionEqualFalse' : {a : _} {A : Set a} (dec : DecidableSet A) {x y : FreeCompletion A} → .((freeCompletionEqual dec x y) ≡ BoolFalse) → (x ≡ y) → False
freeCompletionEqualFalse' dec {x} {y} pr with DecidableSet.eq (decidableFreeCompletion dec) x y
freeCompletionEqualFalse' dec {x} {y} pr with decidableFreeCompletion dec x y
freeCompletionEqualFalse' dec {x} {y} () | inl x₁
freeCompletionEqualFalse' dec {x} {y} pr | inr ans = ans

36
Groups/FreeGroup/Group.agda
View File

@@ -15,10 +15,10 @@ open import Groups.FreeGroup.Word decA
prepend : ReducedWord → FreeCompletion A → ReducedWord
prepend empty x = prependLetter x empty (wordEmpty refl)
prepend (prependLetter (ofLetter y) w pr) (ofLetter x) = prependLetter (ofLetter x) (prependLetter (ofLetter y) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA {ofLetter x} {ofInv x} λ ()))
prepend (prependLetter (ofInv y) w pr) (ofLetter x) with DecidableSet.eq decA x y
prepend (prependLetter (ofInv y) w pr) (ofLetter x) with decA x y
... | inl x=y = w
... | inr x!=y = prependLetter (ofLetter x) (prependLetter (ofInv y) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA {ofLetter x} {ofLetter y} λ pr → x!=y (ofLetterInjective pr)))
prepend (prependLetter (ofLetter y) w pr) (ofInv x) with DecidableSet.eq decA x y
prepend (prependLetter (ofLetter y) w pr) (ofInv x) with decA x y
... | inl x=y = w
... | inr x!=y = prependLetter (ofInv x) (prependLetter (ofLetter y) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA λ pr → x!=y (ofInvInjective pr)))
prepend (prependLetter (ofInv y) w pr) (ofInv x) = prependLetter (ofInv x) (prependLetter (ofInv y) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA {ofInv x} {ofLetter x} (λ ())))
@@ -30,50 +30,50 @@ prependLetter letter a x +W b = prepend (a +W b) letter
prependValid : (w : ReducedWord) (l : A) → (x : PrependIsValid w (ofLetter l)) → prepend w (ofLetter l) ≡ prependLetter (ofLetter l) w x
prependValid empty l (wordEmpty refl) = refl
prependValid (prependLetter (ofLetter l2) w x) l pr = prependLetterRefl
prependValid (prependLetter (ofInv l2) w x) l pr with DecidableSet.eq decA l l2
prependValid (prependLetter (ofInv l2) w x) l pr with decA l l2
prependValid (prependLetter (ofInv l2) w x) .l2 (wordEnding _ x1) | inl refl = exFalso (freeCompletionEqualFalse' decA x1 refl)
... | inr l!=l2 = prependLetterRefl
prependValid' : (w : ReducedWord) (l : A) → (x : PrependIsValid w (ofInv l)) → prepend w (ofInv l) ≡ prependLetter (ofInv l) w x
prependValid' empty l (wordEmpty refl) = refl
prependValid' (prependLetter (ofLetter l2) w x) l pr with DecidableSet.eq decA l l2
prependValid' (prependLetter (ofLetter l2) w x) l pr with decA l l2
prependValid' (prependLetter (ofLetter l2) w x) .l2 (wordEnding _ x1) | inl refl = exFalso (freeCompletionEqualFalse' decA x1 refl)
... | inr l!=l2 = prependLetterRefl
prependValid' (prependLetter (ofInv l2) w x) l pr = prependLetterRefl
prependInv : (w : ReducedWord) (l : A) → prepend (prepend w (ofLetter l)) (ofInv l) ≡ w
prependInv empty l with DecidableSet.eq decA l l
prependInv empty l with decA l l
... | inl l=l = refl
... | inr l!=l = exFalso (l!=l refl)
prependInv (prependLetter (ofLetter l2) w x) l with DecidableSet.eq decA l l
prependInv (prependLetter (ofLetter l2) w x) l with decA l l
... | inl l=l = refl
... | inr l!=l = exFalso (l!=l refl)
prependInv (prependLetter (ofInv l2) w x) l with DecidableSet.eq decA l l2
prependInv (prependLetter (ofInv l2) w x) l with decA l l2
prependInv (prependLetter (ofInv l2) w x) .l2 | inl refl = prependValid' w l2 x
... | inr l!=l2 with DecidableSet.eq decA l l
... | inr l!=l2 with decA l l
prependInv (prependLetter (ofInv l2) w x) l | inr l!=l2 | inl refl = refl
prependInv (prependLetter (ofInv l2) w x) l | inr l!=l2 | inr bad = exFalso (bad refl)
prependInv' : (w : ReducedWord) (l : A) → prepend (prepend w (ofInv l)) (ofLetter l) ≡ w
prependInv' empty l with DecidableSet.eq decA l l
prependInv' empty l with decA l l
... | inl l=l = refl
... | inr l!=l = exFalso (l!=l refl)
prependInv' (prependLetter (ofLetter l2) w x) l with DecidableSet.eq decA l l2
prependInv' (prependLetter (ofLetter l2) w x) l with decA l l2
prependInv' (prependLetter (ofLetter l2) w x) .l2 | inl refl = prependValid w l2 x
... | inr l!=l2 with DecidableSet.eq decA l l
... | inr l!=l2 with decA l l
... | inl refl = refl
... | inr l!=l = exFalso (l!=l refl)
prependInv' (prependLetter (ofInv l2) w x) l with DecidableSet.eq decA l l
prependInv' (prependLetter (ofInv l2) w x) l with decA l l
prependInv' (prependLetter (ofInv l2) w x) l | inl refl = refl
prependInv' (prependLetter (ofInv l2) w x) l | inr l!=l = exFalso (l!=l refl)
prependAndAdd : (a b : ReducedWord) (l : FreeCompletion A) → prepend (a +W b) l ≡ (prepend a l) +W b
prependAndAdd empty b l = refl
prependAndAdd (prependLetter (ofLetter x) w pr) b (ofLetter y) = refl
prependAndAdd (prependLetter (ofLetter x) w pr) b (ofInv y) with DecidableSet.eq decA y x
prependAndAdd (prependLetter (ofLetter x) w pr) b (ofInv y) with decA y x
prependAndAdd (prependLetter (ofLetter x) w pr) b (ofInv .x) | inl refl = prependInv _ _
... | inr y!=x = refl
prependAndAdd (prependLetter (ofInv x) w pr) b (ofLetter y) with DecidableSet.eq decA y x
prependAndAdd (prependLetter (ofInv x) w pr) b (ofLetter y) with decA y x
prependAndAdd (prependLetter (ofInv x) w pr) b (ofLetter .x) | inl refl = prependInv' _ _
... | inr y!=x = refl
prependAndAdd (prependLetter (ofInv x) w pr) b (ofInv y) = refl
@@ -96,13 +96,13 @@ invLeftW empty = refl
invLeftW (prependLetter (ofLetter l) a x) rewrite equalityCommutative (+WAssoc (inverseW a) (prependLetter (ofInv l) empty (wordEmpty refl)) (prependLetter (ofLetter l) a x)) = t
where
t : (inverseW a +W (prepend (prependLetter (ofLetter l) a x) (ofInv l))) ≡ empty
t with DecidableSet.eq decA l l
t with decA l l
... | inl refl = invLeftW a
... | inr l!=l = exFalso (l!=l refl)
invLeftW (prependLetter (ofInv l) a x) rewrite equalityCommutative (+WAssoc (inverseW a) (prependLetter (ofLetter l) empty (wordEmpty refl)) (prependLetter (ofInv l) a x)) = t
where
t : (inverseW a +W (prepend (prependLetter (ofInv l) a x) (ofLetter l))) ≡ empty
t with DecidableSet.eq decA l l
t with decA l l
... | inl refl = invLeftW a
... | inr l!=l = exFalso (l!=l refl)
@@ -111,13 +111,13 @@ invRightW empty = refl
invRightW (prependLetter (ofLetter l) a x) rewrite +WAssoc a (inverseW a) (prependLetter (ofInv l) empty (wordEmpty refl)) | invRightW a = t
where
t : prepend (prependLetter (ofInv l) empty (wordEmpty refl)) (ofLetter l) ≡ empty
t with DecidableSet.eq decA l l
t with decA l l
... | inl refl = refl
... | inr l!=l = exFalso (l!=l refl)
invRightW (prependLetter (ofInv l) a x) rewrite +WAssoc a (inverseW a) (prependLetter (ofLetter l) empty (wordEmpty refl)) | invRightW a = t
where
t : prepend (prependLetter (ofLetter l) empty (wordEmpty refl)) (ofInv l) ≡ empty
t with DecidableSet.eq decA l l
t with decA l l
... | inl refl = refl
... | inr l!=l = exFalso (l!=l refl)

112
Groups/FreeGroup/Lemmas.agda
View File

@@ -1,11 +1,13 @@
{-# OPTIONS --safe --warning=error #-}
open import Sets.Cardinality.Infinite.Definition
open import Sets.EquivalenceRelations
open import Setoids.Setoids
open import Groups.FreeGroup.Definition
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Decidable.Sets
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import LogicalFormulae
open import Semirings.Definition
@@ -14,18 +16,116 @@ open import Groups.Isomorphisms.Definition
open import Groups.FreeGroup.Word
open import Groups.FreeGroup.Group
open import Groups.FreeGroup.UniversalProperty
open import Groups.Abelian.Definition
open import Groups.QuotientGroup.Definition
open import Groups.Lemmas
open import Groups.Homomorphisms.Lemmas
module Groups.FreeGroup.Lemmas {a : _} {A : Set a} (decA : DecidableSet A) where
freeGroupFunctorWellDefined : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → Bijection f → GroupsIsomorphic (freeGroup decA) (freeGroup decB)
GroupsIsomorphic.isomorphism (freeGroupFunctorWellDefined decB {f} bij) = universalPropertyFunction decA (freeGroup decB) λ a → freeEmbedding decB (f a)
GroupIso.groupHom (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)) = universalPropertyHom decA (freeGroup decB) λ a → freeEmbedding decB (f a)
GroupIso.bij (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)) = {!!}
freeGroupNonAbelian : AbelianGroup (freeGroup decA) → (a : A) → Sg (A → True) Bijection
freeGroupNonAbelian record { commutative = commutative } a = (λ _ → record {}) , b
where
b : Bijection (λ _ → record {})
Bijection.inj b {x} {y} _ with decA x y
... | inl pr = pr
... | inr neq = exFalso (neq (ofLetterInjective (prependLetterInjective' decA t)))
where
t : prependLetter {decA = decA} (ofLetter x) (prependLetter (ofLetter y) empty (wordEmpty refl)) (wordEnding (succIsPositive 0) refl) ≡ prependLetter (ofLetter y) (prependLetter (ofLetter x) empty (wordEmpty refl)) (wordEnding (succIsPositive 0) refl)
t = commutative {prependLetter (ofLetter x) empty (wordEmpty refl)} {prependLetter (ofLetter y) empty (wordEmpty refl)}
Bijection.surj b record {} = a , refl
private
subgroupGeneratedBySquares : {c d : _} {C : Set c} {S : Setoid {c} {d} C} {_+_ : C → C → C} (G : Group S _+_) → Set
sub
iso : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → Bijection f → ReducedWord decA → ReducedWord decB
iso decB {f} bij = universalPropertyFunction decA (freeGroup decB) λ a → freeEmbedding decB (f a)
isoHom : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → GroupHom (freeGroup decA) (freeGroup decB) (iso decB bij)
isoHom decB {f} bij = universalPropertyHom decA (freeGroup decB) λ a → iso decB bij (freeEmbedding decA a)
iso2 : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → Bijection f → ReducedWord decB → ReducedWord decA
iso2 decB {f} bij = universalPropertyFunction decB (freeGroup decA) λ b → freeEmbedding decA (Invertible.inverse (bijectionImpliesInvertible bij) b)
iso2Hom : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → GroupHom (freeGroup decB) (freeGroup decA) (iso2 decB bij)
iso2Hom decB {f} bij = universalPropertyHom decB (freeGroup decA) λ b → iso2 decB bij (freeEmbedding decB b)
fixesF : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : A) → iso2 decB bij (iso decB bij (freeEmbedding decA x)) ≡ freeEmbedding decA x
fixesF decB {f} bij x with Bijection.surj bij (f x)
... | _ , pr rewrite Bijection.inj bij pr = refl
fixesF' : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : B) → iso decB bij (iso2 decB bij (freeEmbedding decB x)) ≡ freeEmbedding decB x
fixesF' decB {f} bij x with Bijection.surj bij x
... | _ , pr rewrite pr = refl
uniq : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decA) → x ≡ universalPropertyFunction decA (freeGroup decA) (λ x → iso2 decB bij (iso decB bij (freeEmbedding decA x))) x
uniq decB {f} bij x = universalPropertyUniqueness decA (freeGroup decA) (λ x → iso2 decB bij (iso decB bij (freeEmbedding decA x))) {id} (record { wellDefined = id ; groupHom = refl }) (fixesF decB bij) x
uniqLemm : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decA) → iso2 decB bij (iso decB bij x) ≡ universalPropertyFunction decA (freeGroup decA) (λ x → iso2 decB bij (iso decB bij (freeEmbedding decA x))) x
uniqLemm decB {f} bij x = universalPropertyUniqueness decA (freeGroup decA) (λ i → freeEmbedding decA (underlying (Bijection.surj bij (f i)))) {λ i → iso2 decB bij (iso decB bij i)} (groupHomsCompose (isoHom decB bij) (iso2Hom decB bij)) (λ _ → refl) x
uniq! : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decA) → iso2 decB bij (iso decB bij x) ≡ x
uniq! decB bij x = transitivity (uniqLemm decB bij x) (equalityCommutative (uniq decB bij x))
uniq' : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decB) → x ≡ universalPropertyFunction decB (freeGroup decB) (λ x → iso decB bij (iso2 decB bij (freeEmbedding decB x))) x
uniq' decB {f} bij x = universalPropertyUniqueness decB (freeGroup decB) (λ x → iso decB bij (iso2 decB bij (freeEmbedding decB x))) {id} (record { wellDefined = id ; groupHom = refl }) (fixesF' decB bij) x
uniq'Lemm : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decB) → iso decB bij (iso2 decB bij x) ≡ universalPropertyFunction decB (freeGroup decB) (λ x → iso decB bij (iso2 decB bij (freeEmbedding decB x))) x
uniq'Lemm decB {f} bij x = universalPropertyUniqueness decB (freeGroup decB) (λ i → freeEmbedding decB (f (Invertible.inverse (bijectionImpliesInvertible bij) i))) {λ i → iso decB bij (iso2 decB bij i)} (groupHomsCompose (iso2Hom decB bij) (isoHom decB bij)) (λ _ → refl) x
uniq'! : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decB) → iso decB bij (iso2 decB bij x) ≡ x
uniq'! decB bij x = transitivity (uniq'Lemm decB bij x) (equalityCommutative (uniq' decB bij x))
inBijection : {b : _} {B : Set b} (decB : DecidableSet B) {f : A → B} (bij : Bijection f) → Bijection (iso decB bij)
inBijection decB bij = invertibleImpliesBijection (record { inverse = iso2 decB bij ; isLeft = uniq'! decB bij ; isRight = uniq! decB bij })
freeGroupFunctorWellDefined : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → Bijection f → GroupsIsomorphic (freeGroup decA) (freeGroup decB)
GroupsIsomorphic.isomorphism (freeGroupFunctorWellDefined decB {f} bij) = iso decB bij
GroupIso.groupHom (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)) = universalPropertyHom decA (freeGroup decB) λ a → freeEmbedding decB (f a)
SetoidInjection.wellDefined (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)))) refl = refl
SetoidInjection.injective (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)))) {x} {y} pr = Bijection.inj (inBijection decB bij) pr
SetoidSurjection.wellDefined (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)))) refl = refl
SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)))) {x} = Bijection.surj (inBijection decB bij) x
{-
freeGroupFunctorInjective : {b : _} {B : Set b} (decB : DecidableSet B) → GroupsIsomorphic (freeGroup decA) (freeGroup decB) → Sg (A → B) (λ f → Bijection f)
freeGroupFunctorInjective decB iso = {!!}
everyGroupQuotientOfFreeGroup : {b : _} → (S : Setoid {a} {b} A) → {_+_ : A → A → A} → (G : Group S _+_) → GroupsIsomorphic G (quotientGroupByHom (freeGroup decA) (universalPropertyHom decA {!!} {!!}))
everyGroupQuotientOfFreeGroup = {!!}
everyFGGroupQuotientOfFGFreeGroup : {!!}
everyFGGroupQuotientOfFGFreeGroup = {!!}
freeGroupTorsionFree : {!!}
freeGroupTorsionFree = {!!}
-}
private
mapNToGrp : (a : A) → (n : ℕ) → ReducedWord decA
mapNToGrpLen : (a : A) → (n : ℕ) → wordLength decA (mapNToGrp a n) ≡ n
mapNToGrpFirstLetter : (a : A) → (n : ℕ) → .(pr : 0 <N wordLength decA (mapNToGrp a (succ n))) → firstLetter decA (mapNToGrp a (succ n)) pr ≡ (ofLetter a)
lemma : (a : A) → (n : ℕ) → .(pr : 0 <N wordLength decA (mapNToGrp a (succ n))) → ofLetter a ≡ freeInverse (firstLetter decA (mapNToGrp a (succ n)) pr) → False
lemma a zero _ ()
lemma a (succ n) _ ()
mapNToGrp a zero = empty
mapNToGrp a 1 = prependLetter (ofLetter a) empty (wordEmpty refl)
mapNToGrp a (succ (succ n)) = prependLetter (ofLetter a) (mapNToGrp a (succ n)) (wordEnding (identityOfIndiscernablesRight _<N_ (succIsPositive n) (equalityCommutative (mapNToGrpLen a (succ n)))) (freeCompletionEqualFalse decA λ p → lemma a n ((identityOfIndiscernablesRight _<N_ (succIsPositive n) (equalityCommutative (mapNToGrpLen a (succ n))))) p))
mapNToGrpFirstLetter a zero pr = refl
mapNToGrpFirstLetter a (succ n) pr = refl
mapNToGrpLen a zero = refl
mapNToGrpLen a (succ zero) = refl
mapNToGrpLen a (succ (succ n)) = applyEquality succ (mapNToGrpLen a (succ n))
mapNToGrpInj : (a : A) → (x y : ℕ) → mapNToGrp a x ≡ mapNToGrp a y → x ≡ y
mapNToGrpInj a zero zero pr = refl
mapNToGrpInj a zero (succ zero) ()
mapNToGrpInj a zero (succ (succ y)) ()
mapNToGrpInj a (succ zero) zero ()
mapNToGrpInj a (succ (succ x)) zero ()
mapNToGrpInj a (succ zero) (succ zero) pr = refl
mapNToGrpInj a (succ zero) (succ (succ y)) pr = exFalso (naughtE (transitivity (applyEquality (wordLength decA) (prependLetterInjective decA pr)) (mapNToGrpLen a (succ y))))
mapNToGrpInj a (succ (succ x)) (succ 0) pr = exFalso (naughtE (transitivity (equalityCommutative (applyEquality (wordLength decA) (prependLetterInjective decA pr))) (mapNToGrpLen a (succ x))))
mapNToGrpInj a (succ (succ x)) (succ (succ y)) pr = applyEquality succ (mapNToGrpInj a (succ x) (succ y) (prependLetterInjective decA pr))
freeGroupInfinite : (nonempty : A) → DedekindInfiniteSet (ReducedWord decA)
DedekindInfiniteSet.inj (freeGroupInfinite nonempty) = mapNToGrp nonempty
DedekindInfiniteSet.isInjection (freeGroupInfinite nonempty) {x} {y} = mapNToGrpInj nonempty x y

76
Groups/FreeGroup/Parity.agda
View File

@@ -48,97 +48,97 @@ notWellDefined {BoolFalse} {BoolFalse} x=y = refl
parity : (x : A) → ReducedWord → Bool
parity x empty = BoolFalse
parity x (prependLetter (ofLetter y) w _) with DecidableSet.eq decA x y
parity x (prependLetter (ofLetter y) w _) with decA x y
parity x (prependLetter (ofLetter y) w _) | inl _ = not (parity x w)
parity x (prependLetter (ofLetter y) w _) | inr _ = parity x w
parity x (prependLetter (ofInv y) w _) with DecidableSet.eq decA x y
parity x (prependLetter (ofInv y) w _) with decA x y
parity x (prependLetter (ofInv y) w _) | inl _ = not (parity x w)
parity x (prependLetter (ofInv y) w _) | inr _ = parity x w
parityPrepend : (a : A) (w : ReducedWord) (l : A) → ((a ≡ l) → False) → parity a (prepend w (ofLetter l)) ≡ parity a w
parityPrepend a empty l notEq with DecidableSet.eq decA a l
parityPrepend a empty l notEq with decA a l
parityPrepend a empty l notEq | inl x = exFalso (notEq x)
parityPrepend a empty l notEq | inr x = refl
parityPrepend a (prependLetter (ofLetter r) w x) l notEq with DecidableSet.eq decA a l
parityPrepend a (prependLetter (ofLetter r) w x) l notEq with decA a l
parityPrepend a (prependLetter (ofLetter r) w x) l notEq | inl m = exFalso (notEq m)
parityPrepend a (prependLetter (ofLetter r) w x) l notEq | inr _ = refl
parityPrepend a (prependLetter (ofInv r) w x) l notEq with DecidableSet.eq decA a r
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r with DecidableSet.eq decA l r
parityPrepend a (prependLetter (ofInv r) w x) l notEq with decA a r
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r with decA l r
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inl l=r = exFalso (notEq (transitivity a=r (equalityCommutative l=r)))
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r with DecidableSet.eq decA a l
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r with decA a l
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inl a=l = exFalso (notEq a=l)
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l with DecidableSet.eq decA a r
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l with decA a r
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l | inl x₁ = refl
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l | inr bad = exFalso (bad a=r)
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r with DecidableSet.eq decA l r
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r with decA l r
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl x₁ = refl
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r with DecidableSet.eq decA a l
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r with decA a l
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inl a=l = exFalso (notEq a=l)
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l with DecidableSet.eq decA a r
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l with decA a r
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l | inl a=r = exFalso (a!=r a=r)
parityPrepend a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l | inr x₁ = refl
parityPrepend' : (a : A) (w : ReducedWord) (l : A) → ((a ≡ l) → False) → parity a (prepend w (ofInv l)) ≡ parity a w
parityPrepend' a empty l notEq with DecidableSet.eq decA a l
parityPrepend' a empty l notEq with decA a l
parityPrepend' a empty l notEq | inl x = exFalso (notEq x)
parityPrepend' a empty l notEq | inr x = refl
parityPrepend' a (prependLetter (ofLetter r) w x) l notEq with DecidableSet.eq decA l r
parityPrepend' a (prependLetter (ofLetter r) w x) l notEq | inl m with DecidableSet.eq decA a r
parityPrepend' a (prependLetter (ofLetter r) w x) l notEq with decA l r
parityPrepend' a (prependLetter (ofLetter r) w x) l notEq | inl m with decA a r
... | inl a=r = exFalso (notEq (transitivity a=r (equalityCommutative m)))
... | inr a!=r = refl
parityPrepend' a (prependLetter (ofLetter r) w x) l notEq | inr l!=r with DecidableSet.eq decA a l
parityPrepend' a (prependLetter (ofLetter r) w x) l notEq | inr l!=r with decA a l
... | inl a=l = exFalso (notEq a=l)
... | inr a!=l = refl
parityPrepend' a (prependLetter (ofInv r) w x) l notEq with DecidableSet.eq decA a r
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r with DecidableSet.eq decA l r
parityPrepend' a (prependLetter (ofInv r) w x) l notEq with decA a r
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r with decA l r
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inl l=r = exFalso (notEq (transitivity a=r (equalityCommutative l=r)))
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r with DecidableSet.eq decA a l
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r with decA a l
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inl a=l = exFalso (notEq a=l)
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l with DecidableSet.eq decA a r
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l with decA a r
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l | inl x₁ = refl
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inl a=r | inr l!=r | inr a!=l | inr bad = exFalso (bad a=r)
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r with DecidableSet.eq decA l r
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl l=r with DecidableSet.eq decA a l
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r with decA l r
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl l=r with decA a l
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl l=r | inl a=l = exFalso (notEq a=l)
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl l=r | inr a!=l with DecidableSet.eq decA a r
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inl l=r | inr a!=l with decA a r
... | inl a=r = exFalso (a!=r a=r)
... | inr _ = refl
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r with DecidableSet.eq decA a l
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r with decA a l
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inl a=l = exFalso (notEq a=l)
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l with DecidableSet.eq decA a r
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l with decA a r
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l | inl a=r = exFalso (a!=r a=r)
parityPrepend' a (prependLetter (ofInv r) w x) l notEq | inr a!=r | inr l!=r | inr a!=l | inr x₁ = refl
parityPrepend'' : (a : A) (w : ReducedWord) → parity a (prepend w (ofLetter a)) ≡ not (parity a w)
parityPrepend'' a empty with DecidableSet.eq decA a a
parityPrepend'' a empty with decA a a
... | inl _ = refl
... | inr bad = exFalso (bad refl)
parityPrepend'' a (prependLetter (ofLetter l) w x) with DecidableSet.eq decA a a
parityPrepend'' a (prependLetter (ofLetter l) w x) | inl _ with DecidableSet.eq decA a l
parityPrepend'' a (prependLetter (ofLetter l) w x) with decA a a
parityPrepend'' a (prependLetter (ofLetter l) w x) | inl _ with decA a l
parityPrepend'' a (prependLetter (ofLetter l) w x) | inl _ | inl a=l = refl
parityPrepend'' a (prependLetter (ofLetter l) w x) | inl _ | inr a!=l = refl
parityPrepend'' a (prependLetter (ofLetter l) w x) | inr bad = exFalso (bad refl)
parityPrepend'' a (prependLetter (ofInv l) w x) with DecidableSet.eq decA a l
parityPrepend'' a (prependLetter (ofInv l) w x) with decA a l
... | inl a=l = equalityCommutative (notNot (parity a w))
parityPrepend'' a (prependLetter (ofInv l) w x) | inr a!=l with DecidableSet.eq decA a a
parityPrepend'' a (prependLetter (ofInv l) w x) | inr a!=l | inl _ with DecidableSet.eq decA a l
parityPrepend'' a (prependLetter (ofInv l) w x) | inr a!=l with decA a a
parityPrepend'' a (prependLetter (ofInv l) w x) | inr a!=l | inl _ with decA a l
... | inl a=l = exFalso (a!=l a=l)
... | inr _ = refl
parityPrepend'' a (prependLetter (ofInv l) w x) | inr a!=l | inr bad = exFalso (bad refl)
parityPrepend''' : (a : A) (w : ReducedWord) → parity a (prepend w (ofInv a)) ≡ not (parity a w)
parityPrepend''' a empty with DecidableSet.eq decA a a
parityPrepend''' a empty with decA a a
... | inl _ = refl
... | inr bad = exFalso (bad refl)
parityPrepend''' a (prependLetter (ofLetter l) w x) with DecidableSet.eq decA a l
parityPrepend''' a (prependLetter (ofLetter l) w x) with decA a l
... | inl a=l = equalityCommutative (notNot _)
parityPrepend''' a (prependLetter (ofLetter l) w x) | inr a!=l with DecidableSet.eq decA a a
... | inl _ with DecidableSet.eq decA a l
parityPrepend''' a (prependLetter (ofLetter l) w x) | inr a!=l with decA a a
... | inl _ with decA a l
parityPrepend''' a (prependLetter (ofLetter l) w x) | inr a!=l | inl _ | inl a=l = exFalso (a!=l a=l)
parityPrepend''' a (prependLetter (ofLetter l) w x) | inr a!=l | inl _ | inr _ = refl
parityPrepend''' a (prependLetter (ofLetter l) w x) | inr a!=l | inr bad = exFalso (bad refl)
parityPrepend''' a (prependLetter (ofInv l) w x) with DecidableSet.eq decA a a
parityPrepend''' a (prependLetter (ofInv l) w x) | inl _ with DecidableSet.eq decA a l
parityPrepend''' a (prependLetter (ofInv l) w x) with decA a a
parityPrepend''' a (prependLetter (ofInv l) w x) | inl _ with decA a l
... | inl a=l = refl
... | inr a!=l = refl
parityPrepend''' a (prependLetter (ofInv l) w x) | inr bad = exFalso (bad refl)
@@ -151,10 +151,10 @@ notXor BoolFalse BoolFalse = refl
parityHomIsHom : (a : A) → (x y : ReducedWord) → parity a (_+W_ x y) ≡ xor (parity a x) (parity a y)
parityHomIsHom a empty y = refl
parityHomIsHom a (prependLetter (ofLetter l) x _) y with DecidableSet.eq decA a l
parityHomIsHom a (prependLetter (ofLetter l) x _) y with decA a l
parityHomIsHom a (prependLetter (ofLetter .a) x _) y | inl refl = transitivity (parityPrepend'' a (x +W y)) (transitivity (notWellDefined (parityHomIsHom a x y)) (notXor (parity a x) (parity a y)))
parityHomIsHom a (prependLetter (ofLetter l) x _) y | inr a!=l = transitivity (parityPrepend a (_+W_ x y) l a!=l) (parityHomIsHom a x y)
parityHomIsHom a (prependLetter (ofInv l) x _) y with DecidableSet.eq decA a l
parityHomIsHom a (prependLetter (ofInv l) x _) y with decA a l
parityHomIsHom a (prependLetter (ofInv .a) x _) y | inl refl = transitivity (parityPrepend''' a (x +W y)) (transitivity (notWellDefined (parityHomIsHom a x y)) (notXor (parity a x) (parity a y)))
parityHomIsHom a (prependLetter (ofInv l) x _) y | inr a!=l = transitivity (parityPrepend' a (x +W y) l a!=l) (parityHomIsHom a x y)

4
Groups/FreeGroup/UniversalProperty.agda
View File

@@ -32,7 +32,7 @@ private
where
open Setoid S
open Equivalence eq
prepLemma {S = S} G f (prependLetter (ofInv x) w pr) l with DecidableSet.eq decA l x
prepLemma {S = S} G f (prependLetter (ofInv x) w pr) l with decA l x
... | inl refl = transitive (symmetric identLeft) (transitive (+WellDefined (symmetric invRight) reflexive) (symmetric +Associative))
where
open Group G
@@ -48,7 +48,7 @@ private
where
open Setoid S
open Equivalence eq
prepLemma' {S = S} G f (prependLetter (ofLetter x) w pr) l with DecidableSet.eq decA l x
prepLemma' {S = S} G f (prependLetter (ofLetter x) w pr) l with decA l x
... | inl refl = symmetric (transitive +Associative (transitive (+WellDefined invLeft reflexive) identLeft))
where
open Group G

117
Groups/FreeGroup/Word.agda
View File

@@ -45,125 +45,12 @@ prependLetterInjective' refl = refl
badPrepend : {x : A} {w : ReducedWord} {pr : PrependIsValid w (ofInv x)} → (PrependIsValid (prependLetter (ofInv x) w pr) (ofLetter x)) → False
badPrepend (wordEmpty ())
badPrepend {x = x} (wordEnding pr bad) with DecidableSet.eq (decidableFreeCompletion decA) (ofLetter x) (ofLetter x)
badPrepend {x = x} (wordEnding pr bad) with decidableFreeCompletion decA (ofLetter x) (ofLetter x)
badPrepend {x} (wordEnding pr ()) | inl x₁
badPrepend {x} (wordEnding pr bad) | inr pr2 = pr2 refl
badPrepend' : {x : A} {w : ReducedWord} {pr : PrependIsValid w (ofLetter x)} → (PrependIsValid (prependLetter (ofLetter x) w pr) (ofInv x)) → False
badPrepend' (wordEmpty ())
badPrepend' {x = x} (wordEnding pr x₁) with DecidableSet.eq (decidableFreeCompletion decA) (ofInv x) (ofInv x)
badPrepend' {x = x} (wordEnding pr x₁) with decidableFreeCompletion decA (ofInv x) (ofInv x)
badPrepend' {x} (wordEnding pr ()) | inl x₂
badPrepend' {x} (wordEnding pr x₁) | inr pr2 = pr2 refl
data FreeGroupGenerators : Set a where
χ : A → FreeGroupGenerators
freeGroupGenerators : (w : FreeGroupGenerators) → SymmetryGroupElements (reflSetoid (ReducedWord))
freeGroupGenerators (χ x) = sym {f = f} bij
where
open DecidableSet decA
f : ReducedWord → ReducedWord
f empty = prependLetter (ofLetter x) empty (wordEmpty refl)
f (prependLetter (ofLetter startLetter) w pr) = prependLetter (ofLetter x) (prependLetter (ofLetter startLetter) w pr) (wordEnding (succIsPositive _) ans)
where
ans : freeCompletionEqual decA (ofLetter x) (ofInv startLetter) ≡ BoolFalse
ans with DecidableSet.eq (decidableFreeCompletion decA) (ofLetter x) (ofInv startLetter)
... | bl = refl
f (prependLetter (ofInv startLetter) w pr) with DecidableSet.eq decA startLetter x
f (prependLetter (ofInv startLetter) w pr) | inl startLetter=x = w
f (prependLetter (ofInv startLetter) w pr) | inr startLetter!=x = prependLetter (ofLetter x) (prependLetter (ofInv startLetter) w pr) (wordEnding (succIsPositive _) ans)
where
ans : freeCompletionEqual decA (ofLetter x) (ofLetter startLetter) ≡ BoolFalse
ans with DecidableSet.eq (decidableFreeCompletion decA) (ofLetter x) (ofInv startLetter)
ans | bl with DecidableSet.eq decA x startLetter
ans | bl | inl x=sl = exFalso (startLetter!=x (equalityCommutative x=sl))
ans | bl | inr x!=sl = refl
bij : SetoidBijection (reflSetoid ReducedWord) (reflSetoid ReducedWord) f
SetoidInjection.wellDefined (SetoidBijection.inj bij) x=y rewrite x=y = refl
SetoidInjection.injective (SetoidBijection.inj bij) {empty} {empty} fx=fy = refl
SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofLetter x₁) y pr1} ()
SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) y pr1} fx=fy with DecidableSet.eq decA l x
SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) empty (wordEmpty x₁)} () | inl l=x
SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) empty (wordEnding () x₁)} fx=fy | inl l=x
SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) (prependLetter (ofLetter x₂) y x₁) (wordEmpty ())} fx=fy | inl l=x
SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) (prependLetter (ofLetter x₂) y x₁) (wordEnding pr bad)} fx=fy | inl refl with ofLetterInjective (prependLetterInjective' fx=fy)
... | l=x2 = exFalso ((freeCompletionEqualFalse' decA bad) (applyEquality ofInv l=x2))
SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) (prependLetter (ofInv x₂) y x₁) pr1} () | inl l=x
SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) y pr1} fx=fy | inr l!=x with prependLetterInjective fx=fy
SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) y pr1} fx=fy | inr l!=x | ()
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter x) w1 prX} {empty} fx=fy with prependLetterInjective fx=fy
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter x) w1 prX} {empty} fx=fy | ()
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter x) w1 prX} {prependLetter (ofLetter y) w2 prY} fx=fy = prependLetterInjective fx=fy
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) w2 prY} fx=fy with DecidableSet.eq decA y x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) empty prY} () | inl y=x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofLetter b) w2 x₁) prY} fx=fy | inl y=x with ofLetterInjective (prependLetterInjective' fx=fy)
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofLetter b) w2 x₁) (wordEmpty ())} fx=fy | inl y=x | x=b
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofLetter b) w2 x₁) (wordEnding pr bad)} fx=fy | inl y=x | x=b rewrite x=b | y=x = exFalso (freeCompletionEqualFalse' decA bad refl)
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofInv b) w2 x₁) prY} fx=fy | inl y=x with prependLetterInjective' fx=fy
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofInv b) w2 x₁) prY} fx=fy | inl y=x | ()
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) w2 prY} fx=fy | inr y!=x with prependLetterInjective fx=fy
... | bl = bl
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {empty} fx=fy with DecidableSet.eq decA a x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) empty prX} {empty} () | inl a=x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₂) w1 x₁) prX} {empty} fx=fy | inl a=x with ofLetterInjective (prependLetterInjective' fx=fy)
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₂) w1 x₁) (wordEmpty ())} {empty} fx=fy | inl a=x | x2=x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₂) w1 x₁) (wordEnding pr x3)} {empty} fx=fy | inl a=x | x2=x with freeCompletionEqualFalse' decA x3
... | bl = exFalso (bl (applyEquality ofInv (transitivity a=x (equalityCommutative x2=x))))
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofInv x₂) w1 x₁) prX} {empty} () | inl a=x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {empty} () | inr a!=x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofLetter x₁) y x₂} fx=fy with DecidableSet.eq decA a x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) empty prX} {prependLetter (ofLetter b) y x₂} () | inl a=x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₃) w1 x₁) prX} {prependLetter (ofLetter b) y x₂} fx=fy | inl a=x with ofLetterInjective (prependLetterInjective' fx=fy)
... | x3=x rewrite a=x | x3=x = exFalso (badPrepend' prX)
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofInv x₃) w1 x₁) prX} {prependLetter (ofLetter b) y x₂} fx=fy | inl a=x with prependLetterInjective' fx=fy
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofInv x₃) w1 x₁) prX} {prependLetter (ofLetter b) y x₂} fx=fy | inl a=x | ()
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofLetter x₁) y x₂} () | inr a!=x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv x₁) y x₂} fx=fy with DecidableSet.eq decA a x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) y x₂} fx=fy | inl a=x with DecidableSet.eq decA b x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) y x₂} fx=fy | inl a=x | inl b=x rewrite fx=fy | a=x | b=x = prependLetterRefl
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) empty prX} {prependLetter (ofInv b) y x₂} () | inl a=x | inr b!=x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₃) w1 x₁) prX} {prependLetter (ofInv b) y x₂} fx=fy | inl a=x | inr b!=x with ofLetterInjective (prependLetterInjective' fx=fy)
... | x3=x rewrite a=x | x3=x = exFalso (badPrepend' prX)
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofInv x₃) w1 x₁) prX} {prependLetter (ofInv b) y x₂} () | inl a=x | inr b!=x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) y x₂} fx=fy | inr a!=x with DecidableSet.eq decA b x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) empty x₂} () | inr a!=x | inl b=x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) (prependLetter (ofLetter x₃) y x₁) x2} fx=fy | inr a!=x | inl b=x with ofLetterInjective (prependLetterInjective' fx=fy)
... | x3=x rewrite (equalityCommutative x3=x) | b=x = exFalso (badPrepend' x2)
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) (prependLetter (ofInv x₃) y x₁) x₂} () | inr a!=x | inl b=x
SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) y x₂} fx=fy | inr a!=x | inr b!=x = prependLetterInjective fx=fy
SetoidSurjection.wellDefined (SetoidBijection.surj bij) x=y rewrite x=y = refl
SetoidSurjection.surjective (SetoidBijection.surj bij) {empty} = prependLetter (ofInv x) empty (wordEmpty refl) , needed
where
needed : f (prependLetter (ofInv x) empty (wordEmpty refl)) ≡ empty
needed with DecidableSet.eq decA x x
needed | inl x₁ = refl
needed | inr x!=x = exFalso (x!=x refl)
SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) empty pr} with DecidableSet.eq decA x l
SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter x) empty (wordEmpty refl)} | inl refl = empty , refl
SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter x) empty (wordEnding () x₁)} | inl refl
SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) empty pr} | inr x!=l = prependLetter (ofInv x) (prependLetter (ofLetter l) empty pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA (λ p → x!=l (ofInvInjective p)))) , needed
where
needed : f (prependLetter (ofInv x) (prependLetter (ofLetter l) empty pr) (wordEnding (succIsPositive 0) (freeCompletionEqualFalse decA {ofInv x} {ofInv l} λ p → x!=l (ofInvInjective p)))) ≡ prependLetter (ofLetter l) empty pr
needed with DecidableSet.eq decA x x
... | inl _ = refl
... | inr bad = exFalso (bad refl)
SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) (prependLetter letter w pr2) pr} with DecidableSet.eq decA l x
SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) (prependLetter (ofLetter y) w pr2) pr} | inl l=x rewrite l=x = prependLetter (ofLetter y) w pr2 , prependLetterRefl
SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) (prependLetter (ofInv y) w pr2) pr} | inl l=x = prependLetter (ofInv y) w pr2 , needed
where
needed : f (prependLetter (ofInv y) w pr2) ≡ prependLetter (ofLetter l) (prependLetter (ofInv y) w pr2) pr
needed with DecidableSet.eq decA y x
needed | inl y=x rewrite l=x | y=x = exFalso (badPrepend pr)
needed | inr y!=x rewrite l=x = prependLetterRefl
SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) (prependLetter letter w pr2) pr} | inr l!=x = prependLetter (ofInv x) (prependLetter (ofLetter l) (prependLetter letter w pr2) pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA λ p → l!=x (ofInvInjective (equalityCommutative p)))) , needed
where
needed : f (prependLetter (ofInv x) (prependLetter (ofLetter l) (prependLetter letter w pr2) pr) (wordEnding (succIsPositive (succ (wordLength w))) (freeCompletionEqualFalse decA (λ p → l!=x (ofInvInjective (equalityCommutative p)))))) ≡ prependLetter (ofLetter l) (prependLetter letter w pr2) pr
needed with DecidableSet.eq decA x x
needed | inl x₁ = refl
needed | inr x!=x = exFalso (x!=x refl)
SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofInv l) w pr} = prependLetter (ofInv x) (prependLetter (ofInv l) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA {ofInv x} {ofLetter l} λ ())) , needed
where
needed : f (prependLetter (ofInv x) (prependLetter (ofInv l) w pr) (wordEnding (succIsPositive (wordLength w)) (freeCompletionEqualFalse decA {ofInv x} {ofLetter l} λ ()))) ≡ (prependLetter (ofInv l) w pr)
needed with DecidableSet.eq decA x x
needed | inl x₁ = refl
needed | inr x!=x = exFalso (x!=x refl)