Next: Theorems and Configure Theorems Up: New features in LEGO Version 1.3 Previous: Speedups

LEGO Version 1.3: Then

Previously, the effect of

was to execute command A, then execute command B. ie B was executed on whatever was the current subgoal after A finished. If A left several subgoals, then B was only executed on the first. If A discharged its goal, then B was executed on whatever proof obligation surfaced next.

For this alpha release, the Then tactical has been modified to reflect more accurately the LCF spirit.

Morally, the effect of A Then B should be to execute A, then execute B for each of the subgoals generated by A, if there are any.

Unfortunately, if A leaves us with more than one subgoal, running B on the first may leave the others inaccessible. However, the new implementation tags these inaccessible subgoals with an instruction to execute B automatically as soon as each one resurfaces. Hence B is executed on each subgoal generated by A.

It may be the case that B does not complete the proof of A's first subgoal, and that you may need to intervene. Once you have finished off the branch and the next A-subgoal comes up, B will happen to it before your eyes. This may prove slightly disconcerting.

Here's an example:

  Lego> Goal plus: nat->nat->nat;
  Goal plus
     ?0 : nat->nat->nat
  Lego> Induction 1 Then intros;
  Refine by  nat_elim ([_:nat]nat->nat)
     ?1 : nat->nat
     ?2 : nat->(nat->nat)->nat->nat
  executing delayed Then tactic...               (* intros for ?1 *)
  intros (1) 
    H : nat
     ?3 : nat
  Lego> Refine H;                   (* user finishes off ?1 proof *)
  Refine by  H
  Discharge..  H
     ?2 : nat->(nat->nat)->nat->nat
  executing delayed Then tactic...               (* intros for ?2 *)
  intros (3) 
    x1 : nat
    x1_ih : nat->nat
    H : nat
     ?4 : nat
  Lego> Refine (suc (x1_ih H));
  Refine by  suc (x1_ih H)
  Discharge..  H x1_ih x1
  *** QED ***

Then behaves correctly with respect to Undo. Undo n undoes n user commands. A tactical compound counts as a single command. If you undo a command which was followed by the automatic execution of a delayed Then tactic, you will still return to the state before your command, incidentally undoing the delayed tactic and replacing the tag on its goal.

One slight quirk is what happens to A Then B if A succeeds but B fails. Morally, if any instance of B fails, the whole A Then B should fail. However, the latency in executing some B's makes this impractical. Hence our A Then B really behaves like A Then (Try B).

An ideal implementation of Then requires the ability to switch between different branches of the proof in their different contexts. This is difficult because implicit synthesis of existential variables can cause interference between branches. What has been done falls well short of this ideal, but it nonetheless a powerful and effort-saving tool.