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:

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: Mar 04 2024 at 10:08 UTC