Stream: new members

Topic: Dependent elimination failure

sgcs (Mar 08 2023 at 06:39):

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

1. 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 (Mar 08 2023 at 10:17):

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


Last updated: Dec 20 2023 at 11:08 UTC