Type-theoretic way of dealing with types being finite?

Stream: new members

[Tim Baccaert]

Hi, so I'm pretty new to Lean and I've made my way through most of the introductory material (i.e., Theorem Proving in Lean and Mathematics in Lean). I'm trying to encode the relational model (https://en.wikipedia.org/wiki/Relational_model) into Lean, and I'm running into some issues:

So let's say I have a database schema (you can think of this like a structured excel table where columns are given names):

• Movie [ title, director, actor, rating ]
• Location [ theater, address, phone ]
  A possible entry into the Movie relation could be:

| title | director | actor | rating |
|-------|----------|-------|--------|
| "Foo" | "Bar"    | "Baz" | 5      |

Formally, the way this is usually defined (c.f., http://webdam.inria.fr/Alice/pdfs/all.pdf, page 34) is by defining some infinite sets Rel, Att and Dom which are disjoint from one another. The first set defines names of relations, the second attributes, and the third "constants" (i.e., types of values are 'erased'). A relation in Rel is associated with a (partial) function sort : Rel -> finite_powerset(Att), which maps a relation to a finite set of attributes. Typically sort(R) for some relation name R is referred to as the relation schema. A record (or tuple) over some relation schema U is a total function from U to Dom.

I modeled this into Lean as follows:

inductive Rel where
  | movie
  | location

inductive Att where
  | title
  | director
  | actor
  | rating
  | theater
  | address
  | phone

def type : Att → Type
  | Att.title => String
  | Att.director => String
  | Att.actor => String
  | Att.rating => Nat
  | Att.theater => String
  | Att.address => String
  | Att.phone => String

def sort : Rel → Type
  | Rel.movie => { a : Att // a = Att.title ∨ a = Att.director ∨ a = Att.actor  ∨ a = Att.rating}
  | Rel.location => { a : Att // a = Att.theater ∨ a = Att.address ∨ a = Att.phone }

def MovieRecord : Type := (att : sort Rel.movie) → type att.val
def LocationRecord : Type := (att : sort Rel.location) → type att.val

The main difference here is that I still care about types, i.e., I do not throw all values into a single type/set called "Dom".

The issue I have here is that the subtypes as the output of the function sort are kind of a pain to work with; and I do not really see how I can create concrete "records" that are of the type MovieRecord or LocationRecord. Ideally, I want some sort of "partial function" that takes in a subset of the attributes in Att and assigns them to concrete values of type type att for that specific att.

I can see like, one way in which I could model this but it is super annoying to write proofs with: I can model records as (att : Att) -> Option (type att) or (att : Att) -> Part (type att) but then I do not have the ability to "statically" check whether a tuple has all the right attributes defined. Also the "easy" way would be to model a schema by a single inductive type and have each "relation schema" be a single variant in the type, but then I do not have the ability to actually express properties over just attributes or the type of a specific attribute, and I do need the ability to express proofs using that as a notion.

How do you usually deal with these types of issues in Lean? Is there like a "type theory"-ish way to deal with finite-ness? I have seen some things like Fin or the typeclass Finite in Mathlib but this has not really clicked for me.