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
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
