Stream: Coq users

Topic: Extraction of (ε, δ) proofs

view this post on Zulip PigeonV (May 17 2020 at 16:04):

Hi,
I'm a bit new to Coq. I'd like to build an interactive demo of what a continuity proof computes. continuity_pt_plus from the Reals builtin library returns a Prop, so I can't extract a function that would graph it in a hypothetical js_of_ocaml demo. I've re-implemented a monolithic proof of additivity (?) but I was wondering whether I could slightly adapt the existing library to use sig.
Thanks!

view this post on Zulip Bas Spitters (May 17 2020 at 16:53):

I believe we made those proofs computational in
https://github.com/coq-community/math-classes

view this post on Zulip PigeonV (May 17 2020 at 17:54):

Thanks. I can't find any concrete implementation, maybe it's in CoRN?

view this post on Zulip PigeonV (May 17 2020 at 18:07):

Found it. TIL about CProp...

view this post on Zulip Bas Spitters (May 17 2020 at 18:10):

I expect there are similar lemmas in the reals/fast and reals/faster directories.

Last updated: Oct 13 2024 at 01:02 UTC