Email Gateway (Aug 30 2020 at 14:19): Email Gateway (Aug 30 2020 at 14:19):From: Manuel Eberl <eberlm@in.tum.de>
Somebody asked a question of StackOverflow [1] about why the "subst"
method (which should only affect the first subgoal) implicitly
discharges duplicate subgoals. I checked the code and found that it
somehow calls "distinct_subgoals_tac" somewhere, although I find the
code very difficult to read:
fun eqsubst_tac ctxt occs thms i st =
let val nprems = Thm.nprems_of st in
if nprems < i then Seq.empty else
let
val thmseq = Seq.of_list thms;
fun apply_occ occ st =
thmseq |> Seq.maps (fn r =>
eqsubst_tac' ctxt
(skip_first_occs_search occ searchf_lr_unify_valid) r
(i + (Thm.nprems_of st - nprems)) st);
val sorted_occs = Library.sort (rev_order o int_ord) occs;
in
Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ
sorted_occs) st)
end
end;
In any case, it seems to me that this violates the usual contract that a
tactic that takes a subgoal index should only affect that one subgoal.
I have no idea why it calls distinct_subgoals_tac in the first place. A
simple solution would be to just wrap the entire thing in a
"SELECT_GOAL". The performance impact should be minimal since this
tactic is typically used very sparingly for single rewrite steps; any
heavy rewriting is done with the simplifier anyway.
Any other opinions on this?
Manuel
Email Gateway (Aug 30 2020 at 14:27):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Manuel,
when you apply a conditional rewrite rule in several places with
apply(subst (1 2 3) cond_rule)
where the assumptions of the rule end up as the same subgoal, then the
distinct_subgoals_tac ensures that the user has to discharge the assumptions only once. So
there's a point in eliminating repeated goals. But I agree with you that this should be
confined to the subgoal on which subst is operating.
Andreas
Email Gateway (Aug 31 2020 at 20:35):From: Makarius <makarius@sketis.net>
I have looked at the history: this odd behaviour goes back to 2005 (by Lucas
Dixon), see https://isabelle-dev.sketis.net/rISABELLE366d39e95d3c
In later years we've got sufficiently well-established means to make proof
tools behave the proper way.
It actually turned out very easy to amend that on the spot, see the following
changes for next Isabelle release:
https://isabelle-dev.sketis.net/rISABELLEe5fcbf6dc687
https://isabelle-dev.sketis.net/rAFPcb48e644eda2
(As usual, AFP serves as a sanity check to see if a hypothetical change should
become real.)
Makarius
Last updated: Jul 15 2022 at 23:21 UTC