type constraints

Stream: new members

[Henning Dieterichs]

I have a type T and a fixed predicate P: T -> Prop. Can I make a type X, so that x: X implies x: T and P(x)?

I guess composition can be used to achieve that, but I would need to use x.t to get the underlying T:

def T: Type := ℕ → ℕ
def P : T → Prop
| f := (∀ n: ℕ, (f n < n))

structure X := mk :: (t : T) (prop : P(t))
def foo : ∀ x: X, x.t 10 < 10 := sorry

Are there ways so that X is automatically casted to T?
I don't feel type classes help much, compared to just requiring P as hyptothesis.

class X (t: T) := (prop: P t)
def foo { x: T } [X t] : x 10 < 10 := sorry

Can I somehow state { x: X } and obtain { x: T } [X t]?

[Johan Commelin]

I think you are looking for subtypes: {x : T // P x}

[Adam Topaz]

Checkout subtype P

[Johan Commelin]

Or, without notation subtype P.

[Johan Commelin]

Henning Dieterichs said:

I have a type T and a fixed predicate P: T -> Prop. Can I make a type X, so that x: X implies x: T and P(x)?

You cannot have x : X implies x : _. A term has 1 type (up to definitional equality). Also, you cannot prove that x has type X or type T. It can only be checked by the type checker.

[Henning Dieterichs]

Thanks, subtype is exactly what I was looking for!