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$ Oct 30, 2018 at 10:03


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.