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> 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
