Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Strange behaviour of subst/EqSubst.eqsubst_tac


view this post on Zulip 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

[1]:
https://stackoverflow.com/questions/63657976/subst-refl-closing-duplicate-subgoals-whats-going-on/63658319#63658319

view this post on Zulip 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

view this post on Zulip 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: Dec 08 2021 at 08:24 UTC