feat(algebra/free): free magma, semigroup, monoid

src/algebra/free.lean

@@ -0,0 +1,187 @@
+import tactic.interactive
+
+universes u v
+
+inductive free_magma (α : Type u) : Type u
+| of : α → free_magma
+| mul : free_magma → free_magma → free_magma
+
+namespace free_magma
+
+variables {α : Type u}
+
+instance : has_mul (free_magma α) := ⟨free_magma.mul⟩
+
+@[elab_as_eliminator]
+protected lemma induction_on {C : free_magma α → Prop} (x)
+  (ih1 : ∀ x, C (of x)) (ih2 : ∀ x y, C x → C y → C (x * y)) :
+  C x :=
+free_magma.rec_on x ih1 ih2
+
+variables {β : Type v} [has_mul β] (f : α → β)
+
+def lift : free_magma α → β
+| (of x) := f x
+| (mul x y) := lift x * lift y
+
+@[simp] lemma lift_of (x) : lift f (of x) = f x := rfl
+@[simp] lemma lift_mul (x y) : lift f (x * y) = lift f x * lift f y := rfl
+
+theorem lift_unique (f : free_magma α → β) (hf : ∀ x y, f (x * y) = f x * f y) :
+  f = lift (f ∘ of) :=
+funext $ λ x, free_magma.rec_on x (λ x, rfl) $ λ x y ih1 ih2,
+(hf x y).trans $ congr (congr_arg _ ih1) ih2
+
+end free_magma
+
+namespace magma
+
+inductive free_semigroup.r (α : Type u) [has_mul α] : α → α → Prop
+| intro : ∀ x y z, free_semigroup.r ((x * y) * z) (x * (y * z))
+| left : ∀ w x y z, free_semigroup.r (w * ((x * y) * z)) (w * (x * (y * z)))
+
+def free_semigroup (α : Type u) [has_mul α] : Type u :=
+quot $ free_semigroup.r α
+
+namespace free_semigroup
+
+variables {α : Type u} [has_mul α]
+
+def of : α → free_semigroup α := quot.mk _
+
+@[elab_as_eliminator]
+protected lemma induction_on {C : free_semigroup α → Prop} (x : free_semigroup α)
+  (ih : ∀ x, C (of x)) : C x :=
+quot.induction_on x ih
+
+theorem of_mul_assoc (x y z : α) : of ((x * y) * z) = of (x * (y * z)) := quot.sound $ r.intro x y z
+theorem of_mul_assoc_left (w x y z : α) : of (w * ((x * y) * z)) = of (w * (x * (y * z))) := quot.sound $ r.left w x y z
+theorem of_mul_assoc_right (w x y z : α) : of (((w * x) * y) * z) = of ((w * (x * y)) * z) :=
+by rw [of_mul_assoc, of_mul_assoc, of_mul_assoc, of_mul_assoc_left]
+
+instance : semigroup (free_semigroup α) :=
+{ mul := λ x y, begin
+    refine quot.lift_on x (λ p, quot.lift_on y (λ q, (quot.mk _ $ p * q : free_semigroup α)) _) _,
+    { rintros a b (⟨c, d, e⟩ | ⟨c, d, e, f⟩); change of _ = of _,
+      { rw of_mul_assoc_left },
+      { rw [← of_mul_assoc, of_mul_assoc_left, of_mul_assoc] } },
+    { refine quot.induction_on y (λ q, _),
+      rintros a b (⟨c, d, e⟩ | ⟨c, d, e, f⟩); change of _ = of _,
+      { rw of_mul_assoc_right },
+      { rw [of_mul_assoc, of_mul_assoc, of_mul_assoc_left, of_mul_assoc_left, of_mul_assoc_left,
+          ← of_mul_assoc c d, ← of_mul_assoc c d, of_mul_assoc_left] } }
+  end,
+  mul_assoc := λ x y z, quot.induction_on x $ λ p, quot.induction_on y $ λ q,
+    quot.induction_on z $ λ r, of_mul_assoc p q r }
+
+theorem of_mul (x y : α) : of (x * y) = of x * of y := rfl
+
+variables {β : Type v} [semigroup β] (f : α → β)
+
+def lift (hf : ∀ x y, f (x * y) = f x * f y) : free_semigroup α → β :=
+quot.lift f $ by rintros a b (⟨c, d, e⟩ | ⟨c, d, e, f⟩); simp only [hf, mul_assoc]
+
+@[simp] lemma lift_of {hf} (x : α) : lift f hf (of x) = f x := rfl
+
+@[simp] lemma lift_mul {hf} (x y) : lift f hf (x * y) = lift f hf x * lift f hf y :=
+quot.induction_on x $ λ p, quot.induction_on y $ λ q, hf p q
+
+theorem lift_unique (f : free_semigroup α → β) (hf : ∀ x y, f (x * y) = f x * f y) :
+  f = lift (f ∘ of) (λ p q, hf (of p) (of q)) :=
+funext $ λ x, quot.induction_on x $ λ p, rfl
+
+end free_semigroup
+
+end magma
+
+def free_semigroup (α : Type u) : Type u :=
+α × list α
+
+namespace free_semigroup
+
+variables {α : Type u}
+
+instance : semigroup (free_semigroup α) :=
+{ mul := λ L1 L2, (L1.1, L1.2 ++ L2.1 :: L2.2),
+  mul_assoc := λ L1 L2 L3, prod.ext rfl $ list.append_assoc _ _ _ }
+
+def of (x : α) : free_semigroup α :=
+(x, [])
+
+@[elab_as_eliminator]
+protected lemma induction_on {C : free_semigroup α → Prop} (x)
+  (ih1 : ∀ x, C (of x)) (ih2 : ∀ x y, C (of x) → C y → C (of x * y)) :
+  C x :=
+let ⟨x, L⟩ := x in list.rec_on L ih1 (λ hd tl ih x, ih2 x (hd, tl) (ih1 x) (ih hd)) x
+
+variables {β : Type v} [semigroup β] (f : α → β)
+
+def lift' : α → list α → β
+| x [] := f x
+| x (hd::tl) := f x * lift' hd tl
+
+def lift (x : free_semigroup α) : β :=
+lift' f x.1 x.2
+
+@[simp] lemma lift_of (x : α) : lift f (of x) = f x := rfl
+@[simp] lemma lift_of_mul (x y) : lift f (of x * y) = f x * lift f y := rfl
+
+@[simp] lemma lift_mul (x y) : lift f (x * y) = lift f x * lift f y :=
+free_semigroup.induction_on x (λ p, rfl)
+  (λ p x ih1 ih2, by rw [mul_assoc, lift_of_mul, lift_of_mul, mul_assoc, ih2])
+
+theorem lift_unique (f : free_semigroup α → β) (hf : ∀ x y, f (x * y) = f x * f y) :
+  f = lift (f ∘ of) :=
+funext $ λ ⟨x, L⟩, list.rec_on L (λ x, rfl) (λ hd tl ih x,
+  (hf (of x) (hd, tl)).trans $ congr_arg _ $ ih _) x
+
+end free_semigroup
+
+namespace semigroup
+
+def free_monoid : Type u → Type u := option
+
+namespace free_monoid
+
+attribute [reducible] free_monoid
+instance (α : Type u) [semigroup α] : monoid (free_monoid α) :=
+{ mul := option.lift_or_get (*),
+  mul_assoc := is_associative.assoc _,
+  one := failure,
+  one_mul := is_left_id.left_id _,
+  mul_one := is_right_id.right_id _ }
+attribute [semireducible] free_monoid
+
+def of {α : Type u} : α → free_monoid α := some
+
+variables {α : Type u} [semigroup α]
+
+@[elab_as_eliminator]
+protected lemma induction_on {C : free_monoid α → Prop} (x : free_monoid α)
+  (h1 : C 1) (hof : ∀ x, C (of x)) : C x :=
+option.rec_on x h1 hof
+
+@[simp] lemma of_mul (x y : α) : of (x * y) = of x * of y := rfl
+
+variables {β : Type v} [monoid β] (f : α → β)
+
+def lift (x : free_monoid α) : β :=
+option.rec_on x 1 f
+
+@[simp] lemma lift_of (x) : lift f (of x) = f x := rfl
+
+@[simp] lemma lift_one : lift f 1 = 1 := rfl
+
+@[simp] lemma lift_mul (hf : ∀ x y, f (x * y) = f x * f y) (x y) :
+  lift f (x * y) = lift f x * lift f y :=
+free_monoid.induction_on x (by rw [one_mul, lift_one, one_mul]) $ λ x,
+free_monoid.induction_on y (by rw [mul_one, lift_one, mul_one]) $ λ y,
+hf x y
+
+theorem lift_unique (f : free_monoid α → β) (hf : f 1 = 1) :
+  f = lift (f ∘ of) :=
+funext $ λ x, free_monoid.induction_on x hf $ λ x, rfl
+
+end free_monoid
+
+end semigroup