Thoughts about assumption labelling (including hiding, abbreviation and protection)

HOL4 special assumptions (labels, abbreviations, etc).md

Protecting Assumptions

Certain assumption types are naturally thought of being at least a bit protected. To be protected is to be somewhat immune to destructive changes.

“Destructive Changes”

Changes in Place: at the bottom level, there are relatively few facilities for changing assumptions in place other than with RULE_ASSUM_TAC. Of course, tactics can just access assumption lists directly, but most don't.

• Changes in Place that Strip: the simplification routines fs and gvs (really, the underlying full_simp_tac and global_simp_tac) update in a RULE_ASSUM_TAC-like way but actually insert calls to strip_assume_tac and can also delete vacuous assumptions (those that have become T). Stripping a conjunction turns one assumption into two; stripping a disjunction creates two sub-goals. Stripping an existential is least interesting.

Deleting/Reordering/Insertion: the assumption list can be manipulated with things like pop_assum, {first,last}_x_assum and assume_tac.

Changes that “Have to Get Through”: when SUBST_ALL_TAC is applied with a theorem whose conclusion is of the form v = e, it’s surely the case that all assumptions should be subjected to this. The alternative is to leave them containing “dangling“ references to v that no longer make any sense (all other references have disappeared). It's not clear to me how many more of these sorts of change there might be, but there are clearly possibilities (if the theorem has conclusion (v1,v2) = e and the goal only contains those two variables in that pairing (v1,v2)).

The Case for Protection

Given the above, the idea of protection seems rather fraught. Perhaps it should just be dropped. See https://github.com/HOL-Theorem-Prover/HOL/commit/7edd7ba6445c for code that sets up a grossly general facility for setting up full-blown protection. I suspect most of this should be undone. The abbreviation tactics have a different approach: if an abbreviation assumption loses its desired form (Abbrev(var = exp), with exp not allowed to contain var), then the tag is lost and we drop to a normal assumption.

If the tagging/protection is just a label, what's underneath the label can change dramatically, but the assumption can't be strip_assume-d, so you might move from label -: Phi to label -: ?x. phi x /\ psi x.

For maximum generality, one might imagine registering sanity-transformation functions that get run on every “marked” assumption after a tactic is applied so that they can be rejiggered into an acceptable taste. If this might cause stripping effects, the type of the registered function would have to be thm -> tactic, which I guess is OK.