Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Consider Rob Arthan’s “HOL Constant Definition Done Right” #72

Closed
mn200 opened this issue Jul 25, 2012 · 17 comments
Closed

Consider Rob Arthan’s “HOL Constant Definition Done Right” #72

mn200 opened this issue Jul 25, 2012 · 17 comments

Comments

@mn200
Copy link
Member

mn200 commented Jul 25, 2012

See http://permalink.gmane.org/gmane.comp.mathematics.hol/1555

One potential problem is that it may make OpenTheory inter-operability more difficult.

@xrchz
Copy link
Member

xrchz commented Jul 25, 2012

Consider this for HOL4 on the OpenTheory mailing list as well, then OpenTheory may also adopt it (or not if it's bad). Or else someone (probably me) will write the wrappers. I wouldn't count that problem for much in the deliberation.

@mn200
Copy link
Member Author

mn200 commented Feb 18, 2014

Two issues with HCDDR:

  • it makes new_specification depend on Hilbert Choice, which is unnecessary (though hardly a showstopper, particularly in HOL4 where we have it available very early on)
  • it makes the to-be-derived, “old” form of new_specification depend on pairs.

@xrchz
Copy link
Member

xrchz commented Feb 19, 2014

Neither of those points are true, as far as I understand the proposed new_specification. The rule is specifically designed to depend only on one primitive constant (equality). The current form of new_specification should be derivable directly. Hmm, let me just implement it on a new branch and see.

@xrchz
Copy link
Member

xrchz commented Feb 19, 2014

I misunderstood, you are right. You were talking about how to derive the existing new_specification from the proposed new one (which we could call loose_specification, just to have a different name for it), and the proposal for how to do so does indeed depend on choice and pairs.

One question to consider: if loose_specification is available in Theory (implemented via a primitive in Thm), where should new_specification and new_definition be available from? Is Theory still the right place?

@mn200
Copy link
Member Author

mn200 commented Feb 20, 2014

It'd be ugly to have something that morally depended on pairs in Theory. It'd also be a minor pain to implement as you have to take care to build pairs and the like only at invocation time, not at compile/load time. Given that, it might be nicest to put new_specification into pairLib. But that doesn't seem that nice...

@konrad-slind
Copy link
Contributor

I haven't been keeping up, but we already do something similar for
new_definition:
this is defined in the kernel and any postprocessing needed for
definitions over
varstructs is done via code installed in pairLib by updating hooks provided
in Theory.

Konrad.

On Wed, Feb 19, 2014 at 10:57 PM, Michael Norrish
[email protected]:

It'd be ugly to have something that morally depended on pairs in Theory.
It'd also be a minor pain to implement as you have to take care to build
pairs and the like only at invocation time, not at compile/load time. Given
that, it might be nicest to put new_specification into pairLib. But that
doesn't seem that nice...

Reply to this email directly or view it on GitHubhttps://github.com//issues/72#issuecomment-35589397
.

@xrchz
Copy link
Member

xrchz commented Feb 20, 2014

What about putting the backwards-compatible new_specification much later, like bossLib? Any uses of it prior to that are presumably under our control and can just be ported to loose_specification (the revised new_specification: any better name?).

@mn200
Copy link
Member Author

mn200 commented Feb 20, 2014

This would be fine as long as no existing uses of new_specification before bossLib wanted to use it to define multiple constants in one go. However, there is such an example, namely the definition of DIV and MOD. Luckily, arithmetic now depends on pairs, so you could actually implement new_specification in pairLib, use it in arithmeticTheory and then re-export it from bossLib.

I think loose_specification is a fine name, btw.

@xrchz
Copy link
Member

xrchz commented Feb 20, 2014

loose_specification permits definition of multiple constants simultaneously natively.

@mn200
Copy link
Member Author

mn200 commented Feb 20, 2014

Only if you have equations for them; with DIV and MOD we don't.

@xrchz
Copy link
Member

xrchz commented Feb 21, 2014

Hmm... ok. You could probably just change the MOD_DIV_exist theorem to prove existence of e.g. a function on Booleans that returns either MOD or DIV, rather than depending on pairs properly.

@mn200
Copy link
Member Author

mn200 commented Feb 21, 2014

Because the constants are unique, you could also define them in stages, one after the other using something like

 Div = @f. ?k. f calculates div and k is the remainder

I'm sure you'll think of something.

@mn200
Copy link
Member Author

mn200 commented Feb 21, 2014

Err, the exists will have to be under the scope of a forall m and n representing the arguments to the function.

@xrchz
Copy link
Member

xrchz commented Feb 21, 2014

Looks like there's a more annoying use of new_specification quite early to define define_new_type_bijections. The intended use of the theorem ABS_REP_THM in boolScript.sml has a similar problem to the MOD and DIV problem, but proving a version of the theorem more suitable for loose_specification will be difficult if not impossible.

@xrchz
Copy link
Member

xrchz commented Feb 21, 2014

Perhaps it's worth reconsidering putting the backwards-compatibility wrapper in Theory. It might be possible without pairs (but still using choice) if instead of choosing a tuple we choose a function from some appropriate powerset of booleans (since numbers aren't around either). Hmm that's probably pretty complicated though.

@mn200
Copy link
Member Author

mn200 commented Feb 21, 2014

The function from the booleans also assumes the constants all have the same type

@mn200
Copy link
Member Author

mn200 commented Sep 1, 2015

I believe this is now done.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants