A note on differene between bool and Prop

In the last lecture, professor pointed the difference between bool and Prop. IIUC, In order to express theorem on infinite data, built-in predicate "forall" must be introduced. To use "forall", it must be Prop or Type. (https://coq.inria.fr/refman/Reference-Manual006.html) In below code, "ge 0 n", "geb 0 n = true" is Prop, but "geb 0 n" is bool.

Fixpoint geb(n m: nat) :=
  match n, m with
    | O, _ => true
    | S n', O => false
    | S n', S m' => geb n' m'
  end.

Check (forall n: nat, ge 0 n).
Fail Check (forall n: nat, geb 0 n).
Check (forall n: nat, (geb 0 n = true):Type).
Check (forall n: nat, (geb 0 n = true):Prop).

Also, below article mentions another point. http://adam.chlipala.net/cpdt/html/Predicates.html tl;dr => bool must be computable inside Coq, and it can be used in if-then-else.

' One potential point of confusion in the presentation so far is the distinction between bool and Prop. The datatype bool is built from two values true and false, while Prop is a more primitive type that includes among its members True and False. Why not collapse these two concepts into one, and why must there be more than two states of mathematical truth, True and False?
The answer comes from the fact that Coq implements constructive or intuitionistic logic, in contrast to the classical logic that you may be more familiar with. In constructive logic, classical tautologies like ~ ~ P -> P and P \/ ~ P do not always hold. In general, we can only prove these tautologies when P is decidable, in the sense of computability theory. The Curry-Howard encoding that Coq uses for or allows us to extract either a proof of P or a proof of ~ P from any proof of P \/ ~ P. Since our proofs are just functional programs which we can run, a general law of the excluded middle would give us a decision procedure for the halting problem, where the instantiations of P would be formulas like "this particular Turing machine halts."
A similar paradoxical situation would result if every proposition evaluated to either True or False. Evaluation in Coq is decidable, so we would be limiting ourselves to decidable propositions only.
Hence the distinction between bool and Prop. Programs of type bool are computational by construction; we can always run them to determine their results. Many Props are undecidable, and so we can write more expressive formulas with Props than with bools, but the inevitable consequence is that we cannot simply "run a Prop to determine its truth."

snu-sf-class / pl2016

A note on differene between bool and Prop #52