isabelle

What does the `using` keyword do with `blast`?


Sometimes, using XXX apply blast discharges a proof goal, but apply (blast mod: XXX) doesn't work for mod any of intro, elim or del, with or without !.

What does using actually do to blast?


Solution

  • using does not directly influence blast. It affects the proof state, on which blast operates.

    The using keyword temporally places an established fact from the context as antecedent in the current proof state. The new antecedent has the same status as all the others left of the main ‹⟹› of the proof state. (Might call them “local assumptions”, but technically it's not always something we “assume”.)

    There are some technicalities here, as using affects all goals if there are multiple, but will be forgotten after the next application.

    A minimal example would be:

    lemma
      ‹x = x› ‹y = y›
      using refl
      by assumption+
    

    Because using is transient, apply assumption apply assumption done would not work here. (But using refl apply assumption using refl apply assumption done would.)

    What role the antecedents play, depends on the proof method. (For instance, the proof method cases just ignores antecedents.)

    blast will usually use all antecedents to discharge the current goal. Therefore, using has great effects on how far a blast invocation will get you.

    apply (blast elim/intro:) allows you to temporally add facts as elimination or introduction rules for logic reasoning; del: allows you to temporally remove them. The parallel is that these modifiers have only transient effect, but they affect the intro/elim rule sets, not the proof state. They are more specific because they are only present for certain proof methods (like blast and auto). But they thus also are less general than using. Not every fact makes for a good elimination or introduction rule. This might explain your observation that using ... by blast discharges a goal where by (blast intro: ...) does not.