Induction, "index in target's type is not a variable..."

Stream: new members

[Chris Henson]

I am working with the simply typed lambda calculus (with pairs), following the style in PLFA of terms parameterized by contexts. I tried to prove a simplified version of the permutation lemma, but don't understand this error message. Here is an mwe:

inductive Ty (K : Type)
  | Basic : K → Ty K
  | Arr : Ty K → Ty K →  Ty K
  | Prod : Ty K → Ty K → Ty K

infixr:60 " × " => Ty.Prod
infixr:70 " ⇒ " => Ty.Arr
prefix:90 "` " => Ty.Basic

abbrev Context (K : Type) : Type := List (Ty K)

inductive Lookup {K : Type} : Context K → Ty K → Type
  | z : Lookup (T :: Γ) T
  | s : Lookup Γ T → Lookup (T' :: Γ) T

infix:40 " ∋ " => Lookup

inductive Term {K : Type} : Context K → Ty K → Type
  | var : Γ ∋ a → Term Γ a
  | lam : Term (a :: Γ) b → Term Γ (a ⇒ b)
  | ap  : Term Γ (a ⇒ b) → Term Γ a → Term Γ b
  | cop : Term Γ a → Term Γ b → Term Γ (a × b)
  | fst : Term Γ (a × b) → Term Γ a
  | snd : Term Γ (a × b) → Term Γ b

namespace Term
  infix:40 " ⊢ " => Term
  prefix:50 "ƛ " => lam
  infixl:70 " □ " => ap
  prefix:70 "fst" => fst
  prefix:70 "snd" => snd
  prefix:90 "` " => var
end Term

theorem permute : (τ :: σ :: Γ) ⊢ T → (σ :: τ :: Γ) ⊢ T := by
  intros tm
  induction tm
  /-
  error message: index in target's type is not a variable (consider using the `cases` tactic instead)    τ :: σ :: Γ
  -/

I searched here on Zulip and saw some suggestions about using the generalize tactic, but I wasn't sure if/how that might work here. I'd also like to understand what the message means past just immediately getting past this theorem, if there's some suggested reading/docs.

[Chris Henson]

I think the way that I've stated permute is not quite right either, I'd just like to understand how I can do induction over a term with something cons'd into the context (or understand if/why another approach would be better).

[Kyle Miller]

The induction tactic requires that indices be variables, so that it can substitute in values according to each of the cases. Here's how you use generalize for that:

theorem permute : (τ :: σ :: Γ) ⊢ T → (σ :: τ :: Γ) ⊢ T := by
  intros tm
  generalize htm : τ :: σ :: Γ = ctx at tm
  induction tm

[Kyle Miller]

It's a little silly here because each of the Term constructors have the context as a variable, so this is an unnecessary requirement.

Because of that, you can undo the generalizing at the same time using

induction tm <;> cases htm

(Or <;> subst htm if you wish, it does the same thing)

[Chris Henson]

Thanks! Would you mind explaining roughly what "index" means here? Is it the same meaning as in Coq?

[Henrik Böving]

Index of an inductive type means the same in Coq and Lean yes, in general a lot of the type theory related jargon is interchangeable