Difficulty writing a type

Stream: new members

[Josiah Eldon Bills]

I have the following (simplified) situation:

import data.finset

constant e : Type

def m := e → ℕ
constant p : m → Prop

def v (a: subtype p) (b: e) := ((a: m) b ≠ 0)
def p2 (ms: finset m) := ∀a ∈ ms, p a

def c1 (ms: subtype p2) := finset {b: e // ∀a ∈ ms, v a b}
def c2 (ms: subtype p2) := finset {b: e // ∀a ∈ ms.1, v ⟨a, ms.2 a⟩ b}

Note that the constants (and all the names) are placeholders.

c1 and c2 are two attempts to write the same type. Neither of these is correct, but I cannot figure out how get what I want in a way that lean accepts.

The fundamental problem is that in order to pass a into v, I need a proof that a: subtype p. This data is encoded in ms: subtype p2, but any time I extract an element from ms.1, I lose track of the proof that that element satisfies p. I need a way to give a name not just to an element a, but also to the proof pr: a ∈ ms.1 so that I can pass it to ms.2. Alternatively, I would like to know if there is a simpler way of writing this type that is closer to what I wrote in c1.

Any ideas?

[Josiah Eldon Bills]

I just found def c2 (ms: subtype p2) := finset {b: e // ∀a, ∀g: (a ∈ ms.1), v ⟨a, ms.2 a g⟩ b}. This typechecks, but is still super verbose. Is there a nice, terse way to write this?

[Kevin Buzzard]

I'm finding it hard to imagine what your definitions are supposed to mean. c1 takes an input ms which is a subtype but you write a \in ms which only makes sense for subsets. Types and sets are very different things in lean. Can you describe mathematically what you're trying to define? "I need a proof that a : subtype p" makes no sense; that assertion isn't a proposition. My guess is that you're thinking set-theoretically in a type theory and this is what's causing the confusion rather than any inherent limitations of the system to express what you want to express.

[Yaël Dillies]

If you were talking about being a member of a finset, I would redirect you to docs#finset.attach, but here I'm really not sure what you want.

[Josiah Eldon Bills]

Ok, so m here represents an event driven model, and e here represents the type of events that the model consumes. For any model, there should be some events that are valid to pass it, and some that are not. This is what v represents. Given a finite set of models, I want the type of all finite sets of events such that every event is valid for all models in the set.

[Matt Diamond]

@Josiah Eldon Bills what does p represent here?

[Matt Diamond]

and is validity determined entirely by not returning 0 from m x?

[Matt Diamond]

like do you just want the type of finite sets of model functions that never return 0 for any input?

[Matt Diamond]

is this what you're looking for?

import data.finset.basic

constant event : Type
def model : Type := event → ℕ
def valid (m : model) (e : event) : Prop := m e ≠ 0

def valid_event_set (models : finset model) : Type :=
  { events : finset event // ∀ (e ∈ events) (m ∈ models), valid m e }

[Josiah Eldon Bills]

valid here is a placeholder for the actual condition. My non-minimal version has models returning an option (finset event × model_state), and a model returning none is to be interpreted as the model having a non-specific error processing the event.

My full model type is currently:

def model := model_state → event → nondeterminism → option (finset event × model_state)

p is an arbitrary predicate in my minimal case above, but in my more complete version it is

def deterministic (m: model) := ∀s: model_state, ∀n1 n2:nondeterminism, ∀e: event, m s e n1 = m s e n2
def all_deterministic (models: finset model) := ∀m ∈ models, deterministic m

The idea is that a nondeterminism is a pool of entropy that a model can pull from to change its behavior. A model is deterministic if this is irrelevant to its execution. all_deterministic model_set is the predicate "all models in model_set are deterministic". all_deterministic corresponds to p2 in my minimal example. subtype all_deterministic is "the type of all finite sets of deterministic models".

Your example doesn't work since models is not a subtype all_deterministic but rather is directly a finset model. subtype all_deterministic doesn't have ∈ defined on it, and even if it were to, the elements wouldn't necessarily have type subtype deterministic which valid requires.

[Matt Diamond]

I see, so are you saying that you want a finite set of this subtype of models? What about this:

import data.finset.basic

constant event : Type

def model : Type := event → ℕ
constant deterministic : model → Prop
def deterministic_model := subtype deterministic

def valid (m : model) (e : event) : Prop := m e ≠ 0

def valid_event_set (models : finset deterministic_model) : Type :=
  { events : finset event // ∀ (e ∈ events) (m ∈ models), valid (subtype.val m) e }

[Josiah Eldon Bills]

Ok, that isn't exactly what I want, but it is close (valid should take a deterministic_model). I think what had me hung up is I was trying to use a subtype of a finset, where you suggest using a finset of a subtype.

[Matt Diamond]

well, I have to admit that I'm not exactly an expert in Lean (just a software engineer who likes math) but it makes more sense to me as a programmer to have the subtype focused on the objects, not the sets

[Matt Diamond]

I just naturally conceptualize it as "there's an object of a certain type, and you have a set of them"

[Matt Diamond]

anyone more experienced than me is free to chime in! :)

[Matt Diamond]

I think I can put it a bit more concretely: if you have the subtype on the set, that means if you pass around objects from it, those objects don't have the context of the subtype... it's better to have that information closer to the data, so to speak

[Kevin Buzzard]

@Josiah Eldon Bills "a subtype of a finset" doesn't make sense because a finset is a term, not a type.

[Josiah Eldon Bills]

Correction, I meant a subtype of finset, not a finset. I think there should be a map and a theorem of the following form (don't quite know how to fully define it yet):

import data.finset

universe u
def subtype_finset_to_finset_subtype {α: Type u} {q: α → Prop} (st: {f: finset α // ∀a ∈ f, q a}) : finset (subtype q) := sorry
theorem subtype_finset_to_finset_subtype_bijective (α: Type u) (q: α → Prop) : function.bijective (@subtype_finset_to_finset_subtype α q) := sorry

[Junyan Xu]

There is docs#multiset.pmap but for finsets it seems you have to use docs#finset.attach + docs#finset.map

[Matt Diamond]

(deleted)

[Matt Diamond]

nvm, misunderstood what the issue was

one other idea would be to refactor whatever is giving you a subtype of finset into something that gives you a finset of the subtype... but if that refactor isn't feasible, then Junyan's solution should work

[Matt Diamond]

@Junyan Xu would docs#finset.subtype be helpful here?

[Matt Diamond]

actually that's probably overkill since filter is unnecessary here... but looking at the source code might be instructive