where is `AddMonoid` in Lean?

Stream: general

[Asei Inoue]

I have written such a proof recently:

open Lean Lean.Grind

@[grind =]
theorem sum_append_singleton {α : Type} {l : List α} {x : α} [AddCommMonoid α] :
    (l ++ [x]).sum = l.sum + x := by
  induction l with grind [AddCommMonoid.add_assoc, AddCommMonoid.add_zero, AddCommMonoid.zero_add]

but this theorem needs commutativity?
I think this theorem still holds on additive monoid.
But where is additive monoid in Lean (not mathlib)?

[Kenny Lau]

It seems like you're trying to treat the grind library like mathlib? I'm a bit confused by your intentions here.

[Asei Inoue]

whole proof is here:

import Std.Tactic.Do

def belowZero (operations : List Int) : Bool := Id.run do
  let mut balance := 0
  for op in operations do
    balance := balance + op
    if balance < 0 then
      return true
  return false

namespace List

variable {α : Type}

def HasPrefix (P : List α → Prop) (l : List α) : Prop := ∃ n, P (l.take n)

theorem hasPrefix_iff {P : List α → Prop} {l : List α} :
    l.HasPrefix P ↔ ∃ n, P (l.take n) := by
  simp [HasPrefix]

@[simp, grind =]
theorem hasPrefix_nil {P : List α → Prop} : [].HasPrefix P ↔ P [] := by
  simp [hasPrefix_iff]

@[simp, grind =>]
theorem hasPrefix_of_nil {P : List α → Prop} {l : List α} (h : P []) : l.HasPrefix P := by
  exists 0

@[simp, grind =>]
theorem hasPrefix_of_all {P : List α → Prop} {l : List α} (h : P l) : l.HasPrefix P := by
  exists l.length
  simpa

@[grind =]
theorem hasPrefix_cons {P : List α → Prop} {a : α} {l : List α} :
    (a :: l).HasPrefix P ↔ P [] ∨ l.HasPrefix (fun l' => P (a :: l')) := by
  constructor
  · intro ⟨n, hn⟩
    by_cases nzero : n = 0
    · simp_all
    · right
      exists n - 1
      suffices a :: take (n - 1) l = take n (a :: l) from by
        simp_all
      grind [take_cons]
  · rintro (h | ⟨⟨n, hn⟩⟩)
    · grind
    · exists n + 1

@[grind =]
theorem hasPrefix_append {P : List α → Prop} {l l' : List α} :
    (l ++ l').HasPrefix P ↔ l.HasPrefix P ∨ l'.HasPrefix (fun l'' => P (l ++ l'')) := by
  induction l generalizing P with grind

open Lean Lean.Grind

@[grind =]
theorem sum_append_singleton {α : Type} {l : List α} {x : α} [AddCommMonoid α] :
    (l ++ [x]).sum = l.sum + x := by
  induction l with grind [AddCommMonoid.add_assoc, AddCommMonoid.add_zero, AddCommMonoid.zero_add]

end List

open Std.Do

set_option mvcgen.warning false

theorem belowZero_iff {l : List Int} : belowZero l ↔ l.HasPrefix (fun l => l.sum < 0) := by
  generalize h : belowZero l = res
  apply Id.of_wp_run_eq h
  mvcgen invariants
  · Invariant.withEarlyReturn
    (onContinue := fun xs bal => ⌜bal = xs.prefix.sum ∧ ¬ xs.prefix.HasPrefix (fun l => l.sum < 0)⌝)
    (onReturn := fun r bal => ⌜r = true ∧ l.HasPrefix (fun l => l.sum < 0)⌝)
  with grind

[Robin Arnez]

docs#Lean.Grind.AddCommMonoid is considered a grind internal class, in other words, don't use it for anything that's not grind-related (such as a sum_append_singleton theorem). There is no Lean.Grind.AddMonoid because grind doesn't support anything below AddCommMonoid right now. If you need an algebraic hierarchy, use mathlib. If you don't want mathlib though you can simply use the existing Std property classes (e.g. docs#Std.Associative, docs#Std.LawfulIdentity):

theorem sum_append_singleton {α : Type u} {l : List α} {x : α}
    [Add α] [Zero α] [@Std.Associative α (· + ·)] [@Std.LawfulIdentity α (· + ·) 0] :
    (l ++ [x]).sum = l.sum + x := by
  induction l with simp_all <;> ac_rfl

[Asei Inoue]

@Robin Arnez Thank you, Robin! Std.LawfulIdentity is what I want!