-
Notifications
You must be signed in to change notification settings - Fork 414
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Cannot derive functional induction principle #5767
Comments
Thanks for the report! |
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 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 Now let’s see what that is, why it is in the resulting definition, and why it throws the induction principle generator off. |
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
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
with the error
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.
The text was updated successfully, but these errors were encountered: