Email Gateway (Aug 18 2022 at 17:35): Email Gateway (Aug 18 2022 at 17:35):From: Johan Jeuring <johanj@cs.uu.nl>
We noticed that the Isabelle Reference Manual from 1999 mentions an
interleaving construct for tactics, which has disappeared in the
manual from 2011. Is there a particular reason for this?
We ask because we are working on a paper on interleaving strategies
for solving exercises (with the goal to follow and comment upon
student interactions), and Isabelle seems to be the only prover that
has offered interleave. We can imagine that efficiency might be a
reason to exclude it: the number of possibilities increases (more
than) exponentially in the length of the arguments when interleaving
is used.
Any ideas?
Thanks,
Johan Jeuring
Email Gateway (Aug 18 2022 at 17:35):From: Makarius <makarius@sketis.net>
On Thu, 14 Apr 2011, Johan Jeuring wrote:
We noticed that the Isabelle Reference Manual from 1999 mentions an
interleaving construct for tactics, which has disappeared in the manual
from 2011. Is there a particular reason for this?
It was probably dropped when renovating some of the more ancient manuals,
because it was hardly ever used.
A grep through the sources and its history reveals the following:
* Isabelle2011 provides Seq.interleave (in src/Pure/General/seq.ML)
and INTLEAVE (in src/Pure/tactical.ML) but neither of them is used.
* These operations have been there since the beginnings of recorded
Isabelle history in 1993, see also http://isabelle.in.tum.de/repos/isabelle/annotate/957c887b89b5/src/Pure/tctical.ML#l102
* In prehistoric Isabelle92 there is a single use of the tactical
val prems = goal ZF.thy
"[| f: A->B; g: C->D; A Int C = 0 |] ==> \
\ (f Un g) : (A Un C) -> (B Un D)";
(Contradiction if A Int C = 0, a:A, a:B)
val [disjoint] = prems RL ([IntI] RLN (2, [equals0D]));
by (cut_facts_tac prems 1);
by (rtac PiI 1);
(solve subgoal 2 first!!)
by (DEPTH_SOLVE_1 (eresolve_tac [UnE, Pair_mem_PiE, sym, disjoint] 2
INTLEAVE ares_tac [ex1I, apply_Pair RS UnI1, apply_Pair RS UnI2] 2));
by (REPEAT (eresolve_tac [asm_rl,UnE,rel_Un,PiE] 1));
val fun_disjoint_Un = result();
* In Isabelle93 the same is proved like this, using the "Classical
reasoner" (fast_tac):
val prems = goal ZF.thy
"[| f: A->B; g: C->D; A Int C = 0 |] ==> \
\ (f Un g) : (A Un C) -> (B Un D)";
(Contradiction if A Int C = 0, a:A, a:B)
val [disjoint] = prems RL ([IntI] RLN (2, [equals0D]));
val Pair_UnE = read_instantiate [("c","<?a,?b>")] UnE; (* ignores x: A Un
C *)
by (cut_facts_tac prems 1);
by (rtac PiI 1);
by (REPEAT (ares_tac [rel_Un, fun_is_rel] 1));
by (rtac ex_ex1I 1);
by (fast_tac (ZF_cs addDs [apply_Pair]) 1);
by (REPEAT_FIRST (eresolve_tac [asm_rl, Pair_UnE, sym RS trans]
ORELSE' eresolve_tac [Pair_mem_PiE,disjoint] THEN' atac));
val fun_disjoint_Un = result();
We ask because we are working on a paper on interleaving strategies for
solving exercises (with the goal to follow and comment upon student
interactions), and Isabelle seems to be the only prover that has offered
interleave.
These are just a few lines of rather obvious SML text. When I encountered
it as a young student in 1993 it did not surprise me.
We can imagine that efficiency might be a reason to exclude it: the
number of possibilities increases (more than) exponentially in the
length of the arguments when interleaving is used.
Larry might remember what he did in 1992/1993. We do not have any formal
history, because we started using CVS 1.0 only in summer 1993.
Often such generic strategies have been superseded by specific proof
automation, such as the Classical Reasoner above.
Since tacticals are closely related to parser combinators, you might also
look there in the literature what people did to improve worst-case
complexities.
Makarius
Last updated: Apr 26 2024 at 20:16 UTC