Prelude

Preloaded Propositions and Rules in ask

The prop keyword introduces a new propositional connective by giving a template for the way you write it, with each parameter position showing the parameter type. Prop is the type of propositions. Then, in a where clause, we specify the introduction rules, exactly by giving a typical example of how to use them in a proof. Names which start with a lowercase letter (when not keywords) are schematic variables standing for anything of the right type. By contrast, Identifiers which begin in Uppercase (e.g., ImpI) are constructors which make things, not variables which stand for things.

prop Prop -> Prop where
  prove a -> b by ImpI where
    given a prove b
infixr 1 ->

So, "implies" (written ->) joins two propositions, and you prove a -> b by showing that given a, b follows. The infixr 1 means that -> has low precedence and nests to the right, i.e. a -> b -> c means a -> (b -> c), and (a -> b) -> c really needs those parentheses.

prop Prop & Prop where
  prove a & b by AndI where
    prove a
    prove b
infixr 7 &

To prove a "and" b, prove a and prove b! Again, & nests rightward but has higher precedence than ->, so a & b -> c means (a & b) -> c.

Meanwhile, there is a choice of ways to prove an "or":

prop Prop | Prop where
  prove a | b by OrIL where
    prove a
  prove a | b by OrIR where
    prove b
infixr 6 |

Note that | also nests to the right, and its precedence level is between that of -> and that of &.

We have two base cases. There are propositions False (which cannot be proven) and True (which can be proven with no subgoals).

prop False

prop True where
  prove True by TrueI

Whenever a subgoal is True or introduces False as a hypothesis, ask considers it trivial and does not demand a proof.

We could use -> False as logical negation, but to respect the way negation and implication are independently valid notions, we take

prop Not p where
  prove Not p by NotI where
    given p prove False

which in turn allows us to add classical Contradiction

prove p by Contradiction where
  given Not p prove False

We thought about demanding prove Not (Not p) but that leaves no choice but to invoke NotI, so we saved you a step.