Re: [Hol-info] Adding abstraction to terms
Hi Dylan, I'm not aware of such a "tactical". In fact, I'm uncertain what you are looking for. A tactical is a SML function used to build tactics. An example is "REPEAT". It is of type "tactic -> tactic". Given a tactic, it returns another tactic that applies the argument tactic repeatedly. I guess (please correct me if I'm wrong) that you look for something like "aconv". Given two terms you want to check whether they are "equal with an added abstraction". So I guess you want something like "aebconv" of type "term -> term -> bool" with the following example behaviours aebconv ``( f:(num->bool) ) n`` ``(\x:num. f:(num->bool) x) n`` returns true aebconv ``f:(num->bool)`` ``(\x:num. f:(num->bool) x)`` returns true aebconv returns false if they are not equal. Notice, that I added a missing argument 'x' inside the lambda in both cases. Your original theorems have this typo in. Is this the kind of function you are looking for? In this case, what you are looking for is equivalence up to beta- and eta-reduction. "aconv" checks for alpha-equivalence, i.e. equivalence up to names. I'm not aware of any function that checks equivalence up to beta- and eta-reduction. You could do the reductions and then check the results for alpha-equivalence. There is "beta_conv" and "eta_conv" that do one-top-level step of such conversions. They are both very basic conversions. I.e. given a term t, they try to change it at top-level and return if they succeed a theorem of form |- t = t'. You could apply these repeatedly (DEPTH_CONV) and compare the results with aconv. These names are the ones used by HOL 4, I believe for HOL light they are the same. I have not checked though. Or are you interested in a proof of the equality? This would be in the logic and the statement would actually say that both sides are equal, not that they have the same beta- and eta-normal form. If you tell me more about what you want to do, I can perhaps help better. Best Thomas Tuerk On 06.07.2018 19:01, Dylan Melville wrote: > Is there a tactical that shows that a term is equal to the same term with an > added abstraction, for example: > > |- ( f:(num->bool) ) n <=> (\x:num. f:(num->bool) ) n > > Or even more simply > > |- f:(num->bool) <=> (\x:num. f:(num->bool) ) > -- > 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
Re: [Hol-info] Adding abstraction to terms
Thank you! > On Jul 6, 2018, at 1:04 PM, Mario Xerxes Castelán Castro > wrote: > > This is eta conversion. It is handled in HOL4 by the simplifier and both > HOL4 and HOL Light have conversions called “ETA_CONV” that are more low > level. > > On 06/07/18 12:01, Dylan Melville wrote: >> Is there a tactical that shows that a term is equal to the same term with an >> added abstraction, for example: >> >> |- ( f:(num->bool) ) n <=> (\x:num. f:(num->bool) ) n >> >> Or even more simply >> >> |- f:(num->bool) <=> (\x:num. f:(num->bool) ) >> -- >> 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 -- 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] Adding abstraction to terms
This is eta conversion. It is handled in HOL4 by the simplifier and both HOL4 and HOL Light have conversions called “ETA_CONV” that are more low level. On 06/07/18 12:01, Dylan Melville wrote: > Is there a tactical that shows that a term is equal to the same term with an > added abstraction, for example: > > |- ( f:(num->bool) ) n <=> (\x:num. f:(num->bool) ) n > > Or even more simply > > |- f:(num->bool) <=> (\x:num. f:(num->bool) ) > -- > 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: OpenPGP digital signature -- 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
[Hol-info] Adding abstraction to terms
Is there a tactical that shows that a term is equal to the same term with an added abstraction, for example: |- ( f:(num->bool) ) n <=> (\x:num. f:(num->bool) ) n Or even more simply |- f:(num->bool) <=> (\x:num. f:(num->bool) ) -- 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
