Email Gateway (Aug 22 2022 at 17:52): Email Gateway (Aug 22 2022 at 17:52):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Dear Isabelle-users and experts,
One of the main obstacles in the formal verification of my own on work on
theta functions is Eckert's theorem claiming that the primitive Pythagorean
triangles (including a degenerate case as neutral element) behave like an
abelian group for certain binary operation that he defined.
Reference: ECKERT, Ernest J. The group of primitive Pythagorean triangles.
Mathematics Magazine, 1984, vol. 57, no 1, p. 22-27.
In order to check the associativity of this binary operation, I divided
the problem into several cases corresponding to inequalities, but I didn't
succeed in automatically solving some of these systems of inequalities with
sledgehammer [timeout = 1000]. Also I tried to find a counter-example with
nitpick [timeout = 1000], but it didn't work.
At this point, I'm not sure whether this theorem is true or false. I share
this incomplete my proof with your. Thank you in advance for any
suggestion. In particular, I do not know which solver is best for
inequalities.
Sincerely yours,
Jose M.
theory SumPythIsAssocLemProof
imports Complex_Main
begin
definition preSumPythTwoReal :: "(real * real) ⇒ (real * real) ⇒ (real *
real)" where
"preSumPythTwoReal ≡ λ (a, b) (A, B). (if aA > bB
then (aA - bB, bA + aB)
else (bA + aB, bB - aA) )"
lemma SumPythIsAssocLemTwoReal :
fixes a b u v x y :: real
assumes "a ≥ 0" and "b ≥ 0" and "u ≥ 0" and "v ≥ 0" and "x ≥ 0" and "y ≥
0"
shows "preSumPythTwoReal (a, b) ( preSumPythTwoReal (u, v) (x, y) ) =
preSumPythTwoReal ( preSumPythTwoReal (a, b) (u, v) ) (x, y)"
unfolding preSumPythTwoReal_def
apply (auto split!: if_splits)
apply (simp add: distrib_left distrib_right left_diff_distrib'
right_diff_distrib')
apply (simp add: distrib_left distrib_right left_diff_distrib'
right_diff_distrib')
apply (simp add: distrib_left distrib_right left_diff_distrib'
right_diff_distrib')
apply (simp add: distrib_left distrib_right left_diff_distrib'
right_diff_distrib')
apply (simp add: distrib_left distrib_right left_diff_distrib'
right_diff_distrib')
apply (auto simp: algebra_simps)
using assms(1) assms(2) assms(3) assms(4) assms(5) assms(6)
apply (smt mult_left_less_imp_less mult_nonneg_nonneg)
using assms(1) assms(2) assms(3) assms(4) assms(5) assms(6)
apply (smt mult_left_less_imp_less mult_nonneg_nonneg)
using assms(1) assms(2) assms(3) assms(4) assms(5) assms(6)
apply (smt mult_left_less_imp_less mult_nonneg_nonneg)
using assms(1) assms(2) assms(3) assms(4) assms(5) assms(6)
apply (smt mult_left_less_imp_less mult_nonneg_nonneg)
oops
end
Email Gateway (Aug 22 2022 at 17:52):From: Manuel Eberl <eberlm@in.tum.de>
The problem falls into the QF_NRA fragment of SMT and Z3 and CVC4 claim
they can prove it. CVC4 even produces a proof object for it, but it is
significantly bigger than my patience (I aborted printing it after a few
minutes).
In any case, to my knowledge, Isabelle's smt cannot import proof objects
in non-linear real arithmetic. I don't think we have any decision
procedures for non-linear real arithmetic in Isabelle apart from the SOS
method, but it doesn't seem to be able to solve this particular problem
in a reasonable amount of time either, so I am not quite sure what can
be done other than finding a ‘pen-and-paper’ proof.
Manuel
Email Gateway (Aug 22 2022 at 17:53):From: Laurent Thery <Laurent.Thery@inria.fr>
Hi,
I got puzzled by your problem and try to prove it with Coq.
Hope I will give you enough information so you can replicate it in Isabelle
Your definition has an if splitting everything you get 32 goals.
Coq has the same sos technique for non linear, I use it to
to solve all the subgoals except 4 cases that are degenerated cases.
For two of them you just need to prove the intermediate fact
a * a + b * b <= 0, which leads to a=0 and b = 0
For the other two you have
x * x + y * y <= 0, which leads to x=0 and y = 0
Last updated: Nov 21 2024 at 12:39 UTC