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.
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With