Trying to generalize so I can match

Stream: new members

[sgcs]

I'm trying to mess around with creating a lambda calculus and am having trouble with a specific proof that I'm not sure how to approach in Lean. My MWE is below (there's probably a smaller one, but this keeps everything in context).

inductive Typ where
  | number

abbrev Ctx : Type := List Typ

inductive InCtx : Ctx → Typ → Type where
  | here {Γ : Ctx} {typ : Typ} : InCtx (typ :: Γ) typ
  | there {Γ : Ctx} {typ₁ typ₂ : Typ} : InCtx Γ typ₂ → InCtx (typ₁ :: Γ) typ₂

inductive Term : (Γ : Ctx) → (typ : Typ) → Type where
  | var {Γ : Ctx} {typ : Typ} : (InCtx Γ typ) → Term Γ typ
  | number {Γ : Ctx} (n : Nat) : Term Γ Typ.number
  | «let» {Γ : Ctx} {typ₁ typ₂ : Typ} (t₁ : Term Γ typ₁) (t₂ : Term (typ₁ :: Γ) typ₂) : Term Γ typ₂

abbrev Rename (Γ Δ : Ctx) : Type := ∀ {typ : Typ}, (InCtx Γ typ) → (InCtx Δ typ)

abbrev Subst (Γ Δ : Ctx) : Type := ∀ {typ : Typ}, (InCtx Γ typ) → Term Δ typ

def ext {Γ Δ : Ctx} {typ : Typ} (ρ : Rename Γ Δ) : Rename (typ :: Γ) (typ :: Δ)
  | _, .here => InCtx.here
  | _, .there a => InCtx.there (ρ a)

def rename {Γ Δ : Ctx} {typ : Typ} (ρ : Rename Γ Δ) : (Term Γ typ) → Term Δ typ
  | .var a => Term.var (ρ a)
  | .number num => Term.number num
  | .let t₁ t₂ => Term.let (rename ρ t₁) (rename (ext ρ) t₂)

def exts {Γ Δ : Ctx} {typ : Typ} (σ : Subst Γ Δ) : Subst (typ :: Γ) (typ :: Δ)
  | _, .here => Term.var InCtx.here
  | _, .there a => rename InCtx.there (σ a)

def subst {Γ Δ : Ctx} {typ : Typ} (σ : Subst Γ Δ) : (Term Γ typ) → Term Δ typ
  | .var a => σ a
  | .number num => Term.number num
  | .let t₁ t₂ => Term.let (subst σ t₁) (subst (exts σ) t₂)

def zero {Γ : Ctx} {typ : Typ} (t : Term Γ typ) : Subst (typ :: Γ) Γ
  | _, .here => t
  | _, .there a => Term.var a

abbrev subst_zero {Γ : Ctx} {typ typ' : Typ} (t : Term Γ typ) (t' : Term (typ :: Γ) typ') : Term Γ typ' := subst (zero t) t'

inductive Reduction : {Γ : Ctx} → {typ : Typ} → Term Γ typ → Term Γ typ → Type where
  | ξ_let {Γ : Ctx} {typ : Typ} {t₁ t₁' : Term Γ typ} {t₂ : Term (typ :: Γ) typ} : Reduction t₁ t₁' → Reduction (Term.let t₁ t₂) (Term.let t₁' t₂)
  | β_let {Γ : Ctx} {typ : Typ} {t₁ : Term Γ typ} {t₂ : Term (typ :: Γ) typ} : Reduction (Term.let t₁ t₂) (subst_zero t₁ t₂)

theorem thm
  {Γ : Ctx} {typ₁ typ₂ : Typ} {t₁ t₁' : Term Γ typ₁} {t₂ : Term (typ₁ :: Γ) typ₂}
  (tr : Reduction (Term.let t₁ t₂) (Term.let t₁' t₂)) :
  ∃ tr' : Reduction t₁ t₁', tr = Reduction.ξ_let tr' :=
by
  -- This gives error: tactic 'generalize' failed, result is not type correct - ∀ (tmp : Term Γ typ₂) (tr : Reduction (Term.let t₁ t₂) tmp), ∃ tr', tr = Reduction.ξ_let
  -- generalize Term.let t₁' t₂ = tmp at tr

  match tr with
  | .ξ_let _ => sorry
  -- This gives error
  -- type mismatch
  --   Reduction.β_let
  -- has type
  --   Reduction (Term.let t₁ t₂) (subst_zero t₁ t₂) : Type
  -- but is expected to have type
  --   Reduction (Term.let t₁ t₂) (Term.let t₁' t₂) : Type
  | .β_let => sorry

I'm trying to prove the last theorem (it was originally part of a larger proof but I've made it more isolated to focus on the problem). Essentially, I want to pattern match on tr but can't because Lean tries to unify in the case of β_let. This case is impossible but I'm not sure how or where I can convince Lean of this. I tried generalizing the target term of the reduction so it could be unified, but it says the result is not type correct (I don't totally understand why this is the case). Does anyone have a suggestion for how I can proceed with the proof?

[Kyle Miller]

I think the short answer is that having functions in type indices makes it hard to do cases.

I'm not sure what the best thing to do is, but one strategy you could take is to redefine Reduction have

  | β_let {Γ : Ctx} {typ : Typ} {t₁ : Term Γ typ} {t₂ : Term (typ :: Γ) typ}
      (t₃ : Term Γ typ') (h : subst_zero t₁ t₂ = t₃) : Reduction (Term.let t₁ t₂) t₃

which makes it easier to make progress. (By the way, it looks like you need to use cases instead of match. I don't understand the error, but I'm getting "tag not found". The only difference in syntax is that you drop the .s.)

[Kyle Miller]

I think of this transformation as some kind of "pre-generalization". The biggest tradeoff I see is that dependent elimination might not auto-exclude cases for you, since relevant information is behind equalities inside the constructor.

[sgcs]

Thanks, that seems to get everything working. Does seem a bit unfortunate that I can't generalize in the proof since, as you said, it does have tradeoffs but at least they're manageable.