4 ms·
It would be interesting if you can show how Coq refused to accept the old formula and what error it produced.
by random314 6y ago
It would be interesting if you can show how Coq refused to accept the old formula and what error it produced.
- gopiandcode 6y agoWhen I was attempting to prove Bloom's original incorrect bound, the work never progressed to the point where I was actively working directly on proving his bound - I managed to prove some intermediate theorems, but was unable to work out a way to compose them. The issue ended up being that that I was unable to derive the independence required to prove the inductive step. If you're interested at looking at the sources, I think the following commit was around the place where I was working on this: https://github.com/certichain/ceramist/commit/70927c5b50e21a08f510cfd9555d8324a61c1233 https://github.com/certichain/ceramist/commit/70927c5b50e21a...
- jhanschoo 6y agoNote that you don't really "get <a proof assistant> to refuse to accept" an incorrect result, you just fail to construct a proof for it, as the author talks about in their reply. What you can do, sometimes, is succeed in proving the negation of the incorrect result.