Hi, Iโm afraid this idea doesnโt work, this is basically like using EXTENSION first, then EQ_TAC to prove two directions separately. But in my case, one direction cannot be proved. (Iโve been trying for 2 days), here is the full statements (it requires HOLโs existing measureTheory to be loaded):
val SETS_TO_DISJOINT_SETS = store_thm
("SETS_TO_DISJOINT_SETS",
``!sp sts f. subset_class sp sts /\ f IN (UNIV -> sts) ==>
?g. (g 0 = f 0) /\
(!n. 0 < n ==> (g n = f n INTER (BIGINTER (IMAGE (\i. sp DIFF f i)
(count n))))) /\
(!i j :num. i <> j ==> DISJOINT (g i) (g j)) /\
(BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE g UNIV))``,
โฆ);
More importantly, Iโm trying to figure out why an informal math proof cannot be
translated into a formal one, at least I donโt know how. In general, a
statement about (count n) doesnโt hold automatically for univ(:num), but in
above case I think yes, just I donโt know how.
โChun
> Il giorno 15 set 2018, alle ore 22:40, Waqar Ahmad <12phdwah...@seecs.edu.pk>
> ha scritto:
>
> Hi,
>
> I'd like to try converting the equality to SUBSET form by using
>
> Pred_setTheory.SUBSET_ANTISYM (THEOREM)
> ---------------------------------------
> |- !s t. s SUBSET t /\ t SUBSET s ==> (s = t)
>
> and then use property like
>
> topology_hvgTheory.BIGUNION_MONO_IMAGE (THEOREM) [1]
> ------------------------------------------------
> |- (!x. x IN s ==> f x SUBSET g x) ==>
> BIGUNION (IMAGE f s) SUBSET BIGUNION (IMAGE g s)
>
>
> This way you can figure out the relation between 'f' and 'g'...
>
> [1] http://hvg.ece.concordia.ca/code/hol/DFT/index.php
> <http://hvg.ece.concordia.ca/code/hol/DFT/index.php>
> On Sat, Sep 15, 2018 at 4:27 PM Chun Tian (binghe) <binghe.l...@gmail.com
> <mailto:binghe.l...@gmail.com>> wrote:
> 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
>
> _______________________________________________
> 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>
>
>
> --
> Waqar Ahmad, Ph.D.
> Post Doc at Hardware Verification Group (HVG)
> Department of Electrical and Computer Engineering
> Concordia University, QC, Canada
> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
> <http://save.seecs.nust.edu.pk/waqar-ahmad/>
>
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
