4 ms·
What you state about subtypes is not really true. HOL Light has subtypes baked into the kernel of the system. See https://github.com/jrh13/hol-light/blob/master
by cjfd 5y ago
What you state about subtypes is not really true. HOL Light has subtypes baked into the kernel of the system. See https://github.com/jrh13/hol-light/blob/master/fusion.ml https://github.com/jrh13/hol-light/blob/master/fusion.ml lines 600-637. Coq has sig in the standard library which is not quite it but becomes a lot closer when one assumes proof irrelevance. Also, a COC-based prover can easily be given subsets with a few easy axioms.
Your point that currently it is quite hard to do anything practical in all of the interactive theorem provers is very true, though.
- practal 5y agoI know the kernel of Hol-Light very well, as I implemented proof terms for it [1]. 600-637 do not define subtypes, but entirely new types. And no, you cannot add subtypes to a COC prover easily. [1]: https://link.springer.com/chapter/10.1007/11814771_27 https://link.springer.com/chapter/10.1007/11814771_27
- momentoftop 5y agoHOL Light doesn't have subtyping. If the type system had subtyping, there would be terms that are assigned two different types, where one type is a subtype of the other. So, in a truly subtyped system, you would have it that 3 has both type N and type R, with N being a subtype of R. Instead, in HOL Light, there is a total function from N to R, and a partial function from R to N. HOL Light allows you to carve out new types of existing types using a predicate filter, and this is baked into the kernel in `fusion.ml`. But this doesn't introduce subtyping relations. Importantly, the kernel rule gives you abstraction and representation functions to move between elements of the new type and the original type, but, unlike in a subtyping system, the terms of the newly defined type are not simultaneously elements of the larger type.