## Stream: new members

### Topic: adding simple conditions to hypothesis?

#### Lucas Viana Reis (May 19 2020 at 04:36):

Hi, I'm new to Lean and not sure if there is a more straightforward way to introduce an extra condition on hypothesis like (a : int, a ≠ 0), instead of defining a new type e.g. int_star and writing it like (a : int_star)?

#### Johan Commelin (May 19 2020 at 04:39):

@Lucas Viana Reis You can use subtypes: (a : {n : int // n ≠ 0}).

#### Johan Commelin (May 19 2020 at 04:39):

But most of the time, I would just go for

lemma foobar (a : int) (h : a ≠ 0) : my statement := sorry


#### Johan Commelin (May 19 2020 at 04:40):

That is probably easier at the point where you want to use it.

#### Lucas Viana Reis (May 19 2020 at 04:42):

Interesting, thanks!

#### Lucas Viana Reis (May 19 2020 at 04:52):

Because of course "a number different than 0" is the same as having a number and a proof it is different than zero. It is indeed more useful this way, I just didn't though of it.

#### Lucas Viana Reis (May 19 2020 at 05:03):

How would this idea work with \exists? Define a set A as cool iff ∃(a : nat), A = foobar a h , where foobar (a : nat) (h : a ≠ 0) is a set

#### Mario Carneiro (May 19 2020 at 05:04):

you can say \exists a h, A = foobar a h

#### Mario Carneiro (May 19 2020 at 05:04):

(that said, we try to discourage the use of such "partial functions" to create data)

#### Lucas Viana Reis (May 19 2020 at 05:05):

oh, ok. better to use subtypes then?

#### Mario Carneiro (May 19 2020 at 05:06):

It depends a lot on the application, but we try to totalize when possible

#### Jalex Stark (May 19 2020 at 05:06):

totalize means extend the domain and fill in with garbage? or shrink the source type?

#### Mario Carneiro (May 19 2020 at 05:06):

If the subtype makes sense as a structure with its own suite of operations, it also makes sense to hide the subtype behind a definition and then use that

#### Mario Carneiro (May 19 2020 at 05:07):

Totalize means return garbage out of the proper domain

#### Mario Carneiro (May 19 2020 at 05:07):

or ideally, the least garbage-like garbage you can find

#### Mario Carneiro (May 19 2020 at 05:09):

nat subtraction being an example of this: nat.sub : nat -> nat -> nat even though it isn't "defined" for all inputs; when the inputs don't make sense, that is, a < b, then a - b = 0

#### Mario Carneiro (May 19 2020 at 05:10):

An example of a subtype behind a definition is vector A n, the subtype of list A of length n, or finset A, the subtype of multiset A with no duplicates

#### Yury G. Kudryashov (May 19 2020 at 05:36):

finset is a structure

#### Mario Carneiro (May 19 2020 at 06:06):

true, but it doesn't make too much difference once it's behind a definition. subtype is also a structure, of course

Last updated: May 14 2021 at 07:19 UTC