rfl_without_eta

Stream: mathlib4

[Sebastien Gouezel]

Is there a command to check if two structures are defeq without eta (emulating what instance search does when eta experiment is off)?

[Scott Morrison]

This isn't quite it, but there is Lean.Meta.isDefEqEtaStruct (private, unfortunately), which says:

Return true if b is of the form mk a.1 ... a.n, and a is not a constructor application.
If a and b are constructor applications, the method returns false to force isDefEq to use isDefEqArgs.

[Sebastien Gouezel]

This could definitely be helpful, but I don't know how to access a private function like that. Is there some trick here?

[Patrick Massot]

In the worst case scenario you can copy-paste the code somewhere.

[Matthew Ballard]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20addProjections/near/342713844 Seems so

[Sebastien Gouezel]

I am trying to make things a little bit more coherent, which should give a lot more straight defeqs, but I have problems above my paygrade, in tactic files. For instance, in

def evalSub (rα : Q(Ring $α)) (va : ExSum sα a) (vb : ExSum sα b) : Result (ExSum sα) q($a - $b) :=
  let ⟨_c, vc, pc⟩ := evalNeg sα rα vb
  let ⟨d, vd, (pd : Q($a + $_c = $d))⟩ := evalAdd sα va vc
  ⟨d, vd, (q(sub_pf $pc $pd) : Expr)⟩

I get an error on the last $pd, of the form

application type mismatch
  sub_pf «$pc» «$pd»
argument
  «$pd»
has type
  @HAdd.hAdd «$α» «$α» «$α»
      (@instHAdd «$α»
        (@Distrib.toAdd «$α»
          (@NonUnitalNonAssocSemiring.toDistrib «$α»
            (@NonAssocSemiring.toNonUnitalNonAssocSemiring «$α»
              (@Semiring.toNonAssocSemiring «$α» CommSemiring.toSemiring)))))
      «$a» «$_c» =
    «$d» : Prop
but is expected to have type
  @HAdd.hAdd «$α» «$α» «$α»
      (@instHAdd «$α»
        (@Distrib.toAdd «$α»
          (@NonUnitalNonAssocSemiring.toDistrib «$α»
            (@NonAssocSemiring.toNonUnitalNonAssocSemiring «$α» (@Semiring.toNonAssocSemiring «$α» Ring.toSemiring)))))
      «$a» «$_c» =
    ?m.216710 : Prop

This is on !4#3809. Any idea?

[Scott Morrison]

@Sebastien Gouezel, grep for open private in mathlib4.

[Scott Morrison]

Regarding @Sebastien Gouezel's !4#3840 (for those following along at home, this is the new replacement for !4#3809), I've opened #18967, which backports the change in declaration order. It is not entirely trouble free, but given how much of an improvement this makes in mathlib4, mathlib3 is going to have to cope, I think. :-)

I'm going to consider that PR as sufficient evidence that Sebastien's change is backportable, so I'd propose we move on with merging this PR!

[Sebastien Gouezel]

I'd like first to check that this also gives an improvement in the reenable_eta branch: Since in the long run we will hopefully merge this branch, it would be silly to merge something that would make it worse. I've opened !4#3847 to check this (although I'm not sure of the incantations I will need to use to benchmark this branch against the reenable_eta one).

[Sebastien Gouezel]

I got the benchmarks, but they are useless as they are against the branch without eta. Does anyone know how to get a comparison with respect to the branch reenable_eta?

[Scott Morrison]

I think I see how to do the comparison. We need to separately run !bench on !4#3414, which I've just initiated.

[Scott Morrison]

To do the comparison, click the "Here are the benchmark results for commit 0193bab." link on !4#3847. Then there is a "scale" icon in the top right, with hover text "Compare this run with another". Clicking that, you can search for a commit sha, or branch name. But the relevant commit, 3fc0de82218c8e1285e478f8904a9144b3a5eccd, doesn't have benchmarking data yet. Hopefully it will soon.

[Sebastien Gouezel]

Thanks!

[Mauricio Collares]

The less smart approach is just to change the base branch to reenableeta. I ended up doing that before noticing Scott had a better solution.

[Eric Wieser]

IMO we should merge the backport pr (assuming we decide to merge the mathlib4 PR) rather than just using it as an experiment; it's possible that mathlib 4 will need the same workarounds in unported downstream files, and it seems silly to ask the porters to rediscover them.

[Sebastien Gouezel]

This looks pretty good, according to http://speedcenter.informatik.kit.edu/mathlib4/compare/e7b27246-a3e6-496a-b552-ff4b45c7236e/to/a05abf06-1496-460c-9b45-a8c679bd5221?hash1=6cd73ad26c168dcbe403eccc12cae09c63ef6488 (which compares the previous run of reenableeta with reenableeta + !4#3840)

[Sebastien Gouezel]

(good except for MvPolynomials, which is doubled :-(

[Sebastien Gouezel]

(and the global time has even a small increase -- so maybe it's not a good idea to merge it after all, or as a temporary workaround to help for the current port of linear algebra)

[Sebastien Gouezel]

Results are here (thanks @Mauricio Collares !): https://github.com/leanprover-community/mathlib4/pull/3847#issuecomment-1537966700

Overall green, except for a very bad outcome in MvPolynomial. Not sure if it means we should just drop this, or try to understand what is going on with MvPolynomial.

[Mauricio Collares]

MvPolynomial is a very small file, relative numbers are perhaps misleading

[Sebastien Gouezel]

Yes, it's true, it just has two declarations and it feels pretty quick in both branches. So I would just discard this as irrelevant.

[Eric Rodriguez]

I wonder if that mvpolynomial file uses a different path than most cos it has field stuff. Do we have much field theory ported?

[Matthew Ballard]

The current files also have workarounds which to a part are geared toward the previous set of instance priorities and/or lack of eta. Ripping those out will probably improve performance additionally.

[Scott Morrison]

Merge?

[Johan Commelin]

If there's an increased performance almost everywhere, and the mvpolynomial stuff is so small, why is there still an overall increase in time? That seems quite weird.

[Mauricio Collares]

It's wall clock time, so there's some randomness involved. The benchmark tool didn't flag it as statistically significant.

[Johan Commelin]

otoh, it also didn't flag statistically significant overall improvement...

[Eric Wieser]

Speculatively, we have two problems in linear algebra; ring -> semiring, and comm_semiring -> semiring. We can make both of these behave well separately, but we're still in trouble when we get to comm_ring