Automatically generate Equiv from enum to Fin n

Stream: lean4

[Jesse Slater]

Is there a way that I can automatically generate an Equiv between a finite inductive enum with n elements and Fin n? For example :

inductive α where
  | a
  | b
  | c

open α

def αEquiv : α ≃ (Fin 3) := {
  toFun :=
    λ | a => 0
      | b => 1
      | c => 2

  invFun :=
    λ | 0 => a
      | 1 => b
      | 2 => c

  left_inv := by
    unfold Function.LeftInverse
    aesop

  right_inv := by
    unfold Function.RightInverse Function.LeftInverse
    aesop
}

The goal is to be able to create any finite inductive type and then automatically generate the obvious equivalence so that I can index a vector by meaningful names.

I would also be open to some other way of indexing a vector by meaningful names, this is just the first idea I came up with to achieve that.

[Kyle Miller]

It's not the most efficient approach here, but mathlib4#3198 has a term elaborator named proxy_equiv% that generates an equivalence between a non-recursive inductive type (like your enum type) and some simple type. There should be enough FinEnum instances in mathlib to use this to derive a likely-not-efficient equivalence to Fin 3.

[Kyle Miller]

I can also point you to the DecidableEq derive handler in Lean 4, which for enum types generates the invFun for you. The toFun is already called toCtorIdx and is generated by Lean automatically.

[Kyle Miller]

That derive handler generates ofNat and ofNat_toCtorIdx, which you can make use of if you add deriving DecidableEq after your inductive type.

[Eric Wieser]

docs4#FinEnum is the class for precisely this, right? (Though you'd need to implement the instance for it)

[Eric Wieser]

Why do you need Fin 3 at all though if your intent is to index with meaningful names? You can just use α →ℝ directly

[Jesse Slater]

Thanks, FinEnum looks great. When you say use α →ℝ directly, is the idea to get rid of the vectors entirely? I might be able to do that, but I am using some vector functions which I don't know how to replace. How would I do Vector.map and Vector.toList if I was working with functions instead of vectors?

[Eric Wieser]

What do you mean by "vector"? I assumed you mean Fin 3 → ℝ...

[Eric Wieser]

Vector.map is just composition

[Eric Wieser]

toList requires the equivalence you asked for because you need to choose an order for your elements

[Jesse Slater]

By vector, I mean Mathlib.Data.Vector. I am using vectors of nats. I probably should have made that more clear. It is possible that I could just use Fin n -> Nat, or α -> Nat but this seemed more intuitive to me. The reason I am using vectors is that I am doing entry wise operations with multiple vectors, so I need to make sure they have the same number of elements.
Here are all of the operations I think I need:

Entry wise operations on multiple vectors
Appending vectors together to get longer ones, but maintaining my useful names
Iterating over the elements of a vector, as in foldl

It is not immediately obvious to me how I would do those using the α -> Nat strategy, but I am sure there is a way.

[Mario Carneiro]

Aren't most of those operations already implemented over Fin n -> A vectors? It is used for vectors / matrices

[Mario Carneiro]

Mathlib.Data.Vector is not used much in mathlib

[Jesse Slater]

Where should I look for the functions for Fin n -> A? My problem is that I am very new to Lean, and everything I know is from reading the books and searching mathlib, so I never know if I am missing something. Mathlib.Data.Vector is just the first thing that came up when I was searching for a vector.

[Mario Carneiro]

Vector3 is used more IIRC, but it is still being ported in mathlib4 (there is an open PR about it)

[Mario Carneiro]

it will be easier to peruse the state of things in mathlib3

[Trebor Huang]

As a related thing, what about automatically generating Equiv from structures to nested Sigma types?

[Kyle Miller]

@Trebor Huang Take a look at mathlib4#3198, which gives a term elaborator (proxy_equiv%) for exactly that.

[Kyle Miller]

Eric Wieser said:

docs4#FinEnum is the class for precisely this, right? (Though you'd need to implement the instance for it)

That was what I was suggesting with using proxy_equiv% and relying on FinEnum instances, since it'd be a way to implement that instance automatically.

Just to show what I meant with the other suggestion, I'll post the code here (although it looks like this might not be useful for Jesse).

import Mathlib.Logic.Equiv.Basic
import Mathlib.Tactic.IntervalCases
import Mathlib.Data.FinEnum

inductive α where
  | a
  | b
  | c
  deriving DecidableEq

open α

def αEquiv : α ≃ Fin 3 where
  toFun x := ⟨α.toCtorIdx x, by cases x <;> simp⟩
  invFun x := α.ofNat x
  left_inv := α.ofNat_toCtorIdx
  right_inv := by
    intro ⟨x, h⟩
    interval_cases x <;> rfl

instance : FinEnum α where
  card := 3
  Equiv := αEquiv