Email Gateway (Mar 22 2023 at 22:51): Email Gateway (Mar 22 2023 at 22:51):From: christian@madez.de
In some cases, the proof method algebra fails even though it should work.
The bug can be reproduced in one case with the following theory:
theory Scratch
imports Main
begin
lemma "(- x + 3) * (x + 1) + (x - 1) ^ 2 - 3 = (1::int)"
by algebra
lemma "(- x + 3) * (x + 1) + (x - 1) ^ 2 - 2 = (2::int)"
by algebra
end
I verified the bug occurs on Isabelle2021-1, Isabelle2022 and on the changeset 77699:d5060a919b3f from Mon Mar 20 18:33:56 2023 +0100.
CTRL + left click on the proof method algebra in Isabelle opens the file src/HOL/Groebner_Basis.thy. This points to algebra_tac in Tools/groebner.ML. There we find the definition
fun algebra_tac add_ths del_ths ctxt i =
ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i
We can find the definition of ring_tac in the same file as:
Email Gateway (Mar 22 2023 at 22:55):From: christian@madez.de
I'm sorry I sent the last message truncated. Here is the rest of the message:
fun ring_tac add_ths del_ths ctxt =
Object_Logic.full_atomize_tac ctxt
THEN' presimplify ctxt add_ths del_ths
THEN' CSUBGOAL (fn (p, i) =>
resolve_tac ctxt [let val form = Object_Logic.dest_judgment ctxt p
in case get_ring_ideal_convs ctxt form of
NONE => Thm.reflexive form
| SOME thy => #ring_conv thy ctxt form
end] i
handle TERM _ => no_tac
| CTERM _ => no_tac
| THM _ => no_tac);
I do not see how debug this system like I could with printing state in imperative languages, so I'm lost at this point.
Best,
Christian Weinz
Last updated: Apr 27 2024 at 20:14 UTC