adding simple conditions to hypothesis?

Stream: new members

[Lucas Viana Reis]

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]

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

[Johan Commelin]

But most of the time, I would just go for

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

[Johan Commelin]

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

[Lucas Viana Reis]

Interesting, thanks!

[Lucas Viana Reis]

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]

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]

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

[Mario Carneiro]

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

[Lucas Viana Reis]

oh, ok. better to use subtypes then?

[Mario Carneiro]

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

[Jalex Stark]

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

[Mario Carneiro]

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]

Totalize means return garbage out of the proper domain

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

finset is a structure

[Mario Carneiro]

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