no… by drawing pictures and think it more, this statement is still not true, if the set is general (of type ‘a -> bool).
please forget the whole question. I must have assumed something wrong in earlier places. thanks all the same. —Chun > Il giorno 18 set 2018, alle ore 10:25, Chun Tian (binghe) > <binghe.l...@gmail.com> ha scritto: > > Hi Ramana, > > thanks for your help. Sorry, I realized that the case “a = sp” can be > eliminated from other assumptions, thus I actually have another constraint “a > ≠ sp” in my original goals: > > ∃x. a ⊆ f x > ------------------------------------ > 4. f 0 = ∅ > 5. ∀i j. i ≤ j ⇒ f i ⊆ f j > 6. BIGUNION (IMAGE f 𝕌(:num)) = sp > 21. a ≠ sp > 23. ∀n. f n ⊆ sp > 24. a ⊆ sp > > in this case your opposite proof doesn’t work any more. Also, I replaced the > monotonicity of f into another form, I don’t know which one is easier to use. > The assumption "f 0 = ∅” should be optional, I guess. > > Now this should be a true statement, right? > > —Chun > >> Il giorno 18 set 2018, alle ore 01:26, Ramana Kumar <ram...@kumar.id.au >> <mailto:ram...@kumar.id.au>> ha scritto: >> >> I think this is false. Here's a proof of the opposite, with the type of f >> instantiated to a num set generator: >> >> val thm = Q.prove( >> `¬( >> ∀(f:num->num->bool) a sp. >> (f 0 = ∅) ∧ >> (∀n. f n ⊆ f (SUC n)) ∧ >> (∀n. f n ⊆ sp) ∧ >> (BIGUNION (IMAGE f 𝕌(:num)) = sp) ∧ >> (a ⊆ sp) ⇒ >> ∃x. a ⊆ f x)`, >> rw[] >> \\ qexists_tac`count` >> \\ qexists_tac`UNIV` >> \\ rw[SUBSET_DEF, PULL_EXISTS] >> >- metis_tac[] >> >- ( >> rw[Once EXTENSION] >> \\ qexists_tac`count (SUC x)` >> \\ rw[] ) >> >- ( >> rw[EXTENSION] >> \\ qexists_tac`SUC x` >> \\ rw[] )); >> >> >> On Tue, 18 Sep 2018 at 00:01, Chun Tian (binghe) <binghe.l...@gmail.com >> <mailto:binghe.l...@gmail.com>> wrote: >> sorry, I also have this necessary assumption: >> >> 5. BIGUNION (IMAGE f 𝕌(:num)) = sp >> >> > Il giorno 18 set 2018, alle ore 01:00, Chun Tian (binghe) >> > <binghe.l...@gmail.com <mailto:binghe.l...@gmail.com>> ha scritto: >> > >> > Hi, >> > >> > I ran into the following goal in the proof of a big theorem: >> > >> > ∃x. a ⊆ f x >> > ------------------------------------ >> > 3. f 0 = ∅ >> > 4. ∀n. f n ⊆ f (SUC n) >> > 20. ∀n. f n ⊆ sp >> > 21. a ⊆ sp >> > >> > I have an increasing sequence of sets (f n) from empty to the whole space >> > (sp), and I have a single set “a” (⊆ sp). It looks *obvious* that, I can >> > always choose a big enough index x such that (f x) will contain “a”. But >> > how can I make this argument formal? >> > >> > thanks, >> > >> > Chun >> > >> >> _______________________________________________ >> 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> >
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
