match statement in decidable instance

Stream: new members

[Chris B]

Does anyone know what the decidable_eq ℕ instance in core does that allows it to use the syntax match decidable_eq x y with ... in the recursive case? Trying to use it elsewhere gives me an error.

inductive not_nat
| Z : not_nat
| S : not_nat → not_nat

open not_nat

instance : decidable_eq not_nat
| Z     Z     := is_true rfl
| (S x) Z       := is_false (λ h, not_nat.no_confusion h)
| Z     (S y)   := is_false (λ h, not_nat.no_confusion h)
| (S x) (S y) :=
    match decidable_eq x y with
  --   ...
  -- type mismatch at application
  --   decidable_eq x
  -- term
  --   x
  -- has type
  --   not_nat : Type
  -- but is expected to have type
  --   Sort ? : Type ?

[Mario Carneiro]

If you look at the tactic state in the error message, you will see that not_nat.decidable_eq is what's in the context, so you have to write it like that

[Mario Carneiro]

It's not actually a global definition, it's actually a local constant in disguise (and actually it's not even that, it's a macro disguised as a local constant) so it doesn't work by the same rules w.r.t open

[Mario Carneiro]

The difference between your example and nat.decidable_eq is that nat.decidable_eq was written inside namespace nat rather than merely with nat open

[Mario Carneiro]

this works:

inductive not_nat
| Z : not_nat
| S : not_nat → not_nat

namespace not_nat

instance : decidable_eq not_nat
| Z     Z     := is_true rfl
| (S x) Z       := is_false (λ h, not_nat.no_confusion h)
| Z     (S y)   := is_false (λ h, not_nat.no_confusion h)
| (S x) (S y) :=
    match decidable_eq x y with
    | _ := sorry
    end

end not_nat

[Chris B]

Agh, brutal. I tried some of the qualifiers but definitely not namespace. I'm still trying to get a grasp on how the hierarchical names work in practice. Thanks for the rundown.

[Mario Carneiro]

I think this is actually more like a bug in the way instance names and auxiliaries are handled, so I don't blame you for getting confused