Bounded int

Stream: Is there code for X?

[Bjørn Kjos-Hanssen]

To get computable decidability instances for statements involving bounded integers, is there a convenient way?
For example, a type FinInt b representing -b,...,b that was recognized as decidable would be good.

The following solution is too kludgy when dealing with vectors of bounded ints.

To remove noncomputable here...

noncomputable instance : Decidable (∀ x : ℤ, abs x < 7 → x = x) := by
  exact Classical.dec (∀ (x : ℤ), |x| < 7 → x = x)

... just make the statement for positive and negative numbers separately:

instance : Decidable (∀ x : ℕ, x < 7 → (-x:ℤ) = -x ∧ (x:ℤ) = (x:ℤ)) :=
  Nat.decidableBallLT 7 fun x h ↦ (-x:ℤ) = -x ∧ (x:ℤ) = (x:ℤ)

[Yaël Dillies]

You can use decidable_of_iff (∀ x ∈ Finset.Icc (-7 : ℤ) 7, x = x) your_proof

[Kyle Miller]

import Mathlib

instance {n : ℤ} {p : ℤ → Prop} [DecidablePred p] : Decidable (∀ x : ℤ, abs x < n → p x) :=
  decidable_of_iff (∀ x ∈ Finset.Ioo (-n) n, p x) <| by simp [abs_lt]

#synth Decidable (∀ x : ℤ, abs x < 7 → x = x)
-- succeeds

[Bjørn Kjos-Hanssen]

Nice. And it works with vectors too, like

instance : Decidable (∀ x : Vector (Finset.Icc (-7:ℤ) 7) 3,  x = x) := by exact
  Fintype.decidableForallFintype

[Kyle Miller]

If #synth succeeds, you do not need to write an instance for it.

Both of these succeed:

#synth Decidable (∀ x : Vector (Set.Icc (-7:ℤ) 7) 3, x = x)
#synth Decidable (∀ x : Vector (Finset.Icc (-7:ℤ) 7) 3, x = x)

(I would prefer the first.)