Difference between sumbool and intuitionnistic disjunction

Question

According to Coq's documentation

sumbool is a boolean type equipped with the justification of their value

I thought that was already a property of the disjunction, in the intuitionnistic (or constructive) logic that Coq implements.

For example, to prove an excluded middle p \/ ~p in Coq, you have to do actual work, it is not a logical axiom. So a proof of p \/ q must either be a proof of p or a proof of q.

Then why do we need sumbool p q ?

EDIT

By replacing the tactics by exact proofs, I got more specific error messages. This one is fine :

Lemma sumbool_or : forall p q : Prop, sumbool p q -> p \/ q.
Proof.
  exact (fun (p q : Prop) (H : sumbool p  q) =>
           match H with
           | left p0 => or_introl p0
           | right q0 => or_intror q0
           end).
Qed.

However this one

Lemma or_sumbool : forall p q : Prop, p \/ q -> sumbool p q.
Proof.
  exact (fun (p q : Prop) (H : p \/ q) =>
           match H with
           | or_introl p0 => left p0
           | or_intror q0 => right q0
           end).
Qed.

tells me

Error:
Incorrect elimination of "H" in the inductive type "or":
the return type has sort "Set" while it should be "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Set
because proofs can be eliminated only to build proofs.

I'm a bit surprised. So a primitive like match depends on the sort of thing we want to prove ? It looks low-level lambda-calculus though.

Answer 1

The sumbool type lives in Coq's computationally relevant universe Type (or Set). In particular, we can write programs using functions that return elements of {P} + {Q} (for instance, the standard library's Nat.eq_dec : forall n m : nat, {n = m} + {n <> m}, which tests whether two numbers are equal).

Logical disjunction, on the other hand, belongs to the computationally irrelevant universe Prop. We cannot perform case analysis on a proof of type P \/ Q because Coq was designed to erase proofs when a program is extracted, and such a case analysis might alter the outcome of a computation. This makes it safe for us, for example, to add the excluded middle axiom forall P : Prop, P \/ ~ P without impacting the execution of extracted programs.

It would also be possible to add a strong form of the excluded middle that lives in Type: forall P : Prop, {P} + {~P}; however, if we use this axiom to write programs, we will not be able to execute them.