CODEWITHSUNDEEP
coqproof
setholopolus
setholopolus

Reputation: 265

Parametrizing a Module in Coq

Is there a way to pass a type variable as a parameter to a module in Coq, so that I don't have to keep restating the type variable?

Here's what I mean: I want to prove some basic facts about set theory. Lets start with one part of DeMorgan's laws. Using Ensemble from the standard library, I have:

Require Import Ensembles.

Variable U : Type.

Lemma demorgan1: forall A B: Ensemble U, 
    Included U 
        (Intersection U (Complement U A) (Complement U B)) 
        (Complement U (Union U A B)).

This works, but its really annoying to have all these Us everywhere.

Is there a way I can pass the U as a parameter to the Ensembles module so that all of the objects imported from it will automatically have U passed as the first argument?

Upvotes: 2

Views: 509

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

The Ensembles library is kept for historical reasons, but nowadays it is largely obsolete. It is generally easier to work directly with predicates U -> Prop, which is what Ensemble U unfolds to anyway. But going back to your question, you can achieve what you want by using implicit arguments:

Require Import Ensembles.

Variable U : Type.

Arguments Included {U} _ _.
Arguments Intersection {U} _ _.
Arguments Union {U} _ _.
Arguments Complement {U} _.

Lemma demorgan1: forall A B: Ensemble U,
    Included
        (Intersection (Complement A) (Complement B))
        (Complement (Union A B)).

Implicit arguments are those specified in curly braces in an Arguments declaration or in the header of a definition. Coq tries to automatically infer what these implicit arguments should be instantiated with based on the types of other arguments. In this case, it knows that the first argument of these functions should be U because A, B, etc. have type Ensemble U.

In general, it is not a good idea to override which arguments are implicit in someone else's definition: this choice is part of the interface of the library, and it is good to use it as the authors intended. A well-designed, modern library will generally come with sensible choices of implicit arguments. But in the case of legacy libraries such as Ensembles, overriding them probably makes sense.

Upvotes: 3

Related Questions