easier way to define subtype by restricting constructors?

Stream: new members

[Malvin Gattinger]

I am wondering if there is an easier way to define redStuff in the below, saying "give me the subtype which only uses this subset of type constructors"?

inductive stuff : Type
| red : stuff
| blue : stuff
| inside : stuff -> stuff

open stuff

def onlyRed : stuff -> Prop
| red := true
| blue := false
| (inside s) := onlyRed s

def redStuff := subtype onlyRed

[Alex J. Best]

You could use an inductive Prop instead, which saves you a case

inductive stuff : Type
| red : stuff
| blue : stuff
| inside : stuff -> stuff

open stuff

inductive onlyRed : stuff -> Prop
| red : onlyRed red
| inside {s : stuff} : onlyRed s → onlyRed (inside s)

def redStuff := subtype onlyRed

[Malvin Gattinger]

ah, did not know that before - let me try it out :-)

[Patrick Johnson]

def redStuff := {s : stuff // ∃ n, s = (inside^[n]) red}

[Malvin Gattinger]

Hehe, this also looks nice, and works for my toy example, but in my non-mwe I have an "inside" that takes a list of previous "stuff".

[Malvin Gattinger]

Many thanks to both of you! I managed to write what I wanted for my real use-case, a definition of open and closed tableaus :+1:

inductive tableau : finset formula → Type
| byRule {α : finset formula} { B : finset (finset formula) } : (rule α B) → (∀ β ∈ B, tableau β) → tableau α
| isOpen {α : finset formula} : (¬ ∃ B : finset (finset formula), ∃ r : rule α B, true) → tableau α

inductive isClosedTableau { α B } : tableau α -> Prop
| byRule { r : rule α B } { prev : (∀ β ∈ B, tableau β) } :
    (∀ b, isClosedTableau b)  → isClosedTableau (tableau.byRule r prev)

def closedTableau { α B } := subtype (@isClosedTableau α B)

[Malvin Gattinger]

Hm, it compiles but maybe is not what I wanted. Now I cannot write "closedTableau α" analogous to "tableau α" to indicate the subtype of closed tableaus for that finset. Is there a way to make α explicit but B still implicit? :thinking: