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> 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
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> 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/
------------------------------------------------------------------------------
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
