Stream: Coq users

Topic: Basic integration

Anders Larsson (Sep 08 2022 at 14:32):

What is currently the best way to prove simple integrals in Coq? I guess it could be done in math-comp analysis and there seem to be some older libraries too. There are two unsolved problems on Freeks 100-list that i guess is boils down to simple integrals.

• The Area of a Circle ( http://www.cs.ru.nl/~freek/100/#9 )
• Buffon Needle Problem ( http://www.cs.ru.nl/~freek/100/#99 )

Karl Palmskog (Sep 08 2022 at 14:39):

one recent library on integration: https://depot.lipn.univ-paris13.fr/mayero/coq-num-analysis/ (coq-num-analysis package in Coq opam)

Anders Larsson (Sep 08 2022 at 14:55):

Karl Palmskog said:

one recent library on integration: https://depot.lipn.univ-paris13.fr/mayero/coq-num-analysis/ (coq-num-analysis package in Coq opam)

Nice. I'll have a look. (opam installation failed but that can probably be solved).

$ opam search coq-num-analysis
# Packages matching: match(*coq-num-analysis*)
# No matches found

Karl Palmskog (Sep 08 2022 at 15:05):

you need to do opam update, then opam show coq-num-analysis.1.0.0 works

Karl Palmskog (Sep 08 2022 at 15:07):

and also make sure to add Coq opam released repo as here: https://github.com/coq/opam-coq-archive#usage

Last updated: Oct 01 2023 at 19:01 UTC