Cannot derive functional induction principle

[ineol]

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

In the following snippet, Lean fails to generate the functional induction principle

import Std.Data.HashMap

section worklist

variable (A : Type) (S : Type) [BEq S] [Hashable S]

structure St where
  m : A
  map : Std.HashMap S Nat := ∅

def St.meas' (st : St A S) : Nat := Nat.zero
def run (ss : S) : A :=
  go sorry
where go (st0 : St A S) : A :=
        let st1 := { st0 with map := st0.map.insert ss 0 }
        if let some s := st1.map.get? ss then
          have : st1.meas' ≤ st1.meas' := by sorry -- 1
          have : st1.meas' < st0.meas' := by sorry -- 2
          go st1
        else
          st0.m
      decreasing_by sorry

#check run.go.induct

with the error

Failed to realize constant run.go.induct:
  Cannot derive functional induction principle (please report this issue)
  
    function expected
      @A ⋯

It works if either of the lines marked with 1 and 2 are deleted.

Versions

4.12.0-nightly-2024-10-17

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!

[nomeata]

This is very curious. I have condensed it to

axiom Std.HashMap : Type
axiom Std.HashMap.insert : Std.HashMap → Std.HashMap
axiom Std.HashMap.get? : Std.HashMap → Int → Option Unit


section worklist

variable (S : Type)

structure St where
  m : Bool
  map : Std.HashMap

opaque P : St → Prop
opaque f : St → St := id
opaque g : St → Option Nat

noncomputable
def go1 (ss : Int) (st0 : St) : Bool :=
        let st1 := { st0 with map := st0.map.insert }
        -- let st1 : St := { st0 with map := st0.map.insert } -- type annotation here helps!
        match st1.map.get? ss with -- the ss argument is needed
        | some _ =>
          have : P st1 := sorry -- both needed
          have : P st1 := sorry -- both needed
          go1 ss st1
        | none => true
      termination_by st0
      decreasing_by sorry

#check go1.induct

and then found out that changing the let expression to

        let st1 : St := { st0 with map := st0.map.insert }

i.e. adding a type annotation, unbreaks it!

These functions are very much the same, only with pp.raw there is a difference; the broken one has a [mdata save_info:1 …] around the match.

Now let’s see what that is, why it is in the resulting definition, and why it throws the induction principle generator off.