Some additional findings: 1. ``1/10 = 10/100 <=> T`` seems indeed possible, see theorem RAT_EQ_ALT and the following tests:
REWRITE_RULE [rat_nmr_def, rat_dnm_def]
(SPECL [``1/10``, ``10/100``] RAT_EQ_ALT)
val it =
⊢ (0.1 = 0.10 ) ⇔
(frac_nmr (rep_rat 0.1 ) * frac_dnm (rep_rat 0.10 ) =
frac_nmr (rep_rat 0.10 ) * frac_dnm (rep_rat 0.1 )): thm
but I don’t know how to reduce the result to T…
2. RAT_ADD_CONV seems more powerful:
RAT_ADD_CONV ``1/10q + -10/100``;
val it = ⊢ 0.1 + -10 / 100 = 0: thm
In theory we can detect if the RHS is “0 :rat”, but I failed to implement a
working RAT_EQ_CONV by reducing ``r1 = r2`` to ``r1 + -r2``. (once 1/10 becomes
0.1 and 10/100 becomes 0.10, RAT_ADD_CONV doesn’t work any more, strange…)
—Chun
> Il giorno 14 gen 2019, alle ore 15:45, Heiko Becker <hbec...@mpi-sws.org> ha
> scritto:
>
> 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
>> <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
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
