How to solve 'index in targets type is not a variable'

Stream: general

[Jelmer Firet]

I am trying to formalize a type theory inside Lean.
I currently have:

inductive Term : Nat → Type where [...]
def subst (k : Fin n.succ) (u : Term k) (t : Term n.succ) : Term n := [...]
def Context (n : Nat) := (x : Fin n) → (Term x)
def subst_ctx (k : Fin n.succ) (u : Term k) (Γ : Context n.succ) : Context n := [...]
inductive xtyped : (Context n) → (Term n) → (Term n) → Prop where [...]

Now I want to prove that substitution is consistent with typing:

lemma subst_consistent (tA : xtyped Γ t A) : xtyped (subst_ctx k u Γ) (subst k u t) (subst k u A)

But when I start with induction tA it gives an error:

index in target's type is not a variable (consider using the `cases` tactic instead)
  n.succ

But for the proof I need induction, how can I fix this?

[Asei Inoue]

using generalize tactic?

[Jelmer Firet]

Already tried that, it doesn't work:

generalize n.succ = m at *

gives

tactic 'generalize' failed, result is not type correct

That is because fundamentally subst takes a Term n.succ (and something to substitute in) and returns a Term n. After generalize this does not fit anymore since Term m is not of the form Term n.succ and thus rejected as argument for subst.

[Henrik Böving]

Can you give a full #mwe?

[Jelmer Firet]

I removed the terms related to pairs and equalities:

term.lean

import Mathlib.Data.Finset.Basic

inductive sort where
| succ : sort -> sort
| prod : sort -> sort -> sort


inductive Term : Nat → Type where
| rel (m : Fin n) : Term n
| sort (s : sort) : Term n
| prod (A : Term n) (B : Term n.succ) : Term n
| lambda (A : Term n) (B t : Term n.succ) : Term n
| app (A : Term n) (B : Term n.succ) (t u : Term n) : Term n

lemma Nat.succ_eq_succ {n m : Nat} (eq : n = m) : n.succ = m.succ := by {
  rewrite [eq]
  apply Eq.refl
}

@[simp]
def Term.cast (t : Term n) (h : n = m) : Term m :=
match t with
| rel m         => rel (m.cast h)
| sort s        => sort s
| prod A B      => prod (A.cast h) (B.cast (Nat.succ_eq_succ h))
| lambda A B t  => lambda (A.cast h) (B.cast (Nat.succ_eq_succ h)) (t.cast (Nat.succ_eq_succ h))
| app A B t u   => app (A.cast h) (B.cast (Nat.succ_eq_succ h)) (t.cast h) (u.cast h)

-- def Term.cast (t : Term n) (eq : n = m) : Term m := Eq.rec t eq
@[simp] theorem test.cast_rfl (t : Term n) : t.cast rfl = t := by {
  induction t <;> simp <;> tauto
}

instance : Coe (Term (n.succ + k)) (Term (n + k).succ) where
  coe x := x.cast (Nat.succ_add n k)

instance : Coe (Term (n.succ.succ + k)) (Term (n + k).succ.succ) where
  coe x := x.cast (by rw [Nat.succ_add, Nat.succ_add])

subst.lean

import EttItt.term
import Mathlib.Tactic.Convert
import Mathlib.Tactic.Linarith

instance : Coe (Fin n) (Fin n.succ) where
  coe x := {
    val := x
    isLt := by
      apply Nat.lt_succ_of_lt
      apply x.isLt
  }

@[simp]
def pad (t : Term n) : (Term n.succ) :=
  match t with
  | Term.rel x => Term.rel x
  | Term.sort s => Term.sort s
  | Term.prod A B => Term.prod (pad A) (pad B)
  | Term.lambda A B t => Term.lambda (pad A) (pad B) (pad t)
  | Term.app A B t u => Term.app (pad A) (pad B) (pad t) (pad u)

instance : Coe (Term n) (Term n.succ) where
  coe x := pad x

def pad_greater (le : n ≤ m) (t : Term n) : (Term m) :=
  match Nat.decLt n m with
  | isTrue lt => by
      apply @pad_greater n.succ m _ t
      assumption
  | isFalse eq => by
      convert t
      apply eq_of_ge_of_not_gt le eq

@[simp]
def subst (k : Fin n.succ) (u : Term k) (t : Term n.succ) : Term n :=
  match t with
  | Term.rel x => match Fin.decLt k x with
    | isFalse _ => match Fin.decLe k x with
      | isFalse k_gt_x => Term.rel { val := x, isLt := Nat.lt_of_lt_of_le (Nat.lt_of_not_le k_gt_x) (Nat.le_of_lt_succ k.isLt) }
      | isTrue _ => pad_greater ( Nat.le_of_lt_succ k.isLt) u
    | isTrue k_lt_x => Term.rel {
        val := x.val.pred
        isLt := by
          apply Nat.lt_of_succ_lt_succ
          rewrite [Nat.succ_pred]
          · exact x.isLt
          · apply Nat.not_eq_zero_of_lt
            exact k_lt_x
      }
  | Term.sort s => Term.sort s
  | Term.prod A B => Term.prod (subst k u A) (subst k u B)
  | Term.lambda A B t => Term.lambda (subst k u A) (subst k u B) (subst k u t)
  | Term.app A B t x => Term.app (subst k u A) (subst k u B) (subst k u t) (subst k u x)

@[simp]
def subst' (u : Term n) (t : Term n.succ) : Term n := subst {
    val := n
    isLt := Nat.le.refl
  } u t

ett.lean

import EttItt.term
import EttItt.subst

def Context (n : Nat) := (x : Fin n) → (Term x)
def Context.add (Γ : Context n) (t : Term n) : Context (n.succ) :=
  fun (k : Fin n.succ) =>
    match Nat.decLt k n with
    | isFalse k_ge_n => (@Term.cast n ↑k t (Nat.le_antisymm (Nat.le_of_not_lt k_ge_n) (Nat.le_of_lt_succ k.isLt)))
    | isTrue k_lt_n => Γ {val := k.val, isLt := k_lt_n}
@[simp]
def Context.cast (Γ : Context n) (eq : n = m) : Context m := Eq.rec Γ eq
notation Γ ",," t => Context.add Γ t

inductive xtyped : (Context n) → (Term n) → (Term n) → Prop where
| rel    : xtyped Γ (Term.rel k) (pad_greater k.isLt (Γ k))
| sort   : xtyped Γ (Term.sort s) (Term.sort (sort.succ s))
| prod   ( tyA : xtyped Γ A (Term.sort s1) )
         ( tyB : xtyped (Γ,,A) B (Term.sort s2) )
         : xtyped Γ (Term.prod A B) (Term.sort (sort.prod s1 s2))
| lambda ( tyA : xtyped Γ A (Term.sort s1) )
         ( tyB : xtyped (Γ,,A) B (Term.sort s2) )
         ( tyt : xtyped (Γ,,A) t B )
         : xtyped Γ (Term.lambda A B t) (Term.prod A B)
| app    ( tyA : xtyped Γ A (Term.sort s1) )
         ( tyB : xtyped (Γ,,A) B (Term.sort s2) )
         ( tyt : xtyped Γ t (Term.prod A B) )
         ( tyu : xtyped Γ u A )
         : xtyped Γ (Term.app A B t u) (subst' u B)

def subst_ctx (k : Fin n.succ) (u : Term k) (Γ : Context n.succ) : Context n :=
  fun x => match Nat.decLt x k with
    | isTrue _ => Γ x
    | isFalse k_ge_x => subst {val := k.val, isLt := Nat.lt_succ_of_le (Nat.le_of_not_lt (k_ge_x))} u (Γ x.succ)

lemma subst_consistent (n : Nat) (k : Fin n.succ) (u : Term k) (t A : Term n.succ) (Γ : Context n.succ) (tA : @xtyped n.succ Γ t A) : @xtyped n (subst_ctx k u Γ) (subst k u t) (subst k u A) := by
  induction tA
  admit