I’m afraid that the machinery for working with rationals is in a somewhat
broken state at the moment. The rat_equiv constant is not something that users
should ever need to see as it is used in the construction of the rationals but
isn’t needed subsequently.
I have working on this as a priority and it is a Github issue. Chun Tian’s
demonstration that even 1/10 + 1/100 isn’t handed by RAT_ADD_CONV is very
interesting too.
Thanks all,
Michael
From: Heiko Becker <hbec...@mpi-sws.org>
Date: Monday, 14 January 2019 at 00:05
To: Xero Essential <xqyww...@gmail.com>, hol-info
<hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] How to prove basic equivalency of rational?
Hello,
I am not an expert on ratTheory itself but I briefly looked at your goal. To me
it feels like `1/10:rat = 10/100` is the wrong goal to prove.
Looking at the documentation of ratTheory some theorems use `rat_equiv`
instead. If I restate your goal as
`rat_equiv (abs_frac (1,10)) (abs_frac (10,100))`
it can be proven by
fs[rat_equiv_def, NMR, DNM]
My guess is that your goal is not provable because `1/10` and `10/100`
represent different rational "objects" though they are equivalent (as captured
by `rat_equiv`).
But I am not sure about this. Maybe someone more experienced can comment on
this.
Best regards,
Heiko
On 1/14/19 6:24 AM, Xero Essential wrote:
Hi, every expert.
Maybe I'm a little new to the HOL4 libraries.
But, how could I prove the basic equivalency of rational like `1q / 10 = 10
/ 100`?
The documentation is little and I have searched all the source, but related
conversions and tactics like `RAT_EQ_TAC` are all failed and throw an empty
error.
I looked the source about `RAT_EQ_TAC`, which something about `abs_rat`,
and then I become confused.
Sorry for my bothering, and hope the suggestion.
Thanks.
Qiyuan Xu.
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
