can't spot but (failed to synthesize instance)

Stream: new members

[rzeta0]

I'm doing the final exercise of MoP 6.3. This question isn't about the exercise lesson.

There is a bug in a calc section which I can't identify:

· calc
        0.4 * 1.6 ^ (k + 1 + 1) = 1.6 * (0.4 * 1.6 ^ (k + 1)) := by ring -- < -- error
        _ = (0.4 * 1.6 ^ (k + 1)) +  0.6 * (0.4 * 1.6 ^ (k + 1)):= by ring -- < -- error
        _ = (0.4 * 1.6 ^ (k + 1)) +  0.96 * (0.4 * 1.6 ^ k):= by ring -- < -- error
        _ < ((F (k + 1)):ℚ) + 0.96 * ((F k):ℚ) := by rel [ih2a, ih1a]
        _ < ((F (k + 1)):ℚ) + ((F k):ℚ) := by extra
        _ = ((F (k +1 + 1)):ℚ) := by rw [F]

The error is the same for the 3 highighted lines:

failed to synthesize instance
  HPow Float ℕ Float

I can't find any information online about what this could be. I'd welcome guidance.

It isn't a short proof which is why I haven't replicated it all here. I also can't produce an MWE sadly.

[Julian Berman]

That error says "I don't know how to raise a float to a natural number power and get a resulting float out of that".

[Julian Berman]

Glancing at https://hrmacbeth.github.io/math2001/06_Induction.html#id21, note that in the exercise, there's (0.4 : \Q), not just 0.4 -- so there we have a rational number rather than a float, and likely Lean will be happy. Add that explicit type and see if things work.

[rzeta0]

Thanks Julian - I'll have a go.

[Kyle Miller]

Sadly, a limitation of calc is that you need to manually insert type hints. It's not able to get types out of the goal.

(I got very far along the way toward adding this functionality once, only to come across a test file that showed exactly why this limitation is unavoidable.)

[Daniel Weber]

Do you happen to recall which test file it was? I'm curious

[Kyle Miller]

@Daniel Weber https://github.com/leanprover/lean4/blob/827c6676fd339b147258c05fda75b3cf6dc0fd31/src/Lean/Elab/Calc.lean#L151-L161