CODEWITHSUNDEEP
coqagda
András Kovács
András Kovács

Reputation: 30103

Postulating namespaces in Coq

I would like to have signatures such that I can postulate inhabitants for them. In Agda it looks like this:

record Foo (A : Set) : Set where
  field
    bar : A
    baz : A → A

postulate assumeFoo : Foo ℕ
open Foo assumeFoo

The advantage of this technique is that we can conveniently assemble and parameterize large bundles of postulated theories.

In Coq, I can open modules as namespaces and postulate inhabitants of records, but don't know how to do both for either. Is that possible?

Upvotes: 2

Views: 265

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

There is no exact analog of this feature in Coq. The closest you can get is to use a typeclass. This solves the parameterization issue, but does not provide the same namespace features. Your example would become:

Class Foo (A : Type) := {
  bar : A;
  baz : A -> A
}.

This declares a record with two fields bar and baz. What's special about the Class command is that Coq has a mechanism for filling in implicit arguments when their type was declared as a class. For instance, here is how we would postulate that nat has an instance of Foo:

Section MySection.

Context {fooNat : Foo nat}.

Check bar.

Check baz bar.

End MySection.

Any definitions inside the section would then get an extra fooNat parameter once you leave the section.

You can refer to the Coq manual for more references on typeclasses.

Upvotes: 4

Related Questions