| Hi, the version of “extreal” (extended real numbers) in latest HOL4 has a wrong definition for sum: val _ = Hol_datatype`extreal = NegInf | PosInf | Normal of real`; val extreal_add_def = Define` (extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\ (extreal_add PosInf a = PosInf) /\ (extreal_add a PosInf = PosInf) /\ (extreal_add NegInf b = NegInf) /\ (extreal_add c NegInf = NegInf)`; according to this definition, one could prove the wrong statement ``PosInf + NegInf = NegInf + PosInf = PosInf``, e.g. PROVE [extreal_add_def] ``extreal_add PosInf NegInf = PosInf``;Meson search level: .. val it = ⊢ PosInf + NegInf = PosInf: thm P. S. the original authors have fixed this issue in their latest version of probability theories, which I’m now working on merging them into HOL4. What I don’t quite understand here is, shouldn’t one also prove that ``PosInf + NegInf = NegInf + PosInf = NegInf``, as the last two lines of extreal_add_def stated, but it turns out that this is not true (PROVE command doesn’t return): PROVE [extreal_add_def] ``extreal_add NegInf PosInf = NegInf``;Meson search level: .....................Exception- Interrupt raised of course it can’t be proved, because otherwise it means ``PosInf = NegInf``, contradicting the axioms generated by Hol_datatype, then the whole logic would be inconsistent. But given the fact that above definition can be directly accepted by Define command, does HOL internally resolve potential conflicts by putting a priority on each sub-clauses based on their appearance order? Regards, Chun Tian |
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
