An instance when you can eliminate propositional double negation in coq

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.

• Equality is decidable for naturals. – Derek Elkins Oct 30 '18 at 10:03