structural recursion failed, produced type incorrect term

Stream: lean4

[Henrik Böving]

I've been doing a basic type theory verification project and for a bunch of lemmas over from https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Simple.20Nat.20inequality I've now imported mathlib...interestingly enough this causes structural recursion on one of my proofs to fail in the following way:

fail to show termination for
  Cube.Simple.Expr.Expr.subject_reduction
with errors
structural recursion failed, produced type incorrect term
  application type mismatch
    PProd.fst x.fst func func_type
  argument has type
    (env, []) ⊢ func : Ty.fun t1 ty
  but function has type
    ((env, ctx) ⊢ func : Ty.fun t1 ty) → (func →β t1') → (env, ctx) ⊢ t1' : Ty.fun t1 ty

failed to prove termination, use `termination_by` to specify a well-founded relation

[Henrik Böving]

Here is I think a #mwe

import Lean
import Mathlib.Tactic.Linarith -- Not used in the file but in sorried proofs

open Lean

namespace Simple

inductive Ty where
| nat
| fun (pre : Ty) (image : Ty)
deriving Repr, DecidableEq

inductive Expr where
| bvar (idx : Nat)
| mvar (name : String)
| lam (ty : Ty) (body : Expr) (orig : String)
| const (name : String)
| app (func : Expr) (arg : Expr)
deriving Repr, DecidableEq

namespace Expr

abbrev Context := List Ty
abbrev Env := String → Option Ty

def Context.set (ctx : Context) (n : Nat) (ty : Ty) : Context :=
  match ctx, n with
  | [], 0 => [ty]
  | [], _ + 1 => []
  | _ :: xs, 0 => ty :: xs
  | x :: xs, n + 1 => x :: set xs n ty

@[simp]
theorem Context.set_nil_zero : Context.set [] 0 ty = [ty] := rfl

@[simp]
theorem Context.set_nil_succ : Context.set [] (i + 1) ty = [] := rfl

@[simp]
theorem Context.set_cons_zero : Context.set (x :: xs) 0 ty = ty :: xs := rfl

@[simp]
theorem Context.set_cons_succ : Context.set (x :: xs) (i + 1) ty = x :: (Context.set xs i ty) := rfl

inductive Typing : Env → Context → Expr → Ty → Prop where
| const (in_env : env name = some typ) : Typing env ctx (.const name) typ
| app (func_type : Typing env ctx func (.fun t1 t2)) (arg_type : Typing env ctx arg t1) : Typing env ctx (.app func arg) t2
| lam (body_type : Typing env (t1 :: ctx) body t2) : Typing env ctx (.lam t1 body orig) (.fun t1 t2)
| bvar (idx : Nat) (bound : idx < ctx.length) : Typing env ctx (.bvar idx) (ctx.get ⟨idx, bound⟩)

notation:40 "("Δ ", " Γ ")" " ⊢ " e " : " t => Typing Δ Γ e t

def instantiate (image : Expr) (expr : Expr) (targetIdx : Nat := 0): Expr :=
    match expr with
    | .bvar idx =>
      if idx = targetIdx then
        image
      else
        .bvar idx
    | .app fn arg => .app (instantiate image fn targetIdx ) (instantiate image arg targetIdx )
    | .lam ty body orig => .lam ty (instantiate image body (targetIdx + 1)) orig
    | .mvar name => .mvar name
    | .const name => .const name

theorem Typing.instantiate_preserves (h1 : (env, []) ⊢ v : ty) (h2 : (env, (Context.set ctx i ty)) ⊢ expr : ty') : (env, ctx) ⊢ (instantiate v expr i) : ty' := by sorry

@[simp]
def isLam : Expr → Bool
| .lam .. => true
| _ => false

inductive Value : Expr → Prop where
| lam : Value (.lam ty body orig)
| const : Value (.const name)
| constApp (h : Value v) : Value (.app (.const name) v)
| app (h1 : Value f) (h2 : ¬f.isLam) (h3 : Value v) : Value (.app f v)

inductive BetaStep : Expr → Expr → Prop where
| lamApp : BetaStep (.app (.lam ty body orig) arg) (instantiate arg body)
| leftApp (h : BetaStep t1 t1') : BetaStep (.app t1 t2) (.app t1' t2)
| rightApp (h1 : Value t1) (h2 : BetaStep t2 t2') : BetaStep (.app t1 t2) (.app t1 t2')

def normal_form (R : α → α → Prop) (t : α) : Prop := ¬ ∃ t', R t t'

notation t1 " →β " t2 => BetaStep t1 t2

theorem subject_reduction (expr : Expr) (typed_expr : (env, []) ⊢ expr : ty) (reduces : expr →β expr') : (env, []) ⊢ expr' : ty := by
  cases typed_expr with
  | const => cases reduces
  | app =>
    cases reduces
    case lamApp lam_typed =>
      cases lam_typed with
      | lam body_typed =>
        rw [←Context.set_nil_zero] at body_typed
        apply Typing.instantiate_preserves
        repeat assumption
    case leftApp =>
      apply Typing.app
      apply subject_reduction
      repeat assumption
    case rightApp =>
      apply Typing.app
      assumption
      apply subject_reduction
      repeat assumption
  | lam => cases reduces
  | bvar => cases reduces

end Expr
end Simple

Also the reason my subject reduction lemma has cases instead of induction is because Lean refused to perform induction on my thing for some reason :(

index in target's type is not a variable (consider using the `cases` tactic instead)
  []

[Evgeniy Kuznetsov]

Minimized it a little more:

import Mathlib.Data.Nat.Order.Basic

namespace Simple

inductive Expr where
| app (func arg: Expr)

inductive Typing : List Nat → Expr → Prop where
| app (arg_type : Typing [] arg) : Typing ctx (.app func arg)

theorem subject_reduction (typed_expr : Typing [] expr) (reduces : expr = expr) : Typing [] expr := by
  cases typed_expr with
  | app aty => exact Typing.app (subject_reduction aty rfl)

[Reid Barton]

Further reduced:

import Mathlib.Algebra.Order.Ring.Canonical
import Mathlib.Data.Nat.Basic

namespace Nat

instance linearOrderedCommSemiring : LinearOrderedCommSemiring ℕ :=
  { Nat.commSemiring, Nat.linearOrder with
    lt := Nat.lt, add_le_add_left := @Nat.add_le_add_left,
    le_of_add_le_add_left := @Nat.le_of_add_le_add_left,
    zero_le_one := Nat.le_of_lt (Nat.zero_lt_succ 0),
    mul_lt_mul_of_pos_left := @Nat.mul_lt_mul_of_pos_left,
    mul_lt_mul_of_pos_right := @Nat.mul_lt_mul_of_pos_right,
    exists_pair_ne := ⟨0, 1, ne_of_lt Nat.zero_lt_one⟩ }

end Nat

namespace Simple

inductive Expr where
| app (func arg: Expr)

inductive Typing : List Nat → Expr → Prop where
| app (arg_type : Typing [] arg) : Typing ctx (.app func arg)

theorem subject_reduction (typed_expr : Typing [] expr) (reduces : expr = expr) : Typing [] expr := by
  cases typed_expr with
  | app aty => exact Typing.app (subject_reduction aty rfl)

[Reid Barton]

It seems that the use of tactics somehow prevents it from seeing that it should use structural recursion, and then the instance somehow causes the termination proof to fail for well-founded recursion.

[Evgeniy Kuznetsov]

Leonardo de Moura said:

I pushed support for casesOn applications to the structural and well-founded recursion modules. This is useful for using recursion and cases tactic. For example, we don't need the generalizations steps above nor the decreasing_by anymore. It should work with any tactic that creates casesOn applications (e.g., rcases).
https://github.com/leanprover/lean4/blob/8c23bef39907e2599fb8ade149b7aa68ab4da311/tests/lean/run/casesRec.lean#L35-L49

cases has some structural recursion support

[Henrik Böving]

Reid Barton said:

It seems that the use of tactics somehow prevents it from seeing that it should use structural recursion, and then the instance somehow causes the termination proof to fail for well-founded recursion.

Does it though? The error message claims that it tried to do structural recursion but got something type incorrect while doing so.

[Reid Barton]

I tried the term-mode equivalent and it worked. Also the tactic version worked without the instance.

[Reid Barton]

In the former case the term used structural recursion, in the latter case well-founded recursion.

[Evgeniy Kuznetsov]

Henrik Böving said:

Reid Barton said:

It seems that the use of tactics somehow prevents it from seeing that it should use structural recursion, and then the instance somehow causes the termination proof to fail for well-founded recursion.

Does it though? The error message claims that it tried to do structural recursion but got something type incorrect while doing so.

set_option trace.Elab.definition.wf true shows that Lean was trying to use WF recursion, I guess it failed too

[Henrik Böving]

So shall I just open an issue about this on the mathlib repo? Given the strange fact that this does work out perfectly fine if mathlib is not involved.

[Reid Barton]

I don't think it has anything to do with mathlib per se.

[Henrik Böving]

What is the issue then? If the mathlib import is removed the cases tactic works so clearly mathlib is doing something that confuses the structural recursion algorithm isn't it?

[Reid Barton]

See the version I posted above.

[Reid Barton]

I don't know what the issue is specifically.