5
$\begingroup$

For example, trying to prove that 100,000 <= 1,000,000. But Coq has a stack overflow, meaning it's actually trying to perform the 100k computations.

Coq < Eval compute in le_lt_dec 100000 1000000.
Warning: Stack overflow or segmentation fault happens when working with large
numbers in nat (observed threshold may vary from 5000 to 70000 depending on
your system limits and on the command executed).
Stack overflow.

Does this mean that it is not possible to prove that in Coq? It seems strange that you would actually need to run through every comparison to prove this, because mathematicians in the past never did such things since it would've taken way too much time and effort.

If you try it on smaller numbers, you see that it actually does try to compare each one:

Coq < Eval compute in le_lt_dec 42 42.
     = left
         (Gt.gt_le_S 41 42
            (Lt.le_lt_n_Sm 41 41
               (Gt.gt_le_S 40 41
                  (Lt.le_lt_n_Sm 40 40
                     (Gt.gt_le_S 39 40
                        (Lt.le_lt_n_Sm 39 39
                           (Gt.gt_le_S 38 39
                              (Lt.le_lt_n_Sm 38 38
                                 (Gt.gt_le_S 37 38
                                    (Lt.le_lt_n_Sm 37 37
                                       (Gt.gt_le_S 36 37
                                          (Lt.le_lt_n_Sm 36 36
                                             (Gt.gt_le_S 35 36
                                                (Lt.le_lt_n_Sm 35 35
                                                  (Gt.gt_le_S 34 35
                                                  (Lt.le_lt_n_Sm 34 34
                                                  (Gt.gt_le_S 33 34
                                                  (Lt.le_lt_n_Sm 33 33
                                                  (Gt.gt_le_S 32 33
                                                  (Lt.le_lt_n_Sm 32 32
                                                  (Gt.gt_le_S 31 32
                                                  (Lt.le_lt_n_Sm 31 31
                                                  (Gt.gt_le_S 30 31 (..))))))))))))))))))))))))
     : {42 <= 42} + {42 < 42}

Do proof assistants really need to actually perform these computations in order for it to be proven correct? It seems like there should be a shortcut, and know just from the structure of the proof that 42 <= 42 or 100,000 <= 1,000,000. Is there a way for it to see that it is true without actually performing the calculations?

Also, I am new to Coq, so I could be doing something wrong. Maybe there is a way in Coq to prove without using Eval compute?

In general, I am trying to get a better understanding of how to mechanically prove things like this in practice. If you create a proposition le in Coq, that is just a "proposition that there is an $n$ less than or equal to $m$". But to get a boolean true/false that $100,000 <= 1,000,000$, it was said that I need to first prove the decidability of le by looking at le_lt_dec. So that's where I'm at in the process of trying to learn if that helps.

$\endgroup$
  • $\begingroup$ The title is very misleading. You're not asking about proving that $n\le m$ is decidable, you're asking about proving that $n\le m$. $\endgroup$ – David C. Ullrich Aug 15 '15 at 20:27
  • $\begingroup$ You can prove it, you just shouldn't entrust it to le_lt_dec. If you don't want to construct a proof manually, you can probably go back and forth between nat and BinInt, which should have a much faster and less memory-consuming comparison routine. $\endgroup$ – darij grinberg Aug 15 '15 at 20:27
  • $\begingroup$ Ok, I will update it. I am still learning the terminology/distinctions around decidability. $\endgroup$ – Lance Pollard Aug 15 '15 at 20:27
6
$\begingroup$

Note that, in CoQ, 100000 is actually syntactic shorthand for $S S S S S \ldots 0$. It's not unreasonable that proofs of claims involving such large terms themselves must be quite large. When a mathematician looks at a claim like $1000 \leq 1000000$ and says "obviously", they are taking advantage of the fact that we wrote the claim in decimal notation. If you want to do something similar in CoQ, you could try to prove, e.g., $10 * 10 * 10 \leq 10 * 10 * 10 * 10 * 10$. You can prove such claims using lemmas like forall n, n > 0 -> 10 * n >= n.

You still have to be a little careful, though, since the normal form of, e.g., $10 * 10 * 10 * 10$ is quite large, even though the term itself isn't.

If you want efficient decision procedures for expressions involving such large numbers, you could, among other approaches, make a new inductive type corresponding to arithmetic expressions, code up decision procedures on that, then prove their correctness.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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