4

In short, I am looking for a theorem prover which its underlying logic supports multiple subtyping / subclassing mechanism.( I tried to use Isabelle, but it does not seem to provide a first class support for subtyping. see this )

I would like to define a couple of types among which some are subclasses / subtypes of others. Furthermore, each type might be subtype of more than one type. For example:

Type A
Type B
Type C
Type E
Type F

C is subtype of A
C is also subtype of B
E and F are subtypes of B

PS: I am editing this question again to be more specific (because of a complains about being of-topic!): I am looking for a theorem prover / proof assistance in which I can define the above structure in a straight forward manner (not with workarounds as it is kindly described by some respectable answers here). If I take the types as classes then It seems above subtypings could be easily formulated in C++! So I am looking for a formal system / tool that I can define such a subtyping structure there and I can reason?

Many thanks

Community
  • 1
  • 1
qartal
  • 2,024
  • 19
  • 31
  • S.O. powers that be consider any ? that asks for an open-ended list to be off-topic—even if there is no such regulation. It is as if all open-ended lists of facts are opinion or something similar to that. All ?s must result in a definitive answer as a single fact, not an open-ended list (e.g., an open-ended list of facts). Perhaps the thinking is that when to end an open-ended list is mere opinion, and that the beauty of the length of the list is in the eye of the beholder. – Andreas ZUERCHER Jun 20 '21 at 16:59

3 Answers3

5

PVS has traditionally emphasized "predicate subtyping" a lot, but the system is a bit old-fashioned these days and has fallen behind the other big players that are more active: Coq, Isabelle/HOL, Agda, other HOLs, ACL2.

You did not make your application clear. I reckon that any of the big systems could be applied to the problem, one way or the other. Formalization is a matter to phrase your problem in a suitable way within the given logical environment. Logics are not programming languages, but have the real power of mathematics. Thus with some experience in a particular logic, you will be able to do great and amazing things that you did not expect at first sight.

When choosing your system, lists of particular low-level features are not so relevant. It is more important that you like the general style and culture of the system, before you make a commitment. You can compare that to learning a foreign language. Before you spend months or years to study do you collect features of the grammar? I don't think so.

Makarius
  • 2,165
  • 18
  • 20
4

You include the 'isabelle' tag, and it happens to be that according to "Wiki Subtyping", Isabelle provides one form of subtyping, "coercive subtyping", though as explained by Andreas Lochbihler, Isabelle doesn't really have subtyping like what you're wanting (and others want, too).

However, you're talking in vague generalities, so I easily provide a contrived example that meets the requirements of your 5 types. And though it is contrived, it's not meaningless, as I explain below.

(*The 5 types.*)
  datatype tA = tA_con int rat real
  type_synonym tB = "(nat * int)"
  type_synonym tC = int
  type_synonym tE = rat
  type_synonym tF = real

(*The small amount of code required to automatically coerce from tC to tB.*)
  fun coerce_C_to_B :: "tC => tB" where "coerce_C_to_B i = (0, i)"
  declare [[coercion coerce_C_to_B]]

(*I can use type tC anywhere I can use type tB.*)
  term "(2::tC)::tB"
  value "(2::tC)::tB"

In the above example, it can be seen that types tC, tE, and tF lend themselves naturally, and easily, to being coerced to types tA or tB.

This coercion of types is done quite a bit in Isabelle. For example, the type nat is used to define int, and int is used to define rat. Consequently, nat is automatically coerced to int, though int isn't to rat.

Wrap I (you haven't been using canonical HOL):

  • In your previous question examples, you've been using typedecl to introduce new types, and that doesn't generally reflect how people define new types.
    • Types defined with typedecl are nearly always foundational and axiomatized, such as with ind, in Nat.thy.
    • See here: isabelle.in.tum.de/repos/isabelle/file/8f4a332500e4/src/HOL/Nat.thy#l21
  • The keyword datatype_new is one of the primary, automagical ways to define new types in Isabelle/HOL.
    • Part of the power of datatype_new (and datatype) is its use to define recursive types, and its use with fun, for example with pattern matching.
    • In comparison to other proof assistants, I assume that the new abilities of datatype_new is not trivial. For example, a distinguishing feature between types and ZFC sets has been that ZFC sets can be nested arbitrarily deep. Now, with datatype_new, a type of countable or finite set can be defined that can be nested arbitrarily deep.
  • You can use standard types, such as tuples, lists, and records to define new types, which can then be used with coercions, as shown in my example above.

Wrap II (but, yes, that would be nice):

I could have continued with the list above, but I separate from that list two other keywords to define new types, typedef and quotient_type.

I separate these two because, now, we enter into the realm of your complaint, that the logic of Isabelle/HOL doesn't make it easy, many times, to define a type/subtype relationship.

Knowing nothing much, I do know now that I should only use typedef as a last resort. It's actually used quite a bit in the HOL sources, but then, the developers then have to do a lot of work to make a type defined with it easy to use, such as with fset

Wrap III (however, none are perfect in this imperfect world):

You listed the 3 proof assistants that probably have the largest market share, Coq, Isabelle, and Agda.

With proof assistants, we define your priorities, do our research, and then pick one, but it's like with programming languages. We're not going to get everything with any of them.

For myself, mathematical syntax and structured proofs are very important. Isabelle seems to be sufficiently powerful, so I choose it. It's not a perfect world, for sure.

Wrap IV (Haskell, Isablle, and type classes):

Isabelle, in fact, does have a very powerful form of subclassing, "type classes".

Well, it is powerful, but it is also limited in that you can only use one type variable when defining a type class.

If you look at Groups.thy, you'll see the introduction of class after class after class, to create a hierarchy of classes.

  • isabelle.in.tum.de/repos/isabelle/file/8f4a332500e4/src/HOL/Groups.thy

You also included the 'haskell' tag. The functional programming attributes of Isabelle/HOL, with its datatype and type classes, help tie the use of Isabelle/HOL to the use of Haskell, as demonstrated by the ability of the Isabelle code generator to produce Haskell code.

Community
  • 1
  • 1
noAccountHombre
  • 41
  • 2
2

There are ways to achieve that in agda.

  • Group the functions related to one "type" into fields of record
  • Construct instances of such record for the types you want
  • Pass that record along into proofs that require them

For example:

  record Monoid (A : Set) : Set where
    constructor monoid
    field
      z   : A
      m+  : A -> A -> A
      xz  : (x : A) -> m+ x z == x
      zx  : (x : A) -> m+ z x == x
      assoc : (x : A) -> (y : A) -> (z : A) -> m+ (m+ x y) z == m+ x (m+ y z)
  open Monoid public

Now list-is-monoid = monoid Nil (++) lemma-append-nil lemma-nil-append lemma-append-assoc instantiates (proves) that a List is a Monoid (given the the proofs of Nil being a neutral element, and a proof of associativity).

Sassa NF
  • 5,306
  • 15
  • 22