fix: smart unfolding

See new comment to understand the issue.

closes #1081

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -92,6 +92,11 @@ def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
   let env ← getEnv
   Eqns.getUnfoldFor? declName fun _ => eqnInfoExt.find? env declName |>.map (·.toEqnInfoCore)
 
+@[export lean_get_structural_rec_arg_pos]
+def getStructuralRecArgPosImp? (declName : Name) : CoreM (Option Nat) := do
+  let some info := eqnInfoExt.find? (← getEnv) declName | return none
+  return some info.recArgPos
+
 builtin_initialize
   registerGetEqnsFn getEqnsFor?
   registerGetUnfoldEqnFn getUnfoldFor?

src/Lean/Meta/WHNF.lean

@@ -18,6 +18,14 @@ namespace Lean.Meta
    Smart unfolding support
    =========================== -/
 
+/-
+Forward declaration. It is defined in the module `src/Lean/Elab/PreDefinition/Structural/Eqns.lean`.
+It is possible to avoid this hack if we move `Structural.EqnInfo` and `Structural.eqnInfoExt`
+to this module.
+-/
+@[extern "lean_get_structural_rec_arg_pos"]
+constant getStructuralRecArgPos? (declName : Name) : CoreM (Option Nat)
+
 def smartUnfoldingSuffix := "_sunfold"
 
 @[inline] def mkSmartUnfoldingNameFor (declName : Name) : Name :=
@@ -588,8 +596,52 @@ mutual
             match ((← getEnv).find? (mkSmartUnfoldingNameFor fInfo.name)) with
             | some fAuxInfo@(ConstantInfo.defnInfo _) =>
               -- We use `preserveMData := true` to make sure the smart unfolding annotation are not erased in an over-application.
-              deltaBetaDefinition fAuxInfo fLvls e.getAppRevArgs (preserveMData := true) (fun _ => pure none) fun e₁ =>
-                smartUnfoldingReduce? e₁
+              deltaBetaDefinition fAuxInfo fLvls e.getAppRevArgs (preserveMData := true) (fun _ => pure none) fun e₁ => do
+                let some r ← smartUnfoldingReduce? e₁ | return none
+                /-
+                  If `smartUnfoldingReduce?` succeeds, we should still check whether the argument the
+                  structural recursion is recursing on reduces to a constructor.
+                  This extra check is necessary in definitions (see issue #1081) such as
+                  ```
+                  inductive Vector (α : Type u) : Nat → Type u where
+                    | nil  : Vector α 0
+                    | cons : α → Vector α n → Vector α (n+1)
+
+                  def Vector.insert (a: α) (i : Fin (n+1)) (xs : Vector α n) : Vector α (n+1) :=
+                    match i, xs with
+                    | ⟨0,   _⟩,        xs => cons a xs
+                    | ⟨i+1, h⟩, cons x xs => cons x (xs.insert a ⟨i, Nat.lt_of_succ_lt_succ h⟩)
+                  ```
+                  The structural recursion is being performed using the vector `xs`. That is, we used `Vector.brecOn` to define
+                  `Vector.insert`. Thus, an application `xs.insert a ⟨0, h⟩` is **not** definitionally equal to
+                  `Vector.cons a xs` because `xs` is not a constructor application (the `Vector.brecOn` application is blocked).
+
+                  Remark 1: performing structural recursion on `Fin (n+1)` is not an option here because it is a `Subtype` and
+                  and the repacking in recursive applications confuses the structural recursion module.
+
+                  Remark 2: the match expression reduces reduces to `cons a xs` when the discriminants are `⟨0, h⟩` and `xs`.
+
+                  Remark 3: this check is unnecessary in most cases, but we don't need dependent elimination to trigger the issue                        fixed by this extra check. Here is another example that triggers the issue fixed by this check.
+                  ```
+                  def f : Nat → Nat → Nat
+                    | 0,   y   => y
+                    | x+1, y+1 => f (x-2) y
+                    | x+1, 0   => 0
+
+                  theorem ex : f 0 y = y := rfl
+                  ```
+
+                  Remark 4: the `return some r` in the following `let` is not a typo. Binport generated .olean files do not
+                  store the position of recursive arguments for definitions using structural recursion.
+                  Thus, we should keep `return some r` until Mathlib has been ported to Lean 3.
+                  Note that the `Vector` example above does not even work in Lean 3.
+                -/
+                let some recArgPos ← getStructuralRecArgPos? fInfo.name | return some r
+                let numArgs := e.getAppNumArgs
+                if recArgPos >= numArgs then return none
+                let recArg := e.getArg! recArgPos numArgs
+                if !(← whnf recArg).isConstructorApp (← getEnv) then return none
+                return some r
             | _ =>
               if (← getMatcherInfo? fInfo.name).isSome then
                 -- Recall that `whnfCore` tries to reduce "matcher" applications.

tests/lean/1081.lean

@@ -0,0 +1,37 @@
+def f : Nat → Nat → Nat
+  | 0,   y   => y
+  | x+1, y+1 => f (x-2) y
+  | x+1, 0   => 0
+
+example : f 0 y = y :=
+  rfl -- Error, it does not hold by reflexivity since the recursion is on `y`
+
+example : f 0 0 = 0 := rfl
+
+example : f 0 (y+1) = y+1 := rfl
+
+inductive Vector (α : Type u) : Nat → Type u where
+  | nil  : Vector α 0
+  | cons : α → Vector α n → Vector α (n+1)
+
+namespace Vector
+  def insert (a: α): Fin (n+1) → Vector α n → Vector α (n+1)
+  | ⟨0  , _⟩,        xs => cons a   xs
+  | ⟨i+1, h⟩, cons x xs => cons x $ xs.insert a ⟨i, Nat.lt_of_succ_lt_succ h⟩
+
+  theorem insert_at_0_eq_cons1 (a: α) (v: Vector α n):  v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v :=
+    rfl -- Error, it does not hold by reflexivity because the recursion is on v
+
+  example (a : α) :  nil.insert a ⟨0, by simp_arith⟩ = cons a nil :=
+    rfl
+
+  example (a : α) (b : α) (bs : Vector α n) :  (cons b bs).insert a ⟨0, by simp_arith⟩ = cons a (cons b bs) :=
+    rfl
+
+  theorem insert_at_0_eq_cons2 (a: α) (v: Vector α n):  v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v := by
+    rw [insert]
+
+  theorem insert_at_0_eq_cons3 (a: α) (v: Vector α n):  v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v := by
+    simp only [insert]
+
+end Vector

tests/lean/1081.lean.expected.out

@@ -0,0 +1,12 @@
+1081.lean:7:2-7:5: error: type mismatch
+  rfl
+has type
+  f 0 y = f 0 y : Prop
+but is expected to have type
+  f 0 y = y : Prop
+1081.lean:23:4-23:7: error: type mismatch
+  rfl
+has type
+  insert a { val := 0, isLt := (_ : 0 < Nat.succ n) } v = insert a { val := 0, isLt := (_ : 0 < Nat.succ n) } v : Prop
+but is expected to have type
+  insert a { val := 0, isLt := (_ : 0 < Nat.succ n) } v = cons a v : Prop