Re: [isabelle] Isabelle, Diophantine equations



Jan,

On Friday 22 June 2007 09:35, Jan Pax wrote:
>   could someone please tell me how to handle Diophantine equations in
> Isabelle and give me some simple example?
>   For example how to try to prove or disprove
>
>      all x, exits y, x^4=y^2
>
>      exists x, exists y, x^4 = 1 + x + y^2
>
>      exists x, exists y, x^2 (1 + y) = 1 + x + y^2

it seems that you haven't received a public reply yet, so I'll try to make 
some potentially useful remarks.

- I don't think there's a decision procedure available at the moment which
  specifically targets Diophantine equations.  "arith" should be able to deal
  with linear ones though: e.g.

    lemma "EX (x::int) y. 5*x + 3*y = 1"
      by arith

- Addition and power function are generic in Isabelle, available not only for
  integers, but also for other types.  Since you consider Diophantine
  equations, you'll probably want to use "int" type annotations: e.g.

    lemma "ALL (x::int). EX y. x^4 = y^2"

  Otherwise use "Isabelle > Settings > Show Types" (and possibly "Isabelle >
  Settings > Show Sorts") to show the types inferred by the system.

  Here's a proof of the above lemma:

      apply (rule allI)
      apply (rule_tac x="x^2" in exI)
      apply (simp add: power_mult [symmetric])
    done

- You can use the "ProofGeneral > Find Theorems" feature to search for
  existing lemmas.  E.g. search for theorems containing

    "(_ ^ _) ^ _"

  to find the "power_mult" theorem (among others) that was used in the above
  proof.

- "quickcheck" will try to disprove your current goal by instantiating free
  variables with random values.  This means you can also use it to find
  witnesses for existential statements, by negating the statement: e.g.

    lemma "~ (x::int)^4 = 1 + x + y^2"
      quickcheck

  might print

    Counterexample found:
    x = -1::int
    y = -1::int

  which would suggest the following proof of your second equation:

    lemma "EX (x::int) y. x^4 = 1 + x + y^2"
      apply (rule_tac x="-1" in exI)
      apply (rule_tac x="-1" in exI)
      apply simp
    done

  Likewise for your third equation,

    lemma "~ x^2 * (1 + y) = 1 + x + y^2"
      quickcheck

  might print

    Counterexample found:
    x = -2::int
    y = -1::int


Best,
Tjark





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