21
$\begingroup$

Are there tools in mathlib which let you give computations of integrals which would roughly follow standard methods for solving them? For now let me restrict attention to some undergrad-level integrals, like $\int_0^1xe^x\,dx$, and not anything excessively crazy.

Of course, if our goal is merely to have a proof of a statement of the form $\int_a^bf(x)\,dx=c$ for some known $c$, then proving this in Lean should be possible by finding a function $F(x)$, check $F'(x)=f(x)$, evaluating $F(b)-F(a)$ and appealing to FTC. But this is an approach which is very backwards compared to how this is done by hand (which, at least somewhat implicitly, involves finding such an $F$).

My question is, does Lean have any tools which would let you perform such "by hand" calculations within your code? At the very least it would require support for integration by parts and integration by substitution, and I'm not sure those are in mathlib. Ideally I would also imagine some kind of environment like the calc mode.

If not in Lean, are there similar tools available in other proof assistants?

Just to clarify, I do not mean automated computation of integrals like in CAS. I just mean tools which would let you painlessly perform IBP and substitutions (and perhaps other operations) on given integrals to simplify them.

Improve this question
$\endgroup$
4
  • 8
    $\begingroup$ One of the great advantages of ITPs over CASs is the proof script can encode a witness that might represent a considerable amount of work to produce, without putting that work on the critical path. So while it's certainly possible in principle for Lean to play CAS here and compute the integral itself, I would contend that this is a waste of resources and you should instead precompute (either by Lean or using a CAS) and store the answer and verify it by differentiation. $\endgroup$
    – Mario Carneiro
    Feb 16, 2022 at 13:55
  • 1
    $\begingroup$ I'm curious to know whether there were attempts to formalise parts of Risch algorithm for antiderivative computation. $\endgroup$
    – Dima Pasechnik
    Feb 16, 2022 at 15:43
  • 7
    $\begingroup$ The files github.com/leanprover-community/mathlib/blob/master/test/… and github.com/leanprover-community/mathlib/blob/master/test/… are quite interesting examples of elementary integrals in Lean/mathlib. These are fairly compressed, but show that using mathlib and the simplifier/norm_num many basic steps can be automated in tactic mode. This is still regular tactic mode, but one could imagine trying a few different Ansatzen and letting Lean do several calculation steps to correct your antiderivative within this mode. $\endgroup$
    – Alex J Best
    Feb 16, 2022 at 16:10
  • $\begingroup$ for definite integration, there are verified tools: research.vu.nl/en/publications/… $\endgroup$
    – Dima Pasechnik
    Feb 16, 2022 at 21:19

1 Answer 1

Reset to default
11
$\begingroup$

I'm going to inflate Mario's comment to an answer: You can absolutely write tactics in Lean to do this. What you'll be doing is creating a large part of a CAS, but as a Tactic. This would be largely a waste of effort to do in isolation.

While Lean, especially Lean 4, would be an excellent language in which to create a CAS, this would likely be a rather independent project from mathlib. mathlib is explicitly about classical mathematics. Closed-form integration may be studied in first-year calculus, but it sits in a really odd place that straddles constructive, computational and classical mathematics. This hybrid universe of mathematics has not been studied much at all.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Thank you for posting this, although I wouldn't really say this is appropriate as an answer to the question. Also, what I am suggesting is not a tactic which would do this automatically - rather an environment similar to calc which would aid a person in making such computation. $\endgroup$
    – Wojowu
    Feb 16, 2022 at 18:49
  • $\begingroup$ Certainly Coq has such extensions implemented, but not Lean, as far as I know. $\endgroup$
    – Dima Pasechnik
    Feb 16, 2022 at 19:23
  • $\begingroup$ Hopefully a simple integration tactic will be in mathlib ;) But I agree that if someone wants to implement, like, the complete verified Risch algorithm, it should probably be an independent project. $\endgroup$
    – Trebor ♦
    Feb 18, 2022 at 17:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.