Hi, is the improved version you’re using available somewhere?
—Chun > Il giorno 05 ago 2018, alle ore 18:09, Waqar Ahmad <12phdwah...@seecs.edu.pk> > ha scritto: > > Hi Chun, > > I'm not sure about your potential conflict question but we are now using an > improved definition of "extreal_add_def" > > val extreal_add_def = Define` > (extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\ > (extreal_add (Normal _) a = a) /\ > (extreal_add b (Normal _) = b) /\ > (extreal_add NegInf NegInf = NegInf) /\ > (extreal_add PosInf PosInf = PosInf)`; > > This will rule out the possibility of PosInf + a= PosInf... We do have a plan > to update the probability theory to the latest version in the near future > (Speaking on the behalf of original authors). > > > > On Sun, Aug 5, 2018 at 11:14 AM Chun Tian <binghe.l...@gmail.com > <mailto:binghe.l...@gmail.com>> wrote: > 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 > <http://sdm.link/slashdot>_______________________________________________ > 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> > > > -- > Waqar Ahmad, Ph.D. > Post Doc at Hardware Verification Group (HVG) > Department of Electrical and Computer Engineering > Concordia University, QC, Canada > Web: http://save.seecs.nust.edu.pk/waqar-ahmad/ > <http://save.seecs.nust.edu.pk/waqar-ahmad/> >
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
