Comparison of arithmetic expressions not decidable?

Stream: new members

[Matthew Bouyack]

I've recently run into the limitation that if-then-else can only be used with decidable propositions. I've written some code to search over a sequence of points to find the first that is "close" to another:

def close (r : Int) (u v : Int × Int) : Prop :=
  (u.1 - v.1) ^ 2 + (u.2 - v.2) ^ 2 ≤ r ^ 2

-- Find the first cell close to u, with v being given as a default answer
def get_first_close (r : Int) (u v : Int × Int) (seq : Nat → (Int × Int)) : Nat → (Int × Int)
| 0     => if close r u (seq 0) then (seq 0) else v
| n + 1 => if close r u (seq (n+1))
           then get_first_close r u (seq (n+1)) seq n
           else get_first_close r u v seq n

I would have thought that "close" would be automatically considered decidable since it is just a comparison of two computable arithmetic expressions. Is there a way to make this work without explicitly declaring and proving that close is decidable?

[Aaron Liu]

instance (r : Int) (u v : Int × Int) : Decidable (close r u v) := by
  unfold close
  infer_instance

[Aaron Liu]

You can also fix this by writing abbrev close instead of def close, this will allow typeclass (the thing that figures out automatically that your thing is decidable) to see through the definition of close.

[Matthew Bouyack]

Thanks! That was a very fast response!