An explicit form for the free magma with the associative law

equational_theories.lean

@@ -3,6 +3,7 @@ import equational_theories.Closure
 import equational_theories.Completeness
 import equational_theories.Compactness
 import equational_theories.FreeMagmaImplications
+import equational_theories.FreeMagmas
 import equational_theories.FreeComm
 import equational_theories.MagmaOp
 import equational_theories.Subgraph

equational_theories/FreeMagmas.lean

@@ -0,0 +1,4 @@
+import equational_theories.FreeMagmas.M1
+import equational_theories.FreeMagmas.M2
+import equational_theories.FreeMagmas.M4
+import equational_theories.FreeMagmas.M4512

equational_theories/FreeMagmas/M1.lean

@@ -0,0 +1,32 @@
+import equational_theories.Completeness
+import equational_theories.Equations.All
+import equational_theories.Homomorphisms
+
+namespace M1
+
+variable {α : Type}
+
+theorem models1 : FreeMagma α ⊧ Law1 := by intro ; rfl
+theorem models1' : FreeMagma α ⊧ {Law1} := by simp [satisfiesSet]; exact models1
+
+def extract : FreeMagmaWithLaws α {Law1} →◇ FreeMagma α :=
+  FreeMagmaWithLaws.evalHom Lf models1'
+
+def freeMagmaWith1 : FreeMagmaWithLaws α {Law1} ≃◇ FreeMagma α where
+  toFun := extract
+  invFun x := embed {Law1} x
+  left_inv x := by
+    refine FreeMagmaWithLaws.inductionOn x fun x => ?_
+    induction x with
+    | Leaf => simp [extract]
+    | Fork l r ih1 ih2 =>
+      simp at ih1 ih2
+      have h : l ⋆ r = l ◇ r := Eq.refl (l ⋆ r)
+      simp ; rw [h, embed_fork, MagmaHom.map_op, embed_fork, ih1, ih2]
+  right_inv x := by
+    induction x with
+    | Leaf x => simp [extract]
+    | Fork l r ih1 ih2 =>
+      have h : l ⋆ r = l ◇ r := Eq.refl (l ⋆ r)
+      simp ; rw [h, embed_fork, MagmaHom.map_op, ih1, ih2]
+  map_op' := extract.map_op'

equational_theories/FreeMagmas/M2.lean

@@ -0,0 +1,29 @@
+import equational_theories.Completeness
+import equational_theories.Equations.All
+import equational_theories.Homomorphisms
+
+namespace M2
+
+variable {α : Type} [Inhabited α]
+
+instance : Magma Unit where
+  op _ _ := ()
+
+theorem models2 : Unit ⊧ Law2 := by intro ; simp [satisfiesPhi]
+
+-- Should go in Completeness.lean?
+@[simp] def isModelSingleLaw (E : Law.NatMagmaLaw) : FreeMagmaWithLaws α {E} ⊧ E := by
+  apply FreeMagmaWithLaws.isModel
+  simp
+
+theorem law2_eq2 {G} [Magma G] (h : G ⊧ Law2) (x y : G) : x = y :=
+  h (fun | 0 => x | _ => y)
+
+def freeMagmaWith2 : FreeMagmaWithLaws α {Law2} ≃◇ Unit where
+  toFun _ := ()
+  invFun _ := LfEmbed {Law2} default
+  left_inv x := by
+    simp
+    exact law2_eq2 (isModelSingleLaw Law2) _ _
+  right_inv x := by simp [Function.RightInverse, Function.LeftInverse]
+  map_op' := by simp

equational_theories/FreeMagmas/M4.lean

@@ -0,0 +1,62 @@
+import equational_theories.Completeness
+import equational_theories.Equations.All
+import equational_theories.Homomorphisms
+
+namespace M4
+
+variable {α : Type}
+
+def Left (α : Type) := α
+
+instance : Magma (Left α) where
+  op x _ := x
+
+def left (a : α) : Left α := a
+
+theorem models4 : Left α ⊧ Law4 := by intro ; rfl
+theorem models4' : Left α ⊧ {Law4} := by simp [satisfiesSet]; exact models4
+
+def extract : FreeMagmaWithLaws α {Law4} →◇ Left α :=
+  FreeMagmaWithLaws.evalHom left models4'
+
+theorem law4_eq4 {G} [Magma G] (h : G ⊧ Law4) (x y : G) : x = x ◇ y :=
+  h (fun | 0 => x | _ => y)
+
+def leftmost : FreeMagma α → α
+  | FreeMagma.Leaf a => a
+  | FreeMagma.Fork l _ => leftmost l
+
+theorem leftmost_fork (l r : FreeMagma α) : leftmost (l ⋆ r) = leftmost l := by simp [leftmost]
+
+theorem eval_leftmost {G} [Magma G] (h : G ⊧ Law4) (x : FreeMagma α) (f : α → G) :
+    FreeMagma.evalInMagma f x = f (leftmost x) := by
+  induction x with
+  | Leaf => simp [FreeMagma.evalInMagma, leftmost]
+  | Fork l _ hi _ => simp [FreeMagma.evalInMagma, leftmost, ←law4_eq4 h, hi]
+
+theorem extract_embed (x : FreeMagma α) : extract (embed {Law4} x) = leftmost x := by
+  apply eval_leftmost models4
+
+-- Should go in Completeness.lean?
+@[simp] def isModelSingleLaw (E : Law.NatMagmaLaw) : FreeMagmaWithLaws α {E} ⊧ E := by
+  apply FreeMagmaWithLaws.isModel
+  simp
+
+theorem embed_law4_fork (l r : FreeMagma α) : embed {Law4} (l ⋆ r) = embed {Law4} l := by
+  have h : l ⋆ r = l ◇ r := Eq.refl (l ⋆ r)
+  rw [h, embed_fork]
+  simp [←law4_eq4]
+
+theorem embed_leftmost (x : FreeMagma α) : embed {Law4} x = LfEmbed {Law4} (leftmost x) := by
+  induction x with
+  | Leaf => rfl
+  | Fork l r ih _ => rw [leftmost_fork, embed_law4_fork, ih]
+
+def freeMagmaWith4 : FreeMagmaWithLaws α {Law4} ≃◇ Left α where
+  toFun := extract
+  invFun := LfEmbed {Law4}
+  left_inv x := by
+    refine FreeMagmaWithLaws.inductionOn x fun x => ?_
+    rw [extract_embed, embed_leftmost]
+  right_inv _ := by simp [extract]; rfl
+  map_op' := extract.map_op'

equational_theories/FreeMagmas/M4512.lean

@@ -0,0 +1,117 @@
+import equational_theories.Completeness
+import equational_theories.Equations.All
+import equational_theories.Homomorphisms
+
+namespace M4512
+
+variable {α : Type}
+
+@[simp] def NonEmptyList α := {x : List α | x ≠ []}
+
+@[simp] theorem NonEmptyList_mem (xs : NonEmptyList α) : xs.val ≠ [] := xs.prop
+
+instance : Magma (NonEmptyList α) where
+  op xs ys := ⟨xs ++ ys, by simp⟩
+
+def singleton (x : α) : NonEmptyList α := ⟨[x], by simp⟩
+
+theorem op_append (xs ys : NonEmptyList α) : (xs ◇ ys).val = xs.val ++ ys.val := by
+  simp [Magma.op]
+
+@[elab_as_elim]
+theorem singletonAppendInduction {P : NonEmptyList α → Prop}
+    (hs : ∀ x, P (singleton x)) (ha : ∀ xs ys, P xs → P ys → P (xs ◇ ys))
+    : ∀ xs, P xs
+  | ⟨[], h⟩ => False.elim (h rfl)
+  | ⟨[x], _⟩ => hs x
+  | ⟨x::x'::xs, _⟩ =>
+    let tail : NonEmptyList α := ⟨x'::xs, by simp⟩
+    ha (singleton x) tail (hs x) (singletonAppendInduction hs ha tail)
+
+theorem op_assoc (x y z : NonEmptyList α) : (x ◇ y) ◇ z = x ◇ (y ◇ z) := by
+  simp [Magma.op]
+
+theorem models4512 : NonEmptyList α ⊧ Law4512 := by
+  intro
+  unfold satisfiesPhi
+  simp [FreeMagma.evalInMagma]
+  rw [op_assoc]
+
+theorem models4512' : NonEmptyList α ⊧ {Law4512} := by
+  simp [satisfiesSet]
+  exact models4512
+
+def LfEmbed4512 : α → FreeMagmaWithLaws α {Law4512} := LfEmbed {Law4512}
+
+def foldNonEmpty (f : α → α → α) (xs : List α) (h : xs ≠ []) : α :=
+  match xs with
+  | [] => False.elim (h rfl)
+  | x::xs =>
+    match xs with
+    | [] => x
+    | x'::xs' => f x (foldNonEmpty f (x'::xs') (by simp))
+
+theorem foldNonEmpty_singleton (f : α → α → α) (x : α) (h : [x] ≠ []) : foldNonEmpty f [x] h = x := by
+  simp [foldNonEmpty]
+
+theorem foldNonEmpty_cons (f : α → α → α) (x : α) (xs : List α) (h : xs ≠ []) (h2 : x::xs ≠ []) :
+    foldNonEmpty f (x::xs) h2 = f x (foldNonEmpty f xs h) :=
+  let x'::xs' := xs
+  foldNonEmpty.eq_3 f x x' xs' h2
+
+theorem foldNonEmpty_op4512 {G} [Magma G] (h : G ⊧ Law4512) (xs ys : List G) (hx : xs ≠ []) (hy : ys ≠ []) (hxy : xs ++ ys ≠ []) :
+    foldNonEmpty Magma.op (xs ++ ys) hxy = foldNonEmpty Magma.op xs hx ◇ foldNonEmpty Magma.op ys hy := by
+  have h (x y z : G) : x ◇ (y ◇ z) = (x ◇ y) ◇ z := h λ | 0 => x | 1 => y | _ => z
+  induction xs with
+  | nil => contradiction
+  | cons head tail hi =>
+    simp
+    cases tail with
+    | nil => simp [foldNonEmpty_singleton]; rw [foldNonEmpty_cons]
+    | cons head' tail' =>
+      rw [foldNonEmpty, ←h]
+      -- These two lines have got to be a standard tactic
+      have eq_mul (x y z : G) (heq : y = z) : x ◇ y = x ◇ z := by rw [heq]
+      apply eq_mul
+      apply hi
+
+-- Should go in Completeness.lean?
+@[simp] def isModelSingleLaw (E : Law.NatMagmaLaw) : FreeMagmaWithLaws α {E} ⊧ E := by
+  apply FreeMagmaWithLaws.isModel
+  simp
+
+theorem map_nonEmptyList {α β} (f : α → β) (xs : List α) (h : xs ≠ []) : xs.map f ≠ [] := by
+  simp [h]
+
+def inject : NonEmptyList α →◇ FreeMagmaWithLaws α {Law4512} where
+  toFun xs :=
+    let leaves : List (FreeMagmaWithLaws α {Law4512}) := xs.val.map LfEmbed4512
+    foldNonEmpty Magma.op leaves (map_nonEmptyList LfEmbed4512 xs.val xs.prop)
+  map_op' xs ys := by
+    simp [foldNonEmpty_op4512, op_append xs ys]
+
+theorem inject_singleton (a : α) (xs : NonEmptyList α) (h : xs.val = [a]) : inject xs = LfEmbed4512 a := by
+  simp [inject, DFunLike.coe, h, foldNonEmpty]
+
+def toList4512 : FreeMagmaWithLaws α {Law4512} →◇ NonEmptyList α :=
+  FreeMagmaWithLaws.evalHom singleton models4512'
+
+theorem toList4512_leaf (a : α) : toList4512 (LfEmbed4512 a) = singleton a := by
+  simp [LfEmbed4512, toList4512]
+
+def freeMagmaWith4512 : FreeMagmaWithLaws α {Law4512} ≃◇ NonEmptyList α where
+  toFun := toList4512
+  invFun := inject
+  left_inv x := by
+    refine FreeMagmaWithLaws.inductionOn x fun x => ?_
+    induction x with
+    | Leaf => simp [toList4512]; apply inject_singleton; rfl
+    | Fork l r ih1 ih2 =>
+      have h : l ⋆ r = l ◇ r := Eq.refl (l ⋆ r)
+      rw [h, embed_fork, MagmaHom.map_op, MagmaHom.map_op, ih1, ih2]
+  right_inv := by
+    intro xs
+    induction xs using singletonAppendInduction
+    · rw [inject_singleton, toList4512_leaf]; rfl
+    · rw [MagmaHom.map_op, MagmaHom.map_op]; simp_all
+  map_op' := toList4512.map_op'