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



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.