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?
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.