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 left SE Oct 30 '18 at 10:03

Your Answer

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

Browse other questions tagged or ask your own question.