Suppose st: string -> nat and X stands for the string 'X'.

Given the hypothesis not(st X <> 0), I can successfully derive

assert (st X = 0). { omega. }

But in Coq's constructive logic, a proposition of the form (P -> False) -> False does not in general imply P.

I imagine the fact that st is a function enables one to prove the above theorem. If this is the case, then how does the omega tactic use this fact in the proof?

Though I am aware that omega is an implementation of a certain decision procedure for a weak form of arithmetic, I know almost nothing about how it works.

I am just looking for a general explanation. There's no need for many details.

  • 4
    $\begingroup$ Equality is decidable for naturals. $\endgroup$ – Derek Elkins Oct 30 '18 at 10:03

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.