Re: [Hol-info] How to reduce these lambda equations to F?
Thanks!Actually I was ever taught (by Thomas) to use FUN_EQ_THM to convert relation equations (R = R’) into provable forms (!x y. R x y = R’ x y), but when I was facing lambda functions I didn’t realize they’re essentially the same thing. (Using PAT_X_ASSUM I can precisely target on any single assumptions, thus other assumptions won’t be affected) And I found that, once I got ``!x. x = prefix (label l) x``, actually the `distinct` theorems generated by Datatype will directly lead it to False, no need to call the “size” theorems and use arithmetic stuff, although the latter idea also works. —Chun > Il giorno 07 ago 2017, alle ore 01:33, michael.norr...@data61.csiro.au ha > scritto: > > I would use > > fs[FUN_EQ_THM] > > to expand the assumptions to > > !x. x = prefix (label l) x > > and > > !x. x = p > > respectively. > > Of course, this is a blunt weapon, so you may not wish to use it if other > assumptions are disrupted too much. > > Michael > > On 5/8/17, 04:25, "Chun Tian (binghe)"wrote: > >Hi, > >This is the first time I met the following goal, in which one of the > assumptions should be able to reduce to F (then the goal is resolved): > >R (λt. t) > > 4. (λt. t) = (λt. prefix (label l) t) > >The lambda function has the type of ``CCS -> CCS``, which CCS is my > datatype defined by HOL’s Define command. “prefix” is an constructor of CCS > datatype.I *know* the equation doesn’t hold, because the whatever input > arguments, the resulting CCS on both side must have different “size”, simply > because one is the sub-expression of the other. But how can I actually > reduce it to F? > >The other case is a little different: > >R (λt. t) > > 4. (λt. t) = (λt. p) > >The assumption "(λt. t) = (λt. p)” hold for only one case: when input of > lambda function is exactly “p”. For all other cases the left side doesn’t > equal to the right side. But from the view of two functions, they’re > obviously not identical. But how can I actually reduce it to F? > >Regards, > >Chun Tian > > > > -- > Check out the vibrant tech community on one of the world's most > engaging tech sites, Slashdot.org! http://sdm.link/slashdot > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info signature.asc Description: Message signed with OpenPGP using GPGMail -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] How to reduce these lambda equations to F?
I would use fs[FUN_EQ_THM] to expand the assumptions to !x. x = prefix (label l) x and !x. x = p respectively. Of course, this is a blunt weapon, so you may not wish to use it if other assumptions are disrupted too much. Michael On 5/8/17, 04:25, "Chun Tian (binghe)"wrote: Hi, This is the first time I met the following goal, in which one of the assumptions should be able to reduce to F (then the goal is resolved): R (λt. t) 4. (λt. t) = (λt. prefix (label l) t) The lambda function has the type of ``CCS -> CCS``, which CCS is my datatype defined by HOL’s Define command. “prefix” is an constructor of CCS datatype.I *know* the equation doesn’t hold, because the whatever input arguments, the resulting CCS on both side must have different “size”, simply because one is the sub-expression of the other. But how can I actually reduce it to F? The other case is a little different: R (λt. t) 4. (λt. t) = (λt. p) The assumption "(λt. t) = (λt. p)” hold for only one case: when input of lambda function is exactly “p”. For all other cases the left side doesn’t equal to the right side. But from the view of two functions, they’re obviously not identical. But how can I actually reduce it to F? Regards, Chun Tian -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] How to reduce these lambda equations to F?
Hi Thomas, Thanks! Now I got your points: 1. ``(λt. t) = (λt. p)`` cannot reduce to F unless the underlying type has at least two distinct values (for datatypes with at least two constructors, it’s easily provable by cases analysis, I think). 2. To prove two lambda-functions, say f and g are not identical, it’s enough to choose one special value x and shows that f(x) <> g(x). And this fact depends on theorems but beta-conversion. Now I think I can resolve both cases. Regards, Chun > Il giorno 04 ago 2017, alle ore 21:38, Thomas Tuerk> ha scritto: > > Hi Chun, > > via a subgoal, you can introduce an assumption for a concrete argument. This > should be what you need. I'm thinking of something like > > First show that a CCS q exists with "q <> p" > `?q. q <> p` by ... > > Then use this new q as an argument) > `(\t. t) q = (\t. p) q` by PROVE_TAC[] > Now you are done by BETA reduction and contradicting assumptions. > > Best > > Thomas > > > On 04.08.2017 20:22, Chun Tian (binghe) wrote: >> Hi, >> >> This is the first time I met the following goal, in which one of the >> assumptions should be able to reduce to F (then the goal is resolved): >> >> R (λt. t) >> >> 4. (λt. t) = (λt. prefix (label l) t) >> >> The lambda function has the type of ``CCS -> CCS``, which CCS is my datatype >> defined by HOL’s Define command. “prefix” is an constructor of CCS >> datatype.I *know* the equation doesn’t hold, because the whatever input >> arguments, the resulting CCS on both side must have different “size”, simply >> because one is the sub-expression of the other. But how can I actually >> reduce it to F? >> >> The other case is a little different: >> >> R (λt. t) >> >> 4. (λt. t) = (λt. p) >> >> The assumption "(λt. t) = (λt. p)” hold for only one case: when input of >> lambda function is exactly “p”. For all other cases the left side doesn’t >> equal to the right side. But from the view of two functions, they’re >> obviously not identical. But how can I actually reduce it to F? >> >> Regards, >> >> Chun Tian >> >> >> >> >> -- >> Check out the vibrant tech community on one of the world's most >> engaging tech sites, Slashdot.org! >> http://sdm.link/slashdot >> >> >> ___ >> hol-info mailing list >> >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info > > -- > Check out the vibrant tech community on one of the world's most > engaging tech sites, Slashdot.org! > http://sdm.link/slashdot___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info signature.asc Description: Message signed with OpenPGP using GPGMail -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] How to reduce these lambda equations to F?
Hi Chun, via a subgoal, you can introduce an assumption for a concrete argument. This should be what you need. I'm thinking of something like First show that a CCS q exists with "q <> p" `?q. q <> p` by ... Then use this new q as an argument) `(\t. t) q = (\t. p) q` by PROVE_TAC[] Now you are done by BETA reduction and contradicting assumptions. Best Thomas On 04.08.2017 20:22, Chun Tian (binghe) wrote: > Hi, > > This is the first time I met the following goal, in which one of the > assumptions should be able to reduce to F (then the goal is resolved): > > R (λt. t) > > 4. (λt. t) = (λt. prefix (label l) t) > > The lambda function has the type of ``CCS -> CCS``, which CCS is my datatype > defined by HOL’s Define command. “prefix” is an constructor of CCS datatype. >I *know* the equation doesn’t hold, because the whatever input arguments, > the resulting CCS on both side must have different “size”, simply because one > is the sub-expression of the other. But how can I actually reduce it to F? > > The other case is a little different: > > R (λt. t) > > 4. (λt. t) = (λt. p) > > The assumption "(λt. t) = (λt. p)” hold for only one case: when input of > lambda function is exactly “p”. For all other cases the left side doesn’t > equal to the right side. But from the view of two functions, they’re > obviously not identical. But how can I actually reduce it to F? > > Regards, > > Chun Tian > > > > -- > Check out the vibrant tech community on one of the world's most > engaging tech sites, Slashdot.org! http://sdm.link/slashdot > > > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info