Defining generic extension transition

Stream: new members

[sgcs]

I have the following MWE that implements the transition rule below for a simplified lambda calculus (tried to strip away as much as I could). But there seems to be something that Lean doesn't like with the way I've defined generic_ext_prod since I keep getting a dependent elimination failure in the irrelevant theorem. I was under the impression this can happen when you use functions in the indices of inductive types, but I'm not using any here. Any advice on how I could reformulate it to get it to work? Or maybe there's something in the proof I can do, I haven't had any luck so far.

image.png

inductive Ty where
  | prod : Ty → Ty → Ty

inductive TyOperator where
  | prod : TyOperator → TyOperator → TyOperator

def TyOperator.subst (τ : Ty) : TyOperator → Ty
  | .prod τ_opₗ τ_opᵣ => Ty.prod (τ_opₗ.subst τ) (τ_opᵣ.subst τ)

abbrev Context : Type := List Ty

inductive Expr : Context → Ty → Type where
  | pair {Γ : Context} {τ₁ τ₂ : Ty} : Expr Γ τ₁ → Expr Γ τ₂ → Expr Γ (Ty.prod τ₁ τ₂)
  | projₗ {Γ : Context} {τ₁ τ₂ : Ty} : Expr Γ (Ty.prod τ₁ τ₂) → Expr Γ τ₁
  | projᵣ {Γ : Context} {τ₁ τ₂ : Ty} : Expr Γ (Ty.prod τ₁ τ₂) → Expr Γ τ₂
  | generic_ext
      {Γ : Context} {ρ ρ' τ_out : Ty} (τ_op : TyOperator) :
      τ_out = τ_op.subst ρ' → Expr (ρ :: Γ) ρ' → Expr Γ (τ_op.subst ρ) → Expr Γ τ_out

notation:40 Γ " ⊢ " τ => Expr Γ τ

inductive Transition {Γ : Context} : {τ : Ty} → (Γ ⊢ τ) → (Γ ⊢ τ) → Type where
  | generic_ext_prod
      {ρ ρ'  : Ty} (τ_opₗ τ_opᵣ : TyOperator) (e' : (ρ :: Γ) ⊢ ρ') (e : Γ ⊢ Ty.prod (τ_opₗ.subst ρ) (τ_opᵣ.subst ρ)) :
      Transition (Expr.generic_ext (TyOperator.prod τ_opₗ τ_opᵣ) rfl e' e)
                 (Expr.pair (Expr.generic_ext τ_opₗ rfl e' (Expr.projₗ e)) (Expr.generic_ext τ_opᵣ rfl e' (Expr.projᵣ e)))

notation:40 e₁ " ⟶ " e₂ => Transition e₁ e₂

theorem Transition.irrelevant
  {Γ : Context} {τ : Ty} {e e' : Γ ⊢ τ}
  (tr tr' : e ⟶ e') :
  tr = tr' :=
by
  cases tr with
  | generic_ext_prod =>
      cases tr' with
      | generic_ext_prod => sorry

[sgcs]

Just got back around to trying to get this to work again. Forgot I didn't give the error message:

dependent elimination failed, failed to solve equation
  TyOperator.subst ρ'✝¹ τ_opₗ✝¹ = TyOperator.subst ρ'✝ τ_opₗ✝

Is there some way I can tell Lean that TyOperator.subst is injective and that ρ'✝¹ = ρ'✝ and τ_opₗ✝¹ = τ_opₗ✝? Would it help if I used an inductive type to define the substitution instead of a function?

[sgcs]

OK, using an inductive type seems to get it to work:

inductive Ty where
  | prod : Ty → Ty → Ty

inductive TyOperator where
  | prod : TyOperator → TyOperator → TyOperator

inductive TyOperator.Subst : Ty → TyOperator → Ty → Type where
  | prod
      {τ τₗ' τᵣ' : Ty} {τ_opₗ τ_opᵣ : TyOperator} :
      Subst τ τ_opₗ τₗ' →
      Subst τ τ_opᵣ τᵣ' →
      Subst τ (TyOperator.prod τ_opₗ τ_opᵣ) (Ty.prod τₗ' τᵣ')

abbrev Context : Type := List Ty

inductive Expr : Context → Ty → Type where
  | pair {Γ : Context} {τ₁ τ₂ : Ty} : Expr Γ τ₁ → Expr Γ τ₂ → Expr Γ (Ty.prod τ₁ τ₂)
  | projₗ {Γ : Context} {τ₁ τ₂ : Ty} : Expr Γ (Ty.prod τ₁ τ₂) → Expr Γ τ₁
  | projᵣ {Γ : Context} {τ₁ τ₂ : Ty} : Expr Γ (Ty.prod τ₁ τ₂) → Expr Γ τ₂
  | generic_ext
      {Γ : Context} {ρ ρ' τ_in τ_out: Ty} (τ_op : TyOperator) :
      TyOperator.Subst ρ τ_op τ_in →
      TyOperator.Subst ρ' τ_op τ_out →
      Expr (ρ :: Γ) ρ' → Expr Γ τ_in → Expr Γ τ_out

notation:40 Γ " ⊢ " τ => Expr Γ τ

inductive Transition {Γ : Context} : {τ : Ty} → (Γ ⊢ τ) → (Γ ⊢ τ) → Type where
  | generic_ext_prod
      {ρ ρ' τ_inₗ τ_inᵣ τ_outₗ τ_outᵣ : Ty} (τ_opₗ τ_opᵣ : TyOperator)
      (sₗ : TyOperator.Subst ρ τ_opₗ τ_inₗ) (sₗ' : TyOperator.Subst ρ' τ_opₗ τ_outₗ)
      (sᵣ : TyOperator.Subst ρ τ_opᵣ τ_inᵣ) (sᵣ' : TyOperator.Subst ρ' τ_opᵣ τ_outᵣ)
      (e' : (ρ :: Γ) ⊢ ρ') (e : Γ ⊢ Ty.prod τ_inₗ τ_inᵣ) :
      Transition (Expr.generic_ext (TyOperator.prod τ_opₗ τ_opᵣ) (TyOperator.Subst.prod sₗ sᵣ) (TyOperator.Subst.prod sₗ' sᵣ') e' e)
                 (Expr.pair (Expr.generic_ext τ_opₗ sₗ sₗ' e' (Expr.projₗ e)) (Expr.generic_ext τ_opᵣ sᵣ sᵣ' e' (Expr.projᵣ e)))

notation:40 e₁ " ⟶ " e₂ => Transition e₁ e₂

theorem Transition.irrelevant
  {Γ : Context} {τ : Ty} {e e' : Γ ⊢ τ}
  (tr tr' : e ⟶ e') :
  tr = tr' :=
by
  cases tr with
  | generic_ext_prod =>
      cases tr' with
      | generic_ext_prod => simp_all

I think using a function is a bit more intuitive for me personally though, is there a way to get that approach working for future reference?