Prime ZMod leads to `decide` complaining of free variables

Stream: mathlib4

[Mauricio Collares]

The following example, adapted from the Exponential Ramsey project, doesn't work in Lean 4:

set_option pp.all true in
example [AAAAAAAAA : Fact (Nat.Prime 5)] : ∀ (a : ZMod 5), a = 2 ∧ a = 3 → False := by
  decide

It fails with

expected type must not contain free or meta variables
  ∀ (a : ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5))),
    And
        (@Eq.{1} (ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5))) a
          (@OfNat.ofNat.{0} (ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5))) 2
            (@instOfNat.{0} (ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5))) 2
              (@Semiring.toNatCast.{0} (ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5)))
                (@DivisionSemiring.toSemiring.{0} (ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5)))
                  (@Semifield.toDivisionSemiring.{0} (ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5)))
                    (@Field.toSemifield.{0} (ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5)))
                      (@ZMod.instFieldZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5)) AAAAAAAAA)))))
              (@instNatAtLeastTwo (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))))))
        (@Eq.{1} (ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5))) a
          (@OfNat.ofNat.{0} (ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5))) 3
            (@instOfNat.{0} (ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5))) 3
              (@Semiring.toNatCast.{0} (ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5)))
                (@DivisionSemiring.toSemiring.{0} (ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5)))
                  (@Semifield.toDivisionSemiring.{0} (ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5)))
                    (@Field.toSemifield.{0} (ZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5)))
                      (@ZMod.instFieldZMod (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5)) AAAAAAAAA)))))
              (@instNatAtLeastTwo (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))))) →
      False

The AAAAAAAAA instance clearly appears in the target, but I think that was also the case in Lean 3 and dec_trivial worked then. Is this expected?

[Alex J. Best]

it would certainly be nice to have decide be a bit more user friendly in such situations, but if you put

  revert AAAAAAAAA

before decide it works fine. The error message is complaining that AA..A is free in the goal, revert fixes that

[Kim Morrison]

Do we have an issue tracking this? In my understanding, we all agree that the user facing decide should determine what needs to be reverted automatically, it's just no one has implemented this.

[Mauricio Collares]

I think @Kyle Miller just fixed this (or rather added an option to do so) in lean4#5999, but I never used decide! or dec_trivial in Lean 3 so I don't know what should be in scope for decide vs decide +revert in Lean 4

[Mauricio Collares]

cc @Bhavik Mehta, who had to work around this in ExponentialRamsey (compare with Lean 3)

[Bhavik Mehta]

Will take a look later, but I don't think the revert was the difference here; note I also had to revert in Lean 3. Instead the regression for the project was that I had to make it a separate lemma, and the decide failed (including with the revert) if I didn't.

[Bhavik Mehta]

Oh oops, the issue was indeed the revert! In the Lean 3 version I didn't need to revert the instance, but I needed to revert something else. Whereas in Lean 4, I need to revert both. So indeed Kim's suggested solution would fix this in my example.

[Bhavik Mehta]

Thinking about this more, another possible diagnosis is that in Lean 3, AAAAAAAAA didn't appear in the goal at all, and so didn't need to be reverted.
For instance,

set_option pp.all true in
example : ∀ (a : ZMod 5), a = 2 ∧ a = 3 → False := by
  decide

succeeds. So instead of this being viewed as a breaking change in decide, it could also be viewed as a breaking change in typeclass synthesis

[Bhavik Mehta]

Huh. In fact the Lean 3 version does have AAAAAAAAA in the goal, and the dec_trivial works fine there.

[Mauricio Collares]

Is this related to https://github.com/leanprover-community/mathlib3/pull/3875 ?

[Bhavik Mehta]

I don't believe so - the change there is to make the tactic dec_trivial! do reverts, but the Lean 3 tactic dec_trivial succeeds already, without doing reverts

[Bhavik Mehta]

My guess as to what's actually causing this is that while the Fact (Nat.Prime 5) instance is present, the goal is definitionally equal to a goal where that instance is missing: it's well-defined without that instance, and even though it's used to show that ZMod 5 is a field, all that's needed here is that it's a semiring. Lean 3's dec_trivial was smart enough to see that the instance wasn't actually used, but Lean 4's decide isn't. And so the revert becomes needed in Lean 4 where it wasn't in Lean 3.

[Mauricio Collares]

By the way: I just tested, and decide +revert works to replace the auxiliary lemma (paley_five_bound_aux) on paley_five_bound but not the one (paley_seventeen_helper') on paley_seventeen_bound. It complains about forall_prop_decidable being classical.

[Bhavik Mehta]

Note that seventeen_helper and five_bound_aux aren't analogous; seventeen_bound uses seventeen_helper and a decide call, and in Lean 4 the decide call needed to be separated out to seventeen_helper'. It's this latter one that's analogous to five_bound_aux. I hope you can excuse my awful naming given that these should all be private anyway ;)

[Mauricio Collares]

No, no, the naming's fine! I just made a typo, I indeed meant paley_seventeen_helper'. Edited.

[Mauricio Collares]

In the latter case, it reverted too many things and I think it is trying to use choice for the two Exists propositions:

tactic 'decide' failed for proposition
  ∀ (this : Fact (Nat.Prime 17)),
    (∃ m c, (paleyLabelling (ZMod 17)).MonochromaticOf (↑m) c ∧ ![4, 4] c = #m) →
      (∃ m c, (paleyLabelling (ZMod 17)).MonochromaticOf (↑m) c ∧ 4 = #m) →
        ∀ (a b : ZMod 17), a = 2 ∨ a = 9 ∨ a = 16 → b = 2 ∨ b = 9 ∨ b = 16 → ¬a = b → IsSquare (b - a) → False

[Mauricio Collares]

Ah, that's not the case. Even clearing the corresponding variables, I get

tactic 'decide' failed for proposition
  ∀ (this : Fact (Nat.Prime 17)) (a b : ZMod 17),
    a = 2 ∨ a = 9 ∨ a = 16 → b = 2 ∨ b = 9 ∨ b = 16 → ¬a = b → IsSquare (b - a) → False
since its 'Decidable' instance
  forall_prop_decidable fun this =>
    ∀ (a b : ZMod 17), a = 2 ∨ a = 9 ∨ a = 16 → b = 2 ∨ b = 9 ∨ b = 16 → ¬a = b → IsSquare (b - a) → False
did not reduce to 'isTrue' or 'isFalse'.

[Bhavik Mehta]

Huh, this is a really interesting observation. So what's going on here is that reverting the instance is requiring it to revert the other two hypotheses that are still around (these ones do actually need that instance), and those ones use choice in their definitions (see classical on the second line of the proof). But since Lean 3 never needed to revert the instance, these hypotheses don't even get seen by dec_trivial, and so the proof goes through

[Bhavik Mehta]

Curiously on 4.13.0 (I haven't bumped ExponentialRamsey to 4.14.0-rc locally yet), clearing the variables gives me a recursion depth error instead!

[Bhavik Mehta]

(For some broader context for those following along at home, this one is part of the proof that R(4) = 18, which is the highest known diagonal Ramsey number, and up until ITP this year was the joint largest formally verified Ramsey number.)

[Mauricio Collares]

Ah, the constructive decidability instance in the second case is too big (whatever that means), and then the classical instance kicks in. So clearing h and this and doing set_option synthInstance.maxSize 1024 makes decide +revert work for paley_seventeen_bound as well.