Jan van Brügge (Jan 04 2024 at 19:41): Jan van Brügge (Jan 04 2024 at 19:41):Did anyone have a similar issue: I am working on a tactic in ML (that currently fails at some point), but instead of showing me an error that the tactic failed, the tactic is run again in an endless loop. I never had this before and I don't know how I disable this. I need to SIGKILL isabelle because it exhausts my resources printing in an endless loop
Jan van Brügge (Jan 04 2024 at 19:44):(I've set Multithreading.parallel_proofs := 0 so there is no concurrency going on)
Manuel Eberl (Jan 04 2024 at 19:58):Hard to say without seeing the code. Perhaps there is some non-determinism going on before your tactic?
Jan van Brügge (Jan 04 2024 at 20:00):Nope the tactic has barely started, the lists are each only two elements big
val thm = Goal.prove_sorry lthy (names (fs @ gs @ ts)) (f_prems @ g_prems) goal (fn {context=ctxt, prems=f_prems} => EVERY1 [
rtac ctxt (Drule.rotate_prems nvars (
infer_instantiate' ctxt (replicate (nvars + m) NONE @ map (SOME o Thm.cterm_of ctxt) ts) (
#fresh_co_induct (#inner (hd (#quotient_fps fp_res)))
)
)),
EVERY' (@{map 3} (fn quot => fn mrbnf => fn vvsubst_cctor => EVERY' [
K (print_tac ctxt "foo"),
K no_tac
]) (#quotient_fps fp_res) mrbnfs vvsubst_cctors)
]);
if I comment out the EVERY' part it does stop
Jan van Brügge (Jan 04 2024 at 20:02):but even if the lists were longer K no_tac should abort the whole proof right there
Jan van Brügge (Jan 05 2024 at 10:50):it gets even weirder. I noticed that the begin of the proof is the same as one earlier (aside from whitespace), so I tried copying it and for some reason the EVERY' part is fine now?
val thm = Goal.prove_sorry lthy (names (fs @ gs @ ts)) (f_prems @ g_prems) goal (fn {context=ctxt, prems=f_prems} => EVERY1 [
rtac ctxt (Drule.rotate_prems nvars (infer_instantiate' ctxt (
replicate (nvars + m) NONE @ map (SOME o Thm.cterm_of ctxt) ts
) (#fresh_co_induct (#inner (hd (#quotient_fps fp_res)))))),
EVERY' (@{map 3} (fn quot => fn mrbnf => fn vvsubst_cctor => EVERY' [
REPEAT_DETERM o rtac ctxt impI,
rtac ctxt trans,
rtac ctxt vvsubst_cctor, (* this causes the endless loop *)
K (print_tac ctxt "foo")
]) (#quotient_fps fp_res) mrbnfs vvsubst_cctors)}
]);
However trying to apply a theorem I proved earlier now causes the loop for some reason. This makes no sense whatsoever
Dmitriy Traytel (Jan 05 2024 at 12:16):Maybe you are backtracking in the outer EVERY1? You could try adding a DETERM to the first rtac.
Here is an example that looks a bit like yours. It produces larger and larger unifiers, so eventually the unification bounds triggers termination:
schematic_goal
fixes P :: "'a list ⇒ (_ ⇒ _) ⇒ bool" and f :: "'a list ⇒ 'a list"
shows "P (?g (f xs)) ?g"
apply (tactic ‹EVERY1 [resolve_tac @{context} @{thms list.induct[where P="λxs. P (f (g xs)) g" for g]},
EVERY' [K (print_tac @{context} "foo"), K no_tac]]›)
Indeed that does seem to work. Very surprising behavior
Jan van Brügge (Jan 05 2024 at 12:29):I just added DETERM o in front of the induct theorem at the beginning
Dmitriy Traytel (Jan 05 2024 at 12:34):Welcome to backtracking :smile:
Dmitriy Traytel (Jan 05 2024 at 12:34):But this suggests that your application of the induction theorem allows for infinitely many unifiers?
Dmitriy Traytel (Jan 05 2024 at 12:34):Maybe you want to instantiate more things (either in the theorem or in the goal) to avoid this.
Jan van Brügge (Jan 05 2024 at 12:38):I don't see what the multiple unifiers would be. The proof state looks like this:
((∀a. a ∈ FFVars_T11 x ⟶ f1 a = g1 a) ⟶
(∀a. a ∈ FFVars_T12 x ⟶ f2 a = g2 a) ⟶
(∀a. a ∈ set3_T1 x ⟶ f3 a = g3 a) ⟶
(∀a. a ∈ set4_T1 x ⟶ f4 a = g4 a) ⟶ vvsubst_T1 f1 f2 f3 f4 x = vvsubst_T1 g1 g2 g3 g4 x)
∧ ((∀a. a ∈ FFVars_T21 y ⟶ f1 a = g1 a) ⟶
(∀a. a ∈ FFVars_T22 y ⟶ f2 a = g2 a) ⟶
(∀a. a ∈ set3_T2 y ⟶ f3 a = g3 a) ⟶
(∀a. a ∈ set4_T2 y ⟶ f4 a = g4 a) ⟶ vvsubst_T2 f1 f2 f3 f4 y = vvsubst_T2 g1 g2 g3 g4 y)
and the induction theorem has ?P ?x ∧ ?Q ?y in its conclusion. I fix ?x and ?y.
Dmitriy Traytel (Jan 05 2024 at 12:39):Probably it would be also easy for you to fix ?P and ?Q?
Jan van Brügge (Jan 05 2024 at 12:40):sure, but just for my understanding, why does this cause backtracking here?
Kevin Kappelmann (Jan 05 2024 at 14:47):If x and y are not bound variables, there is no unique mgu.
For example, consider ?f 0 =?= 0 + 1. Both ?f := \_ -> 0 + 1 and ?f := \x -> x + 1 are solutions but neither is more general than the other.
Jan van Brügge (Jan 05 2024 at 14:49):Ah thanks, that makes sense.
Dmitriy Traytel (Jan 05 2024 at 15:38):Nice explanation, Kevin. So it is not non-termination, but just very slow termination (going through 2^12 possible unifiers):
consts FFVars_T11 :: 'a
consts FFVars_T12 :: 'a
consts set3_T1 :: 'a
consts set4_T1 :: 'a
consts vvsubst_T1 :: 'a
consts FFVars_T21 :: 'a
consts FFVars_T22 :: 'a
consts set3_T2 :: 'a
consts set4_T2 :: 'a
consts vvsubst_T2 :: 'a
lemma ind: "foo P x ⟹ bar Q y ⟹ P x ∧ Q y"
sorry
lemma "((∀a. a ∈ FFVars_T11 x ⟶ f1 a = g1 a) ⟶
(∀a. a ∈ FFVars_T12 x ⟶ f2 a = g2 a) ⟶
(∀a. a ∈ set3_T1 x ⟶ f3 a = g3 a) ⟶
(∀a. a ∈ set4_T1 x ⟶ f4 a = g4 a) ⟶ vvsubst_T1 f1 f2 f3 f4 x = vvsubst_T1 g1 g2 g3 g4 x) ∧
((∀a. a ∈ FFVars_T21 y ⟶ f1 a = g1 a) ⟶
(∀a. a ∈ FFVars_T22 y ⟶ f2 a = g2 a) ⟶
(∀a. a ∈ set3_T2 y ⟶ f3 a = g3 a) ⟶
(∀a. a ∈ set4_T2 y ⟶ f4 a = g4 a) ⟶ vvsubst_T2 f1 f2 f3 f4 y = vvsubst_T2 g1 g2 g3 g4 y)"
apply (tactic ‹
let
val i = Unsynchronized.ref 0;
in
TRY (resolve_tac @{context} @{thms ind[where x = x and y = y]} 1 THEN
(fn x => (i := !i + 1; no_tac x))) THEN
(fn x => (@{print} i; all_tac x))
end›)
Backtracking strikes again. :big_smile:
Did I win something?
Last updated: May 04 2024 at 16:18 UTC