Zulip Chat Archive

Stream: new members

Topic: adding simple conditions to hypothesis?


view this post on Zulip 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)?

view this post on Zulip Johan Commelin (May 19 2020 at 04:39):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 19 2020 at 04:40):

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

view this post on Zulip Lucas Viana Reis (May 19 2020 at 04:42):

Interesting, thanks!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 19 2020 at 05:04):

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

view this post on Zulip Mario Carneiro (May 19 2020 at 05:04):

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

view this post on Zulip Lucas Viana Reis (May 19 2020 at 05:05):

oh, ok. better to use subtypes then?

view this post on Zulip Mario Carneiro (May 19 2020 at 05:06):

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

view this post on Zulip Jalex Stark (May 19 2020 at 05:06):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 19 2020 at 05:07):

Totalize means return garbage out of the proper domain

view this post on Zulip Mario Carneiro (May 19 2020 at 05:07):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (May 19 2020 at 05:36):

finset is a structure

view this post on Zulip 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