Algebraic structure on lists (and/or finite tuples)

Stream: Is there code for X?

[Wrenna Robson]

So, uh, we don't seem to have this?

variable (α : Type*) in
#synth AddSemigroup (List α)

This is despite the fact it is pretty easy to define:

instance List.instAddSemigroup {α : Type*} : AddSemigroup (List α) where
  add := List.append
  add_assoc := List.append_assoc

Indeed, we can go further:

instance List.instAddMonoid {α : Type*} : AddMonoid (List α) where
  add := List.append
  add_assoc := List.append_assoc
  zero := []
  zero_add := List.nil_append
  add_zero := List.append_nil

This would be useful to have because it would mean that you could in theory define an AddAction of lists of a type on another type, even if the first type doesn't have a defined monoidal structure.

I also feel like on this basis something like

variable (α : Type*) in
#synth AddSemigroup (Sigma (fun n => Fin n → α))

would be useful: again it would be useful to be able to have an action of Fin n -> α on things in a natural way - but it might be harder to use.

Do we have a different approach to this already in the library?

[Eric Rodriguez]

@Yaël Dillies, any ideas/qualms? I'm in favour of the list one (even potentially replacing ++) but not as sure about the sigma one; it seems likely to cause issues in my head.

[Wrenna Robson]

The sigma one definitely feels dodgy to me, there's a reason a lot of languages don't let you do this to tuples. But I am kinda in the position where it is the one that might be a bit more convenient in some ways.

[Yaël Dillies]

Wait, how would the sigma one even work? That looks very ill-behaved

[Wrenna Robson]

Oh I think it probably doesn't, I'm not sure if it is possible. But certainly Fin.append exists and that's what I'm trying to point to.

[Wrenna Robson]

(The fact that Fin.append_assoc needs a cast in it kinda shows the issue though I think.)

[Wrenna Robson]

In theory I think that that Sigma might be isomorphic to List?

[Eric Wieser]

If you want + to mean ++, you can use docs#FreeAddMonoid

[Eric Wieser]

The sigma one almost exists already as docs#GradedMonoid.GMul.toMul

[Wrenna Robson]

I suppose, but that (FreeAddMonoid) is rather harder to use. If we had another monoid structure on List I would understand it!

[Eric Wieser]

Why is FreeAddMonoid harder to use?

[Wrenna Robson]

Well in this case - because all my theorems are actually written as about tuples so it's doubly hard :P

[Wrenna Robson]

I prefer avoiding type synonyms when it isn't necessary in general.

[Wrenna Robson]

As I say, I came to it from the perspective of "I would like to define an action on tuples, or possibly on lists, on a type"

[Wrenna Robson]

(I would actually like to define an action on arrays in particular but baby steps.)

[Eric Wieser]

Here's another candidate for * on lists:

import Mathlib

variable {m} [Monad m]

@[to_additive]
instance [Mul α] : Mul (m α) where
  mul l₁ l₂ := do return (←l₁) * (←l₂)

@[to_additive]
lemma mul_def [Mul α] (l₁ l₂ : m α) : l₁ * l₂ = (do return (←l₁) * (←l₂)) := rfl

@[to_additive]
instance [One α] : One (m α) where
  one := do return 1

@[to_additive]
lemma one_def [One α] : (1 : m α) = do return 1 := rfl

@[to_additive]
instance [LawfulMonad m] [Monoid α] : Monoid (m α) where
  one_mul l₂ := by simp only [one_def, mul_def, pure_bind, one_mul, bind_pure]
  mul_one l₂ := by simp only [one_def, mul_def, pure_bind, mul_one, bind_pure]
  mul_assoc l₂ := by simp only [mul_def, bind_assoc, pure_bind, bind_pure, mul_assoc, implies_true]

#eval [1, 2, 3] + [4, 5]
#eval [1, 2, 3] * [4, 5]

[Eric Wieser]

(or indeed, on any monad)

[Wrenna Robson]

Yes I was going to ask, what's the * equivalent? Needs some assumptions on the underlying type ofc but

[Wrenna Robson]

I feel as if it should be/could be the convolution? Which I am not sure this is.

[Eric Wieser]

I think i agree those operations could plausibly distribute, but I think it would be bizarre to have them as the default instance on lists

[Wrenna Robson]

Yes, that is somewhere where a type synonym might well make sense. But I would argue that '+' on lists can't really mean anything sensible except for concatenation. I suppose it could be a similar construction as that, so that [1, 2, 3] + [4, 5] = [5, 6, 6, 7, 7, 8].

[Wrenna Robson]

But I would honestly argue that that is more perverse in some ways.

[Eric Wieser]

(I edited my example above so that it has that behavior)

[Wrenna Robson]

Your one has that for multiplication, no?

[Eric Wieser]

It has it for both

[Wrenna Robson]

Oh I see, the to_additive.

[Eric Wieser]

Wrenna Robson said:

Well in this case - because all my theorems are actually written as about tuples so it's doubly hard :P

By tuples do you mean Fin n -> a?

[Wrenna Robson]

Yes.

[Wrenna Robson]

Incidentally I realise "Python does it this way" is a pretty poor argument for anything but as it happens:

>>> [1, 2, 3] + [4, 5]
[1, 2, 3, 4, 5]
>>> [1, 2, 3] * [4, 5]
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: can't multiply sequence by non-int of type 'list'

Other languages with which I'm familiar only let you add lists of the same size (and in that case it's pointwise).

[Eric Wieser]

Python doesn't have a dedicated ++ operator

[Eric Wieser]

(Ok, strictly they do, it's operator.concat, but it is only available via the overloaded + operator)

[Wrenna Robson]

Well, this is true, but I frankly see little need for ++.

[Wrenna Robson]

Like, because ++ is the operation that makes Lists into AddMonoids, we should just use + for it. I don't see any particular benefit in having a special notation for it.

[Eric Wieser]

Well, you'll need to take that up with lean core, and I suspect they do not care for such bike-shedding

[Eric Wieser]

I'm pretty sure we copied ++ from haskell?

[Wrenna Robson]

Indeed, it isn't worth the pain.

[Wrenna Robson]

Yeah Haskell uses it! I like ++ in general. I just wish it was then straightforward to go "btw ++ is also +".

[Wrenna Robson]

I guess fundamentally this is the point of the FreeAddMonoid, but it's mildly a pain that it works like that - I wish List could addact on stuff directly.

[Kevin Buzzard]

We could make HAdd_add.add_add, make another group heirarchy, and enhance to_additive to to_additive_additive.

[Wrenna Robson]

oh no

[Kevin Buzzard]

yeah I'm not sure that idea will go down too well

[Wrenna Robson]

For what it's worth I wasn't saying that!

[Wrenna Robson]

I just think if something walks like a monoid and quacks like a monoid it's quite useful when it is one

[Kevin Buzzard]

Yes but what if something is a monoid in several ways? Then mathlib's position would probably be not to choose. Can you just make the def you want and activate it locally?

[Wrenna Robson]

Yeah, probably - I'm not even sure I need it for List as I say. Though I am not sure I know another definition of AddMonoid for it.

[Wrenna Robson]

I agree that with ambiguity one ought not to choose.

[Kevin Buzzard]

Another definition of AddMonoid: Eric posted a plausible one above assuming an addition on the underlying type. This might well be enough to give people pause.

[Wrenna Robson]

I suppose. I think I'm less comfortable with [0] being 0 than [] being 0?

[Wrenna Robson]

Like the latter feels much more natural to me just for starters.

[Wrenna Robson]

I suppose this is the argument for the FreeAddMonoid way of thinking! And the default interpretation of List is List-as-Monad.

[Wrenna Robson]

Still, I'm not sure I can think of any programming languages where the above is the behaviour of + on lists.

[Wrenna Robson]

(Mostly, as we have currently I guess, it simply isn't allowed.)

[Kevin Buzzard]

Right but there's nothing stopping you making it allowed in your own project, and indeed this might well be the best solution for you.

[Wrenna Robson]

Aye. Sorry.

[Wrenna Robson]

Like as I say I don't need it for List - I was just suggesting something that seemed to me to be natural.

[Wrenna Robson]

But if it doesn't seem that way, and we do have it in some form, albeit via a type synonym, then the answer is - yes we have code for that.

[Kyle Miller]

I think it's fine if there's a def that gives a Monoid structure on List, and then modules can use attribute [local instance] if they want to use monoid notation.

Of course, FreeAddMonoid is the one true List-as-an-additive-monoid :smile: For interfacing between the List and FreeAddMonoid worlds, I guess you need to be careful to always insert docs#FreeAddMonoid.toList and docs#FreeAddMonoid.ofList as appropriate.

[Yaël Dillies]

Wrenna Robson said:

Yes, that is somewhere where a type synonym might well make sense. But I would argue that '+' on lists can't really mean anything sensible except for concatenation. I suppose it could be a similar construction as that, so that [1, 2, 3] + [4, 5] = [5, 6, 6, 7, 7, 8].

To be quite fair, when I saw the notification from eric's ping, I thought you were asking about [1, 2, 3] + [4, 5] = [5, 7]!

[Wrenna Robson]

Err I can't now remember the context of that but sorry.

[Scott Morrison]

I only skimmed this thread, but please do not define a global + operation on Lists.

For me at moment, [1, 2, 3] + [4, 5] = [5, 7, 3] (i.e. pointwise addition, padding with zeros as needed)

[Scott Morrison]

(i.e. using lists as a model for finitely supported functions)

[Eric Wieser]

Yaël Dillies said:

To be quite fair, when I saw the notification from eric's ping, I thought you were asking about [1, 2, 3] + [4, 5] = [5, 8]!

I cannot work out how you are defining this

[Scott Morrison]

I'm pretty sure Yaël's 8 is a typo for 7: the same as my addition, but truncating to the shortest list.

[Ruben Van de Velde]

I'm guessing they're adding the endpoints: [1+4, 3+5], though I couldn't tell you what's useful about that

[Yaël Dillies]

No, Scott is right. This was typo.

[Wrenna Robson]

Scott Morrison said:

I only skimmed this thread, but please do not define a global + operation on Lists.

For me at moment, [1, 2, 3] + [4, 5] = [5, 7, 3] (i.e. pointwise addition, padding with zeros as needed)

Pointwise addition with padding is quite interesting. Wouldn't have occurred to me.

[Wrenna Robson]

List is, on reflection, a very semantically overloaded type.

[Eric Wieser]

Wrenna Robson said:

Incidentally I realise "Python does it this way" is a pretty poor argument for anything but ...

Wrenna Robson said:

List is, on reflection, a very semantically overloaded type.

Perhaps if you're set on copying python, we should copy "in the face of ambiguity, refuse the temptation to guess"

[Wrenna Robson]

Indeed. Frankly it's weird that it does treat + as concat given that principle.

[Trebor Huang]

Julia uses * for string concatenation because multiplication is more often non-commutative

[Wrenna Robson]

That's fun

[Kevin Buzzard]

The only situation I know in mathematics when + isn't commutative is addition of ordinals.

[Wrenna Robson]

I wonder, if you take ++ as *, is there some operation on lists it naturally distributes over?

[Scott Morrison]

x + y = x

[Yakov Pechersky]

Also, if you defined concat as *, then it distributes over trop \comp List.length. Inspired by calculations of degrees on polynomials.

[Wrenna Robson]

That's very nice

[Scott Morrison]

@Yakov Pechersky, could you spell out what you mean?

[Yakov Pechersky]

Tropical multiplication is addition in the underlying semiring. So if we have l1 * l2 := l1 ++ l2, then we have trop (List.length (l1 * l2))) = trop (List.length l1 + List.length l2) = trop (List.length l1) * trop (List.length l2). Perhaps this is distributing in the "wrong" direction.

[Yakov Pechersky]

I guess "distribute" isn't right here, it's more of a "map"

[Scott Morrison]

Yes, it is not distributivity at all. :-)

[Scott Morrison]

My wild conjecture is that x + y = x and x + y = y are the only solutions. :-)

[Thomas Murrills]

Taking x + y to be “longest common prefix of x and y” works for left-distributivity! :)

[Thomas Murrills]

I’m too close to sleeping to check right now if this actually works, but if the “wedge” of two lists is the operation that is like concatenation but “overlaps” them as much as possible—e.g. [5, 2, 3, 1] wedge [2, 3, 1, 6, 7] is [5, 2, 3, 1, 6, 7]—then maybe “longest common prefix wedge longest common suffix” gets you both left and right distributivity?

[Thomas Murrills]

(Assuming your type has decidable equality, of course. I’d tentatively back Scott’s conjecture when talking about a uniform operation over generic lists!)

[Thomas Murrills]

(Actually we might not want to consider the wedge of longest common prefix and sufffix but instead the “longest common outfix”, generated by taking the longest common prefix and concatenating it with the longest common suffix of whatever remained after removing the longest common prefix. E.g. the longest common outfix of [2,2,2] and [2,2,5,2,2] is [2,2,2], but the wedge of the longest common prefix and suffix is [2,2]. I’m not sure what the consequences of the difference are yet…)

[Scott Morrison]

Bonus points for finding literature on this question. :-)

[Trebor Huang]

In the case of natural numbers (i.e. lists of the singleton type), restricting attention to commutative operations, this is a well-known olympiad problem where the only solutions (with some non-triviality requirements) are min and max.

[Thomas Murrills]

Oh, that gives us yet another +! Simply choose the longest (or shortest) list, and e.g. bias left or right when the lists have the same length.

[Thomas Murrills]

I proved that the "longest common outfix" notion above is a solution (given decidable equality)! :)

code

import Mathlib.Data.List.Infix

variable {α : Type} [DecidableEq α] {l₁ l₂ : List α}

/-- `LCP l₁ l₂` denotes the "longest common prefix" of `l₁` and `l₂`. -/
def LCP : List α → List α → List α
| x :: xs, y :: ys => if x = y then x :: LCP xs ys else []
| [], _ | _, [] => []

/-- `LCP l₁ l₂` denotes the "longest common suffix" of `l₁` and `l₂`. -/
def LCS (l₁ l₂ : List α) : List α := LCP l₁.reverse l₂.reverse |>.reverse

/-- `LCO l₁ l₂` denotes the "longest common outfix" of `l₁` and `l₂`.
That is, if `l = LCP l₁ l₂`, and `l₁ = l ++ l₁'`, `l₂ = l ++ l₂'`, then `LCO l₁ l₂` is `(LCP l₁ l₂) ++ LCS l₁' l₂'`.
Note that while this appears biased towards the prefix, it isn't; taking the `LCS` first would result in the same list. -/
def LCO : List α → List α → List α
| l₁@(x :: xs), l₂@(y :: ys) => if x = y then x :: LCO xs ys else LCS l₁ l₂
| [], _ | _, [] => []

@[simp] theorem lco_self : {l : List α} → LCO l l = l
| [] => rfl
| x :: xs => by simp [LCO]; exact lco_self

@[simp] theorem lcp_self : {l : List α} → LCP l l = l
| [] => rfl
| x :: xs => by simp [LCP]; exact lcp_self

@[simp] theorem lcs_self : {l : List α} → LCS l l = l := by simp [LCS]

theorem lcp_comm {l₁ l₂ : List α} : LCP l₁ l₂ = LCP l₂ l₁ := by
  match l₁, l₂ with
  | [], [] | [], _ :: _ | _ :: _, [] => rfl
  | head :: tail, head' :: tail' =>
    simp [LCP]
    by_cases h : head = head'
    · simp [h]; exact lcp_comm
    · simp [h, Ne.symm]

theorem lcs_comm {l₁ l₂ : List α} : LCS l₁ l₂ = LCS l₂ l₁ := by
  match l₁, l₂ with
  | [], [] => rfl
  | _, _ => simp [LCS]; exact lcp_comm

theorem lco_comm {l₁ l₂ : List α} : LCO l₁ l₂ = LCO l₂ l₁ := by
  match l₁, l₂ with
  | [], [] | [], _ :: _ | _ :: _, [] => rfl
  | head :: tail, head' :: tail' =>
    simp [LCO]
    by_cases h : head = head'
    · simp [h]; exact lco_comm
    · simp [h, Ne.symm]; exact lcs_comm

@[simp] theorem lcp_nil_left : LCP [] l₁ = [] := by simp only [LCP]
@[simp] theorem lcs_nil_left : LCS [] l₁ = [] := by simp [LCS]
@[simp] theorem lco_nil_left : LCO [] l₁ = [] := by simp only [LCO]
@[simp] theorem lcp_nil_right : LCP l₁ [] = [] := by rw [lcp_comm]; simp
@[simp] theorem lcs_nil_right : LCS l₁ [] = [] := by rw [lcs_comm]; simp
@[simp] theorem lco_nil_right : LCO l₁ [] = [] := by rw [lco_comm]; simp

@[simp] theorem lcs_append_after_right {l₁} : LCS l₁ (l₂ ++ l₁) = l₁ := by
  induction l₁ using List.reverseRecOn with
  | H0 => simp
  | H1 l a ih =>
    simp [LCS, LCP]
    rw [← List.reverse_append]
    exact ih

@[simp] theorem lco_append_after_right {l₁ l₂ : List α} : LCO l₁ (l₂ ++ l₁) = l₁ := by
  match l₂ with
  | [] => simp [LCO]
  | head :: tail =>
    match l₁ with
    | [] => rfl
    | head' :: tail' =>
      by_cases h : head' = head <;> simp [h, LCO, LCP]
      · rw [List.append_cons]
        exact lco_append_after_right
      · rw [← List.cons_append]
        exact lcs_append_after_right

@[simp] theorem lcs_append_after_left {l₁} : LCS (l₂ ++ l₁) l₁ = l₁ := by
  rw [lcs_comm]; exact lcs_append_after_right

@[simp] theorem lco_append_after_left {l₁} : LCO (l₂ ++ l₁) l₁ = l₁ := by
  rw [lco_comm]; exact lco_append_after_right

@[simp] theorem lcp_singleton_of_not_eq {a₁ a₂ : α} (h : a₁ ≠ a₂) : LCP [a₁] [a₂] = [] := by
  simp [LCP]; exact h

theorem lcp_append_left_distrib : {x : List α} →
    x ++ (LCP l₁ l₂) = LCP (x ++ l₁) (x ++ l₂)
  | [] => rfl
  | x :: xs => by simp [LCP]; exact lcp_append_left_distrib

theorem lco_append_left_distrib : {x : List α} →
    x ++ (LCO l₁ l₂) = LCO (x ++ l₁) (x ++ l₂)
  | [] => rfl
  | x :: xs => by simp [LCO]; exact lco_append_left_distrib

theorem lco_append_right_distrib {l₁ l₂ x : List α} : (LCO l₁ l₂) ++ x = LCO (l₁ ++ x) (l₂ ++ x) :=
  match l₁, l₂ with
  | [], [] => lco_self.symm
  | [], _ :: _ => lco_append_after_right.symm
  | _ :: _, [] => lco_append_after_left.symm
  | head :: tail, head' :: tail' => by
    simp [LCO]
    by_cases h : head = head' <;> simp [h]
    · exact lco_append_right_distrib
    · simp [LCS]
      have hr : x.reverse.reverse = x := List.reverse_reverse _
      rw [← hr, ← List.reverse_append, List.reverse_inj, lcp_append_left_distrib]
      simp

(The code here is just to "get the job done"; it's not a full treatment, and some names are wonky.)

[Thomas Murrills]

(I'm still not sure about the wedge-based operation, but I have to admit that I have my doubts.)

[Thomas Murrills]

Note, though, that both the longest common outfix and the wedge-based idea coincide on List Unit, and represent the min on natural numbers. I wonder if there's a (commutative) listified analogue of the max...?

[Wrenna Robson]

Well this is fun.