subsets inductive type parameter

Stream: new members

[Simon Daniel]

Hi all,
im trying to declare this inductive type I

inductive I (set: Finset α) where
| A: I set
| B: (subset ⊆ set) -> I subset -> I set

that can nest subsets via the .B constructor. Trying to do this seems conceptually wrong because the type parameter has to match set. Maybe someone can out why this would not work and what to do instead :)

[Edward van de Meent]

the problem is that while defining a (dependent) inductive lean does't know about what I subset means. it only knows I set.

[Edward van de Meent]

what is the structure you want to capture?

[Edward van de Meent]

if i understand correctly, some sort of list of sets which are ordered by inclusion?

[Simon Daniel]

one constructor is supposed to contain a expression built out of elements from the set. the other constructor is supposed to allow expressions on a subset of these elements.
Something like
(1+2) can be of type I {1,2} but also I {1,2,3,...}
maybe it is more like type casting?

[Edward van de Meent]

i don't think that an inductive type is what you're looking for then...

[Edward van de Meent]

could you maybe give more detail about how you're (planning on) storing expressions?

[Edward van de Meent]

or tell more generally what kind of project this is for?

[Edward van de Meent]

because this is probably an #xy problem

[Daniel Weber]

inductive I : Finset α → Type u where
| A: (set : Finset α) → I set
| B: (subset set : Finset α) → (h : subset ⊆ set) → I subset → I set

works, but I agree that this seems like a possible xy

[Simon Daniel]

i try to strip down my problem, this is what (i think) I want to accomplish:

inductive I (set: Finset α) where
| Broadcast: (caster: Finset α) -> Nat@caster -> I set -> I set -- @ means only accessible to caster node
| Sub  {subset: Finset α}: (subset ⊆ set) -> I subset set -> I set
| End: I set

The genereall problem is, that i want to model a program that operates on set of nodes (Finset α).
Nodes can broadcast to all nodes in the set.
There are some cases where subprograms only operate on a subset of nodes and should not broadcast to everyone (that is what i try to do via the .Sub constructor).