Email Gateway (Aug 22 2022 at 17:29): Email Gateway (Aug 22 2022 at 17:29):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Dear Eisbach/Isabelle/ML experts,
In his paper
Eckert, Ernest J. "The group of primitive Pythagorean triangles." *Mathematics
Magazine* 57.1 (1984): 22-27.
Eckert defined the function
fun preSumPythTwo :: "(nat * nat) ⇒ (nat * nat) ⇒ (nat * nat)" where
"preSumPythTwo (a, b) (A, B) = (if aA > bB
then (aA - bB, bA + aB)
else (bA + aB, bB - aA) )"
and claimed that it is associative, i.e.,
lemma SumPythIsAssocLemTwo :
fixes a b u v x y :: nat
shows "preSumPythTwo (a, b) ( preSumPythTwo (u, v) (x, y) ) =
preSumPythTwo ( preSumPythTwo (a, b) (u, v) ) (x, y)"
In order to verify his claim, I divided the problem into 16 lemmas with
relatively easy proofs, corresponding to all the possible cases, e.g.,
lemma SumPythIsAssocLemTwoId0000:
fixes a b u v x y :: nat
assumes "au > bv"
and "( fst ( preSumPythTwo (a, b) (u, v) ) ) * x > ( snd (
preSumPythTwo (a, b) (u, v) ) ) * y"
and "ux > vy"
and "a * (fst ( preSumPythTwo (u, v) (x, y) )) > b * (snd ( preSumPythTwo
(u, v) (x, y) ))"
shows "preSumPythTwo (a, b) ( preSumPythTwo (u, v) (x, y) ) =
preSumPythTwo ( preSumPythTwo (a, b) (u, v) ) (x, y)"
I wonder if there is a tactic in Isabelle HOL in order to automatically
generate all the 16 lemmas corresponding to all the possible cases just
from the definition of the function. I ask this question because I want to
generalize Eckert's result from dimension 2 (complex numbers) to dimension
8 (octonions) and this goal can not be done without a good automation.
Sincerely yours,
José M.
Email Gateway (Aug 22 2022 at 17:30):From: Peter Lammich <lammich@in.tum.de>
Hi,
Could you simply split on the ifs in your definition of presum? Isabelles
simplifier will do this with split: if_splits, or, to get more control, you
might call the split method.
As first attempt, you might try to make presum a definition, ie do the pattern
matching in the pairs in the rhs, then unfold presum_def, and then auto split:
if_splits prod.splits
Hope that helps
Peter
Email Gateway (Aug 22 2022 at 17:30):From: Peter Lammich <lammich@in.tum.de>
Hi José,
here is an Eisbach version to generate 16 cases. I changed the
definition of preSumPythTwo to manual case splitting isntead of pattern
matching,
in order to split all products in a first step ... may be this can be
modified to the original definition.
Email Gateway (Aug 22 2022 at 17:30):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Hi Peter
Thanks for your help, it was my first time with Eisbach. I feel that it is
really practical for mathematicians.
José M.
Last updated: Apr 19 2024 at 08:19 UTC