I found a way to prove the goal `abs_rat (abs_frac (1,10)) = abs_rat
(abs_frac (10,100))` and probably a bug about `RAT_EQ_CONV`.
In `ratLib.sml` :
```
val RAT_EQ_CONV:conv = fn term1 =>
let
val eqn = dest_neg term1;
val (lhs,rhs) = dest_eq eqn;
val (lhc, f1) = dest_comb lhs;
val (rhc, f2) = dest_comb rhs;
in
UNDISCH_ALL (SPECL[f1,f2] RAT_EQ)
end
handle HOL_ERR _ => raise ERR "RAT_EQ_CONV" "";
```
The `dest_neg` in 3rd line is weird, who fails when the term isn't
a negation. Maybe the line tries to handle the case of negation and
`dest_neg` was more tolerant in some old version?
Anyway, after removing the line, both `RAT_EQ_CONV` and `RAT_EQ_TAC` work.
And the goal could be proved as:
```
g `abs_rat (abs_frac (1,10)) = abs_rat (abs_frac (10,100))`;
e (FIXED_RAT_EQ_TAC);
e (rw[DNM, NMR]);
```
And then I found another way to prove the simpler form `1q/10 = 10/100`
using `RAT_CALCEQ_TAC`.
But it's also broken in somewhere so I replaced the broken step.
The original definition of `RAT_CALCEQ_TAC` in `ratLib.sml` :
```
val RAT_CALCEQ_TAC =
RAT_CALC_TAC THEN
FRAC_CALC_TAC THEN
REWRITE_TAC[RAT_EQ] THEN
FRAC_NMRDNM_TAC THEN (* Fail, and I don't know why. *)
INT_RING_TAC;
```
And my replacement:
```
val MY_RAT_CALCEQ_TAC =
RAT_CALC_TAC THEN
FRAC_CALC_TAC THEN
REWRITE_TAC[RAT_EQ] THEN
rw[NMR, DNM] THEN (* The replacement does the same thing according
to the comment of origin. *)
INT_RING_TAC;
g `1q/10 = 10/100`;
e (MY_RAT_CALCEQ_TAC);
(* goal : 100 * SGN 10 = 100 * SGN 100 *)
e (rw[SGN_def]);
(* proved. *)
```
Xero Essential <[email protected]> 于2019年1月14日周一 下午1:24写道：
> 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
