Clever Geek Handbook

Theorem Checker / Support Helper (Multiple) Subtyping / Subclassing

Long story short, I am looking for a theorem where its underlying logic supports multiple subtyping / subclassing mechanism. (I tried to use Isabelle but doesn't seem to provide first class subtyping support. See this )

I would like to define several types, among which some are subclasses / subtypes of others. In addition, each type can be a 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'm editing this question again to be more specific (due to complaints that you were in the thread!): I'm looking for a theorem proof / evidential help where I can define the above structure in a straightforward way (not workarounds in ways as kindly described in some respectable answers here). If I take types as classes, then it seems like supertypes can be easily formulated in C ++! So I'm looking for a formal system / tool that I can define there such a subtyping structure and I can reason?

Many thanks

+3


source to share


3 answers


You include the 'isabelle' tag, and it happens, according to the "Subtype Wiki" , Isabelle provides one form of subtyping, "forced subtyping", although, as Andreas Lochbeeler explained, Isabelle doesn't really have subtypes like what you want (and others also want).

However, you are speaking in vague general terms, so I easily provide a contrived example that fits the requirements of your 5 types. While this is contrived, it is not pointless, 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, you can see that types tC

, tE

and are tF

naturally and easily coerced to types tA

or tB

.

This type-coercion is done quite a bit in Isabelle. For example, type is nat

used for definition int

and int

used for definition rat

. Therefore, it is nat

automatically forced to int

, although int

not related to rat

.

Wrap me up (you didn't use canonical HOL):

  • In your previous example questions, you used typedecl

    to introduce new types, which usually does not reflect how people define new types.
    • The types defined with help typedecl

      are almost always based and axiomatized, for example 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 main automatic ways of defining new types in Isabelle / HOL.
    • Part of the cardinality datatype_new

      (s datatype

      ) is its use to define recursive types and its use with fun

      , for example, pattern matching.
    • Compared to other proof assistants, I guess the new abilities are datatype_new

      not trivial. For example, the distinguishing feature between ZFC types and sets was that the ZFC set can be nested arbitrarily deep. Now, with datatype_new

      , you can define the type of a countable or finite set, which can be nested arbitrarily deeply.
  • You can use standard types like tuples, lists, and records to define new types, which can then be coerced, as shown in my example above.

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

I could continue with the list above, but I separate two other keywords from that list to define new types typedef

and quotient_type

.

I separate the two because we now come into the realm of your complaint that the Isabelle / HOL logic does not allow easy and frequent definition of a type / subtype relationship.

Knowing nothing, I now know what I should use typedef

as a last resort. It actually used quite a lot in the HOL sources, but then the developers need to do a lot of work to make the type defined with it easy to use, for example withfset



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

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

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

Mathematical syntax and structured proofs are very important to me. Isabelle seems strong enough, so I choose her. This is not a perfect world, of course.

Wrap IV (Haskell, Isablle and type classes):

Isabella actually has a very powerful form of subclassing "class classes".

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

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

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

You have also included the 'haskell' tag. The Isabelle / HOL functional programming attributes, with its classes datatype

and type, help to associate the use of Isabelle / HOL with the use of Haskell, as evidenced by the Isabelle code generator's ability to generate Haskell code.

+4


source


PVS has traditionally stressed the "subtyping predicate" a lot, but the system is a little old-fashioned these days and has lagged behind other big players who are more active: Coq, Isabelle / HOL, Agda, others HOL, ACL2.

You have not made your expression clear. I believe that any of the larger systems can be applied to the problem one way or another. Formalization is a question to properly correct your problem in a given logical environment. Logic is not programming languages, but the real power of mathematics. This way, with some experience in specific logic, you can do big and amazing things that you didn't expect at first sight.



When choosing your system, lists of specific low-level features are not that important. It's more important that you like the overall style and culture of the system before you commit to it. You can compare this to learning a foreign language. Before spending months or years studying, do you collect the traits of grammar? I do not think so.

+4


source


There are ways to achieve this in agda

.

  • Group functions related to one type into fields record

  • Create instances of this record

    for the types you want
  • Pass this record as evidence claiming 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

creates (proves) that a List

is a Monoid

(given that the proofs Nil

are neutral and associativity proof).

+2


source






More articles:


All Articles