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
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
