Prop is the type of propositions. A proposition is a statement
that could be true or false.
Prop is very similar to
the main difference is that whereas any
Bool can always be
evaluated to see if it is
false, this may not be
possible for a
Prop due to the use of quantifiers (
Any Boolean expression can be used as a proposition.
x > 5, and
(x < y) -> ((x == 2) \/ (x ==
3)) can all be used as propositions.
However, unlike Boolean expressions, propositions can use quantifiers, that is,
exists. For example,
forall x : Z. x^2 >= 0 is a
Prop (but not a
If you type a proposition at the Disco prompt, it will simply print
<Prop> and refuse to evaluate it. If you want to get an idea of
whether a proposition is true or false, you have two options:
holdsfunction tries its best to determine whether a proposition is true or false. If it returns a value at all, it is definitely correct. For example,
holds ((5 < 3) \/ ((2 < 1) -> false))yields
holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (q \/ p))yields
holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q))yields
holds (forall n:N. n < 529)yields
However, sometimes it may simply get stuck in an infinite loop. For example,
holds (forall n:N. n >= 0)will simply get stuck. Even though it is obvious to us that this proposition is true,
holdsis not smart enough to see this; it simply tries evaluating
n >= 0for every natural number, which will never finish.
One can also use the
:testcommand. This command makes a best effort to evaluate a proposition, but only trying a finite number of examples for infinite domains. Additionally, in many cases it can output much more information than a simple
false, for example, showing a counterexample if a
forallis false, or a witness if an
existsis true. For example,
:test forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q)prints
- Certainly false: ∀p. ∀q. p \/ q <-> p /\ q Counterexample: p = false q = true
:test forall n:N. n < 529prints
- Possibly true: ∀n. n < 529 Checked 100 possibilities without finding a counterexample.
Obviously this proposition is false, but Disco apparently does not try a big enough value of
nto be able to tell.
Note that at the moment it is not possible to combine propositions
using logical operators like
->. For example, Disco does not currently accept something like
(forall x : N. x >= 0) /\ (exists x : N. x == 3), although this is
certainly a proposition from a mathematical point of view. This is
something that may be added in the future.