incorrect functional induction principle

[BrunoDutertre]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

On the following example, test.induct is incorrect.

def f (x: Nat): Option Nat :=
  if x > 10 then some 0 else none

def test (x: Nat): Nat :=
  match f x, x with
  | some k, _ => k
  | none, 0 => 0
  | none, n + 1 => test n

#check test.induct

It looks like this:

test.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), motive x) (case2 : motive 0)
  (case3 : ∀ (n : Nat), motive n → motive n.succ) (x : Nat) : motive x

and case1 is missing an assumption like f x = some k.

Steps to Reproduce

Run lean on the example.

Expected behavior:

Something like this:

test.induct (motive : Nat → Prop) (case1 : ∀ (x k : Nat), f x = some k → motive x) (case2 : motive 0)
  (case3 : ∀ (n : Nat), motive n → motive n.succ) (x : Nat) : motive x

Actual behavior:

Wrong induction principle.

Versions

"4.11.0"

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

Thanks for the report! I'll investigate. If I'm lucky then #4149 might already fix it, we'll see.

I was hoping that two separate match statements might fix this, but it fails even worse:
https://live.lean-lang.org/#codez=CYUwZgBJAUAeBcEByBDALgSkQeQA5oEsB7AO2XQngF4AoCCAyWCAPggEYAGCNACxDIBnIgFsQEbiAA2g8SVIgadCKEhoQgtBDiJUmXRWrL6I9AGNeES4iYQA7gT4RjEAD4RhYiAGsIVNt4u7vIk4v4QpmgWEMwOfC70iW4SfmycCUnJZADUHKk8GlokSpmZAMQWIGa+6poAdAQkwACuZmhAA

[BrunoDutertre]

I tried nested match statements but that can cause another problem: #2962

[nomeata]

A quick test confirms my worry that the MVarId.cleanup step is at fault:

[Meta.FunInd] Goal before cleanup:
case hyp
motive : Nat → Prop
t : Nat
f : Nat.ibelow t
k x✝² : Nat
x✝¹ : _root_.f t = some k
x✝ : Nat.ibelow x✝²
⊢ motive x✝²
 

[Meta.FunInd] Goal after cleanup (toClear := [f, x✝]) (toPreserve := []):
case hyp
motive : Nat → Prop
x✝ : Nat
⊢ motive x✝

But if I put too much stuff into toPreserve array, then we also get induction principles that are not nice, because they contain completely unused variables, e.g.

info: ackermann.induct (motive : Nat → Nat → Prop) (case1 : Nat → Nat → ∀ (m : Nat), motive 0 m)
  (case2 : Nat → Nat → ∀ (n : Nat), motive n 1 → motive n.succ 0)
  (case3 : Nat → Nat → ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) :
  ∀ (a a_1 : Nat), motive a a_1

This may need more careful thought, or a possibly a completely different approach. (Maybe instead of the blunt MVarId.cleanUp, only clean up the context very selectively to not remove useful assumptions.)

[nomeata]

Ah, here is a partial work-around for you: If you put h : x in the match you get the assumption at least in two of the three cases:

def f (x: Nat): Option Nat :=
  if x > 10 then some 0 else none

def test (x: Nat): Nat :=
  match f x, h : x with
  | some k, _ => k
  | none, 0 => 0
  | none, n + 1 => test n

/--
info: test.induct (motive : Nat → Prop) (case1 : ∀ (k x : Nat), f x = some k → motive x) (case2 : motive 0)
  (case3 : ∀ (n : Nat), f n.succ = none → motive n → motive n.succ) (x : Nat) : motive x
-/
#guard_msgs in
#check test.induct

But yes, this is not satisfactory.