The Coq mailing list

[Constantine Plotnikov <constantine.plotnikov AT gmail.com>]

Hi!

I’m doing some exploration about applying Curry–Howard correspondence from Object-Oriented Programming to logic. And I’ve discovered that I could get in Coq quite close to it, but I hit some problems on the way. And I do not quite understand if Coq is missing a needed feature or if I miss some Coq feature to complete the experiment. I’ve read documentation on the modules, but it is a bit lacking in examples. And I've not found examples that were close enough to what I want to do.

Let’s start with what I’m trying to do.

-------------------------------------------

Module TestOOP.

  Module Type SemiGroup.
    Parameter T : Type.
    Parameter operation : T -> T -> T.
    Axiom associative_prop : forall a b c : T, operation (operation a b) c = operation a (operation b c).
  End SemiGroup.

  Module Type Monoid.
    Include SemiGroup.
    Parameter identity : T.
    Axiom identity_prop_right : forall a : T, operation a identity = a.
    Axiom identity_prop_left : forall a : T, operation identity a = a.
  End Monoid.

  Module Type Group.
    Include Monoid.
    Parameter inverse : T -> T.
    Axiom inverse_prop_right : forall a: T, operation a (inverse a) = identity.
    Axiom inverse_prop_left : forall a: T, operation (inverse a) a = identity.
  End Group.

  Module Type AbelianGroup.
    Include Group.
    Axiom comutative : forall a b : T, operation a b = operation b a.
  End AbelianGroup.

  Module Type Ring.
    Parameter T : Type.
    Parameter zero : T.
    Parameter one : T.
    Parameter plus : T -> T -> T.
    Parameter unary_minus : T -> T.
    Parameter mult : T -> T -> T.
    Axiom distributive_left : forall a b c : T, mult (plus a b) c = plus (mult a c) (mult b c).
    Axiom distributive_right : forall a b c : T, mult (plus a b) c = plus (mult a c) (mult b c).
    (* does not work after it *)
    Axiom plus_group: AbelianGroup with T := T, operation := plus, identity = zero, inverse = unary_minus.
    Axiom mult_monoid: Monoid with T := T, operation := mult, identity = one.
  End Ring.

  Module ZRing <: Ring.
    Definition T := Z.
    Definition zero = 0%Z.
    ...
    Theorem plus_group : AbelianGroup with T := T, operation := plus, identity = zero, inverse = unary_minus).
      (* proof that it exists with specified operators *)
    End plus_group.
  End ZRing.
 

End TestOOP.

-------------------------------------------------------------------------

This is a classical definition that integer is a ring and was supposed to be used as a sample of correspondence between OOP and logic. But I’ve not found a clear way to use module types as types. The currently used way is some syntax that reflects my intention. The definition “p : AbelianGroup(…)” in context means that all elements of it are available with context as proposition prefixed by “p” like “p.inverse” as function or “p.associative_prop” as proposition, just like for module access. To introduce this proposition to context one needs to define a completely specified module (with all parameters passed to module construction or defined as definitions or theorems within the module). The parameter “p” is like a tuple argument here. All its elements could be passed separately, so there are no excess logical problems.

So, I’m trying to figure out how to proceed. There seems to be a way to use inductive types for this, and I plan to investigate if this is possible later.  However, modules look like the right thing to use here, so I would like to see if I’ve missed something. The inference rules at document at https://coq.inria.fr/doc/language/core/modules.html?highlight=modules suggest that modules could be actually used as types, but I’ve not found a way to do it.

I came to this when I was trying to apply CFC from the concepts of interfaces and classes to Coq. An interface corresponds to syntactically correct theory. A class corresponds to a satisfied theory. Both interfaces and types could be used in OOP. Module also corresponds to the concept of theory from Mathematical Logic, so it looks like it might be also usable as type.

Best Regards, Constantine