It’s possible that both definitions will turn into applications of Hilbert
choice applied to equivalent predicates.
If inf1 s = @x. P x, and inf2 s = @x. Q x, but it happens that !x. P x <=> Q x,
then it is indeed the case that inf1 = inf2, even on arguments where you’d
prefer them not to be defined. Equally though, it’s quite reasonable to
imagine that they weren’t defined so conveniently, and you will just have
s has-a-lower-bound ==> (inf1 s = inf2 s)
In this situation, I might prove the above, and then replace all the
occurrences of one with the other under the expectation that the theorems about
the one that is replaced are just as true of the other.
Michael
From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
Date: Thursday, 21 February 2019 at 20:52
To: hol-info <hol-info@lists.sourceforge.net>
Subject: [Hol-info] The equivalence of two definitions of "inf" (infimum) of
real sets?
Hi,
(this is another (strange) question about undefined values in total functions)
currently there’re two definitions of “inf” (infimum) for real sets in HOL4,
one is at “src/real/realScript.sml”:
[inf_def] Definition
⊢ ∀p. inf p = -sup (λr. p (-r))
The other is at “src/probability/iterateScript.sml”, ported from HOL Light:
[inf] Definition
⊢ ∀s.
inf s =
@a. (∀x. x ∈ s ⇒ a ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ a
I believe they’re both correct definitions, as the related theorems derived
from them all make senses. However, if I load “iterateTheory”, or
“real_topologyTheory” which in turn uses “iterateTheory”, than all theorems
about the “inf” defined at “realTheory” would be invalid, as they’re not for
the latest “inf”. Thus my goal is to merge the two definitions of “inf” and
have a precise union of all theorems about them.
Usually this kind of definition merging is done by changing the later
definition (in iterateTheory) into an equivalent theorem, i.e. to prove that
|- ∀s. inf s = @a. (∀x. x ∈ s ⇒ a ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ a
given the definition: inf p = -sup (λr. p (-r))
But I *feel* this is impossible, because “inf” of real set is not defined on
all real sets. If I temporarily use ``inf’`` as the alternative definition of
“inf” in iterateTheory, the above equivalent theorem becomes:
|- ∀s. inf s = inf’ s
but for s = {}, or any real sets without a lower bound, either “inf s” or “inf’
s” is not defined, should above theorem still be proved? If not, then I have
to re-prove all “inf” theorems in iterateTheory using lemmas from realTheory.
This is more difficult.
Regards,
Chun Tian
P. S. in extrealTheory, “sup” and “inf” are really total functions, thus much
easier to work with, e.g. I can prove things like: (in at least one of my Math
book, it said “inf {} = PosInf” must be specially defined, but this is actually
not needed)
[sup_empty] Theorem
⊢ sup ∅ = NegInf
[inf_empty] Theorem
⊢ inf ∅ = PosInf
[inf_univ] Theorem
⊢ inf 𝕌(:extreal) = NegInf
[sup_univ] Theorem
⊢ sup 𝕌(:extreal) = PosInf
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
