Decidability

Many useful instances of are provable constructively and the ProveDecidable  tactic is set up to construct these proofs in a systematic way. To discuss it, we first introduce the abstraction:

which can be found in the core_2 theory. It turns out that the property can be inferred for many P from knowing that for the immediate subterms Q of P. ProveDecidable takes advantage of this fact and attempts to prove goals of the form

by backchaining with any lemmas in the Nuprl library that have names with prefix decidable__.  (Note the two underscores.) There are many examples of such lemmas in the core_2 theory. ProveDecidable is usually invoked via the Decide tactic:

Decide (Q:term)

Used to case-split on whether proposition Q is true or false. Generates two main subgoals; one with the new assumption Q and the other with the new assumption . Decide also creates a subgoal and immediately runs the ProveDecidable tactic on this subgoal. ProveDecidable generates only subgoals with labels in the aux class. If ProveDecidable fails then Decide fails too. To understand why, use the tactic Assert to assert and run the ProveDecidable1 tactic to try and prove this assertion. ProveDecidable1 will generate subgoals with label decidable? to indicate those components of Q that it couldn't prove were decidable. Use ProveDecidable1 rather than ProveDecidable; ProveDecidable fails when it sees such subgoals.