auto-coercion hell

Stream: mathlib4

[Kevin Buzzard]

Here's a maths theorem: $\sum_{0\leq i<n}i^5=(4(n(n-1)/2)^3-(n(n-1)/2)^2)/3.$ The hard part is finding the statement; the proof is "trivial by induction". The theorem involves subtraction and division, so my rule of thumb in Lean is to get the heck out of the naturals ASAP. In Lean 3 my formalisation would look like this:

-- lean 3
import tactic

open_locale big_operators
open finset

lemma sum_fifths (n : ℕ) : ∑ i in range n, (i : ℚ)^5 = (4*(n*(n-1)/2)^3-(n*(n-1)/2)^2)/3 :=
begin
  induction n with d hd,
  { simp, },
  { rw [finset.sum_range_succ, hd],
    simp,
    ring }
end

Note that I coerce i to ℚ on the left hand side, and in lean 3 this was enough to tell lean that the right hand side was to be treated as a rational.

In Lean 4 I'm expecting the proof to be just as simple, but I'm having real trouble writing the statement neatly because I don't properly understand the new way of things with coercions: see lean4#1915 . Here are more and more desperate efforts to get the thing compiling; I finally win but have apparently created a term so monstrous that simp no longer does the base case :-(

import Mathlib

open BigOperators
open Finset

example (n : ℕ) : ∑ i in range n, (i : ℚ)^5 = (4*(n*(n-1)/2)^3-(n*(n-1)/2)^2)/3 := sorry
-- failed to synthesize instance `HPow ℚ ℕ ℕ`

example (n : ℕ) : ∑ i in range n, (i : ℚ)^5 =
  ((4 : ℚ)*(n*(n-1)/2)^3-(n*(n-1)/2)^2)/3 := sorry
-- failed to synthesize instance `HMul ℚ ℕ ?m.2408`
-- failed to synthesize instance `HDiv ℕ ℚ ℚ`

example (n : ℕ) : ∑ i in range n, (i : ℚ)^5 =
  ((4 : ℚ)*(↑n*(↑n-1)/2)^3-(↑n*(↑n-1)/2)^2)/3 := sorry
-- same errors

example (n : ℕ) : ∑ i in range n, (i : ℚ)^5 =
    ((4 : ℚ)*(↑n*(↑n-1 : ℚ)/2)^3-(↑n*(↑n-1 : ℚ)/2)^2)/3 := by -- compiles!
  induction' n with d hd
  { simp } -- (deterministic) timeout at 'simp'
  sorry

I did get this one working:

lemma sum_cubes (n : ℕ) : ∑ i in range n, (i : ℚ)^3 = ((↑n*(↑n-1)/2 : ℚ)^2 : ℚ) := by
  induction' n with d hd
  { simp }
  { rw [Finset.sum_range_succ, hd]
    simp
    ring }

again I'm just randomly adding up-arrows and coercions to Q, so it's definitely possible, but I am not a fan of this trial and error approach. Are there rules of thumb here? Note that this used to be easy.

[Kevin Buzzard]

lemma sum_fifths (n : ℕ) : ∑ i in range n, (i : ℚ)^5 = ((4*(n*(n-1 : ℚ)/2)^3-(n*(n-1 : ℚ)/2)^2)/3 : ℚ):= by
  induction' n with d hd
  { simp only [show Nat.zero = (0 : ℕ) by rfl] -- deterministic timeout :-/
    sorry }
  sorry

Why am I in this hell?

[Yakov Pechersky]

I think simp now tries hard to do rfl style matches or decide in the end? I've have very slow simps also whenever I have a some_finset \mem Finset.filter p univ, which I "fix" by doing simp only [mem_filter, mem_univ].

[Eric Wieser]

The problem is not necessarily the new coercion rules, but the fact that a / b no longer requires a, b, and a / b to be the same type and so Lean can no longer work out the type of b from the type of a

[Kevin Buzzard]

Here's a mathlib4-free version of the hell:

import Std.Data.Rat.Basic

example (n : Nat) (i : Rat) : i = (4*(n*(n-1)/2)^3-(n*(n-1)/2)^2)/3 := sorry
-- failed to synthesize instance `HPow Nat Nat Rat`

[Kevin Buzzard]

@Mario Carneiro you thought about this the first time it came up. Can you see a simple way to get that example above compiling? I am having to insert tons of explicit casts to get this to typecheck. Note that this is not a pathological example, the RHS is $\sum_{i<n}i^5$ and this came up in an undergrad question.

[Kevin Buzzard]

To un-xy, my goal was to port this lean 3 proof that (∑ i in range n, i^3) ∣ (3 * ∑ i in range n, i^5) and I'm running into two issues (the coercion issue and the fact that simp can't do the base case of the induction for the formula for sum of 5th powers)

[Kevin Buzzard]

I can see possible hacks where you clear denominators and try and get things to work over integers, but I find this a bit distasteful. My proof avoids all of this by doing the calculations over Q where it's (in theory) much easier, and then using int.cast_inj at the last minute.

[Eric Wieser]

Is it sufficient to put an arrow before every n?

[Kevin Buzzard]

import Std.Data.Rat.Basic

example (n : Nat) (i : Rat) : i = (4*(↑n*(↑n-1)/2)^3-(↑n*(↑n-1)/2)^2)/3 := sorry
/-
scratch.lean:3:37
failed to synthesize instance
  HPow Nat Nat Rat
scratch.lean:3:53
failed to synthesize instance
  HPow Nat Nat Rat
-/

[Eric Wieser]

Does Lean 4 have an equivalent of #print instances HPow? I guess docs4#HPow answers my question but it's annoying to have to leave the editor

[Matthew Ballard]

If you tell Lean each power is a Nat it won’t complain.

[Eric Wieser]

I think your imports are too minimal

[Eric Wieser]

There is no power operation on the rationals in std

[Eric Wieser]

This was the minimal number of annotations I had to put in:

import Mathlib.Data.Rat.Basic

example (n : Nat) (i : Rat) : i = (4*(n*(n-(1 : ℚ))/2)^3-(n*(n-(1 : ℚ))/2)^2)/3 := sorry

[Kevin Buzzard]

So my argument is that we can't expect people to have to work this out, this is not great at all.

[Kevin Buzzard]

The game isn't "find the minimal coercions that work in each case", the system seems to be broken here.

[James Gallicchio]

an idea: ocaml-style Namespace.( whatever + operations / 2 * i - want) syntax for arithmetic. So that way you can write Rat.( 4*(n*...) ) and know all of the arithmetic operations are the Rat versions of those operations.

[James Gallicchio]

doesnt have to be a generalpurpose language feature, just a special solution for distinguishing Nat/Int/Rat/Real arithmetic, since it can be hard to distinguish them (and they're not always equivalent)

[James Gallicchio]

We might already have the tools necessary to do this, by adding a new namespace eg Rational.Notation with high-priority default instances of all the arithmetic specialized to Rat. and then open Rational.Notation in ... is a way of locally forcing stuff to be in Rational

[Eric Wieser]

I wonder if disabling the default behavior that 37 is a nat would help here