I want to use induction on an integer variable, doing an inductive step both in the positive and negative direction.
Consider the following theorem (for demonstration, no matter if it makes sense):
theorem exmpl (x : ℤ) : (x = 5):=
begin
induction x,
-- inductive steps
end
which produces in Leans tactic state:
case int.of_nat
x: ℕ
⊢ int.of_nat x = 5
case int.neg_succ_of_nat
x: ℕ
⊢ -[1+ x] = 5
Reasonably, the induction produces two cases, one for the positive and one for the negative direction. But what also happens is that x has now become a natural number and in the goals it changed to int.of_nat x and -[1+ x].
As my induction operates inside of the integers, I would assume that those types are some kind of „subset“ of them, presumably having more useful properties than integers. The Lean Reference states that the second one seems to be „an implicit argument that should be inferred by type class resolution”, without explaining further what that means.
While this conversion is probably necessary for certain applications, in my use case I just want to continue working with integers and have not found a good way to convert the goals back to using integers.
So my questions are:
x was converted to, what do they mean and why does the conversion make sense?The induction tactic in Lean uses an induction principle based on the definition of the type. For the natural numbers, this induction principle is the well known one. For the integers, the definition is slightly non intuitive and gives a not very useful induction principle.
In Lean the integers are defined as the disjoint union of two copies of the natural numbers. This gives you two functions from nat to int, the canonical embedding sending n to n, and another map sending n to -(n + 1). Every integer is uniquely of the form n or -(n + 1) for n a natural number, and the induction principle for integers basically considers these two cases, which is not that useful. In Lean these two maps nat to int are called int.of_nat and int.neg_succ_of_nat, and -[1+ x] is notation for int.neg_succ_of_nat.
So although induction turned x into a natural number, int.of_nat x and -[1+ x] are still both integers.
If you want a more useful way of inducting on integers you could use the theorem int.induction_on defined in data.int.basic in mathlib https://leanprover-community.github.io/mathlib_docs/data/int/basic.html You might be able to use this by importing this file (there are docs about imstalling and importing mathlib files on the mathlib website) and using induction x using int.induction_on (this method doesn't always work) or something like apply int.induction_on x or refine int.induction_on x _ _ _ might also work.
It's also worth mentioning that it's fairly rare to use induction when working with integers in Lean and mostly you just use the library theorem to prove most of what you want.