From d1e47120381314bcde230ef4affc1e2d777bf66f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Mar 2022 15:49:14 -0700 Subject: [PATCH] fix: smart unfolding See new comment to understand the issue. closes #1081 --- .../Elab/PreDefinition/Structural/Eqns.lean | 5 ++ src/Lean/Meta/WHNF.lean | 56 ++++++++++++++++++- tests/lean/1081.lean | 37 ++++++++++++ tests/lean/1081.lean.expected.out | 12 ++++ 4 files changed, 108 insertions(+), 2 deletions(-) create mode 100644 tests/lean/1081.lean create mode 100644 tests/lean/1081.lean.expected.out diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index e5603b6d22..f9308b8a2d 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/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? diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 9b902fce0f..4dad9c83c2 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/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. diff --git a/tests/lean/1081.lean b/tests/lean/1081.lean new file mode 100644 index 0000000000..7a85300181 --- /dev/null +++ b/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 diff --git a/tests/lean/1081.lean.expected.out b/tests/lean/1081.lean.expected.out new file mode 100644 index 0000000000..e593e6ad56 --- /dev/null +++ b/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