goal "P & Q --> Q & P"Hal responds by reminding you of the top-level goal and showing what subgoals you currently have:
P & Q --> Q & P 1. empty |- P & Q --> Q & PYou can then do the proof interactively from the bottom up, by repeatedly applying a particular sequent calculus rule to a particular subgoal. In this case, we might proceed as follows:
by (impR 1) P & Q --> Q & P 1. P & Q |- Q & PHere we've applied the implication right rule to subgoal 1, yielding the new subgoal of proving Q & P under the assumption P & Q. Next we apply the conjunction left rule to that subgoal which leaves us having to prove Q & P under the two assumptions P and Q:
by (conjL 1) P & Q --> Q & P 1. P, Q |- Q & PNext we apply the conjunction right rule to that subgoal, yielding two subgoals:
by (conjR 1) P & Q --> Q & P 1. P, Q |- Q 2. P, Q |- RBoth of those are instances of the basic axiom, so we just have to apply that twice:
by (basic 2) P & Q --> Q & P 1. P, Q |- Q by (basic 1) P & Q --> Q & P No subgoals left!When there are no subgoals left, we have proved the theorem.
goal "(ALL x.P(x)) --> P(a)" (ALL x. P(x)) --> P(a) 1. empty |- (ALL x. P(x)) --> P(a) by (impR 1) (ALL x. P(x)) --> P(a) 1. ALL x. P(x) |- P(a) by (allL 1) (ALL x. P(x)) --> P(a) 1. P(?_a), ALL x. P(x) |- P(a) by (unify 1) (ALL x. P(x)) --> P(a) No subgoals left!Note how the left rule for universal quantification introduces a fresh metavariable ?_a. The unify tactic tries to find a substitution for the metavariables which will make the subgoal be an instance of the basic axiom. In this case it succeeds using the substitution which maps ?_a to the ordinary variable a.
goal "EX z. P(z) --> (ALL x. P(x))" EX z. P(z) --> (ALL x. P(x)) 1. empty |- EX z. P(z) --> (ALL x. P(x)) by (exR 1) EX z. P(z) --> (ALL x. P(x)) 1. empty |- P(?_a) --> (ALL x. P(x)) EX z. P(z) --> (ALL x. P(x)) by (impR 1) EX z. P(z) --> (ALL x. P(x)) 1. P(?_a) |- ALL x. P(x), EX z. P(z) --> (ALL x. P(x)) by (allR 1) EX z. P(z) --> (ALL x. P(x)) 1. P(?_a) |- P(_b), EX z. P(z) --> (ALL x. P(x)) _b not in ?_a by (exR 1) EX z. P(z) --> (ALL x. P(x)) 1. P(?_a) |- P(?_c) --> (ALL x. P(x)), P(_b), EX z. P(z) --> (ALL x. P(x)) _b not in ?_a by (impR 1) EX z. P(z) --> (ALL x. P(x)) 1. P(?_c), P(?_a) |- ALL x. P(x), P(b), EX z. P(z) --> (ALL x. P(x)) _b not in ?_a by (unify 1) EX z. P(z) --> (ALL x. P(x)) No subgoals left!One of the interesting features of this proof is the way in which the new variable _b generated by the application of the universal quantification right rule is constrained not to be free in any term which gets substituted for the metavariable ?_a. This restriction is shown under the current set of subgoals and prevents the proof from being finshed off with an application of unify straight after the first application of allR.
goal "P --> P & (P & (P & P))" P --> P & (P & (P & P)) 1. empty |- P --> P & (P & (P & P)) by (impR 1) P --> P & (P & (P & P)) 1. P |- P & (P & (P & P))then it's obvious that we'll have to apply conjunction right and the basic axiom several times. Instead of doing that by applying the individual tactics manually, we can use the tacticals repeat and || to produce a new tactic that does the whole thing in one go:
by (repeat ((conjR 1) || (basic 1))) P --> P & (P & (P & P)) No subgoals left!The || tactical combines two tactics into the tactic that tries to do the first and, if that fails, then tries to do the second. The repeat tactical takes a single tactic as argument and returns the tactic which repeatedly applies that argument until it fails.
Hal has some useful tactics built from the elementary logical rules using tacticals. These can prove quite a few things automatically and can significantly shorten interactive proofs. The depth tactic, for example, does a depth-first search of the proof tree. This can get stuck down dead-ends, but works quite often:
goal "~ (EX x. ALL Y. J(x,y) <-> ~J(y,y))" ~(EX x. ALL Y. J(x, y) <-> ~J(y, y)) 1. empty |- ~(EX x. ALL Y. J(x, y) <-> ~J(y, y)) by depth ~(EX x. ALL Y. J(x, y) <-> ~J(y, y)) No subgoals left!
goal : string -> unit Parses its argument as a formula and makes that the current goal. by : tactic -> unit Attempts to apply its argument to the current proof state. all : tactic no : tactic The tactics which always fail and succeed, respectively. conjL, conjR, disjL, disjR, impL, impR, negL, negR, iffL, iffR, exL, exR, allL, allR, basic : int -> tactic Apply the appropriate sequent calculus rule to the numbered subgoal. safeSteps : int -> tactic Applies a sequence of `safe' rules to the numbered subgoal. quant : int -> tactic Expands quantifiers in numbered subgoal. depth : tactic Solves all subgoals by depth-first search (incompletely). step : int -> tactic Tries to use safe steps on numbered subgoal, otherwise using unification and quantifier expansion. depthIt : int -> tactic Solves all subgoals using depth-first iterative deepening with increment given as argument. Compared to depth, this is slower but doesn't get stuck down blind alleys. --, ||, |@| : tactic * tactic -> tactic (infix) Sequential composition, committed and non-commited choice of tactics. try : tactic -> tactic Attempts to apply its argument. repeat : tactic -> tactic Keeps on trying to apply its argument until it fails. repeatDeterm : tactic -> tactic Like repeat, but only considers the first result from each iteration.The syntax of logical formulae should be fairly obvious from the above examples. Just to summarise the ASCII representation of the connectives:
Universal quantification : ALL x. Existential quantification : EX x. Conjunction : & Disjunction : | Implication : --> Biimplication : <-> Negation : ~
MLj home | Comments to: mlj@dcs.ed.ac.uk |