proofManagerLib.expand

`expand`

proofManagerLib.expand : tactic -> proof

Applies a tactic to the current goal, stacking the resulting subgoals.

The function expand is part of the subgoal package. It may be abbreviated by the function e. It applies a tactic to the current goal to give a new proof state. The previous state is stored on the backup list. If the tactic produces subgoals, the new proof state is formed from the old one by removing the current goal from the goal stack and adding a new level consisting of its subgoals. The corresponding justification is placed on the justification stack. The new subgoals are printed. If more than one subgoal is produced, they are printed from the bottom of the stack so that the new current goal is printed last.

If a tactic solves the current goal (returns an empty subgoal list), then its justification is used to prove a corresponding theorem. This theorem is incorporated into the justification of the parent goal and printed. If the subgoal was the last subgoal of the level, the level is removed and the parent goal is proved using its (new) justification. This process is repeated until a level with unproven subgoals is reached. The next goal on the goal stack then becomes the current goal. This goal is printed. If all the subgoals are proved, the resulting proof state consists of the theorem proved by the justifications.

The tactic applied is a validating version of the tactic given. It ensures that the justification of the tactic does provide a proof of the goal from the subgoals generated by the tactic. It will cause failure if this is not so. The tactical VALID performs this validation.

For a description of the subgoal package, see set_goal.

Failure

expand tac fails if the tactic tac fails for the top goal. It will diverge if the tactic diverges for the goal. It will fail if there are no unproven goals. This could be because no goal has been set using set_goal or because the last goal set has been completely proved. It will also fail in cases when the tactic is invalid.

Example

- expand CONJ_TAC;
- expand CONJ_TAC;
OK..
NO_PROOFS! Uncaught exception:
! NO_PROOFS

- g `(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])`;
> val it =
    Proof manager status: 1 proof.
    1. Incomplete:
         Initial goal:
         (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2; 3])

     : proofs

- expand CONJ_TAC;
OK..
2 subgoals:
> val it =
    TL [1; 2; 3] = [2; 3]


    HD [1; 2; 3] = 1

     : proof

- expand (REWRITE_TAC[listTheory.HD]);
OK..

Goal proved.
|- HD [1; 2; 3] = 1

Remaining subgoals:
> val it =
    TL [1; 2; 3] = [2; 3]

     : proof

- expand (REWRITE_TAC[listTheory.TL]);
OK..

Goal proved.
|- TL [1; 2; 3] = [2; 3]
> val it =
    Initial goal proved.
    |- (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2; 3]) : proof

In the following example an invalid tactic is used. It is invalid because it assumes something that is not on the assumption list of the goal. The justification adds this assumption to the assumption list so the justification would not prove the goal that was set.

- g `1=2`;
> val it =
    Proof manager status: 2 proofs.
    2. Completed: |- (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2; 3])
    1. Incomplete:
         Initial goal:
         1 = 2

     : proofs
- expand (REWRITE_TAC[ASSUME (Term `1=2`)]);
OK..

Exception raised at Tactical.VALID:
Invalid tactic
! Uncaught exception:
! HOL_ERR

Note that an invalid tactic may “succeed”. Thus, where tac1 is invalid, and tac2 is valid (and both succeed), FIRST [tac1, tac2] is invalid. For example, where theorem uth is [p] |- q and uth' is [p'] |- q

1 subgoal:
val it =

q
------------------------------------
  p
:
   proof

> e (FIRST (map ACCEPT_TAC [uth', uth])) ;
OK..

Exception raised at Tactical.VALID:
Invalid tactic [...]

> e (FIRST (map (VALID o ACCEPT_TAC) [uth', uth])) ;
OK..

Goal proved.
 [p] |- q

Doing a step in an interactive goal-directed proof.

expand

Failure

Example

See also

`expand`