Zulip Chat Archive

Stream: new members

Topic: match statement in decidable instance


view this post on Zulip Chris B (Jul 19 2019 at 02:53):

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 ?

view this post on Zulip Mario Carneiro (Jul 19 2019 at 02:55):

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

view this post on Zulip Mario Carneiro (Jul 19 2019 at 02:56):

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

view this post on Zulip Mario Carneiro (Jul 19 2019 at 02:58):

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

view this post on Zulip Mario Carneiro (Jul 19 2019 at 02:58):

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

view this post on Zulip Chris B (Jul 19 2019 at 03:01):

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.

view this post on Zulip Mario Carneiro (Jul 19 2019 at 03:02):

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


Last updated: May 14 2021 at 03:27 UTC