inductive set in Lean

Stream: lean4

[Stepan Holub]

Hello,
I am wondering whether Lean has some automation for inductive definitions. I have in mind something like inductive-set in Isabelle where the definition produces automatically a bunch of useful theorems about cases, and (structural) induction.

[Adam Topaz]

When you create an inductive type, a few additional declarations are automatically added to the environment as well. If you can give a concrete example of something you're looking for, that would help answer your question.

[Stepan Holub]

I am trying to define a submonoid generated by a given set inductively (two conditions: unit is included, and the set is closed under the multiplication by an element from the generating set, say, from the left).
I expect Lean to generate for me the structural induction theorem based on that definition alone.

[Adam Topaz]

import Mathlib

variable {M : Type*} [Monoid M] (S : Set M)

inductive genSubmonoid : Set M where
  | of (m : M) : m ∈ S → genSubmonoid m
  | mul {m n : M} : genSubmonoid m → genSubmonoid n → genSubmonoid (m * n)
  | one : genSubmonoid 1

#check genSubmonoid.rec

[Adam Topaz]

you can see all the things that were added automatically using #print prefix genSubmonoid

[Adam Topaz]

or using whatsnew

[Adam Topaz]

I.e.

import Mathlib.Init.Set
import Mathlib.Algebra.Group.Defs
import Mathlib.Tactic

variable {M : Type*} [Monoid M] (S : Set M)

whatsnew in
inductive genSubmonoid : Set M where
  | of (m : M) : m ∈ S → genSubmonoid m
  | mul {m n : M} : genSubmonoid m → genSubmonoid n → genSubmonoid (m * n)
  | one : genSubmonoid 1

[Stepan Holub]

Thank you very much. That is what I was looking for.

A side remark on my motivation: in Mathlib.Algebra.Group.Subgroup.Basic they say

There are also theorems about the subgroups generated by an element or a subset of a group, defined both inductively and as the infimum of the set of subgroups containing a given element/subset.

and I could not find the promised inductive definition (it was perhaps removed as redundant, since the induction principle follows easily from the infimum?)

[Adam Topaz]

the definition is in terms of an infimum, but there should be an induction principle proved for that definition. Let me look for it.

[Adam Topaz]

Here you go: Submonoid.closure_induction

[Adam Topaz]

There should be analogous statements for subgroups, etc.

[Stepan Holub]

Yes, thank you. I am aware of the Submonoid.closure_induction theorem.

My point was not the induction theorem itself, but rather a general way of obtaining such theorems. In this case, it is interesting that the induction theorem is (easily) proved using the infimum definition, (specifically closure_le, rather than by something like genSubmonoid.rec produced by your inductive definition above (and which is very instructive)

[Adam Topaz]

The general way of obtaining such theorems is by using Galois insertions (which is more-or-less closure_le itself).

[Adam Topaz]

Whenever you have a Galois insertion, you can define such a "closure" operator, which will end up being the analogue of the infimum definition.