Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Bug in the algebra method for ideal membership

Email Gateway (Aug 22 2022 at 21:13):

From: Rodrigo Raya <rodrigo.raya@epfl.ch>
Dear all,

Below I show an example which should go through using the algebra tactic:

lemma ideal_membership_2:
  fixes x0 x1 y0 y1 t :: "'b::idom"
  assumes "x0 ≠ 0" "y0 ≠ 0" "x1 ≠ 0" "y1 ≠ 0"
  shows "∃ q1 q2 q3 q4.
          y0^2 - x1^2 =
              q1*(-1 + x0^2 + y0^2 - t^2 * x0^2 * y0^2) +
              q2*(-1 + x1^2 + y1^2 - t^2 * x1^2 * y1^2) +
              q3*(x0 * y0 - x1 * y1) +
              q4*(x1 * y0 + x0 * y1)
        "       using assms apply algebra

but in fact fails with the exception:

exception Option raised (line 82 of "General/basics.ML")

It looks like there may be a bug in the ideal_tac tactic of groebner.ML.

I have tried to figure out myself what may be the problem but have not
succeeded so far.

I would thank any advice or insight you can give me to debug this problem.

Best,

Rodrigo Raya

Email Gateway (Aug 23 2022 at 09:07):

From: Makarius <makarius@sketis.net>
On 10/01/2020 15:52, Rodrigo Raya wrote:

Below I show an example which should go through using the algebra tactic:

lemma ideal_membership_2:
  fixes x0 x1 y0 y1 t :: "'b::idom"
  assumes "x0 ≠ 0" "y0 ≠ 0" "x1 ≠ 0" "y1 ≠ 0"
  shows "∃ q1 q2 q3 q4.
          y0^2 - x1^2 =
              q1*(-1 + x0^2 + y0^2 - t^2 * x0^2 * y0^2) +
              q2*(-1 + x1^2 + y1^2 - t^2 * x1^2 * y1^2) +
              q3*(x0 * y0 - x1 * y1) +
              q4*(x1 * y0 + x0 * y1)
        "       using assms apply algebra

but in fact fails with the exception:

exception Option raised (line 82 of "General/basics.ML")

For now, I have made a tracker item here: https://isabelle-dev.sketis.net/T21

It looks like there may be a bug in the ideal_tac tactic of groebner.ML.

I have tried to figure out myself what may be the problem but have not
succeeded so far.

I would thank any advice or insight you can give me to debug this problem.

Debugging works by building relevant parts of Isabelle with the ML debugger
enabled, and then run the test with suitable options.

Here is my test file for "isabelle jedit -l Pure":

theory Scratch
imports "HOL.Groebner_Basis"
begin

declare [[ML_exception_debugger]]

lemma ideal_membership_2:
fixes x0 x1 y0 y1 t :: "'b::idom"
assumes "x0 ≠ 0" "y0 ≠ 0" "x1 ≠ 0" "y1 ≠ 0"
shows "∃ q1 q2 q3 q4.
y0^2 - x1^2 =
q1*(-1 + x0^2 + y0^2 - t^2 * x0^2 * y0^2) +
q2*(-1 + x1^2 + y1^2 - t^2 * x1^2 * y1^2) +
q3*(x0 * y0 - x1 * y1) +
q4*(x1 * y0 + x0 * y1)
"
using assms apply algebra

end

This will load all required theories of Isabelle/HOL into the Pure session.
You can then use C-hover-click on "algebra" to get to its definition.

Over there you will see its use of Groebner.algebra_tac and you can change the
preceeding ML command for that module like this:

ML_file_debug ‹Tools/groebner.ML›

Back to Scratch.thy you will now get a more informative exception trace.

The crash is due to "try" and "|> the" here:
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/HOL/Tools/groebner.ML#l875

If you insert a dummy invocation of (isolate_variables evs ps) without try, it
will crash in a more informative way.

From there you can continue digging into this implementation by Amine Chaieb.

Makarius

Email Gateway (Aug 23 2022 at 09:07):

From: Laurent Thery <Laurent.Thery@inria.fr>
Hi,

I am not an Isabelle expert but did you try if this

lemma ideal_membership_2:
fixes x0 x1 y0 y1 t z0 :: "'b::idom"
shows "∃ q0 q1 q2 q3 q4.
y0^2 - x1^2 =
q0*(1 + x0 * y0 * x1 * y1 * z0) +
q1*(-1 + x0^2 + y0^2 - t^2 * x0^2 * y0^2) +
q2*(-1 + x1^2 + y1^2 - t^2 * x1^2 * y1^2) +
q3*(x0 * y0 - x1 * y1) +
q4*(x1 * y0 + x0 * y1)
"

succeeds. If it succeeds this means that there is a problem with
how degenerated cases (_ ≠ 0) are handled.

Last updated: Apr 20 2024 at 12:26 UTC