Proof of sum of Fintype broke after updating lean

Stream: new members

[Michael Fishman]

I have a function over a Fintype that sums to one. In leanprover/lean4:v4.8.0-rc1, I can prove that it sums to 1 using rfl. In leanprover/lean4:v4.26.0-rc2, the same proof fails. How do I repair the proof?

import Mathlib
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Algebra.Order.BigOperators.Group.Finset

open Finset BigOperators

inductive Color
  | Blue
  | Red
deriving Repr, Fintype, Nonempty, DecidableEq

def uniform_color (c : Color) : ℚ :=
  match c with
    | Color.Blue => 1/2
    | Color.Red => 1/2

def my_sum := ∑ x, uniform_color x

#check my_sum -- ℚ
#eval my_sum -- mkRat 1 1
#check mkRat 1 1 -- mkRat 1 1 : ℚ


def my_sum_is_one : my_sum = (mkRat 1 1) := by rfl

Error message:

Tactic `rfl` failed: The left-hand side
  my_sum
is not definitionally equal to the right-hand side
  mkRat 1 1

[Michael Fishman]

When using leanprover/lean4:v4.8.0-rc1, mathlib is on a5eb48ce9eb3a014115cc27e69f022a7d2edd44e
When using leanprover/lean4:v4.26.0-rc2, mathlib is on d5c9558e75342a10d6321e6a8c798a14f68ae23c

[emlis]

I tried a few different methods to fix this. It seems that rfl' is the best option here. It works without adding the extra axioms that native_decide introduces (like Lean.trustCompiler).

Here is the comparison of the different approaches I tested:

import Mathlib

open Finset BigOperators

inductive Color
  | Blue
  | Red
deriving Repr, Fintype, Nonempty, DecidableEq

def uniform_color (c : Color) : ℚ :=
  match c with
    | Color.Blue => 1/2
    | Color.Red => 1/2

def my_sum := ∑ x, uniform_color x

#check my_sum -- ℚ
#eval my_sum -- mkRat 1 1
#check mkRat 1 1 -- mkRat 1 1 : ℚ
#reduce mkRat 1 1
#reduce my_sum


def my_sum_is_one : my_sum = (mkRat 1 1) := by native_decide
def my_sum_is_one' : my_sum = (mkRat 1 1) := by {
  unfold my_sum
  conv => enter [1, 1]; rw [show univ = {Color.Blue, Color.Red} by rfl]
  simp [uniform_color, field]; ring
}
def my_sum_is_one'' : my_sum = (mkRat 1 1) := by rfl'


/--
info: 'my_sum_is_one' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound]
-/
#guard_msgs in
#print axioms my_sum_is_one
/--
info: 'my_sum_is_one'' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms my_sum_is_one'
/--
info: 'my_sum_is_one''' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms my_sum_is_one''

[Eric Wieser]

unseal Rat.add Rat.inv Rat.mul in
def my_sum_is_one : my_sum = (mkRat 1 1) := rfl

also works