Hi Thomas, thanks for detailed explanations!
—Chun > Il giorno 05 ago 2018, alle ore 19:58, Thomas Tuerk <tho...@tuerk-brechen.de> > ha scritto: > > Hi Chun, Waqar, > > "Define" does indeed give priority to earlier clauses. Under the hood pattern > compilation takes place. So what is actually is going on for >> 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)`; > > Is similar to what would happen for > > val extreal_add_def = Define` > (extreal_add a b = case (a, b) of > (Normal x, Normal y) => (Normal (x + y)) > | (PosInf, _) => PosInf > | (_, PosInf) => PosInf > | (NegInf, _) => NegInf > | (_, NegInf) => NegInf > > In both cases, the pattern match (case-expression) is compiled to a decision > tree using various heuristics. This tree contains implicitly a complete list > of distinct patterns. > Distinct means that the patterns don't overlap. Complete means that they > cover every possible value. For case-expressions you get the decision tree > itself back. For top-level pattern matches you get a list of non-overlapping > patterns back that are used for the returned definition theorem. If you look > at the result of the original definition, you will see that the actual > definition theorem is > > |- !y x v5 v3 v2 a. > (extreal_add (Normal x) (Normal y) = Normal (x + y)) /\ > (extreal_add PosInf a = PosInf) /\ > (extreal_add NegInf PosInf = PosInf) /\ > (extreal_add (Normal v2) PosInf = PosInf) /\ > (extreal_add NegInf NegInf = NegInf) /\ > (extreal_add NegInf (Normal v5) = NegInf) /\ > (extreal_add (Normal v3) NegInf = NegInf) > > Here you see that the original clauses disappeared. Instead patterns from > resulting from this pattern compilation are used. Notice that similar to SML > and other functional languages, Define gives precedence to earlier clauses. > > Most case-expressions are simple and pattern compilation is not an issue. > However, for more complicated cases it can be hard to predict what the > results will be. If you are interested, I recommend having a look at section > 6.4 of the description manual. I personally try not to use non-trivial > definitions directly, but use the theorems produced by Define to prove > simple, manually stated sanity check lemmata. I believe this makes proofs > more robust and helps me detect problems with my definitions earlier. > > Best > > Thomas > > > On 05.08.2018 18:09, Waqar Ahmad via hol-info wrote: >> 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/> >> >> >> >> ------------------------------------------------------------------------------ >> 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> > > ------------------------------------------------------------------------------ > 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
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
