Propositions

Prop is the type of propositions. A proposition is a statement that could be true or false. Prop is very similar to Bool; the main difference is that whereas any Bool can always be evaluated to see if it is true or false, this may not be possible for a Prop due to the use of quantifiers (forall and exists).

Any Boolean expression can be used as a proposition. For example, true, 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, forall or exists. For example, forall x : Z. x^2 >= 0 is a Prop (but not a Bool).

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:

  • The built-in holds function 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 true
    • holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (q \/ p)) yields true
    • holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q)) yields false
    • holds (forall n:N. n < 529) yields false

    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, holds is not smart enough to see this; it simply tries evaluating n >= 0 for every natural number, which will never finish.

  • One can also use the :test command. 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 true or false, for example, showing a counterexample if a forall is false, or a witness if an exists is true. For example,

    • :test forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q) prints

      - Test is false: ∀p. ∀q. p \/ q <-> p /\ q
        Counterexample:
          p = false
          q = true
      
    • However, :test forall n:N. n < 529 prints

      - Test passed: ∀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 n to be able to tell.

Note that at the moment it is not possible to combine propositions using logical operators like /\, \/, or ->. 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.