From 57951d15141f1031df422ea40003b00888bec2df Mon Sep 17 00:00:00 2001 From: Franklin Dyer Date: Sat, 5 Oct 2024 16:56:59 -0600 Subject: [PATCH] renamed FreeMonoid.lean to FreeSemigroup.lean and cleaned up inconsistent naming --- equational_theories/{FreeMonoid.lean => FreeSemigroup.lean} | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) rename equational_theories/{FreeMonoid.lean => FreeSemigroup.lean} (96%) diff --git a/equational_theories/FreeMonoid.lean b/equational_theories/FreeSemigroup.lean similarity index 96% rename from equational_theories/FreeMonoid.lean rename to equational_theories/FreeSemigroup.lean index a2f628ab..83ef4223 100644 --- a/equational_theories/FreeMonoid.lean +++ b/equational_theories/FreeSemigroup.lean @@ -118,7 +118,7 @@ theorem AssocImpliesSgrProjFaithful {α : Type _} {G : Type _} [Magma G] (assoc apply Eq.trans $ congrArg (fun s ↦ (_ ◇ s) ◇ _) (AssocImpliesSgrProjFaithful assoc f tl2) trivial -def insertSemigroupSorted {n : Nat} (i : Fin n) (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) := +def insertSgrSorted {n : Nat} (i : Fin n) (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) := match ls with | j .+ => if i ≤ j then i ,+ j .+ else j ,+ i .+ | j ,+ lstail => if i ≤ j then i ,+ j ,+ lstail else j ,+ i ,+ lstail @@ -126,10 +126,10 @@ def insertSemigroupSorted {n : Nat} (i : Fin n) (ls : FreeSemigroup (Fin n)) : F def insertionSortSgr {n : Nat} (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) := match ls with | i .+ => i .+ - | i ,+ lstail => insertSemigroupSorted i (insertionSortSgr lstail) + | i ,+ lstail => insertSgrSorted i (insertionSortSgr lstail) theorem CommSgrImpliesInsertSortedFaithful {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G) - : ∀ i : Fin n, ∀ ls : FreeSemigroup (Fin n), evalInSgr f (insertSemigroupSorted i ls) = (f i) ◇ evalInSgr f ls := + : ∀ i : Fin n, ∀ ls : FreeSemigroup (Fin n), evalInSgr f (insertSgrSorted i ls) = (f i) ◇ evalInSgr f ls := fun i ls ↦ match ls with | j .+ => by have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j .+) (j ,+ i .+)