Re: [Hol-info] Prove BIGUNION (IMAGE f 𝕌(:num)) by induction on (count n)?

[Chun Tian (binghe)]

Hi again,

It seems that my original question has a positive answer. I got a proof from 
Thomas Tuerk saying:

val BIGUNION_IMAGE_COUNT_IMP_UNIV =
   ⊢ ∀f g.
         (∀n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ⇒
         (BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num)))

that’s amazing...

—Chun


(* provided by Thomas Tuerk, amazing! *)
val BIGUNION_IMAGE_COUNT_IMP_UNIV = store_thm
  ("BIGUNION_IMAGE_COUNT_IMP_UNIV",
  ``!f g. (!n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ==>
          (BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE g UNIV))``,
 (* proof *)
   `!f g. (!n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ==>
          (BIGUNION (IMAGE f UNIV) SUBSET BIGUNION (IMAGE g UNIV))`
       suffices_by PROVE_TAC [SUBSET_ANTISYM]
 >> REWRITE_TAC [SUBSET_DEF]
 >> REPEAT STRIP_TAC
 >> rename1 `e IN BIGUNION _`
 >> Know `?n. e IN BIGUNION (IMAGE f (count n))`
 >- (FULL_SIMP_TAC std_ss [IN_BIGUNION, IN_IMAGE, PULL_EXISTS, IN_COUNT] \\
     rename1 `e IN f n'` \\
     Q.EXISTS_TAC `SUC n'` \\
     Q.EXISTS_TAC `n'` \\
     ASM_SIMP_TAC arith_ss [])
 >> STRIP_TAC
 >> `e IN BIGUNION (IMAGE g (count n))` by PROVE_TAC []
 >> FULL_SIMP_TAC std_ss [IN_BIGUNION, IN_IMAGE, PULL_EXISTS, IN_UNIV]
 >> METIS_TAC []);


> Il giorno 16 set 2018, alle ore 08:37, Chun Tian (binghe) 
> <binghe.l...@gmail.com> ha scritto:
> 
> Cancel this question. Finally I found a way to reduce the original goal to
> 
>       ∀n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))
> 
> but it deeply relies on the definition of g, otherwise it seems impossible.  
> Sorry for disturbing.
> 
> —Chun
> 
>> Il giorno 15 set 2018, alle ore 22:26, Chun Tian (binghe) 
>> <binghe.l...@gmail.com> ha scritto:
>> 
>> Hi,
>> 
>> I have a need to prove that, for two certain functions f, (g :num->’a set)
>> 
>>      BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
>> 
>> Following its informal proof, it seems only possible to prove the following 
>> result (by induction) first:
>> 
>>      !(n :num). BIGUNION (IMAGE f (count n)) = BIGUNION (IMAGE g (count n))
>> 
>> but once I got this intermediate result, how I can reach to the original 
>> statement? Is there any other assumption needed for going from finite to 
>> infinite union?
>> 
>> Thanks,
>> 
>> Chun Tian
>> 
> 

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