You can use:

a(conv_tac(ONCE_MAP_C z_float_conv));

to change things like "3.0" into "real 3" or "3.5" into "7/2" and then rewriting in the proof context 'z_reals will do the arithmetic for you.

We don't do this automatically in the proof context 'z_reals in case you have floating literals like 1.2e3333333 which would take ages to expand. Perhaps we should have another proof context 'z_floats for use at the user's discretion to do the expansion as part of rewriting.



On 26 Mar 2009, at 18:18, Artur Oliveira Gomes wrote:


Thank you.
Just one more question: and how about floating numbers?
How to prove it?

For example:

set_merge_pcs["'z_reals", "z_library"];
set_goal([], %SZT% 0.4 %mem% 0.1 ..%down%R 1.9 %>%);


With those steps, ProofPower change the goal to:

%SZT%0.1 %leq%%down%R 0.4 %and% 0.4 %leq%%down%R 1.9%>%

How can I prove it?

Thanks again.


Artur Oliveira Gomes
Proofpower mailing list

Proofpower mailing list

Reply via email to