4 ms·

There are lots of missing bits here. For instance, you seem to assume that a = sign(a) * abs(a). Why? And both sign and abs are not defined. So you say abs(a)

There are lots of missing bits here. For instance, you seem to assume that a = sign(a) * abs(a). Why? And both sign and abs are not defined. So you say abs(a) >= 0 and sign(a) \in {-1, 1}. Why? For instance, what is sign(0)? Are you assuming a construction of integers from the natural numbers such that for any n < 0, there is an integer abs(n) and n = -1 * abs(n)? If so, don't you need to include that (or at least reference it)? Later you assume that all integers are even or odd. Why? These are niggling details that don't matter when you have chalk in hand, but do matter when speaking to a system like lean4.

olivierduval 2y ago
You're right that a lot that is "usually defined" in math has to be explicitly defined in theorem prover/proof assistant * abs(x) is usually defined as "x if x >=0 and -x if x < 0" * sign(x) is usually defined as "1 if x >=0 and -1 if x < 0" * with these definitions, it follows that for any x, x = sign(x) * abs(x) (by definition applied for each cases >=0 and <0, assuming that all integer are either >=0 or <0) Showing that any integer is either even or odd seem less obvious