Email Gateway (Aug 18 2022 at 10:35): Email Gateway (Aug 18 2022 at 10:35):From: Jan Pax <pax0@seznam.cz>
Hi,
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
Thank you, Jan Pax
Email Gateway (Aug 18 2022 at 10:36):From: Tjark Weber <tjark.weber@gmx.de>
Jan,
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. 5x + 3y = 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
Last updated: May 03 2024 at 04:19 UTC