Re: [ProofPower] Real Numbers - Proofs
Hi there Now I know how to prove it: using z_R_=_conv. Thanks anyway, Artur 2009/3/25 Artur Oliveira Gomes artur.o.go...@gmail.com Hi there, How could I prove that given two real numbers, 20 and 30, that 20 =40? Moreover, given three real numbers, 20, 30 and 40, how could I prove that 30 in 20..40. Regards, -- Artur Oliveira Gomes -- Artur Oliveira Gomes ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Real Numbers - Proofs
Artur, You may like to know that there is a so-called component proof context called 'z_reals which will make evaluation of real arithmetic expressions happen automatically when you rewrite. Try: set_merge_pcs['z_reals, z_library]; set_goal([], %SZT% real 30 %mem% real 20 ..%down%R real 40 %%); a(rewrite_tac[z_%bbR%_dot_dot_def]); Regards, Rob. Artur Oliveira Gomes wrote: Hi there Now I know how to prove it: using z_R_=_conv. Thanks anyway, Artur 2009/3/25 Artur Oliveira Gomes artur.o.go...@gmail.com mailto:artur.o.go...@gmail.com Hi there, How could I prove that given two real numbers, 20 and 30, that 20 =40? Moreover, given three real numbers, 20, 30 and 40, how could I prove that 30 in 20..40. Regards, -- Artur Oliveira Gomes -- 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
Re: [ProofPower] Real Numbers - Proofs
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
