Defining a Finset in Lean4

Question

I am currently trying to define a finset (of a collection of finite images of some function).

More specifically, given a fixed mapping between the maximal chains of a partially ordered set (of which there are finitely many) to a list in another partially ordered set, I want to define a finset of these image lists. The final goal is to use Finset.sort to order the lists lexicographically. There are some lemmas and definitions that I have left in the full code at the bottom.

Given two partial orders P and A, where P is finite, we can define a map edgeLabeling from the edges of P to A. (a ⋖ b means a < b and there is no other element x such that a < x < b)

variable {P : Type*} [PartialOrder P] [Fintype P]

def edges (P : Type*) [PartialOrder P] : Set (P × P) := {(a, b) | a ⋖ b }

abbrev edgeLabeling (P A : Type*) [PartialOrder P] := edges P → A

Then, given some edge labeling, we can map the maximal chains of P to lists in A. (we have that maximalChains P is of type Finset (List P); and that edgePairs m is the list of the pairs of adjacent elements in the chain m)

abbrev chain (L : List P) : Prop := List.Chain' (· < ·) L

abbrev maximal_chain (L: List P) : Prop := chain L ∧ ∀ L' : List P, chain L' -> List.Sublist L L' -> L = L'

abbrev maximalChains (P : Type*) [PartialOrder P] [Fintype P] : Finset (List P) := Set.toFinset { L | maximal_chain L }

def mapMaxChain (l : edgeLabeling P A) (m : maximalChains P) : List A := List.map (fun e => l e) <| edgePairs m

Finally, what I want to do is to define the following as a Finset.

abbrev maxAChains (l : edgeLabeling P A) : Finset (List A) := Set.toFinset {mapMaxChain l L | L : maximalChains P}

Here is the full code, I apologise if it is convoluted:

import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Fintype.List
import Mathlib.Data.Set.Finite
import Mathlib.Order.Cover

noncomputable section

open List Classical
namespace List 

variable {P : Type*} [PartialOrder P] [Fintype P]

def adjPairs (α : Type*) : List α  → List (α × α)
  | [] => []
  | _ :: []  => []
  | a :: b :: l =>  ((a, b) : α × α) :: (b :: l).adjPairs

lemma adjPairs_cons {a b :α} {L : List α} : (a,b) ∈ (a::b::L).adjPairs:= by sorry

lemma adjPairs_tail {h a b : α} {tail : List α} : (a,b) ∈ tail.adjPairs → (a,b) ∈ (h::tail).adjPairs:= by sorry

def adjEPairs (L : List α) : List ({e : α × α  | e ∈ L.adjPairs}) := match L with
  | [] => []
  | _ :: [] => []
  | a :: b :: l =>  ⟨(a, b), List.adjPairs_cons⟩ :: (List.map (fun e => ⟨e.val, List.adjPairs_tail e.prop ⟩) <| List.adjEPairs (b :: l))

def edges (P : Type*) [PartialOrder P] : Set (P × P) := {(a, b) | a ⋖ b }

abbrev edgeLabeling (P A : Type*) [PartialOrder P] := edges P → A

abbrev chain (L : List P) : Prop := List.Chain' (· < ·) L

abbrev maximal_chain (L: List P) : Prop := chain L ∧ ∀ L' : List P, chain L' -> List.Sublist L L' -> L = L'

lemma chain_nodup {L : List P} (h : chain L) : L.Nodup := by sorry

lemma max_chain_mem_edge {P : Type*} [PartialOrder P] {L: List P} {e: P × P} : maximal_chain L →  e ∈ L.adjPairs → e ∈ edges P:= by sorry

instance : Fintype (Set.Elem { L : List P | L.Nodup }) := inferInstanceAs (Fintype { L : List P // L.Nodup })

instance : Fintype { L : List P | maximal_chain L } := Set.fintypeSubset { L : List P | L.Nodup} fun _ h ↦ Set.mem_setOf_eq.mpr (chain_nodup (Set.mem_setOf_eq.mp h).1)

abbrev maximalChains (P : Type*) [PartialOrder P] [Fintype P] : Finset (List P) := Set.toFinset { L | maximal_chain L }

def edgePairs {P : Type*} [PartialOrder P] [Fintype P] (L : maximalChains P) : List (edges P) := 
List.map (fun e => ⟨e.val, max_chain_mem_edge  (Set.mem_setOf_eq.mp (Set.mem_toFinset.mp L.prop))  e.prop⟩) <| L.val.adjEPairs

def mapMaxChain (l : edgeLabeling P A) (m : maximalChains P) : List A := List.map (fun e => l e) <| edgePairs m

abbrev maxAChains (l : edgeLabeling P A) : Finset (List A) := Set.toFinset {mapMaxChain l L | L : maximalChains P}

Answer 1

Working with subsets (possibly finite) of a type.

There are many ways in Lean to take about a subset of a Type.

Prop

You can describe a subset by a property. This works especially well if you are using that property as an assumption:

theorem foo {P : Type u} [PartialOrder P] (L : List P) (h : maximal_chain L) : ...

but is harder to work with when you need to talk about the set or type of objects having that property.

Subtypes (possibly using type class FinType)

If you have a prop p, you can turn it into a subtype with {x : A \\ p x}, or in your case { L : List P \\ maximal_chain L }. A subtype is a type that lives in Type u. An element of the subtype is a pair of two pieces of information, the value x.val and a proof x.prop that the property p holds of x.val.

So you can use the subtype as input combining (L : List P) (h : maximal_chain L) into just (m : MaximalChains P) where MaximalChains is the subtype of all maximal chains in P.

If your subtype is finite, you can prove this and register it as an instance of the typeclass FinType.

Subtypes are useful when you need a type. They are also easy to work with.

Set and FinSet

Alternately, you can use Sets and FinSets with {x : A \\ p x}. Unlike subtypes, they are not types (but can be coerced as we will see). They also don't exactly contain the information about p either.

If you use a Set or FinSet as a Type (as you often did in your code), it will coerce the set s to the subtype {x \\ x ∈ s}. This is close to the subtype {x \\ p x} but note there is a level of direction since x.prop is now x ∈ s.

You can also convert any type (including a subtype) to its corresponding maximal subset via Set.univ or FinSet.univ.

I personally would avoid Sets and Finsets when it isn't clear they are needed using a combination of Props and subtypes instead. These are easy to work with and go between.

Images

One setting where Sets and FinSets are important is with images. For the thing you are trying to do, you are constructing the image {mapMaxChain l L | L : maximalChains P}. While this isn't incorrect, Lean has special support for images on Set and FinSet. Importantly, if you use FinSet.image then you are guaranteed a FinSet as output. (If you think of Set or FinSet as a container like List, then you can view Set.image and FinSet.image as the analog of List.map.)

Solution

Putting it all together here is some code (with a few sorrys that you can fill in), starting at edges which replaces the FinSets with finite subtypes and solves your final construction with FinSet.image (using FinSet.univ to convert the Subtype to a FinSet).

I also was a bit more careful about the universes when it mattered (like when you have both P and A).

One could probably also do it leaving in the FinSets but I was having trouble and it didn't seem natural to me.

def Edges (P : Type u) [PartialOrder P] : Type u := { e : (P × P) // e.1 ⋖ e.2 }

abbrev EdgeLabeling (P A : Type u) [PartialOrder P] := (Edges P) → A

abbrev chain (L : List P) : Prop := List.Chain' (· < ·) L

abbrev maximal_chain (L: List P) : Prop := chain L ∧ ∀ L' : List P, chain L' -> List.Sublist L L' -> L = L'

def maxChainAdjPairToEdge {P : Type u} [PartialOrder P] {L: List P} {e: P × P} : maximal_chain L -> e ∈ L.adjPairs → Edges P := by sorry

abbrev MaximalChains (P : Type u) [PartialOrder P] : Type u := { L : List P // maximal_chain L }

instance (P : Type u) [PartialOrder P] [Fintype P] : Fintype (MaximalChains P) := sorry

def edgePairs {P : Type*} [PartialOrder P] (L : MaximalChains P) : List (Edges P) := 
L.val.adjEPairs.map (fun e => maxChainAdjPairToEdge L.prop e.prop)

def mapMaxChain {P A : Type u} [PartialOrder P] (l : EdgeLabeling P A) (m : MaximalChains P) : List A := (edgePairs m).map l

def maxAChains {P A : Type u} [PartialOrder P] [Fintype P] (l : EdgeLabeling P A) : Finset (List A) := Finset.image (mapMaxChain l) (Finset.univ : Finset (MaximalChains P))