Finite sets with named elements

Stream: Is there code for X?

[Nathaniel Virgo]

Is there a way to create a finite set along with an identifier for each element?

My use case is creating examples for chemical reaction networks and related things. The goal is to have a nice neat syntax for examples, so that I can introduce example networks and then prove things about them.

Here's some code to show what I mean:

import Mathlib.Tactic -- for `deriving Fintype`

structure ReactionNetwork where
  species : Type
  [species_finite : Fintype species]
  reactions : Finset ((Multiset species) × (Multiset species))

section

inductive exampleSpecies where
  | H₂ | O₂ | H₂O | CH₄ | CO₂
  deriving DecidableEq, Fintype

open exampleSpecies

def exampleNetwork : ReactionNetwork where
  species := exampleSpecies
  reactions := {
    ⟨ {H₂, H₂ , O₂}, {H₂O, H₂O} ⟩,
    ⟨ {CH₄, O₂, O₂}, {CO₂, H₂O, H₂O} ⟩
  }

end

It shouldn't be hard to improve the way reactions are presented, but it's cumbersome to introduce a name for the set of species, exampleSpecies in this case. It would be much nicer if the example would look more like

def exampleNetwork : ReactionNetwork where
  species := FiniteSet { H₂ , O₂ , H₂O , CH₄ , CO₂ }
  reactions := {
    ⟨ {H₂, H₂ , O₂}, {H₂O, H₂O} ⟩,
    ⟨ {CH₄, O₂, O₂}, {CO₂, H₂O, H₂O} ⟩
  }

where the species type is introduced anonymously, along with identifiers for all of its elements. Is something like this possible to achieve? I don't mind if it means making the type of species different, as long as I'll be able to reason about it as a finite set.

[Riccardo Brasca]

You are probably looking for enumerated types.

[Nathaniel Virgo]

Isn't that what I already have in the example?

[Riccardo Brasca]

Oh sorry, admittedly I only read the first sentence.

[Jakub Nowak]

By FiniteSet you mean docs#Finset? That might be #xy problem. What's wrong with your first code, why do you need FiniteSet? You can use docs#Finset.univ to obtain elements of exampleSpecies as a docs#Finset.

[Nathaniel Virgo]

I don't mean Finset, since that's a finite subset of a type. I just mean a finite type, so Fin n for some n, or anything equivalent to it.

The problem with my first code example is that the syntax is cumbersome. I have to introduce a name, exampleSpecies, just to define the set of species. I'd rather write code that looks like the second example.

There's nothing wrong with the first example semantically, but I don't like the syntax, because it forces me to define a separate type for the set of species when logically it's part of the reaction network, not an independent type. This is boilerplate that needs to be copied for each example, and I'd rather avoid that.

It's not really a big issue, but I figured it might be possible, because Lean's syntax is so flexible.

[Nathaniel Virgo]

The second example could be written as

def exampleNetwork : ReactionNetwork where
  species := Fin 5
  reactions := {
    ⟨ {0, 0, 1}, {2, 2} ⟩,
    ⟨ {3, 1, 1}, {4, 2, 2} ⟩
  }

I'm asking for code that works exactly like that, except that you can give the elements names to make it more readable.

[Jakub Nowak]

If you use Fin 5 that you could also do H₂ + H₂, which you probably wouldn't want to.

[Nathaniel Virgo]

Fair enough - that's another reason to want a finite set where the elements aren't numbers.

[Jakub Nowak]

So a new type is exactly what you want. And afaik Lean doesn't have syntax for anonymous enums (nor for anonymous structs), so you need to name this enum. You can name it exampleNetwork_species to make the relation more obvious.

[Nathaniel Virgo]

Sure - my original question could be phrased as "does Lean have anonymous enums?" - my examples were just meant to demonstrate a use case for them.

[Robin Arnez]

Something like this?

import Mathlib.Tactic -- for `deriving Fintype`

structure ReactionNetwork where
  species : Type
  [species_finite : Fintype species]
  reactions : Finset ((Multiset species) × (Multiset species))

open Lean Meta Elab Term Command
elab "declare_enum% " "{" names:ident,* "}" : term => do
  let name ← mkAuxDeclName `enum
  let name : Ident := mkIdent (`_root_ ++ name)
  let cmd : Syntax.Command ← `(inductive $name:ident where $[| $names:ident]* deriving DecidableEq, Fintype)
  liftCommandElabM (elabCommand cmd)
  elabTerm name none

def exampleNetwork : ReactionNetwork where
  species := declare_enum% { H₂, O₂, H₂O, CH₄, CO₂ }
  reactions := {
    ⟨ {.H₂, .H₂ , .O₂}, {.H₂O, .H₂O} ⟩,
    ⟨ {.CH₄, .O₂, .O₂}, {.CO₂, .H₂O, .H₂O} ⟩
  }

[Nathaniel Virgo]

That seems to do it! I'll try using it.