Dependent elimination failure

Stream: new members

[sgcs]

I have the following code:

inductive Vector (α : Type u) : Nat → Type u where
  | nil : Vector α 0
  | cons {n : Nat} : α → Vector α n → Vector α (Nat.succ n)

infix:67 " :: " => Vector.cons

inductive Ty where
  | string

abbrev Context : Nat → Type := Vector Ty

inductive Any : Fin n → Ty → Context n → Prop where
  | here : Any 0 τ (τ :: Γ)
  | there : Any i τ₂ Γ → Any i.succ τ₂ (τ₁ :: Γ)

theorem any_injective :
  Any i τ Γ →
  Any i τ' Γ →
  τ = τ' :=
by
  intro a
  induction a generalizing τ' with intro a'
  | here => cases a'; rfl
  | there a ih =>
      match a' with
      | Any.there a' => sorry

I'm trying to prove injectivity for Any and have a couple of questions:

1. Why when I try to match on a', I get the following error and how can I resolve it?

tactic 'cases' failed, nested error:
dependent elimination failed, failed to solve equation
  i✝¹.1 = i✝.1
at case @Any.there after processing

2. Is there somewhere in the tactic state that I can see the constraints the compiler has? For example, I would expect in the above snippet that the unnamed i✝ in the Any.there case would relate to the original i like i = i✝.succ. I've been experimenting a lot in Agda and am used to being able to see such constraints.

[Kyle Miller]

My understanding of the basic issue is that it's wanting to get an equality between a variable and something else when processing indices to types, and with i.1 = j.1 it's not able to go any further. One option is to do cases on one of these variables first, and another is to generalize.

I didn't know about induction ... with intro ... syntax (is it new? it looks like you can put a single tactic after with that applies to all cases before using the | clauses); in any case, you can simplify it a bit by changing your theorem to take named arguments.

theorem any_injective (a : Any i τ Γ) (a' : Any i τ' Γ) :
  τ = τ' :=
by
  induction a generalizing τ' with
  | here => cases a'; rfl
  | there a ih =>
      -- we want to give `i` a name:
      rename_i x i τ₂ Γ τ₁
      cases i -- option 1
      generalize h : Fin.succ i = j at a' -- option 2
      match a' with
      | Any.there a' => sorry