Email Gateway (Aug 17 2022 at 14:14): Email Gateway (Aug 17 2022 at 14:14):From: jdavis27@uiuc.edu
Hello,
I am having difficulty proving the following:
lemma "(1::real) * (1::real) = (1::real)";
lemma "(1::real) / (1::real) = (1::real)";
The "arith" tactic does not support multiplication, as
explained in previous messages. What is the recommended
approach to reasoning about multiplication of reals? I've
just begun to incorporate the theory of real numbers into my
work, so explicit proof steps would be especially helpful.
Thank you,
Justin S. Davis
Formal Methods Group @ UIUC
Email Gateway (Aug 17 2022 at 14:14):From: Lawrence Paulson <lp15@cam.ac.uk>
Use "auto" or "simp" to perform constant folding.
We aren't especially geared up for real literals, but you can perform
simple arithmetic on fixed-point constants as shown in this example:
lemma "3/10 + 70/100 = (x::real)"
apply (simp add: Ring_and_Field.add_frac_eq)
This simplifies to "x=1".
Larry Paulson
Last updated: May 03 2024 at 04:19 UTC