Hi Michael, thanks for the explanation in details! Now I finally understand why the two versions of `sup` can be proved equivalent, while the two "inf" cannot. Any way, I'll follow your idea and submit a fix of the duplicated definitions of `inf` soon.
--Chun
Il 23/02/19 07:00, michael.norr...@data61.csiro.au ha scritto:
> 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
>
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
