Zulip Chat Archive

Stream: general

Topic: understanding hint: try cases on indices


view this post on Zulip Kris Brown (Jul 14 2020 at 21:59):

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?

view this post on Zulip Reid Barton (Jul 14 2020 at 22:01):

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

view this post on Zulip Reid Barton (Jul 14 2020 at 22:01):

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

view this post on Zulip Reid Barton (Jul 14 2020 at 22:04):

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.

view this post on Zulip Reid Barton (Jul 14 2020 at 22:15):

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

view this post on Zulip Reid Barton (Jul 14 2020 at 22:18):

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

view this post on Zulip Reid Barton (Jul 14 2020 at 22:20):

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

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

view this post on Zulip Reid Barton (Jul 14 2020 at 22:22):

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

view this post on Zulip Kris Brown (Jul 15 2020 at 07:53):

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!


Last updated: May 14 2021 at 00:42 UTC