LibrarySearch application type mismatch (Nat + Subsingleton)

Stream: mathlib4

[Yakov Pechersky]

This is blocking mathlib4#669, where adding eq_of_zero_eq_one in the presence of CommSemiring Nat breaks the LibrarySearch test file. MWE:

import Mathlib.Tactic.LibrarySearch

class MulZeroOneClass (M₀ : Type u) extends Mul M₀, Zero M₀, One M₀ where
  zero_mul : ∀ a : M₀, 0 * a = 0
  mul_zero : ∀ a : M₀, a * 0 = 0
  one_mul : ∀ a : M₀, 1 * a = a
  mul_one : ∀ a : M₀, a * 1 = a

open MulZeroOneClass (zero_mul mul_zero one_mul mul_one)

variable {M₀ : Type u} [MulZeroOneClass M₀]

theorem subsingleton_of_zero_eq_one (h : (0 : M₀) = 1) : Subsingleton M₀ :=
  ⟨fun a b => by rw [←mul_one a, ←h, mul_zero, ←mul_one b, ←h, mul_zero]⟩

theorem eq_of_zero_eq_one (h : (0 : M₀) = 1) (a b : M₀) : a = b :=
  @Subsingleton.elim _ (subsingleton_of_zero_eq_one h) a b

namespace Nat

instance : MulZeroOneClass Nat where
  mul_one := Nat.mul_one
  one_mul := Nat.one_mul
  zero_mul := Nat.zero_mul
  mul_zero := Nat.mul_zero

end Nat

example (x y : Nat) : x + y = y + x := by library_search
/-
application type mismatch
  congrArg (@OfNat.ofNat Nat 0) (congrArg (@Zero.toOfNat0 Nat) rfl)
argument has type
  Zero.toOfNat0 = Zero.toOfNat0
but function has type
  Zero.toOfNat0 = { ofNat := One.one } → 0 = 0
-/

[Wojciech Nawrocki]

I am looking at this now, but maybe someone can beat me to it :)

[Yakov Pechersky]

I tried using set_option trace.Tactic.librarySearch true and editing the tactic to see why it thinks it can prove 0 = 1 but didn't get anywhere

[Wojciech Nawrocki]

Indeed the actual bug seems to be in solve_by_elim

set_option trace.solveByElim true in
example : (@OfNat.ofNat ℕ 0 Zero.toOfNat0) = @OfNat.ofNat ℕ 1 One.toOfNat1 := by
  solve_by_elim

the tactic suceeds but fails to typecheck.

[David Renshaw]

I can look at this for a bit now if you have a mwe with just solve_by_elim. (I recently touched that code.)

[David Renshaw]

ah, yep, seeing that behavior. weird

[David Renshaw]

[Meta.Tactic.solveByElim] Working on: ⊢ OfNat.ofNat 0 = OfNat.ofNat 1
[Meta.Tactic.solveByElim] Trying to apply: rfl  of type ?m.4307 = ?m.4307
[Meta.Tactic.solveByElim] Trying to apply: congrArg  of type ∀ (f : ?m.4310 → ?m.4311),
      ?m.4312 = ?m.4313 → f ?m.4312 = f ?m.4313
[Meta.Tactic.solveByElim] Working on: case h
    ⊢ Zero.toOfNat0 = { ofNat := One.one }
[Meta.Tactic.solveByElim] Trying to apply: rfl  of type ?m.4335 = ?m.4335
[Meta.Tactic.solveByElim] Trying to apply: congrArg  of type ∀ (f : ?m.4338 → ?m.4339),
      ?m.4340 = ?m.4341 → f ?m.4340 = f ?m.4341
[Meta.Tactic.solveByElim] Working on: case h.h
    ⊢ CommMonoidWithZero.toZero = ?m.4341
[Meta.Tactic.solveByElim] Trying to apply: rfl  of type ?m.4357 = ?m.4357

[Wojciech Nawrocki]

example : (@OfNat.ofNat ℕ 0 Zero.toOfNat0) = @OfNat.ofNat ℕ 1 One.toOfNat1 := by
  apply congrArg
  apply congrArg
  apply rfl

[Wojciech Nawrocki]

Shows Goals accomplished and fails typechecking; it is fine if apply lets you write yourself into a corner, but this seems like a Lean bug.

[David Renshaw]

wow!

[David Renshaw]

self contained:

class Zero.{u} (α : Type u) where
  zero : α

instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
  zero := 0

class One (α : Type u) where
  one : α

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
  one := 1

example : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
  apply congrArg
  apply congrArg
  apply rfl

[David Renshaw]

@Wojciech Nawrocki do you want to report this on the Lean4 repo, or should I?

[Wojciech Nawrocki]

Go ahead please! @David Renshaw

[David Renshaw]

https://github.com/leanprover/lean4/issues/1870

[Moritz Doll]

it seems to be the second apply that causes problems (you can replace the first by refine and the third by exact)

[Moritz Doll]

example : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
  refine congrArg _ ?_
  apply congrArg _
  exact rfl

fails with the same error, but inserting ?_ gives a sensible error