Artur,

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.


Regards,

Rob.


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

Rob,

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 %>%);

a(rewrite_tac[z_%bbR%_dot_dot_def]);

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.

Regards,


--
Artur Oliveira Gomes
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com


_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to