understanding hint: try cases on indices

Stream: general

[Kris Brown]

I'm having trouble understanding a lean suggestion for an error I have. Firstly, I'm trying to define equality for an inductive type, MWE below:

 def type_map : ℕ → Type
   | 0 := nat
   | _ := bool

  instance has_deq_typemap_image : Π(i: ℕ), decidable_eq (type_map i)
   | 0            := nat.decidable_eq
   | (nat.succ _) := bool.decidable_eq

  --cannot @[derive decidable_eq]
  inductive Foo : Type → Type
   | mk (i: ℕ): Foo (type_map i)

  instance deq_foo : Π{i: Type}, decidable_eq (Foo i) -- has error
   | _ (Foo.mk 0) (Foo.mk 0) := by {simp only [], exact is_true trivial}
   | _ (Foo.mk (nat.succ _)) (Foo.mk (nat.succ _)) := by {simp only [], exact is_true trivial}
   -- | _ (Foo.mk 0) (Foo.mk (nat.succ _)) := sorry -- if uncommented, then error on nat.succ _, expects 0

I'm a bit weary of the last type signature, since it's important that it's not possible for an arbitrary type i to have Foo i (it's only possible to have Foo nat or Foo bool. But I suppose plugging in some other type should lead to absurdity, which implies decidable equality.

In any case, I'd expect error to be that my patterns are incomplete, but instead it is "cases tactic failed, unsupported equality between type and constructor indices (only equalities between constructors and/or variables are supported, try cases on the indices): bool = type_map b_1". What exactly the hint is suggesting beyond what I already tried?

[Reid Barton]

There's no way this could ever work in the VM anyways, so you might as well just use classical I guess.

[Reid Barton]

Oh wait maybe that's not true, I just noticed you have the data i : nat.

[Reid Barton]

Is this what you want? Foo nat is a nat that has to be zero. Foo bool is a nat that has to not be zero. Others are uninhabited.

[Reid Barton]

I think it would be possible to complete this approach, but mostly this seems like a strange thing to do...

def aux : Π (α β : Type) (f : Foo α) (g : Foo β), decidable (f == g)
| _ _ (Foo.mk 0) (Foo.mk 0) := is_true heq.rfl
| _ _ (Foo.mk 0) (Foo.mk (nat.succ n)) := _
| _ _ (Foo.mk (nat.succ n)) (Foo.mk 0) := _
| _ _ (Foo.mk (nat.succ n)) (Foo.mk (nat.succ m)) := _

instance deq_Foo : Π (α : Type), decidable_eq (Foo α) :=
λ α f g, decidable_of_decidable_of_iff (by apply aux) heq_iff_eq

[Reid Barton]

I'm not sure whether you can do it without making use of the fact that bool and nat happen to be provably unequal.

[Reid Barton]

This would achieve the same result with less mind-bending involved, I think:

structure Foo' (α : Type) : Type :=
(i: ℕ) (h : α = type_map i)

[Reid Barton]

Regarding the original error, if you try to write the definition using recursors, I think you will see where things go wrong.

[Kris Brown]

For context I was working on an application of Hoare logic involving types like Expr A, Var A where Expr and Var are Type -> Type, but I had restricted the possible A types to the image of a function Index -> Type (for some inductive type Index with everything in the image having decidable equality). But I've now managed to restructure things a bit to avoid this weirdness. Still, your explanation of how to tackle this is very helpful for understanding Lean!