Zulip Chat Archive

Stream: new members

Topic: type constraints


view this post on Zulip Henning Dieterichs (Nov 02 2020 at 12:40):

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]?

view this post on Zulip Johan Commelin (Nov 02 2020 at 12:42):

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

view this post on Zulip Adam Topaz (Nov 02 2020 at 12:43):

Checkout subtype P

view this post on Zulip Johan Commelin (Nov 02 2020 at 12:43):

Or, without notation subtype P.

view this post on Zulip Johan Commelin (Nov 02 2020 at 12:45):

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.

view this post on Zulip Henning Dieterichs (Nov 02 2020 at 12:55):

Thanks, subtype is exactly what I was looking for!


Last updated: May 18 2021 at 16:25 UTC