Re: [Hol-info] Dealing with INFINITE num set ...

2019-02-16 Thread Chun Tian (binghe) 
Ah, thanks! sorry, I didn't see your replies before posting my last one.

Your proofs are much much shorter than mine, I'll use your versions instead!

--Chun

Il 16/02/19 22:48, Konrad Slind ha scritto:
> Rephrasing things might bring clarity:
> 
> load "pred_setLib";
> open pred_setTheory;
> 
> val set_ss = (arith_ss ++ pred_setLib.PRED_SET_ss);
> 
> val lem = Q.prove
> (`~(?N. INFINITE N /\ !n. N n ==> P n) <=> !N. N SUBSET P ==> FINITE N`,
>  rw_tac set_ss [EQ_IMP_THM,SUBSET_DEF,IN_DEF]
>   >- (`FINITE P \/ ?n. P n /\ ~P n` by metis_tac []
>        >> imp_res_tac SUBSET_FINITE
>        >> full_simp_tac std_ss [SUBSET_DEF, IN_DEF])
>   >- metis_tac[]);
> 
> From this and the original assumption, you should be able to get that P
> is finite, so has a maximum element.
> 
> Konrad.
> 
> 
> 
> On Fri, Feb 15, 2019 at 1:12 PM Chun Tian (binghe)
> mailto:binghe.l...@gmail.com>> wrote:
> 
> Hi,
> 
> I'm blocked at the following (strange) situation:
> 
> I have an infinite set of integers (num) in which each integer n
> satisfies a property P(n):
> 
> ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n
> 
> Suppose above proposition is NOT true, how can I derive that, there must
> exist a number m such that for all n >= m, P(n) does NOT hold? i.e.
> 
> ?m. !n. m <= n ==> ~(P n)
> 
> Thanks in advance,
> 
> Chun Tian
> 
> ___
> 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

Re: [Hol-info] Dealing with INFINITE num set ...

2019-02-16 Thread Chun Tian (binghe) 
Cancel above questions. They're finally proved by myself using
FINITE_WEAK_ENUMERATE, FINITE_BIJ_COUNT_EQ, etc. [1]

   [infinity_bound_lemma]  Theorem

  ⊢ ∀N m. INFINITE N ⇒ ∃n. m ≤ n ∧ n ∈ N

   [infinity_often_lemma]  Theorem

  ⊢ ∀P. ¬(∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n) ⇔ ∃m. ∀n. m ≤ n ⇒ ¬P n

(they are related to Borel-Cantelli Lemma in Probability Theory)

Still want to know if there're shorter, more elegant proofs ... and
thanks all the same.

--Chun

[1]
https://github.com/binghe/HOL/blob/Probability-11/src/probability/util_probScript.sml
(line 1595-1638)

Il 15/02/19 20:46, Chun Tian (binghe) ha scritto:
> And also this one:
> 
> Given `INFINITE N` and a fixed number `m`, how can I assert the
> existence of another number `n` such that,
> 
> m <= n /\ n IN N
> 
> i.e. prove that
> 
> ``!N m. INFINITE N ==> ?n. m <= n /\ n IN N``
> 
> --Chun
> 
> Il 15/02/19 20:11, Chun Tian (binghe) ha scritto:
>> Hi,
>>
>> I'm blocked at the following (strange) situation:
>>
>> I have an infinite set of integers (num) in which each integer n
>> satisfies a property P(n):
>>
>> ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n
>>
>> Suppose above proposition is NOT true, how can I derive that, there must
>> exist a number m such that for all n >= m, P(n) does NOT hold? i.e.
>>
>> ?m. !n. m <= n ==> ~(P n)
>>
>> Thanks in advance,
>>
>> Chun Tian
>>
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Dealing with INFINITE num set ...

2019-02-16 Thread Konrad Slind 
This can be proved by contradiction, using the fact that the set of numbers
less than any given number is finite.

val lemB = Q.prove
(`!N m. INFINITE N ==> ?n. m <= n /\ n IN N`,
 spose_not_then strip_assume_tac
  >> `FINITE (count m)` by metis_tac [FINITE_COUNT]
  >> `N SUBSET (count m)`
  by (rw_tac set_ss [SUBSET_DEF]
   >> `~(m <= x)` by metis_tac []
   >> decide_tac)
  >> metis_tac [SUBSET_FINITE])

On Fri, Feb 15, 2019 at 1:47 PM Chun Tian (binghe) 
wrote:

> And also this one:
>
> Given `INFINITE N` and a fixed number `m`, how can I assert the
> existence of another number `n` such that,
>
> m <= n /\ n IN N
>
> i.e. prove that
>
> ``!N m. INFINITE N ==> ?n. m <= n /\ n IN N``
>
> --Chun
>
> Il 15/02/19 20:11, Chun Tian (binghe) ha scritto:
> > Hi,
> >
> > I'm blocked at the following (strange) situation:
> >
> > I have an infinite set of integers (num) in which each integer n
> > satisfies a property P(n):
> >
> > ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n
> >
> > Suppose above proposition is NOT true, how can I derive that, there must
> > exist a number m such that for all n >= m, P(n) does NOT hold? i.e.
> >
> > ?m. !n. m <= n ==> ~(P n)
> >
> > Thanks in advance,
> >
> > Chun Tian
> >
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Dealing with INFINITE num set ...

2019-02-16 Thread Konrad Slind 
Rephrasing things might bring clarity:

load "pred_setLib";
open pred_setTheory;

val set_ss = (arith_ss ++ pred_setLib.PRED_SET_ss);

val lem = Q.prove
(`~(?N. INFINITE N /\ !n. N n ==> P n) <=> !N. N SUBSET P ==> FINITE N`,
 rw_tac set_ss [EQ_IMP_THM,SUBSET_DEF,IN_DEF]
  >- (`FINITE P \/ ?n. P n /\ ~P n` by metis_tac []
   >> imp_res_tac SUBSET_FINITE
   >> full_simp_tac std_ss [SUBSET_DEF, IN_DEF])
  >- metis_tac[]);

>From this and the original assumption, you should be able to get that P is
finite, so has a maximum element.

Konrad.



On Fri, Feb 15, 2019 at 1:12 PM Chun Tian (binghe) 
wrote:

> Hi,
>
> I'm blocked at the following (strange) situation:
>
> I have an infinite set of integers (num) in which each integer n
> satisfies a property P(n):
>
> ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n
>
> Suppose above proposition is NOT true, how can I derive that, there must
> exist a number m such that for all n >= m, P(n) does NOT hold? i.e.
>
> ?m. !n. m <= n ==> ~(P n)
>
> Thanks in advance,
>
> Chun Tian
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info