Strange `field_simp` failure

Stream: mathlib4

[Adam Topaz]

One of the students in my formalization class found the following curious behavior of field_simp:

import Mathlib.Tactic

class Test (M : Type) extends Mul M -- comment out this line...

example (x y z : F) [Field F] (h₁ : z ≠ 0) (h₂ : 1 - z ≠ 0) :
    (x + y/z) + x * z/(1 - z) = (x - y)/(1-z) + y/(z * (1-z)) := by
  field_simp
  ring -- fails

Commenting out the Test class line makes the example work just fine. Also, replacing Mul with Add in the definition of Test also fixes the issue. I spent a few minutes trying to minimize the example, but couldn't find a smaller example.

[Damiano Testa]

Adam, I am assuming that you are working in a project that depends on Mathlib, right?

Within Mathlib, adding variable {F}/variable {F : Type _} switches the behaviour: Test confuses ringfield_simp, omitting it makes it work.

import Mathlib.Tactic

variable {F}

--class Test (M : Type) extends Mul M -- uncomment this line...

example (x y z : F) [Field F] (h₁ : z ≠ 0) (h₂ : 1 - z ≠ 0) :
    (x + y/z) + x * z/(1 - z) = (x - y)/(1-z) + y/(z * (1-z)) := by
  field_simp
  ring -- fails

However, variable {F : Type*} seems to work fine regardless of the presence of Test.

[David Renshaw]

on the first example, with set_option trace.Tactic.field_simp true I see

[Tactic.field_simp] ✅ discharge z ≠ 0
[Tactic.field_simp] ✅ discharge 1 - z ≠ 0
[Tactic.field_simp] ✅ discharge z ≠ 0
[Tactic.field_simp] ❌ discharge z * (1 - z) ≠ 0
  [Tactic.field_simp] ❌ discharge IsLeftRegular z
  [Tactic.field_simp] ❌ discharge IsRightRegular (1 - z)
[Tactic.field_simp] ✅ discharge 1 - z ≠ 0
[Tactic.field_simp] ❌ discharge z * (1 - z) ≠ 0
  [Tactic.field_simp] ❌ discharge IsLeftRegular z
  [Tactic.field_simp] ❌ discharge IsRightRegular (1 - z)
[Tactic.field_simp] ❌ discharge z * (1 - z) ≠ 0
  [Tactic.field_simp] ❌ discharge IsLeftRegular z
  [Tactic.field_simp] ❌ discharge IsRightRegular (1 - z)
[Tactic.field_simp] ❌ discharge z * (1 - z) ≠ 0
  [Tactic.field_simp] ❌ discharge IsLeftRegular z
  [Tactic.field_simp] ❌ discharge IsRightRegular (1 - z)
[Tactic.field_simp] ✅ discharge 1 - z ≠ 0
[Tactic.field_simp] ❌ discharge z * (1 - z) ≠ 0
  [Tactic.field_simp] ❌ discharge IsLeftRegular z
  [Tactic.field_simp] ❌ discharge IsRightRegular (1 - z)
[Tactic.field_simp] ❌ discharge z * (1 - z) ≠ 0
  [Tactic.field_simp] ❌ discharge IsLeftRegular z
  [Tactic.field_simp] ❌ discharge IsRightRegular (1 - z)

and then when I comment out the class command I see

[Tactic.field_simp] ✅ discharge z ≠ 0
[Tactic.field_simp] ✅ discharge 1 - z ≠ 0
[Tactic.field_simp] ✅ discharge z ≠ 0
[Tactic.field_simp] ✅ discharge z * (1 - z) ≠ 0
  [Tactic.field_simp] ✅ discharge z ≠ 0
  [Tactic.field_simp] ✅ discharge 1 - z ≠ 0
[Tactic.field_simp] ✅ discharge 1 - z ≠ 0
[Tactic.field_simp] ✅ discharge (1 - z) * (z * (1 - z)) ≠ 0
  [Tactic.field_simp] ✅ discharge 1 - z ≠ 0
  [Tactic.field_simp] ✅ discharge z * (1 - z) ≠ 0
    [Tactic.field_simp] ✅ discharge z ≠ 0
    [Tactic.field_simp] ✅ discharge 1 - z ≠ 0
[Tactic.field_simp] ✅ discharge z * (1 - z) ≠ 0
  [Tactic.field_simp] ✅ discharge z ≠ 0
  [Tactic.field_simp] ✅ discharge 1 - z ≠ 0

[David Renshaw]

Ah, the problem is that F is an auto-implicit (as Damiano also discovered).

[David Renshaw]

This works as expected:

example {F : Type*} (x y z : F) [Field F] (h₁ : z ≠ 0) (h₂ : 1 - z ≠ 0) :
    (x + y/z) + x * z/(1 - z) = (x - y)/(1-z) + y/(z * (1-z)) := by
  field_simp; ring

[Adam Topaz]

Ok, yes, I agree that auto implicit had something to do with it in the original example, but I still have no idea why the following doesn't work

import Mathlib.Tactic

set_option autoImplicit false

class Test (M : Type) extends Mul M -- comment out this line...

example {F : Type _} (x y z : F) [Field F] (h₁ : z ≠ 0) (h₂ : 1 - z ≠ 0) :
    (x + y/z) + x * z/(1 - z) = (x - y)/(1-z) + y/(z * (1-z)) := by
  field_simp
  ring -- fails

but the following works just fine:

import Mathlib.Tactic

set_option autoImplicit false

example {F : Type _} (x y z : F) [Field F] (h₁ : z ≠ 0) (h₂ : 1 - z ≠ 0) :
    (x + y/z) + x * z/(1 - z) = (x - y)/(1-z) + y/(z * (1-z)) := by
  field_simp
  ring -- works

[Adam Topaz]

Aha! This works as well:

import Mathlib.Tactic

set_option autoImplicit false

class Test (M : Type _) extends Mul M -- comment out this line...

example {F : Type _} (x y z : F) [Field F] (h₁ : z ≠ 0) (h₂ : 1 - z ≠ 0) :
    (x + y/z) + x * z/(1 - z) = (x - y)/(1-z) + y/(z * (1-z)) := by
  field_simp
  ring -- works

[Adam Topaz]

So it actually looks like the issue has to do with universes somehow!

[David Renshaw]

With {F : Type _}, the universe of F is a metavariable

[David Renshaw]

with {F : Type*}, the universe is explicitly bound

[Adam Topaz]

I understand, but why does adding class Test ... change the behavior?

[Adam Topaz]

In the {F : Type _} case.

[Sebastien Gouezel]

Rule of thumb: left of the colon, always use Type* or Type u, never Type _.

[Adam Topaz]

I'm not looking for rules of thumb. I want to understand what's actually going on.

[Matthew Ballard]

Do you have just (M : Type) there?

[Kevin Buzzard]

Yeah. Changing it to the evil Type _ fixes it :-)

[Matthew Ballard]

Sounds like it is bailing after failing to unify the first universe pair it finds

[David Renshaw]

yeah, my working principle is that if metavariables are showing up in my goal view, then all bets are off

[Adam Topaz]

yeah exactly. that's another mystery

[Matthew Ballard]

Ah, the old "field_simp refused to clear denominators"

[Adam Topaz]

Oh that's been pointed out before?

[Matthew Ballard]

In my experience, that is the number one type of failure. I still have an open PR that helps with this and other things

[Matthew Ballard]

But I got pulled away

[Adam Topaz]

Oh, that's precisely what's happening.... field simp will not clear the z * (1 - z) denominators, but it clears z and (1-z).

[Sebastien Gouezel]

Funny fact: if you replace example with lemma, it works. But it fails with def.

[Matthew Ballard]

Oh my

[Adam Topaz]

Ok, now I'm even more confused.

[Adam Topaz]

Just to clarify, I know very well when to use explicit universes Type u and/or Type*. This came up when one of the students in my class was playing around with some code I wrote during class. I think such issues really don't look good for newcomers :-/

[Eric Rodriguez]

Is this the thing about lemma forcing elaboration of the expected type?

[Eric Rodriguez]

Or has that vanished since lean3?

[Mauricio Collares]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Failure.20of.20TC.20search.20in.20.60simp.60.20with.20.60etaExperiment.60.2E/near/356781639

[Matthew Ballard]

Lean really wants Group F in the failure case

[Matthew Ballard]

Actually in both cases

[Adam Topaz]

yeah I think the trace that David posted above is quite telling.

[Adam Topaz]

FWIW, here's a slightly smaller example to play with:

import Mathlib.Tactic

set_option autoImplicit false

class Test (M : Type) extends Mul M -- comment out this line...

example {F : Type _} (z w : F) [Field F] (h₁ : z ≠ 0) (h₂ : w ≠ 0) :
    1 + 1 / z + 1 / w = (w + z) / (z * w) + 1 := by
  field_simp
  ring -- fails

[Adam Topaz]

Moving the 1 + to the other side of the LHS of the equality makes the example work again :rofl:

[Matthew Ballard]

It wants docs#div_eq_iff

[Matthew Ballard]

It gets that in both cases. But it cannot discharge z * (1 -z) ≠ 0 with docs#mul_ne_zero

[Matthew Ballard]

It looks like it has trouble with Mul F

[Matthew Ballard]

[Tactic.field_simp] ❌ discharge z * (1 - z) ≠ 0 ▼
  [Meta.Tactic.simp.unify] @sub_self:1000, failed to unify
        ?a - ?a
      with
        1 - z
  [Meta.Tactic.simp.discharge] @tsub_eq_zero_of_le, failed to synthesize instance
        CanonicallyOrderedAddCommMonoid F
  [Meta.Tactic.simp.discharge] @CharTwo.sub_eq_add, failed to synthesize instance
        CharP F 2
  [Meta.Tactic.simp.unify] @Ordinal.enum_le_enum:1000, failed to unify
        ¬?r (Ordinal.enum ?r ?o' ?ho') (Ordinal.enum ?r ?o ?ho)
      with
        z * (1 - z) ≠ 0
  [Meta.Tactic.simp.rewrite] @ne_eq:1000, z * (1 - z) ≠ 0 ==> ¬z * (1 - z) = 0
  [Meta.Tactic.simp.discharge] @mul_ne_zero, failed to synthesize instance
        Mul F

[Matthew Ballard]

[Meta.synthInstance] 💥 Mul F ▼
  [] new goal Mul F ▼
    [instances] #[@Semigroup.toMul, @MulOneClass.toMul, @MulZeroClass.toMul, @Distrib.toMul, @NonUnitalNonAssocSemiring.toMul, @NonUnitalNonAssocRing.toMul, @CanonicallyOrderedCommSemiring.toMul, @Test.toMul]
  [] 💥 apply @Test.toMul to Mul F ▼
    [tryResolve] 💥 Mul F ≟ Mul ?m.5577

[Matthew Ballard]

A have : Mul F := inferInstance is totally fine though. And it isn't any secret timeout

[Matthew Ballard]

Perhaps there is something about how the discharger is written

[Matthew Ballard]

No it most likely due to something with universe unification

[Adam Topaz]

Here's a fully minimal example

import Mathlib.Tactic

set_option autoImplicit false

class Test (M : Type) extends Mul M -- comment out this line...

example {F : Type _} (z w : F) [Field F] (h₁ : z ≠ 0) (h₂ : w ≠ 0) : z * w ≠ 0 := by
  field_simp

[Matthew Ballard]

simp doesn't close it either

[Adam Topaz]

Sure, but I wouldn't expect it to.

[Matthew Ballard]

But it does apply mul_eq_zero

[Adam Topaz]

the full simp trace without the class:

[Meta.Tactic.simp.unify] @Ordinal.enum_le_enum:1000, failed to unify
      ¬?r (Ordinal.enum ?r ?o' ?ho') (Ordinal.enum ?r ?o ?ho)
    with
      z * w ≠ 0

[Meta.Tactic.simp.rewrite] @ne_eq:1000, z * w ≠ 0 ==> ¬z * w = 0

[Meta.Tactic.simp.rewrite] @mul_ne_zero:1000, z * w = 0 ==> False

[Meta.Tactic.simp.unify] @Ordinal.enum_le_enum:1000, failed to unify
      ¬?r (Ordinal.enum ?r ?o' ?ho') (Ordinal.enum ?r ?o ?ho)
    with
      ¬False

[Meta.Tactic.simp.rewrite] not_false_eq_true:1000, ¬False ==> True

and with the class, here are the first few lines of the trace:

[Meta.Tactic.simp.unify] @Ordinal.enum_le_enum:1000, failed to unify
      ¬?r (Ordinal.enum ?r ?o' ?ho') (Ordinal.enum ?r ?o ?ho)
    with
      z * w ≠ 0

[Meta.Tactic.simp.rewrite] @ne_eq:1000, z * w ≠ 0 ==> ¬z * w = 0

[Meta.Tactic.simp.discharge] @mul_ne_zero, failed to synthesize instance
      Mul F

[Adam Topaz]

this is the usual simp trace, but with the field_simp tactic.

[Adam Topaz]

I suppose this is something you already noticed, Matt?

[Matthew Ballard]

Yeah, it just blows up at the Mul F synthesis

[Adam Topaz]

Changing Test to either

class A (X : Type)
  [inst : Mul X]

or

class A (X : Type) [Mul X]

both resolve the issue as well.

[Matthew Ballard]

simp does not appear to need this

Matthew Ballard said:

[Meta.synthInstance] 💥 Mul F ▼
  [] new goal Mul F ▼
    [instances] #[@Semigroup.toMul, @MulOneClass.toMul, @MulZeroClass.toMul, @Distrib.toMul, @NonUnitalNonAssocSemiring.toMul, @NonUnitalNonAssocRing.toMul, @CanonicallyOrderedCommSemiring.toMul, @Test.toMul]
  [] 💥 apply @Test.toMul to Mul F ▼
    [tryResolve] 💥 Mul F ≟ Mul ?m.5577

More precisely

[Matthew Ballard]

I would nice to pull this out of field_simp

[Heather Macbeth]

I think there's also a positivity bug here. Note that this works:

import Mathlib.Tactic

class Test (M : Type) extends Mul M -- comment out this line...

example (x y z : ℚ)  (h₁ : z ≠ 0) (h₂ : 1 - z ≠ 0) :
    (x + y/z) + x * z/(1 - z) = (x - y)/(1-z) + y/(z * (1-z)) := by
  field_simp
  ring

[Heather Macbeth]

I'm guessing the issue is:

import Mathlib.Tactic.Positivity
import Mathlib.Data.Rat.Order

example (z : F) [Field F] (h₁ : z ≠ 0) (h₂ : 1 - z ≠ 0) : z * (1 - z) ≠ 0 := by
  positivity -- fails

example (z : ℚ) (h₁ : z ≠ 0) (h₂ : 1 - z ≠ 0) : z * (1 - z) ≠ 0 := by
  positivity -- works

[Heather Macbeth]

i.e. perhaps the multiplication positivity discharger is specialized unnecessarily to ordered fields?

[Matthew Ballard]

Can at least reduce to import Mathlib.Tactic.FieldSimp

[Heather Macbeth]

I'm guessing this line is too demanding.

[Matthew Ballard]

If I yank out positivity from field_simp it still fails

[Matthew Ballard]

Actually if I yank out the whole discharger it still fails

[Heather Macbeth]

My guess: there are two different bugs, and Adam's was not caught earlier because people usually use field_simp on ordered fields and positivity was covering for Adam's bug.

[Matthew Ballard]

With the same error of course

[Matthew Ballard]

Set dis to none here and we still end up not synthesizing Mul F

[Matthew Ballard]

syntax (name := myfieldSimp) "myfield_simp" : tactic

elab_rules : tactic
| `(tactic| myfield_simp) => withMainContext do
  let loc := expandOptLocation (mkOptionalNode none)
  let thms0 ← getSimpTheorems

  let some ext ← getSimpExtension? `field_simps | throwError "field_simps not found"
  let thms ← ext.getTheorems

  let ctx : Simp.Context := {
     simpTheorems := #[thms,thms0]
     congrTheorems := (← getSimpCongrTheorems)
  }

  _ ← simpLocation ctx none loc

still has the same behavior

[Matthew Ballard]

This still has the Mul F synthesization problem. You need to register_simp_attr mysimp in a dependent file.

import Mathlib.Init.ZeroOne
import Mathlib.Tactic.Attr.Register

universe u v w

class Semigroup' (α : Type u) extends Mul α

open Lean Elab Tactic Meta

syntax (name := mySimp) "my_simp" : tactic

elab_rules : tactic
| `(tactic| my_simp) => withMainContext do
  let loc := expandOptLocation (mkOptionalNode none)

  let some ext ← getSimpExtension? `mysimp | throwError "💩"
  let thms ← ext.getTheorems

  let ctx : Simp.Context := {
     simpTheorems := #[thms]
  }

  _ ← simpLocation ctx none loc

class Test (M : Type) extends Mul M -- comment out this line...

@[mysimp]
theorem ne_eq' {α : Sort v} (a b : α) : (a ≠ b) = ¬(a = b) := rfl

@[mysimp]
theorem mul_ne_zero' {M₀ : Type w} [Mul M₀] [Zero M₀] {a b : M₀}
    (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 := sorry

set_option trace.Meta.Tactic.simp true in
example {F : Type _} (z w : F) [Semigroup' F] [Zero F] (h₁ : z ≠ 0) (h₂ : w ≠ 0) : z * w ≠ 0 := by
  my_simp

[Matthew Ballard]

Forgot

[Meta.isLevelDefEq] 💥 0 =?= ?u.4092 ▼
  [stuck] 0 =?= ?u.4092

[Matthew Ballard]

Looks like a problem unifying universe number literals because (M : Type 10) behaves the same

[Matthew Ballard]

I assume we never recover from a stuck universe unification problem?

[Matthew Ballard]

Smaller

import Mathlib.Init.ZeroOne

universe u w

class Semigroup' (α : Type u) extends Mul α

class Test (M : Type 10) extends Mul M -- comment out this line...

theorem mul_ne_zero' {M₀ : Type w} [Mul M₀] [Zero M₀] {a b : M₀} : ¬ (a * b = 0) := sorry

set_option trace.Meta.isLevelDefEq true in
set_option trace.Meta.Tactic.simp true in
example {F : Type _} (z w : F) [Semigroup' F] [Zero F] :  ¬ (z * w = 0) := by
  simp only [mul_ne_zero'] -- failed to synthesize instance Mul F

[Matthew Ballard]

Mathlib free

universe u v w

def TooShort (M : Type w) : Prop := sorry

class Semigroup' (α : Type u) extends Mul α

class Test (M : Type 10) extends Mul M

theorem mul_ne_zero' {M₀ : Type v} [Mul M₀] : TooShort M₀ := sorry

set_option trace.Meta.isLevelDefEq true in
set_option trace.Meta.Tactic.simp true in
example {F : Type _} [Semigroup' F] : TooShort F := by
  simp only [mul_ne_zero']

/-
[Meta.isLevelDefEq] 💥 10 =?= ?u.63 ▼
  [stuck] 10 =?= ?u.63

[Meta.Tactic.simp.discharge] @mul_ne_zero', failed to synthesize instance
      Mul F
-/

[Matthew Ballard]

Change Semigroup' to Mul and it succeeds. Change (F : Type _) to a variable or change (M : Type 10) to a variable and it succeeds

[Matthew Ballard]

Sadly I would have to use «Too$hort»

[Damiano Testa]

If you swap Semigroup' and Test it succeeds.

[Matthew Ballard]

Instance priority

[Matthew Ballard]

Can I open private with core files?

[Alex J. Best]

Matthew Ballard said:

Can I open private with core files?

you should be able to yes

[Matthew Ballard]

Can I alias the declaration at the same time?

[Mario Carneiro]

you can do an alias after opening it, or use export private instead

[Matthew Ballard]

Oh, export private is more pleasant

[Matthew Ballard]

The reason this fails is because the metacontext depth (2) exceeds the metavariable depth for
?u from (F : Type _) (0) so it is not assignable.

I am still confused as to why there are metavariables of depth > 0 around here

[Meta.synthInstance] 💥 Mul.{?_uniq.63} _uniq.73 ▼
  [] new goal Mul.{?_uniq.63} _uniq.73 ▼
    [instances] #[Uno.toMul.{?_uniq.105}, Dos.toMul]
  [] 💥 apply Dos.toMul to Mul.{?_uniq.63} _uniq.73 ▼
    [tryResolve] 💥 Mul.{?_uniq.63} _uniq.73 ≟ Mul.{10} ?_uniq.106 ▼
      [isDefEq] 💥 Mul.{?_uniq.63} _uniq.73 =?= Mul.{10} ?_uniq.106 ▼
        [] 💥 _uniq.73 =?= ?_uniq.106 ▼
          [] _uniq.73 [nonassignable] =?= ?_uniq.106 [assignable]
          [] 💥 Type.{10} =?= Type.{?_uniq.63} ▼
            [isLevelDefEq] 💥 10 =?= ?u.63 ▼
              [] ?u.63 is not assignable
              [] 10 is not assignable
              [] At depth 2
              [] [(_uniq.65, 0), (_uniq.66, 0), (_uniq.63, 0), (_uniq.69, 0), (_uniq.88, 0), (_uniq.62, 0), (_uniq.100, 1), (_uniq.68, 0), (_uniq.105, 2)] -- A list of current metavariables in the context and their depths
              [] [Mul.{?_uniq.100} ?_uniq.101, Type.{?_uniq.100}]
              [stuck] Here I am 10 =?= ?u.63

(I added some more verbosity to my toolchain for this output)

[Matthew Ballard]

I changed the example a bit

universe u v w

def TooShort (M : Type w) : Prop := sorry

class Uno (α : Type u) extends Mul α

class Dos (M : Type 10) extends Mul M -- comment out this line...

theorem short_short {M₀ : Type v} [Mul M₀] : TooShort M₀ := sorry

set_option pp.raw true in
set_option trace.Meta.isLevelDefEq true in
set_option trace.Meta.synthInstance true in
set_option trace.Meta.isDefEq true in
set_option trace.Debug.Meta.Tactic.simp true in
example {F : Type _} [Uno F] : TooShort F := by
  simp only [short_short]

[Matthew Ballard]

I am guessing there is +1 from entering the simp and +1 from TC for Mul in short_short

[Matthew Ballard]

_uniq.105 arises from a list of the available instances but doesn't play any role in the unification problem at hand itself. The same is true for _uniq.100

[Matthew Ballard]

If I comment out to remove the depth 2 metavariable,

class Uno (α : Type u) --extends Mul α

then I get something I understand less

[Meta.isDefEq] ✅ TooShort.{?_uniq.85} ?_uniq.86 =?= TooShort.{?_uniq.48} _uniq.58 ▼
  [] ✅ ?_uniq.86 =?= _uniq.58 ▼
    [] ?_uniq.86 [assignable] =?= _uniq.58 [nonassignable]
    [] ✅ Type.{?_uniq.85} =?= Type.{?_uniq.48} ▼
      [isLevelDefEq] ✅ ?u.85 =?= ?u.48
  [isLevelDefEq] ✅ ?u.85 =?= ?u.48 ▼
    [] ✅ ?u.48 =?= ?u.48

[Meta.synthInstance] 💥 Mul.{?_uniq.48} _uniq.58 ▼
  [] new goal Mul.{?_uniq.48} _uniq.58 ▼
    [instances] #[Dos.toMul]
  [] 💥 apply Dos.toMul to Mul.{?_uniq.48} _uniq.58 ▼
    [tryResolve] 💥 Mul.{?_uniq.48} _uniq.58 ≟ Mul.{10} ?_uniq.90 ▼
      [isDefEq] 💥 Mul.{?_uniq.48} _uniq.58 =?= Mul.{10} ?_uniq.90 ▼
        [] 💥 _uniq.58 =?= ?_uniq.90 ▼
          [] _uniq.58 [nonassignable] =?= ?_uniq.90 [assignable]
          [] 💥 Type.{10} =?= Type.{?_uniq.48} ▼
            [isLevelDefEq] 💥 10 =?= ?u.48 ▼
              [] ?u.48 is not assignable
              [] 10 is not assignable
              [] At depth 2
              [] [(_uniq.85, 1), (_uniq.50, 0), (_uniq.73, 0), (_uniq.51, 0), (_uniq.54, 0), (_uniq.48, 0), (_uniq.53, 0), (_uniq.47, 0)]
              [] [Mul.{?_uniq.85} ?_uniq.86, Type.{?_uniq.85}]
              [stuck] Here I am 10 =?= ?u.48

Why I am depth 2 when all my metavariables are at most 1? Why is _uniq.85 appearing when it gets assigned to _uniq.48 when unifying TooShort?