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