Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Application of method algebra fails


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

view this post on Zulip 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: Mar 04 2024 at 10:08 UTC