DecidableEq diamond

Stream: mathlib4

[Joël Riou]

The following should work

import Mathlib.Data.MvPolynomial.CommRing
import Mathlib.Data.Finset.Basic

open MvPolynomial Finset

lemma test (n : ℕ) (P : MvPolynomial ℕ ℚ)
    (h : Disjoint (vars (X n : MvPolynomial ℕ ℚ)) (vars P)) : n ∈ (X n - P).vars := by
  rw [vars_sub_of_disjoint _ h, vars_X, mem_union, Finset.mem_singleton]
  exact Or.inl rfl

but rw [mem_union] fails as

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  fun a b => instDecidableEqNat a b
inferred
  fun a b => Classical.propDecidable (a = b)

(This appeared in !4#3355 at https://github.com/leanprover-community/mathlib4/pull/3355/files#diff-f33593ea969bf958e5cb05e696cc502c949d9abfd4241a1f4be934e01466c818R259-R271 )

[Eric Wieser]

I would guess docs4#MvPolynomial.vars_sub_of_disjoint is to blame

[Eric Wieser]

It is missing a DecideableEq argument

[Eric Wieser]

Removing open Classical from that file should make the problem obvious

[Joël Riou]

Thanks, but then there is another DecidableEq diamond on the set σ →₀ ℕ of functions which are zero almost everywhere...

[Joël Riou]

(I will try to investigate this another day.)

[Kevin Buzzard]

Is open Classical ever correct? Since I learnt the basic rule of thumb ("if the statement doesn't compile, add decidable instances; if the proof doesn't compile, use the classical tactic in the proof) I've never had this particular diamond issue (which used to plague my code before I understood the rule of thumb and was in fact the reason Jason KY and I wrote the basic finsum API)

[Eric Wieser]

In lean 4 there's no reason to use it now the classical tactic works properly and the variable inclusion rules have changed

[Eric Wieser]

(except obviously when porting)

[Eric Wieser]

That is to say, def foo := by classical; exact if p then x else y didn't work well in Lean 3, and was the main reason that the locale was still useful

[Joël Riou]

After getting rid of open Classical in 6 extra files, I could get RingTheory.WittVector.WittPolynomial to compile, but it seems I have broken everything else :innocent:

[Kyle Miller]

There's also a difference between how instance arguments are handled between Lean 3 and Lean 4. Now there's a check that the instance argument is the "right" one, but in Lean 3 a theorem like docs4#Finset.mem_union would be happy to just use the instance argument that was already there in the expression.

@Joël Riou If you made a variant of Finset.mem_union that takes the decidable instance as an implicit argument rather than an instance argument, I'd expect your original example to work.

[Kyle Miller]

Yeah, this works:

import Mathlib.Data.MvPolynomial.CommRing
import Mathlib.Data.Finset.Basic

open MvPolynomial Finset

theorem Finset.mem_union' {_ : DecidableEq α} {s t : Finset α} {a : α} :
    a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t := Finset.mem_union

lemma test (n : ℕ) (P : MvPolynomial ℕ ℚ)
    (h : Disjoint (vars (X n : MvPolynomial ℕ ℚ)) (vars P)) : n ∈ (X n - P).vars := by
  rw [vars_sub_of_disjoint _ h, vars_X, mem_union', Finset.mem_singleton]
  exact Or.inl rfl

[Kyle Miller]

I think we're going to have to figure out the new right way to handle instance arguments in rewrite theorems, since the rules of thumb that worked for Lean 3 don't apply perfectly to Lean 4.

I believe @Matthew Ballard had an example of Lean 3 style (where you have instance arguments rather than implicit arguments for everything that can be picked up from the LHS) causing timeouts for some algebraic structures in Lean 4, though I can't find the thread right now.

[Matthew Ballard]

There have been a few. One example RingTheory.Polynomial.Basic

• https://github.com/leanprover-community/mathlib4/blob/05186d6b6b04357326f679db65b90e45c6c8f8ed/Mathlib/RingTheory/Polynomial/Basic.lean#L864
• https://github.com/leanprover-community/mathlib4/blob/05186d6b6b04357326f679db65b90e45c6c8f8ed/Mathlib/RingTheory/Polynomial/Basic.lean#L1285 and below

[Matthew Ballard]

I think @Eric Wieser had some also. If you grep for (_) you will find a good chunk of them (I would guess)

[Kyle Miller]

Oh right, I forgot about the (_) solution to switch the argument from being elaborated as an instance argument. Here's how that looks here:

lemma test (n : ℕ) (P : MvPolynomial ℕ ℚ)
    (h : Disjoint (vars (X n : MvPolynomial ℕ ℚ)) (vars P)) : n ∈ (X n - P).vars := by
  rw [vars_sub_of_disjoint _ h, vars_X, @mem_union _ (_), Finset.mem_singleton]
  exact Or.inl rfl

[Matthew Ballard]

You can force Lean to use unification in place of typeclass synthesis if you use (_) in place of _ when filling in all parameters (or what Kyle said :)

[Eric Wieser]

In the long run it would be better to fix the classical issues, but I guess the above is a faithful port

[Eric Wieser]

It's a shame the instance arguments are all un-named so we can't use (inst12 := _) instead

[Eric Wieser]

(Sure, it's unhygienic; but I'd rather see inst12 than count 12 underscores)

[Matthew Ballard]

I agree. Is there metaprogramming solution (or approximation)?

[Kyle Miller]

@Matthew Ballard I was just experimenting with something like that in the form of a no_inst% term elaborator that turns every instance implicit into an implicit argument:

import Mathlib.Data.MvPolynomial.CommRing
import Mathlib.Data.Finset.Basic
import Lean

namespace NoInst
open Lean Elab Lean.Parser.Term
open Meta Command

syntax (name := no_inst) "no_inst% " ident : term

@[term_elab no_inst]
def no_inst_elab : Elab.Term.TermElab := fun stx _ =>
  match stx with
  | `(no_inst% $name) => do
    if let some e ← Term.resolveId? name (withInfo := true) then
      logInfo m!"no_inst% for type {← inferType e}"
      let e' ← forallTelescope (← inferType e) fun args _ => do
        let mut lctx ← getLCtx
        for arg in args do
          let decl := lctx.getFVar! arg
          if decl.binderInfo.isInstImplicit then
            lctx := lctx.setBinderInfo decl.fvarId .implicit
        withLCtx lctx (← getLocalInstances) do
          mkLambdaFVars args (mkAppN e args)
      logInfo m!"no_inst% created type {← inferType e'}"
      return e'
    else
      -- Generate error:
      Term.elabTerm name none
  | _ => throwUnsupportedSyntax

end NoInst


open MvPolynomial Finset

lemma test (n : ℕ) (P : MvPolynomial ℕ ℚ)
    (h : Disjoint (vars (X n : MvPolynomial ℕ ℚ)) (vars P)) : n ∈ (X n - P).vars := by
  rw [vars_sub_of_disjoint _ h, vars_X, no_inst% mem_union, Finset.mem_singleton]
  exact Or.inl rfl

[Matthew Ballard]

Nice! I think turning all [] into {} might not work so well in practice though. In my experience, I've had to mix and match.

[Kyle Miller]

For rewriting, it'd be better to keep track whether the instance argument is only for the RHS and leave those alone. Do you know if there are other heuristics?

[Matthew Ballard]

Would it make sense to try unification and fall back to synthesis if that fails?

[Kyle Miller]

I think you're getting into "changes to Lean 4 core" territory here. Anne Baanen I believe was the one who made that change to Lean 3, and it's been a nice feature.

[Matthew Ballard]

Yeah, it seems complicated to implement well

[Matthew Ballard]

Unfortunately, I don't have good rules for when to do which except if it times out, then switch to {}

[Matthew Ballard]

Is there any way to manually pick the instance argument(s) as Eric suggested?

[Matthew Ballard]

I guess: "earlier instance parameters in the signature tend to be less problematic than later ones" has been fairly true

[Kyle Miller]

@Matthew Ballard Here's another term elaborator. This time de_inst% mem_union 2 takes argument index 2, checks that it's an instance implicit, and then turns it into an implicit. You can give it as many argument indices as you want, like de_inst% f 3 5 7.

import Mathlib.Data.MvPolynomial.CommRing
import Mathlib.Data.Finset.Basic
import Lean

namespace NoInst
open Lean Elab Lean.Parser.Term
open Meta Command

syntax (name := de_inst) "de_inst% " ident num* : term

@[term_elab de_inst]
def no_inst_elab : Elab.Term.TermElab := fun stx _ =>
  match stx with
  | `(de_inst% $name $nums*) => do
    let nums := nums.map (·.getNat)
    if let some e ← Term.resolveId? name (withInfo := true) then
      let e' ← forallTelescope (← inferType e) fun args _ => do
        let mut lctx ← getLCtx
        for i in nums do
          if i == 0 || i > args.size then
            throwError "${name} does not have argument index {i}"
          let arg := args[i - 1]!
          let decl := lctx.getFVar! arg
          if not decl.binderInfo.isInstImplicit then
            throwError "argument index {i} (of type {← inferType arg}) is not an instance implicit"
          lctx := lctx.setBinderInfo decl.fvarId .implicit
        withLCtx lctx (← getLocalInstances) do
          mkLambdaFVars args (mkAppN e args)
      return e'
    else
      -- Generate error:
      Term.elabTerm name none
  | _ => throwUnsupportedSyntax

end NoInst

open MvPolynomial Finset

lemma test (n : ℕ) (P : MvPolynomial ℕ ℚ)
    (h : Disjoint (vars (X n : MvPolynomial ℕ ℚ)) (vars P)) : n ∈ (X n - P).vars := by
  rw [vars_sub_of_disjoint _ h, vars_X, de_inst% mem_union 2, Finset.mem_singleton]
  exact Or.inl rfl

[Kyle Miller]

The indexing could also be with respect to the instance implicit arguments themselves, but this a little easier.

[Matthew Ballard]

Great! Yeah, I think either specifying the index or type manually probably has the widest use without getting seriously into the guts of the synthesis algorithm

[Eric Wieser]

I think the big win here would be specifying the type of the target argument

[Eric Wieser]

Perhaps foo (_ : Bar := val) would be a reasonable syntax request for core?

[Kyle Miller]

That syntax at least seems unambiguous, and it might not be that crazy of a feature since something like foo (x : Bar := val) could still be valid and be helpful for elaboration of both val and foo. I guess you still have to decide how this works when there are multiple matches, either if there are two Bars or if you allow Bar to have placeholders.

[Kyle Miller]

In the meantime, it's not so hard to implement this as a term elaborator, with syntax like with_args% foo (_ : Bar := val).

[Joël Riou]

Now !4#3355 changes 29 files, but it compiles!

[Eric Wieser]

It sounds to me like it would be worth backporting some of these changes just to check they don't cause trouble elsewhere

[Scott Morrison]

Gah, what's going on here? I thought we decided long ago not to have any decidability instances in the polynomial library?

[Eric Wieser]

I think we decided to not have them in definitions

[Eric Wieser]

Lemmas without them are harder to use than lemmas with them

[Eric Wieser]

Because they introduce non-canonical decidability instances into the goal

[Joël Riou]

The problem arose while porting WittVector.WittPolynomial. In the proof of xInTermsOfW_vars_aux, there are some manipulations on Finset ℕ. Some lemmas used in the proof involve the DecidableEq instance coming from the integers and some involve the one obtained by classical. Lean3 rw was able to deal with that; but it is not so in Lean4. By adding DecidableEq in many places as I eventually did in !4#3355 I could have this PR compile. However, I think that either we can make rw work following Kyle suggestion or we should just completely get rid of any global DecidableEq instance that is not classical.decEq...

[Eric Wieser]

!4#3355 changes a lot more than it needs to, as discussed in the backport

[Joël Riou]

I have made other attempts, and it eventually reduces to the problem I have mentionned just above.

[Eric Wieser]

@Joël Riou, my point is that #18791 (+621 −426, the backport) adds decidable_eq arguments to both defs (which Scott is rightly opposed to) and lemmas (which I think we recently agreed was a good thing)

[Eric Wieser]

I have created a smaller PR at #18848 (+154 −90) which should hopefully be less controversial. Getting mv_polynomial.vars right will need more care so as to not break everything downstream like it seem to in #18791 I've added the changes to this file too.

[Eric Wieser]

@Scott Morrison, are you happy with #18848? (other than the 10 files of forward-porting burden it creates)

[Scott Morrison]

I better sleep before attempting to read the changes, but at least the PR description I'm happy with. :-)

[Eric Wieser]

:ping_pong: on the above. I probably won't have time to respond to any review feedback this week, but it would be good not to forget about it

[Anne Baanen]

:ping_pong: answered!

[Eric Wieser]

The forward-port, !4#4007, is ready for (careful) review. This uses up 10 spots on #out-of-sync.

[Eric Wieser]

The DecidableEq problems in this PR are all gone

[Eric Wieser]

I got the whole thing building, but some of the porting had introduced some mistakes, so after fixing them there are some things to cleanup

[Eric Wieser]

Annoyingly rw [Finset.sum_congr rfl] no longer seems to work

[Mauricio Collares]

!4#3355 for reference

[Joël Riou]

!4#3355 compiles now. Thanks very much @Eric Wieser for your efforts!

[Eric Wieser]

Looking over the diff against the mathport output, it looks like there are a few places that are missing porting note (at least one of them is one I introduced!)

[Eric Wieser]

The sum_eq_zero thing you mention is particularly strange; is it still a problem with all the other fixes?