Fixes bug with metavariable instantiations in THEN/THENL

[PetrosPapapa]

Summary

The THEN and THENL tacticals are not propagating metavariable instantiations properly when dealing with multiple subgoals.

More specifically, (delayed) metavariable instantiations are propagated forward from one subgoal to the next, but not backwards.

For example, assume we have 2 subgoals g1 and g2 and that we apply tactics tac1 and tac2 respectively using THENL, i.e. something like ... THENL [ tac1 ; tac2 ]. If tac1 produces metavariable instantiations, they will be propagated to g2 before tac2 is applied. However, if tac2 produces metavariable instantiations, tac1 and its justification will not be aware of them. It will instead produce a theorem containing uninstantiated metavariables.

Steps to reproduce

Assume this goal:

g `p ==> ?q. (q ==> q) /\ q` ;;

Warning: Free variables in goal: p
val it : goalstack = 1 subgoal (1 total)

`p ==> (?q. (q ==> q) /\ q)`

This works fine:

e (DISCH_TAC THEN META_EXISTS_TAC);;
e (CONJ_TAC);;
e (DISCH_THEN ACCEPT_TAC);;
e (FIRST_ASSUM (UNIFY_ACCEPT_TAC [`q:bool`]));;

val it : goalstack = No subgoals

And the justification works fine too:

top_thm();;

val it : thm = |- p ==> (?q. (q ==> q) /\ q)

If you try to package the proof, however, it will not work:

prove (`p ==> ?q. (q ==> q) /\ q`, 
       DISCH_TAC THEN META_EXISTS_TAC THEN CONJ_TAC THENL [
       DISCH_THEN ACCEPT_TAC;
       FIRST_ASSUM (UNIFY_ACCEPT_TAC [`q:bool`])
       ]);;

Exception: Failure "EXISTS".

CONJ_TAC does not use metavariable instantiations so it works, but META_EXISTS_TAC complains! This is because its justification receives the correct metavariable instantiation, but the theorem provided from subsequent goals is not instantiated. More specifically, DISCH_THEN ACCEPT_TAC is generating the theorem |- q ==> q instead of the theorem |- p ==> p. The instantiation [`p`,`q`] generated by UNIFY_ACCEPT_TAC in the second subgoal is not propagated properly to the first subgoal and its justification.

The following should also work and give us {p,p} ?- p as the new goal:

g `p ==> ?q. (q ==> q) /\ q` ;;
e (DISCH_TAC THEN META_EXISTS_TAC THEN CONJ_TAC THENL [
       DISCH_TAC;
       FIRST_ASSUM (UNIFY_ACCEPT_TAC [`q:bool`])
     ]);;

Exception: Failure "EXISTS".

Solution

There are 2 changes required:

1. In seqapply within THEN/THENL, the goals gls1 generated by the first tactic/subgoal must be instantiated with the metavariable instantiation insts2 (if any) generated by the other tacs.
2. In compose_justs, the justification just1 of the first tactic must be made aware of the same instantiation insts2.

The second point was the hardest to figure out, because it was not initially clear why insts2 is not propagated from the goalstate where it is clearly provided. However, both VALID (in interactive proofs) and TAC_PROOF (in packaged proofs) run the justification starting with null_inst and not the instantiation propagated in the goalstate. This means it is entirely the responsibility of THEN/THENL to propagate metavariable instantiations from tactic to tactic during justification.

Notably, top_thm() works fine, but this is thanks to the way the by refinement is implemented. The change made to compose_justs in THEN/THENL match what by already does in interactive mode.

Validation

I have tested this in a few examples that have naturally occured in my work.

The changes are relatively minor, mirror what happens in other functions (such as by) and only affect metavariable usage.

However, THEN/THENL are core tacticals and affect pretty much every single HOL Light proof, so happy to receive advice, peer review, or suggestions for other means of testing, if necessary.

[jrh13]

Thanks, now merged in. It's a reflection of how little I use the metavariables feature that this bug stayed around for about 20 years!