Skip to content

Home

Jump to bottom
Conor McBride edited this page Jan 24, 2021 · 17 revisions

ask

Still very much under construction, ask is a proof assistant designed to assist in the teaching of logic to beginners. Its syntax is based on the Haskell programming language, using nested indentation to indicate tree structure, and many of the same layout and identifier conventions, so it may help Haskell beginners, too. At the moment, it can handle propositional logic, but watch this space...

To use ask, you feed in a partial proof, and out comes a new version of that proof which is at least as good, and hopefully better. You ask, and the machine collaborates with you on your proof document. It fills in missing subgoals, and I'm afraid to say, it comments out things it can't understand or doesn't see the point of. (Error reporting is terse, just now, but will improve.) Subgoals which need input from you are left as stubs, marked with ?. When your proof has no stubs and ask can't see any way to make it better, returning your input unchanged, that means it agrees with your proof and you've completed it!

Example

Here's a typical completed proof

prove p & q -> q & p by ImpI where
  given p & q prove q & p by AndI where
    prove q from p & q
    prove p from p & q

Before getting into the detail, notice its shape:

blah blah blah where
  rhubarb rhubarb
  rhubarb rhubarb

Each proof has a head at the top, then where, then an indented block of zero or more subproofs. (If there are no subproofs, you may skip the where.) Each subproof must be indented by at least one space (two is recommended) and all subproofs from the same head must be indented the same amount.

Detail

Interactive Proof

Let's work through our example proof a step at a time. We start with a top-level stub

prove p & q -> q & p ?

We have no hypotheses and our goal is an implication (because & has higher precedence than ->). So we need to prove an implication, and that's what the rule ImpI is for. We replace the stub method ? with the more progressive method by ImpI and send

prove p & q -> q & p by ImpI

Faced with this, ask matches the goal and the rule ImpI with the available rules and finds that, yes, you can prove a -> b by ImpI, if you substitute a = p & q and b = q & p, and that yields subgoal given p & q prove q & p, which gets returned as a stub

prove p & q -> q & p by ImpI where
  given p & q prove q & p ?

We now have one hypothesis, so we may choose either to analyse that hypothesis or proceed with the goal. Let's bash on with the latter. We send

prove p & q -> q & p by ImpI where
  given p & q prove q & p by AndI

and that matches the AndI rule, so back comes

prove p & q -> q & p by ImpI where
  given p & q prove q & p by AndI where
    prove q ?
    prove p ?

Each of those subgoals follows from the hypothesis, so we may send

prove p & q -> q & p by ImpI where
  given p & q prove q & p by AndI where
    prove q from p & q
    prove p from p & q

and ask is happy. Why? Well, for prove q from p & q, ask wants, firstly, to check that p & q even holds. It's given as a hypothesis, so no need to say anything. Next it unpacks the reason for p & q: it must have come from AndI with subproofs of p and q, so now we face given p, q prove q but that is also obvious by appeal to hypothesis. The same happens for p. If you want to spell out all the appeals to hypotheses, you can:

prove p & q -> q & p by ImpI where
  given p & q prove q & p by AndI where
    prove q from p & q where
      prove p & q given
      given p, q prove q given
    prove p from p & q where
      prove p & q given
      given p, q prove p given

will also be accepted.

Meanwhile, consider the road not taken. We could have said

prove p & q -> q & p by ImpI where
  given p & q prove q & p from p & q

and despite the fact that our goal is neither p nor q, ask makes progress, breaking down p & q into two separate hypotheses p and q

prove p & q -> q & p by ImpI where
  given p & q prove q & p from p & q where
    given p, q prove q & p ?

so now when we say

prove p & q -> q & p by ImpI where
  given p & q prove q & p from p & q where
    given p, q prove q & p by AndI

the two generated subgoals follow without further comment. We can still say

prove p & q -> q & p by ImpI where
  given p & q prove q & p from p & q where
    given p, q prove q & p by AndI
      prove q given
      prove p given

if we want. Note that the hypotheses available are those which are given on the path through the proof from the top to the particular subproof we're working on. As you work on subproofs within subproofs, more hypotheses may be given, but no hypothesis is forgotten.

Clone this wiki locally