integral_undef

Stream: general

[Yaël Dillies]

Do we agree that docs#integral_undef is a terrible name? I've been looking several times in the past for the lemma that says that a non-integrable function has integral zero, and I'm only finding it now. I was looking for not_integrable.

[Ruben Van de Velde]

integral_eq_zero_of_not_integrable? Maybe a little long

[Sebastien Gouezel]

Yes, that's a terrible name. You get used to it, but it's pretty much impossible to discover unless you browse the file. integral_of_not_integrable would be better.

[Yaël Dillies]

integral_of_not_integrable is the name I guessed, yes. I will add an alias for discoverability, unless you hate the current name so much that you want a rename.

[Anatole Dedecker]

Actually I would say that we could make it a naming pattern for all the default values like that, I would be happy with integral_of_undef, deriv_of_under, csSup_of_undef and so on

[Yaël Dillies]

Okay but now you must know whether something holds by definition or because it's a consequence of something earlier.

[Yaël Dillies]

That sounds implementation-detaily.

[Anatole Dedecker]

Well I only have examples in mind where it is clear what is needed for a definition to make sense, but I get your point. I don’t have strong feelings about this anyway, just felt like the name is not that bad

[Yury G. Kudryashov]

In each case listed by @Anatole Dedecker, "of undef" means "in a situation when the textbooks say that the value is undefined".

[Yaël Dillies]

Then let's at least have a discoverable alias. I don't mind too much about removing the undef name.

[Eric Rodriguez]

I wonder if we could have a tactic that does this sort of stuff, much like nontriviality (that is, gives you that wlog it's integrable by discharging the other case with simp)

[Yaël Dillies]

That would be great, but we would need it to handle not just integrability, but also measurability, nonemptiness, nonzeroness...

[Damiano Testa]

I can try to give it a go, beginning with a simple case-split: is this non-integrable/integrable, trying to discharge the main goal replacing the integral with zero in one branch, and adding the hypothesis integrable ... in the other.

[Damiano Testa]

Here is a very quick implementation:

import Mathlib.MeasureTheory.Integral.Bochner

open Lean Elab Tactic Meta

macro "unint " f:ident : tactic => do
  (`(tactic| (
      (by_cases h_int : MeasureTheory.Integrable $f)
      (pick_goal 2)
      (simp [h_int, MeasureTheory.integral_undef] <;> done )
    )
  ))

open MeasureTheory

universe u v

variable {α : Type u} {E : Type v}

variable [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasureSpace α]

example (f : α → E) : (∫ (a : α), f a) = 0 := by
  unint f
  sorry
  /- state:
  α: Type u
  E: Type v
  inst✝³: NormedAddCommGroup E
  inst✝²: NormedSpace ℝ E
  inst✝¹: CompleteSpace E
  inst✝: MeasureSpace α
  f: α → E
  h_int✝: Integrable f
  ⊢ (∫ (a : α), f a) = 0
  -/

[Damiano Testa]

If anyone has any "real world" example where they would like to test this tactic, I would be happy to take a look and see what goes wrong with it!

[Yaël Dillies]

I really want the general tactic to be called junk.

[Damiano Testa]

Sure, junk would probably also case-split on Nat-subtraction, right? :smile:

[Damiano Testa]

Since macros can be expanded, maybe this could be the first iteration of junk...

[Yaël Dillies]

Yes and yes, that's exactly what I'm thinking. You have a general tactic junk which calls extensions that each deal with junk values in a specific case (0 in a group_with_zero, a ≤ b when b - a : ℕ is in the goal, integrability, nonemptiness, ...).

[Damiano Testa]

I agree with you, Yaël, and had a "split nat_sub" tactic in mathlib3. I'd be happy to implement and extend it in mathlib4, but would start with this one, that seems easier.

[Damiano Testa]

Maybe we should have a Tactic.Junk namespace and put all the helper tactics for junk in there.

[Damiano Testa]

So, the tactic above could be a stub for Tactic.Junk.integrable.

[Damiano Testa]

And junk matches the target with all the Junk.whatever that are implemented and adds the various assumptions.

[Damiano Testa]

We could even try to have a meta-tactic that takes the predicate and the "junk lemmas" as input and produces a macro expansion like unint above.

[Damiano Testa]

Then we could feed all of these trivial case splits to the meta-tactic and get rid of a bunch of junk cases.

[Yaël Dillies]

I think we don't want to hardcode the "junk lemmas" into the tactic because that would be too much work to maintain. Instead, we should assume these junk lemmas are in the simp set and try to discharge the goal using simp.

[Damiano Testa]

Naturally, some case-splits will be harder and would not fall under this scheme, but many of the ones proposed above probably would.

[Damiano Testa]

I am a little wary of leaving a "not-only" simp call in a tactic...

[Damiano Testa]

Maybe we could have a junk attribute and use simp only [junk-attribute-lemmas].

[Yaël Dillies]

That's still more work than just calling simp, but it's at least less work than curating the list from within the tactic.

[Damiano Testa]

(Wrt to simp [no-only], note that above I followed the simp by done to try to mitigate this...)

[Yaël Dillies]

I don't see the problem in calling simp to finish a goal, though.

[Damiano Testa]

Anyway, we can try with a simple simp and see how it works out.

[Damiano Testa]

Ok, I'll try to write the meta-tactic that basically does the above, but takes MeasureTheory.Integrable as a user-input.

[Yaël Dillies]

The interesting part of the tactic would be for it to figure out what you want to junk on.

[Damiano Testa]

Btw, MeasureTheory.integral_undef is not a simp-lemma.

[Yaël Dillies]

It really should :grimacing:

[Damiano Testa]

So, simp [h_int] does not actually work.

[Damiano Testa]

Anyway, I'll experiment with whatever simp-call works, and we can then discuss about the best way of proceeding.

[Damiano Testa]

Yaël Dillies said:

The interesting part of the tactic would be for it to figure out what you want to junk on.

To begin with, it could probably match the head-symbol of the target with the implemented junk-tactics. It might even recurse inside the target goal, looking for applicable junks.

[Damiano Testa]

However, this seems like a problem to be addressed later, once the "basic junk-tactics" already work.

[Damiano Testa]

docs4#tsum_eq_zero_of_not_summable is also not simp.

[Yury G. Kudryashov]

Why integral_undef should be a simp lemma, as opposed to a @[junk] lemma?

[Yaël Dillies]

For the same reason that docs#div_zero is a simp lemma.

[Yury G. Kudryashov]

div_zero matches syntactically. tsum_eq_zero_of_not_summable tries to prove not (summable _) for each tsum you have.

[Yaël Dillies]

Does that actually make any difference performance-wise?

[Damiano Testa]

Regardless of performance, here is some reason why I think that having a junk attribute could be useful.

[Damiano Testa]

The junk tactic should make a case split on some Prop. If some lemmas are marked @junk, then the tactic could try to match the expression of the target with some of the assumption of the junk-lemmas and "understand" automatically what Prop it should split on, simply inspecting the type of the target.

[Damiano Testa]

The junk attribute could even have an optional hypothesis, defaulting to the first assumption that begins with not.

[Yaël Dillies]

But then you're going to need tagging many lemmas with @[junk], or do you want to also fall back on simp?

[Damiano Testa]

So far, the junk tactic is basically a way of doing

  by_cases [...]
  . simp [something]
  . _

I think that the more it can figure out what to case on and which lemmas to use in simp automatically, the better.

[Damiano Testa]

I am happy to fall back on simp, but all considerations of efficiency and workability would have to be tested against some attempt, I think.

[Damiano Testa]

Also, I think that the heuristic "case on an assumption that is a negation" is probably getting you a good chunk of junk splits correctly right away.

[Damiano Testa]

For the remaining ones, like Summable, Integrable,... we use the attribute.

[Damiano Testa]

I am imagining something like what used to happen with to_additive: you have to teach it a dictionary, and then it takes off. Same here: if you introduce a suitable junk value, you teach it to junk.

[Yaël Dillies]

So you want to tag the possible case splits, not the lemmas to use? That's what I had in mind too.

[Damiano Testa]

The case splits take a Prop, so this is certainly one piece of the equation. In some cases, simp will close the junk goal, but in some others it will not. The junk attribute might guide in this choice.

[Yury G. Kudryashov]

nontriviality relies on the default simp set + lemmas tagged with nontriviality

[Yury G. Kudryashov]

Because after you apply lemmas that assume Subsingleton, you may get a goal like a * 0 = 0

[Damiano Testa]

In a current attempt, this works:

attribute [simp] tsum_eq_zero_of_not_summable
attribute [simp] MeasureTheory.integral_undef

example (f : α → E) : (∫ a, f a) = 0 ∨ Integrable f := by
  junk_gen Integrable f
  exact Or.inr ‹_›

example (f : ℕ → E) : (∑' x, f x) = 0 ∨ Summable f := by
  junk_gen Summable f
  exact Or.inr ‹_›

The two "features" are

• I tagged as simp lemmas, two lemmas that are not simp and
• that I give explicitly the Prop on which to case split.

I think that the junk tag could help with making the tactic automatically select the right Prop and also using a more suitable simp set.

[Damiano Testa]

Ideally, junk would try to produce the Prop and then call simp + junk-attribute to close the trivial goal.

[Damiano Testa]

And like nontriviality, it could ask for a hint, in case it does not find a good Prop.

[Yury G. Kudryashov]

BTW, !4#4955

[Damiano Testa]

I wonder whether it is better to have

• several ad hoc tactics and then a unified one that simply tries each one of the ad hoc ones, or
• a single tactic that does all the splitting internally.

[Damiano Testa]

Maybe it is the tactics that should be tagged with junk, not the lemmas.

[Damiano Testa]

So each tactic could get its special support and then the junk tactic brings them all together.

[Yury G. Kudryashov]

In case of inhabit and nontriviality, you often need to speciry the type.

[Eric Wieser]

I'm not convinced it's worth buildings tactics for what seems to amount to by_cases something, { simp }.

[Eric Wieser]

Even nontriviality R isn't really much more useful that casesI subsingleton_or_nontrivial R

[Yury G. Kudryashov]

I like nontriviality

[Damiano Testa]

I kind of like the idea of having a tactic that dispatches with the trivial cases-splits. I agree though, that it is essentially doing by_cases X; { simp }; and not much else.

[Damiano Testa]

Another situation with special support could be Polynomial, where the case-split on whether the polynomial is 0 or not, could also replace degrees with nat_degree and reduce as much as possible to Nat, instead of WithBot Nat.

[Yury G. Kudryashov]

The issue with doing case split on, e.g., Integrable is that often you have two integrals and the formula works because either both functions are integrable, or both functions are not integrable.

[Damiano Testa]

Yuri, if you have a good example of where the case-split would help with the proof, let me know and I can try out the junk tactic.

[Yury G. Kudryashov]

See, e.g., src4#tsum_mul_left

[Yury G. Kudryashov]

The case else is not trivial and depends on whether a = 0 or not.