Keeping a def computable with inversion

Stream: mathlib4

[Willem vanhulle]

I have defined a probability mass function and want to normalise it. Normalisation is possible but it forces me to mark the result as “non computable”.

I have a suspicion that this makes theorems about the normalised measure harder or impossible to check.

The reason that it is like that is probably that I cannot invert a natural number safely because it can be zero. How do invert a nonzero natural number without introducing the “noncomputable” keyword?

[Edward van de Meent]

could you give a #mwe ? if you're talking about docs#PMF, i don't think your function is returning natural numbers...

[Kevin Buzzard]

No, noncomputable has nothing to do with making theorems harder or impossible. The vast majority of the definitions in the parts of mathlib I work in are noncomputable, this is a computer science thing to do with use of #eval and #reduce, not theorem proving.

[Edward van de Meent]

fwiw, division by zero is computable on the natural numbers:

-- no `noncomputable` needed
def foo : Nat -> Nat := fun x => 1 / x

[Willem vanhulle]

Ah yes, I was probably having reals but they were integers by coincidence. @Edward van de Meent. Okay so I should not worry about the nomcomputable. I was wondering if this problem was related to my inability to proof switching is the most optimal strategy in the Monty Hall brain teaser. I tried to use Bayes theorem from Mathlib. I can send a MWE example with sorries.

[Willem vanhulle]

Kevin Buzzard said:

No, noncomputable has nothing to do with making theorems harder or impossible. The vast majority of the definitions in the parts of mathlib I work in are noncomputable, this is a computer science thing to do with use of #eval and #reduce, not theorem proving.

So the noncomputable keyword is unrelated to usage of the “decide” macro?

[Edward van de Meent]

sort of

[Edward van de Meent]

if the Decidable instance reduces to .ofTrue or .ofFalse, you're fine. this is more likely when all your functions are computable, but it can happen that that it isn't the case but still reduces

[Kevin Buzzard]

You won't be able to use the decide tactic for noncomputable things, but if you're working with the real numbers (for which equality is undecidable) you'll almost certainly not be using this tactic at all.

[Edward van de Meent]

Kevin Buzzard said:

You won't be able to use the decide tactic for noncomputable things

it's subtle though:

import Mathlib

-- this is noncomputable
noncomputable example : Decidable ((.none : Option ℝ) ≠ (1 : ℝ)) := inferInstance

example : (.none : Option ℝ) ≠ (1 : ℝ) := by
  decide -- succeeds

here noncomputableInst is noncomputable, but the decide tactic is able to use it anyway.

[Edward van de Meent]

otoh, free variables can stop something which is decidable (and computable) from reducing:

-- this is computable
example : ∀ (n m : ℕ), Decidable (n = m) := inferInstance

example (n : ℕ) : n = n := by
  -- decide -- has a hard-coded error for free variables
  apply of_decide_eq_true
  rfl -- fails too

[Kevin Buzzard]

The details are indeed subtle but I maintain that "if you're doing probability theory then you don't need to worry at all about noncomputability" is an accurate overview.

[Kyle Miller]

Willem vanhulle said:

Ah yes, I was probably having reals but they were integers by coincidence.

There are other tactics better suited for doing arithmetic (e.g. norm_num and linarith). The decide tactic can be useful, but to me it often feels like the wrong tool unless there really is a general algorithm.

Real numbers are sort of computable in some senses, but also not really (there's no algorithm to decide whether or not two general real numbers are equal).

Side question: what in the world is docs#Real.decidableEq doing as a global instance? That's just docs#Classical.decEq, so not an algorithm in any sense. This is the reason @Edward van de Meent's example seems to work, along with the fact that the Option decidable equality instance won't ask Real.decidableEq to do anything in the none/some case.

[Kyle Miller]

Willem vanhulle said:

I can send a MWE example with sorries.

Is this the MWE? #mathlib4 > Bayes theorem in Monty Hall problem @ 💬

[Willem vanhulle]

Yes, I started on proving that the H and E are measurable sets. But no progress so far.

Kyle Miller zei:

Willem vanhulle said:

I can send a MWE example with sorries.

Is this the MWE? #mathlib4 > Bayes theorem in Monty Hall problem @ 💬

[Sébastien Gouëzel]

Kyle Miller said:

Side question: what in the world is docs#Real.decidableEq doing as a global instance?

We know that there won't ever be a true computing DecidableEq instance on the reals. So there is no cost in having the classical one around, and there is the benefit that you can apply all the lemmas needing DecidableEq without any more fuss.

[Kyle Miller]

One cost is that tactics that use decide (like simp +decide) might think it can apply, then fruitlessly reduce the synthesized instance.

[Edward van de Meent]

actually, if you try that, you'll see that the error message is suitably helpful to not be too much of a headache

[Kyle Miller]

simp +decide doesn't show error message. I'm talking about automation that repeatedly tries reducing something that's not going to reduce. I think all Decidable instances should be able to reduce.

[Kyle Miller]

I suspect Real having these "bad" global Decidable instances isn't a big deal, but poisoning the reducibility of the global instances isn't something that should be done lightly.

[Kyle Miller]

Conceivably there's some proposition p and a diamond of instances where when the Real ones are present the resulting Decidable p instance is not reducible, but when they are removed it becomes reducible. That's the sort of risk here (independent of the small performance issue I just mentioned). It's a small risk, but the risk is there.

Maybe they should at least be marked as having low priority...

[Sébastien Gouëzel]

Any LinearOrder in Mathlib has DecidableEq. I remember the old Lean 3 times when we had LinearOrder and DecidableLinearOrder (maybe called DiscreteLinearOrder just to add to the confusion). It was causing a lot of pain for essentially no gain, so we decided to merge them. I don't remember any issue it would have created since then (but I'm not saying it won't ever create one!)

[Eric Wieser]

Kyle Miller said:

Conceivably there's some proposition p and a diamond of instances where when the Real ones are present the resulting Decidable p instance is not reducible, but when they are removed it becomes reducible.

I guess this can happen for something like Decidable ((1 : Real) = 1)

[Eric Wieser]

But I think in general we try to avoid Decidable (x = y) instances, and only have the fully quantified DecidableEq Real ones

[Aaron Liu]

Kyle Miller said:

Conceivably there's some proposition p and a diamond of instances where when the Real ones are present the resulting Decidable p instance is not reducible, but when they are removed it becomes reducible. That's the sort of risk here (independent of the small performance issue I just mentioned). It's a small risk, but the risk is there.

Then that's just a bad instance, since it would lead to diamonds.

[Kyle Miller]

@Sébastien Gouëzel I don't see any problem with having them be merged — it's fine having a classical DecidableEq instances safely inside the LinearOrder instance. It's the global instances that are suspect.

Sébastien Gouëzel said:

there is the benefit that you can apply all the lemmas needing DecidableEq without any more fuss.

This makes me wonder why we have definitions needing DecidableEq in the first place, if in practice we're going to thwart the decidability system?

Over in the Fintype world, we added Finite, which let us remove global noncomputable instances that were poisoning computability.

[Sébastien Gouëzel]

There is a global instance from LinearOrder to DecidableEq (I mean, registered as an instance, not just a field in the definition). So if we want the reals to be a linear order, they have to have a DecidableEq instance also.

[Kyle Miller]

(I've said this before, but I think that having mathematical definitions use Decidable is a compromise, one that (1) increases the awkwardness of doing mathematical reasoning and (2) is lowest common denominator for computation, so it's in practice not living up to being a practical way to have mathematical definitions that are also executable. I know Eric says that at least for small examples it's useful being able to compute, and also sometimes it's nice when defeqs work out and make things more convenient (at the cost of heavy rfls!), but long term I don't see how we can keep this up. It seems much less costly for learning and for development to have a decidability-free theory and good automation to do computations. That includes synthesizing efficient programs to run to do the computation (reflection).)

[Kyle Miller]

Ah, I missed that, thanks @Sébastien Gouëzel. That's a strong constraint.

[Sébastien Gouëzel]

Some people (inclusing I think @Kim Morrison, or myself) would definitely prefer a completely classical mathlib, without any decidability in it, but I don't think we'll get there, unfortunately.

[Kevin Buzzard]

I would also prefer this (I say this after having to add random DecidableEq stuff recently to a bunch of declarations for no obvious reason other than "it's how we do this in mathlib"); I wonder whether we could make classicality happen with carefully-chosen csimp? I know that Bhavik will have a very different opinion because they actually use decide to prove things, whereas I don't think I have ever done this.

[Kyle Miller]

One step would be a FiniteSet type (a Set bundled with a Set.Finite proof). Finset is a large source of unnecessary decidability. This wouldn't be to replace Finset, but it would be parallel to it, like Finite and Fintype. (Theory about Finset might drift to FiniteSet, especially if we have some good simp sets that can turn expressions about Finsets into FiniteSets.) We'd also want to be able to evaluate FiniteSets, but I don't think the story is really that different from Finset in the end, as far as tactics go.

Another would be a noncomputable version of if that's purely classical (maybe if!?), just to save needing to write open Classical in, which makes it feel like you're doing something wrong.

[Kyle Miller]

I'm basically just reiterating myself though.

#mathlib4 > Why is `Polynomial` noncomputable? @ 💬 @Kevin Buzzard: Rather than csimp per se, I think there's a future where a tactic like decide could synthesize an algorithm based on the specifics of what needs to be decided. (The grind tactic does a lot of this sort of thing as well — it's great at deciding things about polynomials, even if the underlying ring isn't "computable"!)

[Kyle Miller]

More about grind: when it sees some arithmetic it needs to prove, it can use a custom polynomial type that has been design for very fast kernel computations. It "reflects" the goal into this custom type, does the computation there, and uses it to justify a calculation about the goal — meanwhile it avoids actually computing anything using the goal's types (e.g. it might be a polynomial with Real coefficients).

[Eric Wieser]

Kyle Miller said:

Another would be a noncomputable version of if that's purely classical (maybe if!?), just to save needing to write open Classical in, which makes it feel like you're doing something wrong.

Or maybe just classical% if, since often there is something else in the if that also also needs classical logic anyway

[Eric Wieser]

Certainly open scoped Classical in is non-ideal, as its long, and it also encourages doing things at the command-level when actually we usually want it at the term-level

[Kevin Buzzard]

Kevin Buzzard said:

I would also prefer this (I say this after having to add random DecidableEq stuff recently to a bunch of declarations for no obvious reason other than "it's how we do this in mathlib"); I wonder whether we could make classicality happen with carefully-chosen csimp? I know that Bhavik will have a very different opinion because they actually use decide to prove things, whereas I don't think I have ever done this.

Oh this is happening to me again so I may as well make my comment more precise: group homology and cohomology seems to be demanding [DecidableEq G] everywhere and it's making my files look uglier and weirder-looking to mathematicians. Why has this happened I wonder?

groupCohomology.{u} {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) (n : ℕ) : ModuleCat k

[Eric Wieser]

Ultimately it comes from here, which looks ok

[Eric Wieser]

Actually, I think it's just unused

[Eric Wieser]

I have no idea why it's there

[Eric Wieser]

I guess we never got the DecidableEq linter from lean 3 that complained if decidability was only used in the proof?

[Kevin Buzzard]

That if is all about decidable equality on the index set (which is the naturals or integers), not on G, so I am skeptical about this claim (but I'm in a group cohomology meeting so can't think about this right now, sorry)

[Eric Wieser]

PR incoming

[Eric Wieser]

#26352

[Eric Wieser]

I prefer to think of this kind of noise in the same vein as "Why did you use Ring when Semiring would suffice", rather than that Decidable is somehow evil; while there are plenty of mathematicians who don't care about Decidable at all, the same is surely also true of semirings, or of free modules vs vector spaces, or char zero vs char-not-two, ....

[Kevin Buzzard]

Hmm, this did not completely solve the problem, to my surprise. docs#groupHomology is still demanding [DecidableEq G] (which sounds like nonsense to me). One can chase this back in RepresentationTheory/Homological/GroupHomology/Basic.lean to groupHomology.inhomogeneousChains.d_eq which needs Rep.coinvariantsTensorFreeLEquiv which involves Finsupp which it seems pollutes everything.

[Eric Wieser]

Right, I think that ultimately falls back on docs#Finsupp.curry

[Eric Wieser]

This is probably a case where it's reasonable to add an ooen scoped Classical inside groupHomology

[Eric Wieser]

I deliberately skipped it in that PR because it would be a bigger change, so made sense to do separately

[Eric Wieser]

Somewhat interestingly, it would be possible to implemented a potential DFinsupp.curry computably without decidable equality, but it is not possible to implement docs#DFinsupp.sigmaCurry without it

[Aaron Liu]

Since finsupps aren't really being used for computation, could we maybe make Finsupp.curry noncomputable using the classical instance and just put [DecidableEq α] in all the API lemmas that need it?

[Eric Wieser]

I don't think that's worth it; anything mathematical using finsupp dowstream should be using it as an implementation detail, and is free to supply a classical instance as part of that implementation.

[Aaron Liu]

what about polynomials

[Eric Wieser]

Yes, the implementation of polynomials is free to provide a classical instance of DecidableEq Nat to the underlying finsupp if it so chooses (which is essentially what currently happens).

[Aaron Liu]

Eric Wieser said:

Yes, the implementation of polynomials is free to provide a classical instance of DecidableEq Nat to the underlying finsupp if it so chooses (which is essentially what currently happens).

No but the classical instance isn't the fault of polynomials, it comes from docs#Finsupp.zipWith which is part of the finsupp api and so should remain computable I think?

[Eric Wieser]

My "essentially" was doing some heavy lifting I'm afraid